(* load core theories (like Int and Bool), and import to top-level
namespace
thus, e.g., we can write < instead of Int.< *)
require import AllCore.
lemma not_and (a b : bool) :
!(a /\ b) => !a \/ !b.
proof.
move => not_or_a_b. (* introduce as assumption left side of => *)
case a. (* split into cases when a is true and false *)
(* a is true *)
simplify. (* apply logical simplification rules *)
move => a_true.
case b.
(* b is true *)
move => b_true.
simplify.
have contrad : a /\ b. (* sub-lemma *)
trivial. (* try to solve goal by simple logic transformations *)
trivial. (* trivial looks for contradictory assumptions *)
(* b is false *)
trivial.
(* a is false *)
trivial.
qed.
lemma not_and' (a b : bool) :
!(a /\ b) => !a \/ !b.
proof.
(* ; means apply to all subgoals generated by
running *)
case a; trivial.
qed.
lemma not_and'' (a b : bool) :
!(a /\ b) => !a \/ !b.
proof.
(* "smt." means use any known lemmas, "smt(...)." says use only listed lemmas
plus what solvers have built-in *)
smt().
qed.
lemma ex (x y : int) :
!(x < y /\ y < x) => ! x < y \/ ! y < x.
proof.
apply not_and. (* infers how a/b should be instantiated *)
qed.
(*
search [!] (\/) (/\).
lemma nosmt negb_and: forall (a b : bool), ! (a /\ b) <=> !a \/ !b.
*)
lemma ex' (x y : int) :
!(x < y /\ y < x) => ! x < y \/ ! y < x.
proof.
(* can apply an <=> when either left-to-right or right-to-left => needed *)
apply negb_and.
qed.