(* 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.