Library withlpo
Require Import prelude.
Section CB.
Variable lpo : forall p, (Σ n : nat, p n = true) + (forall n, p n = false).
Variable A B : Type.
Variable f : A -> B.
Variable g : B -> A.
Variable f_inj : injective f.
Variable g_inj : injective g.
Variable dec_range_f : forall b, decidable (range f b).
Variable dec_range_g : forall a, decidable (range g a).
Inductive C : A -> Type :=
C_i : forall b : B, (forall a, f a = b -> C a) -> C (g b).
Inductive FC (PC : A -> Type) : A -> Type :=
FC_i : forall b : B, (forall a, f a = b -> PC a) -> FC PC (g b).
Notation "'ø'" := (fun _ => False).
Lemma C_FCω : forall a, C a -> Σ n : nat , iter n FC ø a.
intros.
induction X.
destruct (dec_range_f b).
- destruct r.
specialize (X x e).
destruct X as [n X].
exists (S n).
simpl.
constructor.
intros.
replace a with x by (apply f_inj; congruence); assumption.
- exists 1.
constructor.
intros ? ?; apply f0. exists a; assumption.
Qed.
Lemma FCω_C : forall a, (Σ n : nat, iter n FC ø a) -> C a.
intros ? [n p]; revert a p.
induction n.
+ intros ? [].
+ simpl.
intros ? p.
inversion p; subst.
constructor. intros ? H; apply IHn, X, H.
Qed.
Lemma dec_FC : forall PC, (forall a, PC a + ¬ PC a) -> forall a, FC PC a + ¬ FC PC a.
intros PC decPC a.
destruct (dec_range_g a).
+ destruct r; subst.
destruct (dec_range_f x).
- destruct r as [a ?]; subst.
destruct (decPC a).
* left; constructor; intros.
apply f_inj in H; subst; assumption.
* right.
intro; apply f0.
inversion X; subst.
apply X0.
apply g_inj; auto.
- left; constructor; intros; exfalso; eauto.
apply f0.
exists a; assumption.
+ right; intros; apply f0.
destruct X.
exists b; reflexivity.
Qed.
Lemma dec_FC_n : forall n a, iter n FC ø a + ¬ iter n FC ø a.
induction n.
- intros; right; auto.
- intros.
apply (dec_FC _ IHn).
Qed.
Lemma dec_C : forall a, C a + ¬ C a.
intros a; destruct (lpo (fun n => if dec_FC_n n a then true else false)) as [[? ?] | ?].
+ destruct (dec_FC_n x a); [|inversion e].
left; apply FCω_C. exists x; assumption.
+ assert (forall n, ¬ iter n FC ø a).
{
intros n.
specialize (e n); destruct (dec_FC_n n a);[inversion e|]; assumption.
}
right; intro.
apply C_FCω in X.
destruct X.
eapply H; eassumption.
Qed.
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 dec_C a with
inl c => g_inv _ c
| inr _ => f a
end.
Definition f_inv (b : B) : ¬ C (g b) -> A :=
fun nc =>
match dec_range_f 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 (dec_range_f b).
- exact (π₂ r0).
- exfalso; apply p; constructor; intros; exfalso; eauto.
apply f0; exists a; assumption.
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 dec_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 (dec_C a) as [c|nc]; unfold r_inv.
+ destruct (dec_C (g (g_inv a c))).
- apply g_g_inv_eq.
- exfalso; rewrite g_g_inv_eq in *; auto.
+ destruct (dec_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 (dec_C (g a)); intros ? ?.
+ rewrite H; apply g_inv_g_eq.
+ destruct (dec_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 more_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 (dec_C a).
+ right; apply g_g_inv_eq.
+ left; reflexivity.
Qed.
End CB.
Section CB.
Variable lpo : forall p, (Σ n : nat, p n = true) + (forall n, p n = false).
Variable A B : Type.
Variable f : A -> B.
Variable g : B -> A.
Variable f_inj : injective f.
Variable g_inj : injective g.
Variable dec_range_f : forall b, decidable (range f b).
Variable dec_range_g : forall a, decidable (range g a).
Inductive C : A -> Type :=
C_i : forall b : B, (forall a, f a = b -> C a) -> C (g b).
Inductive FC (PC : A -> Type) : A -> Type :=
FC_i : forall b : B, (forall a, f a = b -> PC a) -> FC PC (g b).
Notation "'ø'" := (fun _ => False).
Lemma C_FCω : forall a, C a -> Σ n : nat , iter n FC ø a.
intros.
induction X.
destruct (dec_range_f b).
- destruct r.
specialize (X x e).
destruct X as [n X].
exists (S n).
simpl.
constructor.
intros.
replace a with x by (apply f_inj; congruence); assumption.
- exists 1.
constructor.
intros ? ?; apply f0. exists a; assumption.
Qed.
Lemma FCω_C : forall a, (Σ n : nat, iter n FC ø a) -> C a.
intros ? [n p]; revert a p.
induction n.
+ intros ? [].
+ simpl.
intros ? p.
inversion p; subst.
constructor. intros ? H; apply IHn, X, H.
Qed.
Lemma dec_FC : forall PC, (forall a, PC a + ¬ PC a) -> forall a, FC PC a + ¬ FC PC a.
intros PC decPC a.
destruct (dec_range_g a).
+ destruct r; subst.
destruct (dec_range_f x).
- destruct r as [a ?]; subst.
destruct (decPC a).
* left; constructor; intros.
apply f_inj in H; subst; assumption.
* right.
intro; apply f0.
inversion X; subst.
apply X0.
apply g_inj; auto.
- left; constructor; intros; exfalso; eauto.
apply f0.
exists a; assumption.
+ right; intros; apply f0.
destruct X.
exists b; reflexivity.
Qed.
Lemma dec_FC_n : forall n a, iter n FC ø a + ¬ iter n FC ø a.
induction n.
- intros; right; auto.
- intros.
apply (dec_FC _ IHn).
Qed.
Lemma dec_C : forall a, C a + ¬ C a.
intros a; destruct (lpo (fun n => if dec_FC_n n a then true else false)) as [[? ?] | ?].
+ destruct (dec_FC_n x a); [|inversion e].
left; apply FCω_C. exists x; assumption.
+ assert (forall n, ¬ iter n FC ø a).
{
intros n.
specialize (e n); destruct (dec_FC_n n a);[inversion e|]; assumption.
}
right; intro.
apply C_FCω in X.
destruct X.
eapply H; eassumption.
Qed.
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 dec_C a with
inl c => g_inv _ c
| inr _ => f a
end.
Definition f_inv (b : B) : ¬ C (g b) -> A :=
fun nc =>
match dec_range_f 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 (dec_range_f b).
- exact (π₂ r0).
- exfalso; apply p; constructor; intros; exfalso; eauto.
apply f0; exists a; assumption.
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 dec_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 (dec_C a) as [c|nc]; unfold r_inv.
+ destruct (dec_C (g (g_inv a c))).
- apply g_g_inv_eq.
- exfalso; rewrite g_g_inv_eq in *; auto.
+ destruct (dec_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 (dec_C (g a)); intros ? ?.
+ rewrite H; apply g_inv_g_eq.
+ destruct (dec_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 more_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 (dec_C a).
+ right; apply g_g_inv_eq.
+ left; reflexivity.
Qed.
End CB.