Skip to content

Instantly share code, notes, and snippets.

@relrod

relrod/foo.v

Created January 15, 2015 16:59
Show Gist options
  • Save relrod/faff823451a848bd03bb to your computer and use it in GitHub Desktop.
Save relrod/faff823451a848bd03bb to your computer and use it in GitHub Desktop.
Download ZIP
Proving de Morgan's laws in Coq because I have no life.
Raw
foo.v
Theorem de_morgan_1 : forall b1 b2 : bool,
negb (orb b1 b2) = andb (negb b1) (negb b2).
Proof.
intros.
destruct b1.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
Theorem de_morgan_2 : forall b1 b2 : bool,
negb (andb b1 b2) = orb (negb b1) (negb b2).
Proof.
intros.
destruct b1.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment