Skip to content

Instantly share code, notes, and snippets.

@srbmiy

srbmiy/ssrnat001.v

Created December 20, 2014 10:49
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save srbmiy/31a74ec01b8961c4f506 to your computer and use it in GitHub Desktop.
Save srbmiy/31a74ec01b8961c4f506 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ssrnat001.v
Require Import ssreflect ssrbool ssrnat.
Definition nand_b (b0 : bool) (b1 : bool) : bool :=
match b0 with
| true => (~~ b1)
| false => true
end.
Lemma nand_lemma : forall (b0 b1 : bool), (nand_b b0 b1) = (~~(b0 && b1)).
Proof.
move=> b0 b1.
case b0.
simpl; reflexivity.
simpl; reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment