(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li

    T05

**)

Section CW2.


Variable People : Set.

Variables Male Female : People -> Prop.
(* Male x = x is a male
   Female x = x is a female
*)

Variable Parent : People -> People -> Prop.
(* Parent x y = x is the parent of y *)


Definition Father (x y : People) :=
  Male x /\ Parent x y.

Definition Mother (x y : People) :=
  Female x /\ Parent x y.

Definition Sibling (x y : People) :=
   ~ (x = y) /\ exists p : People, Parent p x /\ Parent p y.

Definition halfSibling (x y : People) :=
  Sibling x y /\ (exists p, (Parent p x /\ ~ Parent p y) \/ (Parent p y /\ ~Parent p x)).

Definition halfSibling2 (x y : People) :=
  ~ ((exists f : People, Father f x /\ Father f y) <-> (exists m : People, Mother m x /\ Mother m y)).

Require Import Coq.Logic.Classical.

Variable A B  : Set.

Variable P : A -> Prop.
Variables R : A -> B -> Prop.

Lemma demorgan2 : (~ forall x : A, P x) <-> exists x : A, ~ P x.
split; intro.
apply NNPP. intro.
apply H.
intro.
apply NNPP.
intro.
apply H0.
exists x.
assumption.

destruct H.
intro.
apply H.
apply H0.
Qed.

Lemma dp : (exists x:A, True) -> exists x:A, P x -> forall x:A, P x.
intros.
destruct H.
destruct (classic (forall x : A, P x)).
exists x.
intro.
exact H0.
assert (exists x0 : A, ~P x0).
apply demorgan2.
exact H0.
destruct H1.
exists x0.
intro.
destruct (H1 H2).
Qed.

End CW2.

Section T5.

Load Arith.

(** try to find out some useful lemmas in Arith **)
Lemma n_Sn : forall n : nat, n <> S n.
intro.
intro.
induction n.
discriminate H.
apply IHn.
apply peano8.
assumption.
Qed.

Lemma eq_les_S : forall m n : nat, m = n -> S m = S n.
intros.
rewrite H.
reflexivity.
Qed.

Lemma eq_add_S : forall m n, S m = S n -> m = n.
intros.
fold (pred (S m)).
rewrite H.
unfold pred.
reflexivity.
Qed.

Fixpoint g (m n : nat) {struct m} : nat :=
  match m with 
  | 0 => n
  | S m' => S (g m' n)
  end.

(* What is g? Try a few examples *)
Eval compute in (g 1 2).
Eval compute in (g 10 12).

(* How to define mutiplication *)

Fixpoint mul (m n : nat) {struct m} : nat :=
  match m with
    | 0 => 0
    | S m' => n + (mul m' n)
  end.

(* The decidable even function *)

Fixpoint even (m : nat) : bool :=
  match m with
    | 0 => true
    | S m' => negb (even m')
  end.


Theorem nneven : forall n: nat, even (n + n) = true.
intro.
induction n.
simpl.
reflexivity.
simpl.
rewrite plus_comm.
simpl.
rewrite IHn.
simpl.
reflexivity.
Qed.

Theorem sym : forall a b : nat, a = b -> b = a.
intros.
symmetry.
assumption.
Qed.

(* These should be proved by yourselves *)
Axiom mult_comm : forall n m, n * m = m * n.

Axiom mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.

Axiom mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.

Theorem binomial : forall m n : nat, (m + n) * (m + n) = m * m + 2 * m * n + n * n.
intros.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
rewrite mult_plus_distr_l.
rewrite plus_assoc.
assert (m * n + n * m = 2 * m  * n).
simpl.
rewrite<- plus_n_O.
rewrite mult_plus_distr_r.
pattern (n * m).
rewrite mult_comm.
reflexivity.
rewrite<- H.
rewrite plus_assoc.
reflexivity.
Qed.

Lemma t2 : forall n, n = S n -> n = n + 1.
intros.
destruct (n_Sn n H).
Qed.


(* Do not erase the following line in your cw *)
Notation "m <= n" := (leq m n).

Theorem le2n : forall n : nat, n <= (n + n).
intro.
unfold leq.
exists n.
reflexivity.
Qed.

(**To prove Even is decidable (optional)
Notice : the proofs use inversion which may not be allowed to use in cw, here just the idea of how to prove some predicates are decidable **)

Inductive Even : nat -> Prop :=
  | z : Even 0
  | e : forall n: nat, Even n -> Even (S (S n)).
                                               
Lemma even_odd : forall n, exists k, n = k + k \/ n = S (k + k).
induction n.
exists 0.
left.
split.
destruct IHn.
destruct H.
exists x.
right.
rewrite H.
split.
exists (S x).
left.
rewrite H.
rewrite plus_n_Sm.
split.
Qed.

Lemma double_even : forall k, even (k + k) = true.
intros.
induction k.
split.
rewrite<- plus_n_Sm.
simpl.
rewrite IHk.
split.
Qed.



Lemma double_Even : forall k, Even (k + k).
intros.
induction k.
exact z.

rewrite<- plus_n_Sm.
exact (e (k + k) IHk).
Qed.

Lemma not_Even : forall k, ~ Even (S (k + k)).
intros.
intro.
induction k.
inversion H.
apply IHk.
rewrite<- plus_n_Sm in H.
inversion H.
exact H1.
Qed.

Theorem e_sound : forall m, Even m -> even m = true.
intros.
destruct (even_odd m).
destruct H0.
rewrite H0.
apply double_even.
rewrite H0 in H.
destruct (not_Even x H).
Qed.


Theorem e_compl : forall m, even m = true -> Even m.
intros.
destruct (even_odd m).
destruct H0.
rewrite H0.
apply double_Even.
rewrite H0.
rewrite H0 in H.
simpl in H.
rewrite double_even in H.
discriminate H.
Qed.

Theorem e_dec : forall m, Even m <-> even m = true.
split.
apply e_sound.
apply e_compl.
Qed.


End T5.