Section Basic.
(*Basic Logical Reasoning *)
Variables A B : Prop.
Goal A /\ B -> B /\ A.
Proof.
Qed.
(* Coq basic theory implements an intuitionistic logic which does not prove
Pierce law but a weaker version of it (not not P => P) is not a basic axiom *)
Variables P Q : Prop.
Lemma PierceI : ((P->Q)->P)-> ~ ~ P.
Proof.
Qed.
(* A special library can be loaded to add classical reasoning *)
Require Import Classical.
Lemma Pierce : ((P->Q)->P)->P.
(* Excursion: this is actually known under the name "Pierce Law".
It is not a theorem in Pure (since Pure is intuitionistic),
but a theorem in HOL: *)
(* solution *)
Qed.
End Basic.
Section Equational.
(* Very Basic Equational Reasoning *)
(* no automation at all: the example from the course *)
Variable E : Type.
Variables a b c:E.
Variable f : E*E -> E.
Variable g : E -> E.
Lemma A: f(a,b) = a -> f(f(a,b),b) = c -> g a = g c.
Qed.
End Equational.
Section Xor.
Definition xor (A B :Prop) : Prop := (A /\ ~ B) \/ (~ A /\ B).
Lemma xor_refl A : xor A ~A.
Proof. (* requires classical reasoning *)
Qed.
End Xor.
Section Sets.
Variable E : Type.
Definition incl A B := forall x : E, A x -> B x.
Variable A B C : E -> Prop.
Lemma incl_trans : incl A B -> incl B C -> incl A C.
Proof.
Qed.
Ens Sets.
Section FirstOrder.
Variable E : Type.
Variable A : Prop.
Variable B : E -> Prop.
Lemma all_istr:
(forall x, A -> B x) <-> (A -> forall x, B x).
Proof.
Qed.
Variable P : E -> E -> Prop.
Lemma ex_all : (forall x, exists y, P x y) -> forall y, exists x, P x y.
Proof.
(* Possible to prove ? *)
Abort.
(* Coq does not assume that Type are non-empty *)
Variable e:E.
Lemma ex_all2 : (forall x, forall y, P x y) -> exists y, forall x, P x y.
Proof.
Qed.
End FirstOrder.