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