Section Lesson4.


(* ------------ Propositional Logic ------------ *)

Variables Q P :Prop.


Lemma ex1 : (P -> Q) -> ~Q -> ~P.
Proof.
intros.
intro.
apply H0.
apply H.
exact H1.
Qed.

Axiom RAA : forall A:Prop, (~A->False) -> A .  (* classical *)

Lemma ex2 : (~Q -> ~P) -> P -> Q.   (* this result is only valid classically *)
Proof.
intros.
apply RAA.
intro.
apply H.
assumption.
assumption.
Qed.


Theorem ex3 : forall A:Prop, A -> ~~A.
Proof.
intros.
intro.
apply H0; exact H.
Qed.

Lemma ex3' : forall A:Prop, A -> ~~A.
Proof.
intros.
red.     (* does only the unfolding of the head of the goal *)
intro.
unfold not in H0.
apply H0; assumption.
Save.

Goal forall A:Prop, A -> ~~A.
intros.
unfold not.
intro H0; apply H0; assumption.
Abort.





Lemma ex4 : P /\ Q -> Q /\ P.
Proof.
intro H.
split.
destruct H as [H1 H2].
exact H2.
destruct H; assumption.
Qed.


Lemma ex5 : P \/ Q -> Q \/ P.
Proof.
intros.
destruct H as [h1 | h2].
right.
assumption.
left; assumption.
Qed.


Variable B :Prop.
Variable C :Prop.

Lemma ex6 : (P->Q) /\ (B->C) /\ P /\ B -> Q/\C.  (* exercise *)


Lemma ex7 : ~ (P /\ ~P).    (* exercise *)


Lemma ex8 : (P\/Q)/\~P -> Q.   (* exercise *)


Lemma ex9 : ~(P \/ Q) <-> ~P /\ ~Q.   
Proof.
red.
split.
intros.
split.
(*unfold not in H.*)
intro H1.
apply H.
left; assumption.
intro H1; apply H; right; assumption.

intros H H1.
destruct H.
destruct H1.
apply H; assumption.
apply H0; assumption.
Qed.


Lemma ex9' : ~(P \/ Q) <-> ~P /\ ~Q.
Proof.
tauto.
Abort.


(* ------------ First-Order Logic ------------ *)


Variable X :Set.
Variable t :X. 
Variables R W : X -> Prop.

Lemma ex10 : R(t) -> (forall x, R(x) -> ~W(x)) -> ~W(t).
Proof.
intros.
apply H0.
exact H.
Qed.


Lemma ex11 : forall x, R x -> exists x, R x.
Proof.
intros.
exists x.
assumption.
Qed.


Lemma ex12 : (exists x, ~(R x)) -> ~ (forall x, R x).
Proof.
intros H H1.
destruct H as [x0 H0].
apply H0.
apply H1.
Qed.



Theorem ex12' :  forall y, (forall x, (R x) /\ (W x)) -> (R y).
Proof.
intros.
destruct H with y.
assumption.
Qed.



(* Exercise *)
Lemma ex13 : (forall x, R x) \/ (forall x, W x) -> forall x, (R x) \/ (W x).


Variable G : X->X->Prop.

(* Exercise *)
Lemma ex14 : (exists x, exists y, (G x y)) -> exists y, exists x, (G x y).



(* ------------ Dealing with the equality ------------ *)

Require Import Arith.

Check O.
Check S.
Print nat.

Check  (S (S (S O))).

Eval compute in 3+5*2.

(* Finding existing proofs *)

Search le.

SearchPattern (_ + _ <= _ + _).

SearchRewrite (_+(_-_)).

SearchAbout ge.

Lemma ex15 : 1 <= 3.
Proof.
Search le.
apply le_S.
apply le_S.
apply le_n.
Qed.


Lemma ex16 : forall x y:nat, x <= 5 -> 5 <= y -> x <= y.
Proof.
intros.
Search le.
Check le_trans.
apply le_trans with (m:=5).
assumption.
assumption.
Qed.


Lemma ex17 : forall x y:nat, (x + y) * (x + y) = x*x + 2*x*y + y*y.
Proof.
intros.
SearchRewrite (_ * (_ + _)).
rewrite mult_plus_distr_l.
SearchRewrite ((_ + _) * _).
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_r.
SearchRewrite (_ + (_ + _)).
rewrite plus_assoc.
Check plus_assoc.
rewrite <- plus_assoc with (n := x * x).
SearchPattern (?x * ?y = ?y * ?x).
rewrite mult_comm with (n:= y) (m:=x).
SearchRewrite (S _ * _).
pattern (x * y) at 1. rewrite <- mult_1_l.
rewrite <- mult_succ_l.
SearchRewrite (_ * ( _ * _)).
rewrite mult_assoc.
reflexivity.
Qed.

Lemma ex18 : forall n:nat, n <= 2*n.
Proof.
induction n.
simpl.
Search le.
apply le_refl.
simpl.
Search le.
apply le_n_S.
SearchPattern (_<= _ + _).
apply le_plus_l.
Qed.


End Lesson4.