Section Basic.
(*Basic Logical Reasoning *)

Variables A B : Prop.

Goal A /\ B -> B /\ A.
Proof.
intro H.
destruct H.
apply conj.
assumption.
assumption.
Qed.

Goal A /\ B -> B /\ A.
Proof.
intros (H1,H2); split; assumption.
Qed.


Goal A /\ B -> B /\ A.
Proof.
tauto.
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.
(* tauto. *)
intros H1 H2.
apply H2.
apply H1.
intro H3.
case H2.
assumption.
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 *)        
(* tauto. *)
intro.
apply NNPP.
apply PierceI.
assumption.
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.
intros H1 H2.
assert (a = c).
transitivity (f(a,b)).
rewrite H1.
reflexivity.
transitivity (f (f (a, b), b)).
f_equal.
f_equal.
symmetry.
assumption.
assumption.
rewrite H.
reflexivity.
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, use lemme classic*)
unfold xor.
destruct (classic A).
left; auto.
right; auto.

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.
unfold incl; intros.
(* auto. solves the goal *)
apply H0.
apply H.
assumption.
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.
split.
intros H1 H2 x.
apply H1.
assumption.
intros H1 x H2.
apply H1.
assumption.
Qed.

Lemma all_istr': 
    (forall x, A -> B x) <-> (A  -> forall x, B x).
Proof.
(* intuition. *)
split; intros.
apply H.
assumption.
apply H.
assumption.
Qed.

Variable P : E -> E -> Prop.

Lemma ex_all : (forall x, exists y, P x y) -> forall y, exists x, P x y.


(* 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.
(* firstorder. *)
intro H.
exists e.
intro x.
apply H.
Qed.

(* Possible to prove ? *)



  
End FirstOrder.