(** Introduction to Formal Reasoning (G52IFR)
    Li Nuo

    T01
**)

Section T01.


(** What is the basic things we have learnt in Coq? **)
(** What is the corresponding introduction and elimination tactics for
them? **)

Variable P Q R : Prop.

Variable Tomorrow_will_rain : Prop.

(** think of every proposition before you start to prove it **)

(** It is impossible to have both something and the negation of it **)
Lemma Inconsistency : ~ (P /\ ~ P).
intro.
destruct H as [p np].
apply np.
exact p.
Qed.

Lemma T2 : (P -> Q) -> (P /\ (Q -> R)) -> Q /\ R.
intros pq pqr.
destruct pqr.
split.
apply pq.
assumption.
apply H0.
apply pq.
assumption.
Qed.

(**
Lemma T3 : (P /\ R -> Q /\ R) -> P -> Q.
unprovable **)

(**
Lemma T4 : Q \/ P -> Q.
unprovable **)


Lemma T5 : Q \/ Q -> Q.
intro.
destruct H as [q | q].
exact q.
exact q.
Qed.

Lemma T6 : (P \/ Q -> R) <-> (P -> R) /\ (Q -> R).
split.
intro.
split.
intro p.
apply H.
left.
assumption.
intro q.
apply H.
right.
exact q.

intros.
destruct H.
destruct H0.
apply H.
exact H0.

apply H1.
exact H0.
Qed.

Lemma AndOrDist : P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
split.

intro.
destruct H.

destruct H0.
left.
split;
assumption.

right.
split;
assumption.


intro.
destruct H.
destruct H.
split.
assumption.
left.
assumption.

destruct H.
split.
assumption.
right.
exact H0.
Qed.


Require Import Coq.Logic.Classical.

(** classic : forall P : Prop , P \/ ~ P **)
(** In classical logic, we do not have to give evidence to prove something **)


Lemma Classic_Example : Tomorrow_will_rain \/ ~ Tomorrow_will_rain.
(** Its impossible to have any evidence of whether it will rain tomorrow **)
destruct (classic Tomorrow_will_rain).
left.
assumption.
right.
assumption.
Qed.

(**
exact (classic Tomorrow_will_rain).
Qed.
**)

Lemma Eq1 : P \/ Q <-> ~ P -> Q.
split.
intros.
destruct H.

destruct (H0 H).
exact H.
intro.


destruct (classic P).

left.
assumption.

right.
apply H.
exact H0.
Qed.