Q19よくわかってない

4.v

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

Definition Modus_tollens : forall P Q : Prop, ~Q /¥ (P -> Q) -> ~P
  := fun _ _ h p => let (q,f) := h in q (f p).

Definition Disjunctive_syllogism : forall P Q : Prop, (P ¥/ Q) -> ~P -> Q
  := fun _ _ pq np => match pq with
  | or_introl p => match np p with end
  | or_intror q => q
  end.

Definition tautology_on_Set : forall A : Set, A -> A
  := fun _ a => a.

Definition Modus_tollens_on_Set : forall A B : Set, (B -> Empty_set) * (A -> B) -> (A -> Empty_set)
  := fun _ _ h a => let (b,f) := h in b (f a).

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

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

Module Q18.
Require Import Arith.

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

Definition NatPlus(n m : Nat) : Nat :=
  fun _ s z => n _ s (m _ s z).

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 NatPlus, Nat2nat.
induction n; simpl.
- induction m.
  + reflexivity.
  + simpl. rewrite IHm. reflexivity.
- rewrite IHn. reflexivity.
Qed.
End Q18.

Module Q19.
Parameter A : Set.
Definition Eq : A -> A -> Prop := fun a b =>
  forall T : A -> Prop, T a -> T b.

Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros.
split; intro.
- apply H. reflexivity.
- rewrite H. intro. intro. assumption.
Qed.
End Q19.

Module Q20.
Section Q19_Type.
Variable A : Type.
Definition Eq : A -> A -> Prop := fun a b =>
  forall T : A -> Prop, T a -> T b.

Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros.
split; intro.
- apply H. reflexivity.
- rewrite H. intro. intro. assumption.
Qed.
End Q19_Type.

Definition surjection (A B : Set) (f : A -> B)
  := forall b, exists a, f a = b.

Lemma nat_natbool_no_surjection :
  forall A, ~ exists f, surjection A (A -> bool) f.
Proof.
intros A Hs. destruct Hs as [f Hs].
set (X := fun x => negb (f x x)).
unfold surjection in Hs. specialize Hs with X.
destruct Hs as [a HfaX].
assert (H : f a a = X a).
  rewrite HfaX. reflexivity.
unfold X in H.
destruct (f a a); inversion H.
Qed.

Theorem nat_natbool_diff: nat <> (nat->bool).
Proof.
intro.
apply Eq_eq in H. unfold Eq in H.
specialize H with (fun A => exists f, surjection nat A f). simpl in H.
eapply nat_natbool_no_surjection. apply H.
exists (fun x => x).
intro. exists b. reflexivity.
Qed.
End Q20.