(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li and Nicolai Kraus

    T02 Predicate Logic
**)




Section Family.


Variable People : Set.

(** some people **)

Hypothesis Ann : People.
Hypothesis Kate : People.
Hypothesis Peter : People.


(** We have two predicates about the gender **)
Variables Male Female : People -> Prop.
(** Male x = "x is male" **)

Variables Child : People -> People -> Prop.
(** Child x y = "x is the Child of y" **)


(** Kate is the daughter of Ann **)
Hypothesis h1 : Female Kate /\ Child Kate Ann.


(** Kate and Peter are (half or full) siblings **)
Hypothesis h2 : exists p : People, Child Kate p /\ Child Peter p.


(** Kate and Peter are 'full' siblings **)
Hypothesis h3 : exists dad : People, exists mum : People, 
   Child Kate dad /\ Child Kate mum /\ Child Peter dad /\ Child Peter mum
   /\ mum <> dad.
 (** h2 /\ h2 = h2**)
 (** mum <> dad  is the same as   not (mum = dad)   **)

(** same again! **)
Hypothesis h4 : forall p : People, Child Kate p <-> Child Peter p.


(** No one is the parent of all the others **)
Hypothesis h5 : ~ exists p : People, forall c : People, Child c p.


(** There is someone with exactly one child **)
Hypothesis h6 : exists p : People, exists c : People, Child c p /\
   forall d : People, Child d p -> d = c. 


End Family.






Section Misc.

Variable A : Set.
Variable P : A -> Prop.
Variable Q : Prop.



Lemma curry_dependend : (exists x : A, P x) -> Q 
                      <->
           forall x : A, P x -> Q.
split.
intro.
intros x p.
apply H.
exists x.
assumption.

intros p2q p.
destruct p as [a pa].

apply (p2q a).
exact pa.
Qed.

(**

A x B -> C

<=== (un)curry ===>

A -> B -> C

**)

Lemma sym : forall x y : A, x = y -> y = x.
intros x y.
intro p.
rewrite <- p. (** or just without <- **)
reflexivity.
Qed.



(** if there is much time, we can do the following: **)

(** the two axioms for classical logic are equivalent: **)

Lemma TND_NNPP : (forall P : Prop, P \/ ~P) <-> (forall P : Prop, ~~P -> P).
split.
intros pnp P0 nnp.
destruct (pnp P0) as [p0 | np0].
assumption.
destruct (nnp np0).

intro nnp2p.
intro P0.
apply nnp2p. (** what exactly happens here? Try to figure it our! *)
intro nTNDp0.
apply nTNDp0.
right.
intro p0.
apply nTNDp0.
left.
exact p0.
Qed.


Require Import Coq.Logic.Classical.

(** with classical logic, we therefore can show "reductio ad absurdum" : **)

Lemma reductio_ad_absurdum : (forall P : Prop, ~~P -> P).
assert (tnd_nnpp := TND_NNPP).
destruct tnd_nnpp as [important notImportant].
apply important.
intro.
exact (classic P0).
Qed.

(** but it is in the library anyway... **)

Lemma reductio_ad_absurdum2 : (forall P : Prop, ~~P -> P).
apply NNPP.
Qed.


End Misc.