(* 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. qed. lemma not_and' (a b : bool) : !(a /\ b) => !a \/ !b. proof. (* ; means apply to all subgoals generated by running *) 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 *) qed. lemma ex (x y : int) : !(x < y /\ y < x) => ! x < y \/ ! y < x. proof. 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 *) qed.