coq_practice_4_(16~18).v

Definition tautology : forall P : Prop, P -> P
  := fun p => fun p => p.



Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun p q (H : ~ q /\ (p -> q)) ( H0 : p) => 
  match H with
  | conj H1 H2 => H1 (H2 H0)
  end.


Definition Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q
  := fun p q (H: (p \/ q)) (H0: ~p)=>
  match H with
  | or_introl H1 => match (H0 H1) return q with end
  | or_intror H2 => H2
  end.

Definition tautology_on_Set : forall A : Set, A -> A
  := fun a (H: a) => H.

Definition Modus_tollens_on_Set : forall A B : Set, (B -> Empty_set) * (A -> B) -> (A -> Empty_set)
  := fun a b (H : (b -> Empty_set) * (a -> b)) (H0 : a) => ((fst H)((snd H) H0 )).
 
Definition Disjunctive_syllogism_on_Set : forall A B : Set, (A + B) -> (A -> Empty_set) -> B
  := fun a b  (H: (a + b)) (H0: (a -> Empty_set )) => 
  match H with
  | inl H1 => match (H0 H1) return b with end
  | inr H1 => H1
  end.


Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  refine (fun P Q R => _).
  refine (fun H => _).
  refine (match H with | or_introl HP => _ | or_intror HnQR => _ end).
    refine (conj _ _).
      refine (or_introl _).
      refine (HP).
      refine (or_introl _).
      refine (HP).
    refine (conj _ _).
      refine (or_intror _).
      refine (fun HQ => _).
      refine (HnQR _).
      refine (or_introl _).
      refine (HQ).
      refine (or_intror _).
      refine (fun HR => _).
      refine (HnQR _).
      refine (or_intror _).
      refine (HR).
Qed.




Require Import Arith.

Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).


(*
nat_iter O f => λx-> f x
nat_iter 2 f => λx-> f f f x
*)

Definition NatPlus(n m : Nat) : Nat := 
  fun p q r =>n p q (m p q r).

Definition nat2Nat : nat -> Nat := nat_iter.

Definition Nat2nat(n : Nat) : nat := n _ S O.


Lemma NatPlus_plus :
  forall n m, Nat2nat (NatPlus (nat2Nat n) (nat2Nat m)) = n + m.
Proof.

  assert (forall p q,(nat2Nat p) _ S q = p + q).
    unfold nat2Nat.
    intros.
    induction p.
    simpl.
    reflexivity.
    simpl.
    rewrite IHp.
    reflexivity.
  
  

  unfold Nat2nat.
  unfold NatPlus.
  unfold nat2Nat.
  unfold nat_iter.
  induction n.
    intros.
    induction m.
      trivial.

      simpl.
      rewrite IHm.
      trivial.


    unfold NatPlus in H.
    unfold nat2Nat in H.
    unfold nat_iter in H.
    destruct m.

      simpl.
      apply NPeano.Nat.succ_inj_wd.
      rewrite (H n).
      trivial.
     

     simpl.
     apply NPeano.Nat.succ_inj_wd.
     rewrite (H m O).
     assert (S (m + O) = S m).
       apply NPeano.Nat.succ_inj_wd.
       apply plus_0_r.
     rewrite H0.
     rewrite (H n (S m)).
     trivial.

Qed.