課題24, 25 がわからなさすぎるのでとりあえずここまで

5.v

Module Q21.
Require Import Classical.
Lemma ABC_iff_iff : forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
intros.
pose (HA := classic A). pose (HB := classic B). pose (HC := classic C).
destruct HA; destruct HB; destruct HC; tauto.
Qed.

Goal
  forall P Q R : Prop,
  (IF P then Q else R) ->
  exists b : bool,
  (if b then Q else R).
Proof.
intros.
destruct H as [H|H]; destruct H as [H1 H2].
- exists true.  assumption.
- exists false. assumption.
Qed.

Require Import ClassicalDescription.

Definition func : forall P : nat -> Prop, nat -> bool := fun P n =>
  if excluded_middle_informative (P n) then true else false.

Goal
  forall P Q R : nat -> Prop,
  (forall n, IF P n then Q n else R n) ->
  exists f : nat -> bool,
  (forall n, if f n then Q n else R n).
Proof.
intros. exists (func P).
intro n. unfold func. specialize (H n).
destruct (excluded_middle_informative (P n));
  destruct H as [H|H]; destruct H; try contradiction; assumption.
Qed.
End Q21.

Module Q22.
Require Import ClassicalDescription FunctionalExtensionality.

Record isomorphism{A B : Type} (f : A -> B) : Prop := {
  inverse : B -> A;
  is_retraction b : f (inverse b) = b;
  is_section a : inverse (f a) = a
}.

Notation isomorphic A B :=
  (exists f, @isomorphism A B f).

Lemma neg_unique :
  forall A,
    { isomorphic (A -> Empty_set) Empty_set } +
    { isomorphic (A -> Empty_set) unit }.
Proof.
intro.
pose (H := excluded_middle_informative (exists _:A, True)).
destruct H.
- left. destruct e as [a _].
  exists (fun f => f a). exists (fun e _ => e).
  + intros. reflexivity.
  + intros f. pose (fa := f a). inversion fa.
- right.
  exists (fun _ => tt).
  exists (fun _ a => match n (ex_intro (fun _ => True) a I) return Empty_set
                     with end).
  + intro. destruct b. reflexivity.
  + intros. apply functional_extensionality. intro. contradiction.
Qed.
End Q22.

Module Q23.
Definition compose {A B C} (f : A -> B) (g : B -> C) :=
  fun x => g (f x).

Parameter X Y : Type.
Parameter f : X -> Y.

Axiom epi : forall Z (g h : Y -> Z), compose f g = compose f h -> g = h.

Require Import ClassicalDescription FunctionalExtensionality.

Lemma surj : forall y, exists x, f x = y.
Proof.
intro y. apply NNPP. intro H.
pose (g := fun x => if excluded_middle_informative (x = y) then true else false).
pose (h := fun _:Y => false).
assert (Heqgh : g = h).
  apply epi. apply functional_extensionality. intro.
  unfold compose, g, h. destruct (excluded_middle_informative (f x = y)).
  contradict H. exists x. assumption. reflexivity.
assert (Heq : g y = h y) by (rewrite Heqgh; reflexivity).
unfold g, h in *. destruct (excluded_middle_informative (y = y)).
inversion Heq. apply n. reflexivity.
Qed.

Require Import IndefiniteDescription.

Lemma split_epi : exists g, compose g f = id.
Proof.
pose (Hg := fun y => constructive_indefinite_description _ (surj y)). simpl in Hg.
pose (g := fun y => let (x,_) := Hg y in x). exists g.
apply functional_extensionality. intro y. unfold compose, id, g.
clear g. destruct (Hg y). assumption.
Qed.
End Q23.