Require Import Setoid.
Axiom PNP : forall p : Prop, p \/ ~p.
Lemma L0 : forall  (x y : Prop), x->y->x.
Proof.
   intros x y.
   intros H1 H2.
   assumption.
   Qed.

Lemma L1: forall (x y : Prop), x -> (x \/ y).
Proof.
    intros x y.
    intros H1.
    left.
    exact H1.
    Qed.

Lemma L2: forall (x y : Prop), x->y->(x/\y).
Proof.
    intros x y.
    intros H1 H2.
    split.
    exact H1.
    exact H2.
    Qed.


Lemma L3: forall (x y : Prop), (x->y)->(~y->~x).
Proof.
    intros x y.
    intros H1 H2.
    intro H3.
    apply (H2 (H1 H3)).
    Qed.

Theorem T2: forall (e f g h  : Prop), (e->(f/\~g))->((f\/g)->h)->e->h.
Proof.
    intros e f g h.
    intros H1.
    intros H2.
    intros H3.
    apply H1 in H3.
    destruct H3 as [H3a H3b].
    assert (H4 : f->(f\/g)).
    apply L1.
    apply (H2 (H4 H3a)).
    Qed.

Theorem T3: forall x : Prop, x<->~~x.
Proof.
    intro x.
    split.
    intro H1.
    intro H2.
    apply (H2 H1).
    intro H3.
    destruct (PNP x) as [H9a | H9b].
    exact H9a.
    apply H3 in H9b.
    contradict H9b.
    Qed.

Theorem DM1: forall (p q : Prop), ~(p\/q)<->(~p/\~q).
Proof.
    intros p q.
    split.
    intro H1.
    split.
    intro H2.
    destruct H1.
    left.
    exact H2.
    intro H3.
    destruct H1.
    right.
    exact H3.
    intro H4.
    intro H5.
    destruct H4.
    destruct H5.
    apply (H H1).
    apply (H0 H1).
    Qed.


Theorem DM2: forall (p q :Prop), ~(p/\q) <-> (~p\/~q).
Proof.
     intros p q.
     split.
     intro H1.
     destruct (PNP p).
     destruct (PNP q).
     destruct H1.
     split.
     exact H.
     exact H0.
     right.
     exact H0.
     left.
     exact H.
     intro H1.
     destruct H1.
     intro H2.
     destruct H2.
     apply (H H0).
     intro H3.
     destruct H3.
     apply (H H1).
     Qed.

Theorem T10 {T: Type} : forall (p : T -> Prop), ~(exists x, p x) <-> (forall x, ~p x).
Proof.
    intros p.
    split.
    intro H1.
    intro x.
    intro H2.
    destruct H1.
    exists x.
    assumption.
    intro H1.
    intro H2.
    destruct H2.
    apply (H1 x).
    exact H.
    Qed.

Theorem T11 {T: Type} : forall (p : T -> Prop), ~(forall x, p x) <-> (exists x, ~p x).
Proof.
    intro p.
    split.
    intro H1.
    destruct (PNP (exists x , ~p x)).
    assumption.
    destruct H1.
    rewrite T10 in H.
    intro x.
    apply T3.
    apply (H x).
    intro H1.
    intro H2.
    admit.
    Qed.

Theorem T12 {T:Type}:
      forall (p q r : Prop),
      p\/(q/\r) <-> (p\/q)/\(p\/r).
Proof.
intros p q r.
split.
intro H1.
split.
destruct H1.
left.
assumption.
destruct H as [H1a H1b].
right.
assumption.
destruct H1.
left.
assumption.
destruct H as [H1a H1b].
right.
assumption.

intro H1.
destruct H1 as [H1a H1b].
destruct H1a as [H1aa | H1ab].
left.
assumption.
destruct H1b as [H1ba | H1bb].
left.
assumption.
right.
split.
assumption.
assumption.

Qed.

Theorem T13 {T:Type}:
      forall (p q r : Prop),
      p/\(q\/r) <-> (p/\q)\/(p/\r).
Proof.
intros p q r.
split.
intro H1.
destruct H1 as [H1a H1b].
destruct H1b as [H1ba | H1bb].
left.
split.
assumption.
assumption.
right.
split.
assumption.
assumption.
intro H1.
destruct H1 as [H1a | H1b].
destruct H1a as [H1ba  H1bb].
split.
assumption.
left.
assumption.
destruct H1b as [H1ba  H1bb].
split.
assumption.
right.
assumption.


Qed.

Theorem T100 {T1 T2: Type} {w: T1} : forall (A: T1 ->Prop) (B: T2->Prop), (forall x ,(exists y, A x /\ B y)) -> (exists y ,(forall x, A x /\ B y)).
Proof.
    intros A B.
    intro H1.
    destruct (PNP (exists y, B y)) as [H2a | H2b].
    destruct H2a as [y H2a].
    exists y.
    intro x.
    split.
    specialize (H1 x).
    destruct H1 as [z [H1a _]].
    assumption.
    assumption.
    destruct H2b.
    destruct (H1 w) as [y [_ H1b]].
    exists y.
    assumption.
    Qed.


Theorem  T101 {T1 T2: Prop} {w: T1} : forall (A: T1 ->Prop) (B: T2->Prop), (forall x ,(exists y, A x /\ B y)) -> ((forall x, A x) /\ (exists y, B y)).
Proof.
    intros A B.
    intro H1.
    split.
    intro x.
    specialize (H1 x).
    destruct H1 as [y [H1a H1b]].
    assumption.
    specialize (H1 w).
    destruct H1 as [y [_ H1b]].
    exists y.
    assumption.
    Qed.

