Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/negb_involutive.v

Created September 23, 2016 00:17
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/12f21bf4caa71487aada21ea4dfc8262 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/12f21bf4caa71487aada21ea4dfc8262 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
negb_involutive.v
Definition pred (A: Type) := A -> bool.
Definition complement {A : Type} p : pred A := fun x => negb (p x).
Lemma remove_complement : forall (A : Type) (p : pred A),
(complement (complement p)) = p.
Proof.
intros A p. unfold complement. rewrite negb_involutive.
A : Type
p : pred A
============================
(fun x : A => negb (negb (p x))) = p
Error: Found no subterm matching "negb (negb ?M1808)" in the current goal.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment