(** Introduction to Formal Reasoning (G52IFR) Nuo Li T02 Predicate Logic Read this part carefully in the coursework. **) Section Ex1. Variable P Q : Prop. Require Import Coq.Logic.Classical. Lemma Pierce : ((P -> Q) -> P) -> P. destruct (classic P) as [p | np]. intro. exact p. intro. apply H. intro p. destruct (np p). Qed. End Ex1. Section T. (** Quantifiers, rules and <> **) Variable Node : Set. Variable Connect : Node -> Node -> Prop. Variable Independent : Node -> Prop. Variables A : Set. Variables P : A -> Prop. Variables Q : Prop. (** If A is connected to B then vice versa **) Hypothesis h1 : forall A B : Node, Connect A B -> Connect B A. (** If A is linked to B and B is linked to C then A is linked to C **) Hypothesis h2 : forall A B C : Node, Connect A B -> Connect B C -> Connect A C. (** There is a node being connected with all the others **) Hypothesis h3 : exists A : Node, forall x : Node, x <> A -> Connect A x. (** Indepedent node is a node that is not connected to anyone (including itself) **) Hypothesis h4 : forall A : Node, Independent A <-> (forall B : Node, ~Connect A B). (** this is hard to interpret so we can use example **) (** P : if x is white **) (** Q : Game Over **) Lemma t2 : (exists x : A, P x) -> Q <-> forall x : A, P x -> Q. split. intros. apply H. exists x. exact H0. intros. destruct H0. apply (H x). exact H0. Qed. Lemma t3 : forall x y : A, x = y -> P x = P y. intros. rewrite H. reflexivity. Qed. Lemma t4 : (exists x : A, True) -> ~ (forall x y : A, x <> y). intro. destruct H. intro. apply (H0 x x). reflexivity. Qed. (** The drink pub problem **) End T.