Theorem T102 {w : Type} : forall (A B : Type->Prop), ((exists x, A x) -> (exists y, B y)) -> (exists x, A x -> (exists y, B y)).
Proof.
    intros A B.
    intro H1.
    exists w.
    intro H2.
    destruct H1.
    exists w.
    assumption.
    exists x.
    assumption.
    Qed.

Theorem T103 {w:Type}:
     forall (X Y Z A:Type->Prop),
     (forall x, (X x \/ Y x -> Z x))->
     (forall x, (Z x \/ A x -> X x/\ Y x))->
     (forall x, X x <-> Z x).
Proof.
intros X Y Z A.
intro H1.
intro H2.
intro x.
split.
intro H3.
specialize (H1 x).
assert (X x \/ Y x).
left.
assumption.
apply (H1 H).
admit.
Qed.

Require Import Arith.
Require Import Setoid.

Eval cbv in (S 5).

Theorem out_plus_0_l : forall a , 0+a = a.
Proof.
    intro a.
    rewrite -> plus_0_l.
    reflexivity.
    Qed.

Theorem out_plus_0_r : forall a , a+0 = a.
Proof.
    intro a.
    induction a.
    reflexivity.
    unfold plus.
    fold plus.
    rewrite -> IHa.
    reflexivity.
    Qed.

Lemma L4 : forall a b : nat, S a + b = S(a+b).
Proof.
    intros a b.
    unfold plus.
fold plus.
reflexivity.
Qed.

Lemma L5: forall a b : nat, a + S b = S(a+b).
Proof.
intros a b.
induction a.
reflexivity.
unfold plus.
fold plus.
rewrite -> IHa.
reflexivity.
Qed.

Theorem our_plus_comm: forall a b :nat, a+b = b+a.
Proof.
intros a b.
induction a.
rewrite -> out_plus_0_r.
rewrite -> out_plus_0_l.
reflexivity.
unfold plus.
fold plus.
rewrite -> IHa.
rewrite -> L5.
reflexivity.
Qed.


Theorem our_plus_assoc: forall a b c:nat, a+(b+c) = a+b+c.
Proof.
intros a b c.
induction a.
unfold plus.
fold plus.
reflexivity.
unfold plus.
fold plus.
rewrite -> IHa.
reflexivity.
Qed.

Theorem our_mult_0_l: forall a:nat, 0*a = 0.
Proof.
intros a.
reflexivity.
Qed.

Theorem our_mult_0_r: forall a:nat, a*0 = 0.
Proof.
intros a.
induction a.
reflexivity.
unfold mult.
fold mult.
rewrite -> IHa.
reflexivity.
Qed.

Theorem our_mult_1_l: forall a:nat, 1*a = a.
Proof.
intros a.
unfold mult.
rewrite -> out_plus_0_r.
reflexivity.
Qed.

Theorem our_mult_1_r: forall a:nat, a*1 = a.
Proof.
intros a.
induction a.
reflexivity.
unfold mult.
fold mult.
rewrite -> IHa.
unfold plus.
reflexivity.
Qed.


Lemma L6: forall a b : nat, S a * b = b + a*b.
Proof.
intros a b.
unfold mult.
fold mult.
reflexivity.
Qed.

Lemma L7: forall a b : nat, a * S b = a + a * b.
Proof.
intros a b.
induction a.
unfold mult.
reflexivity.
unfold mult.
fold mult.
rewrite IHa.
unfold plus.
fold plus.
rewrite -> our_plus_assoc.
rewrite -> our_plus_assoc.
rewrite -> (our_plus_comm b a).
reflexivity.
Qed.

Theorem our_mult_comm: forall a b :nat, a*b = b*a.
Proof.
intros a b.
induction a.
unfold mult.
fold mult.
rewrite -> our_mult_0_r.
reflexivity.
unfold mult.
fold mult.
rewrite -> IHa.
rewrite -> L7.
reflexivity.
Qed.

Theorem our_mult_distr_r : forall a b c : nat,  (a+b)*c = a*c + b*c.
Proof.
intros a b c.
induction a.
reflexivity.
rewrite -> L4.
unfold mult.
fold mult.
rewrite -> IHa.
rewrite -> our_plus_assoc.
reflexivity.
Qed.


Theorem our_mult_distr_l : forall a b c :nat , a*(b+c) = a * b + a * c.
Proof.
intros a b c.
rewrite -> (our_mult_comm _ (b+c)).
rewrite -> our_mult_distr_r.
rewrite -> (our_mult_comm b a).
rewrite -> (our_mult_comm c a).
reflexivity.
Qed.



Theorem our_mult_assoc: forall a b c:nat, a*(b*c) = a*b*c.
Proof.
intros a b c.
induction a.
unfold mult.
reflexivity.
unfold mult.
fold mult.
rewrite -> IHa.
rewrite -> our_mult_distr_r.
reflexivity.
Qed.

Inductive day : Type :=
| sunday : day
| monday : day
| tuesday : day
| wednsday : day
| thursday : day
| friday : day
| saturday : day.

Inductive nat' : Type :=
| z : nat'
| S : nat' -> nat'.

Inductive bin : Type :=
| E : bin
| B0 : bin -> bin
| B1 : bin -> bin.

Definition next_day  (d : day) : day :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednsday
| wednsday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
end.