CoqEx16-18.v

(* Q16 *)
Definition tautology : forall P : Prop, P -> P := 
  fun (P : Prop) (H : P) => H.


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


Definition Disjunctive_syllogism : 
  forall P Q : Prop, (P \/ Q) -> ~P -> Q 
:=
  fun (P Q : Prop) (p_or_q : P \/ Q) (np : ~P) =>
    match p_or_q with
    | or_introl p => False_ind Q (np p)
    | or_intror q => q
    end.
   
 
Definition tautology_on_Set : forall A : Set, A -> A :=
  fun (A : Set) (a : A) => a.

Definition Modus_tollens_on_Set :
  forall A B : Set, (B -> Empty_set) * (A -> B) -> (A -> Empty_set)
:=
  fun (A B : Set) pair a => let (nb,a2b) := pair in nb (a2b a).

Definition Disjunctive_syllogism_on_Set : 
  forall A B : Set, (A + B) ->  (A -> Empty_set) -> B :=
  fun (A B : Set) a_or_b na => 
    match a_or_b with
    | inl a => Empty_set_rect (fun _ => B) (na a) 
    | inr b => b
    end.

(* Q17 *)
Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  refine (fun P Q R => _). (*intros P Q R.*)
  refine (fun H => _). (*intros H.*)
  refine (match H with | or_introl HP => _ 
                       | or_intror HnQR => _ end). (* destruct H as [HP | HnQR].*)
  - refine (conj _ _). (*split.*)
    + refine (or_introl _). (* left. *)
      refine HP. (* exact HP *)
    + refine (or_introl _). (* left. *)
      refine HP. (* exact HP.*)
  - refine (conj _ _). (* split. *)
    + refine (or_intror _). (* right. *)
      refine (fun HQ => _). (* intros HQ. *)
      refine (HnQR _). (* apply HnQR. *)
      refine (or_introl _). (* left.*)
      refine HQ. (* exact HQ.  *)
    + refine (or_intror _). (* right. *)
      refine (fun HR => _) . (* intros HR. *)
      refine (HnQR _). (* apply HnQR. *)
      refine (or_intror _). (* right. *)
      refine HR. (* exact HR. *)
Qed.

(* Q18 *)
Require Import Arith.
Definition Nat : Type := forall A : Type, (A -> A) -> (A -> A).

Definition NatPlus (n m : Nat) : Nat :=
  fun (A : Type) (f : A -> A) (a : A) => n A f (m A f a).

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.
  intros.
  unfold Nat2nat.
  unfold nat2Nat.
  unfold NatPlus.
  induction n.
  simpl.
  induction m.
  simpl.
  reflexivity.
  simpl.
  f_equal.
  apply IHm.
  simpl.
  f_equal.
  apply IHn.
  Qed.