(** {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 *)