(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)
(** {2 Propositional logic} *)
predicate a
predicate b
(** arbitrary predicate variables *)
goal and_left: a /\ b -> a
(** almost trivial goal *)
goal excluded_middle : a \/ not a
(** note that the logic is classical, not intuitionistic *)
goal pierce : ((a -> b) -> a) -> a
(** even if it contains no negation, this formula is not
provable in intuitionistic logic *)
goal imp_assoc_to_the_right: a -> a -> a
(** be aware that implication associates to the right *)
goal imp_does_not_assoc_to_the_left : (a -> a) -> a
(** Must not be proved. Why3 hint: type 'g' on a failed
proof attempt by CVC4 or Z3 to get a counterexample *)