(** 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.