(* logic-examp.ec *) require import AllCore. (* here's a lemma for learning some simple Ambient Logic proof techniques *) lemma negb_or (a b : bool) : !(a \/ b) <=> !a /\ !b. proof. split. (* proving ! (a \/ b) => !a /\ !b *) move => not_or. split. case a. move => a_true. simplify. have contrad : a \/ b. left. trivial. trivial. trivial. case b. move => b_true. simplify. have contrad : a \/ b. right. trivial. trivial. trivial. (* proving !a /\ !b => ! (a \/ b) *) move => and_not. elim and_not => a_false b_false. case (a \/ b). move => or. elim or. trivial. trivial. trivial. qed. (* now we can use negb_or to prove: *) lemma foo (x y z : int) : !(x < y \/ y < z) <=> ! x < y /\ ! y < z. proof. apply negb_or. 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. split => [not_or | [] not_a not_b]. split. case a => [a_true | //]. have // : a \/ b by left. case b => [b_true | //]. have // : a \/ b by right. case (a \/ b) => [[] // | //]. 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. case a. case b. trivial. trivial. case b. trivial. trivial. qed. (* and we can tighten this up: *) lemma negb_or''' (a b : bool) : !(a \/ b) <=> !a /\ !b. proof. by case a. (* equivalent to `case a => //` *) qed.