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