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

    T01
**)

Section T01.


(**

1. Remember the basics:

Connectives:

and do not forget the precedence of connectives.

Introduction and elimination for tactics: 

**)

Variable P Q R : Prop.

Variable Tomorrow_will_rain : Prop.

(** 
The approach to prove something in constructive logic is of course constructing
proof terms
**)


(** warm up **)

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

(** 
Tautology : something always true e.g. P -> P,  P /\ Q -> Q /\ P and all the theorems 

Negation in constructive logic is defined as:

~ P = P -> False

What are True and False?
something true is something exists (or we can construct), something false is just something that CANNOT exist in the system (notice the difference with classical logic what we will talk later) 
**)

Lemma triv : True.
split.
Qed.

(** If we have False we can prove anything, the system just crashes! **) 

Lemma exFalso : False -> Q.
intro f.
destruct f.
Qed.

(**
so "P -> False" means that once we have P we achieve "False" which is not allowed.
so ~P actually works as "we do not allow P to be true so it is definitely false
**)

(** hint: Before writing tactics,
try to think of whether it is obvious that you cannot construct it or not

e.g. P -> Q  and P -> P

it could save your time.

But beware that something you, for the moment, cannot construct the proof for it could be
1. unprovable
   - unprovable in constructive logic
   - wrong
2. difficult

**)


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

can we construct Q from what we have?

unprovable **)

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


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

(** try to interpret "code" so that it looks simpler **)

Lemma T5 : (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.

(**

Constructive logic vs Classical logic


In classical logic, we do not have to give evidence to prove something

**)
Require Import Coq.Logic.Classical.
(** With this you can use

classic : forall P : Prop , P \/ ~ P

so that you are able to prove something classical **)

Lemma Classic_Example : Tomorrow_will_rain \/ ~ Tomorrow_will_rain.
(** It is impossible to have any evidence something has not happened yet **)
destruct (classic Tomorrow_will_rain).
left.
assumption.
right.
assumption.
Qed.

Lemma Equivalent1 : 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.


(** Try to prove a small quiz: there are three blocks,

Green
Unknown
Not Green

How to prove there must be two adjacent pair of blocks

Green
Not Green

  **)