(* logic-examp.ec *)
require import AllCore. (* core theories *)
(* here's a lemma for learning some simple Ambient Logic
proof techniques; in fact, it's already in EasyCrypt's
library with the same name; and smt() will prove it *)
lemma negb_or (a b : bool) :
!(a \/ b) <=> !a /\ !b.
proof.
qed.
(* now we can use negb_or to prove: *)
lemma foo (x y z : int) :
!(x < y \/ y < z) <=> ! x < y /\ ! y < z.
proof.
qed.
(* we can make the proof of negb_or more compact using more
complex introduction patterns: *)
lemma negb_or' (a b : bool) :
!(a \/ b) <=> !a /\ !b.
proof.
qed.
(* the above was nice for learning ambient techniques, but for
these propositional logic lemmas, EasyCrypt makes it easier
to work via case analysis - essentially via truth tables *)
lemma negb_or'' (a b : bool) :
!(a \/ b) <=> !a /\ !b.
proof.
qed.
(* and we can tighten this up: *)
lemma negb_or''' (a b : bool) :
!(a \/ b) <=> !a /\ !b.
proof.
qed.
(* and we could have simply used smt() *)
(* and we can tighten this up: *)
lemma negb_or'''' (a b : bool) :
!(a \/ b) <=> !a /\ !b.
proof.
qed.