Library exercise
Require Import prelude.
Section CB.
Variable EM : forall A : Type, A + ¬ A.
Variable A B : Type.
Variable f : A -> B.
Variable g : B -> A.
Variable f_inj : injective f.
Variable g_inj : injective g.
Inductive C : A -> Type :=
C_i : forall b : B, (forall a, f a = b -> C a) -> C (g b).
Definition g_inv (a : A) : C a -> B :=
fun p => match p with
C_i b _ => b
end.
Lemma g_g_inv_eq : forall a p, g (g_inv a p) = a.
intros ? []; reflexivity.
Qed.
Lemma g_inv_g_eq : forall b p, g_inv (g b) p = b.
intros; apply g_inj, g_g_inv_eq.
Qed.
Definition r : A -> B :=
fun a => match EM (C a) with
inl c => g_inv _ c
| inr _ => f a
end.
Definition f_inv (b : B) : ¬ C (g b) -> A :=
fun nc =>
match EM (Σ a, f a = b) with
inl p => π₁ p
| inr p => match nc (C_i b (curry (C := fun a _ => C a) (fun q => match p q return C (π₁ q) with end))) with end
end.
Lemma f_f_inv_eq : forall b p, f (f_inv b p) = b.
intros ? ?; unfold f_inv.
destruct (EM (Σ a, f a = b)).
- exact (π₂ s).
- exfalso; apply p; constructor; intros; exfalso; eauto.
Qed.
Lemma f_inv_f_eq : forall a p, f_inv (f a) p = a.
intros; apply f_inj, f_f_inv_eq.
Qed.
Definition r_inv : B -> A :=
fun b => match EM (C (g b)) with
inl c => g b
| inr c => f_inv _ c
end.
Lemma r_rinv : section_retraction r r_inv.
intros a; unfold r.
destruct (EM (C a)) as [c|nc]; unfold r_inv.
+ destruct (EM (C (g (g_inv a c)))).
- apply g_g_inv_eq.
- exfalso; rewrite g_g_inv_eq in *; auto.
+ destruct (EM (C (g (f a)))).
- exfalso; apply nc. inversion c; subst.
apply X, g_inj; auto.
- apply f_inv_f_eq.
Qed.
Lemma rinv_r : section_retraction r_inv r.
intros a; unfold r_inv, r.
case_eq (EM (C (g a))); intros ? ?.
+ rewrite H; apply g_inv_g_eq.
+ destruct (EM (C (f_inv a f0))).
- exfalso; apply f0; constructor; intros; subst.
rewrite f_inv_f_eq in c; assumption.
- apply f_f_inv_eq.
Qed.
Lemma inverse_r_r_inv : inverse r r_inv.
split; [apply r_rinv | apply rinv_r].
Qed.
Lemma isomorphism_r : isomorphism r.
exists r_inv; apply inverse_r_r_inv.
Qed.
Theorem CB : Σ r : A -> B, isomorphism r.
exists r; apply isomorphism_r.
Qed.
Theorem explicit_CB : Σ r : A -> B, isomorphism r × (forall a, (r a = f a) + (g (r a) = a)).
exists r; split; [apply isomorphism_r|].
intros; unfold r; destruct (EM (C a)).
+ right; apply g_g_inv_eq.
+ left; reflexivity.
Qed.
End CB.
Section CB.
Variable EM : forall A : Type, A + ¬ A.
Variable A B : Type.
Variable f : A -> B.
Variable g : B -> A.
Variable f_inj : injective f.
Variable g_inj : injective g.
Inductive C : A -> Type :=
C_i : forall b : B, (forall a, f a = b -> C a) -> C (g b).
Definition g_inv (a : A) : C a -> B :=
fun p => match p with
C_i b _ => b
end.
Lemma g_g_inv_eq : forall a p, g (g_inv a p) = a.
intros ? []; reflexivity.
Qed.
Lemma g_inv_g_eq : forall b p, g_inv (g b) p = b.
intros; apply g_inj, g_g_inv_eq.
Qed.
Definition r : A -> B :=
fun a => match EM (C a) with
inl c => g_inv _ c
| inr _ => f a
end.
Definition f_inv (b : B) : ¬ C (g b) -> A :=
fun nc =>
match EM (Σ a, f a = b) with
inl p => π₁ p
| inr p => match nc (C_i b (curry (C := fun a _ => C a) (fun q => match p q return C (π₁ q) with end))) with end
end.
Lemma f_f_inv_eq : forall b p, f (f_inv b p) = b.
intros ? ?; unfold f_inv.
destruct (EM (Σ a, f a = b)).
- exact (π₂ s).
- exfalso; apply p; constructor; intros; exfalso; eauto.
Qed.
Lemma f_inv_f_eq : forall a p, f_inv (f a) p = a.
intros; apply f_inj, f_f_inv_eq.
Qed.
Definition r_inv : B -> A :=
fun b => match EM (C (g b)) with
inl c => g b
| inr c => f_inv _ c
end.
Lemma r_rinv : section_retraction r r_inv.
intros a; unfold r.
destruct (EM (C a)) as [c|nc]; unfold r_inv.
+ destruct (EM (C (g (g_inv a c)))).
- apply g_g_inv_eq.
- exfalso; rewrite g_g_inv_eq in *; auto.
+ destruct (EM (C (g (f a)))).
- exfalso; apply nc. inversion c; subst.
apply X, g_inj; auto.
- apply f_inv_f_eq.
Qed.
Lemma rinv_r : section_retraction r_inv r.
intros a; unfold r_inv, r.
case_eq (EM (C (g a))); intros ? ?.
+ rewrite H; apply g_inv_g_eq.
+ destruct (EM (C (f_inv a f0))).
- exfalso; apply f0; constructor; intros; subst.
rewrite f_inv_f_eq in c; assumption.
- apply f_f_inv_eq.
Qed.
Lemma inverse_r_r_inv : inverse r r_inv.
split; [apply r_rinv | apply rinv_r].
Qed.
Lemma isomorphism_r : isomorphism r.
exists r_inv; apply inverse_r_r_inv.
Qed.
Theorem CB : Σ r : A -> B, isomorphism r.
exists r; apply isomorphism_r.
Qed.
Theorem explicit_CB : Σ r : A -> B, isomorphism r × (forall a, (r a = f a) + (g (r a) = a)).
exists r; split; [apply isomorphism_r|].
intros; unfold r; destruct (EM (C a)).
+ right; apply g_g_inv_eq.
+ left; reflexivity.
Qed.
End CB.