Set Implicit Arguments.
Unset Strict Implicit.
Open Scope type.
Require Import Lia List.
Notation "x 'el' L" := (In x L) (at level 70).
Notation "x 'nel' L" := (~ In x L) (at level 70).
Notation "L '<<=' L'" := (incl L L') (at level 70).
Notation pi1 := proj1_sig.
Notation pi2 := proj2_sig.
(* Retracts of nat *)
Class retract X Y :=
{
I : X -> Y;
R : Y -> X;
HIR : forall x, R (I x) = x;
}.
Definition discrete X :=
forall (x y : X), { x = y } + { x <> y }.
Existing Class discrete.
Local Instance retract_discrete X Y :
retract X Y -> discrete Y -> discrete X.
Proof.
intros r d x x'. destruct (d (I x) (I x')) as [H|H].
- left. enough (Some x = Some x') by congruence. rewrite <- (HIR x), <- (HIR x'). now rewrite H.
- right. intros Hx. apply H. now rewrite Hx.
Qed.
Local Instance countable_discrete X :
retract X nat -> discrete X.
Proof.
intros r. eapply retract_discrete; try apply r. intros n n'. decide equality.
Qed.
Lemma discrete_indec X (x : X) (L : list X) :
discrete X -> { x el L } + { x nel L }.
Proof.
intros H. induction L; cbn.
- now right.
- destruct (H a x) as [H1|H1]; auto.
destruct (IHL) as [H2|H2]; auto.
right. tauto.
Qed.
(* Finite functions implemented as lists *)
Definition table X Y := list (X * Y).
Notation dom f :=
(map fst f).
Notation ran f :=
(map snd f).
Lemma dom_el X Y (f : table X Y) a b :
(a, b) el f -> a el dom f.
Proof.
intros H. apply in_map_iff. now exists (a, b).
Qed.
Lemma ran_el X Y (f : table X Y) a b :
(a, b) el f -> b el ran f.
Proof.
intros H. apply in_map_iff. now exists (a, b).
Qed.
Local Hint Resolve dom_el ran_el : core.
Fixpoint im X Y {X_dec : discrete X} (f : table X Y) a : option Y :=
match f with
| nil => None
| (c, d)::f => if X_dec a c then Some d else im f a
end.
Lemma im_some X Y {X_dec : discrete X} (f : table X Y) a b :
im f a = Some b -> (a, b) el f.
Proof.
induction f as [|[c d] f IH]; cbn; try congruence.
destruct X_dec as [H|H]; subst.
- intros [=]; subst. now left.
- intros H'. right. now apply IH.
Qed.
Lemma im_none X Y {X_dec : discrete X} (f : table X Y) a :
im f a = None -> a nel dom f.
Proof.
induction f as [|[c d] f IH]; cbn; try congruence.
destruct X_dec as [H|H]; subst.
- congruence.
- firstorder.
Qed.
Notation flip f :=
(map (fun p => (snd p, fst p)) f).
Lemma flip_el X Y (f : table X Y) x y :
(x, y) el f <-> (y, x) el flip f.
Proof.
induction f as [|[x' y']]; cbn; try tauto. split.
- rewrite IHf. intuition. left. congruence.
- rewrite IHf. intuition. left. congruence.
Qed.
Lemma double_flip X Y (f : table X Y) :
flip (flip f) = f.
Proof.
induction f; cbn; intuition; cbn; congruence.
Qed.
Section Abstract.
(* Assumptions regarding the invertable abstract structure A *)
Variable structure : Type -> Type -> Type.
Variable srev : forall {X Y}, structure X Y -> structure Y X.
Hypothesis srev_invol : forall {X Y} {S : structure X Y}, srev (srev S) = S.
(* Assumptions regarding the abstract isomorphism property ~ *)
Variable iso : forall {X Y}, structure X Y -> X -> X -> Y -> Y -> Prop.
Hypothesis iso_eq : forall {X Y} {S : structure X Y} x x' y y', iso S x x' y y' -> (x = x' <-> y = y').
Hypothesis iso_rev : forall {X Y} {S : structure X Y} x x' y y', iso S x x' y y' -> iso (srev S) y y' x x'.
Definition tiso X Y (S : structure X Y) (f : table X Y) :=
forall x x' y y', (x, y) el f -> (x', y') el f -> iso S x x' y y'.
(* Assumptions regarding the one-step extension function mu *)
Variable find : forall {X Y}, structure X Y -> X -> table X Y -> Y.
Hypothesis find_iso : forall {X Y} {S : structure X Y} f x, x nel dom f -> tiso S f -> tiso S ((x, find S x f) :: f).
(* Definition of the refined extension function mu' *)
Definition step X Y {RX : retract X nat} (S : structure X Y) x (f : table X Y) : table X Y :=
(x, match im f x with Some b => b | None => find S x f end) :: f.
Lemma incl_tiso X Y (S : structure X Y) (f f' : table X Y) :
tiso S f -> f' <<= f -> tiso S f'.
Proof.
unfold tiso. intuition.
Qed.
Lemma step_tiso X Y {RX : retract X nat} (S : structure X Y) (f : table X Y) n :
tiso S f -> tiso S (step S n f).
Proof.
intros H. unfold step.
destruct im as [y|] eqn : Hy.
- eapply incl_tiso; try apply H. apply im_some in Hy. intuition.
- apply im_none in Hy. now apply find_iso.
Qed.
Lemma flip_tiso X Y (S : structure X Y) f :
tiso S f -> tiso (srev S) (flip f).
Proof.
intros Hf x x' y y' H1 H2. apply iso_rev.
apply Hf; try now apply flip_el.
Qed.
(* Fix countable X and Y related by a structure SXY *)
Variable X Y : Type.
Variable SXY : structure X Y.
Variable RX : retract X nat.
Variable RY : retract Y nat.
(* Construction and verification of stages L_n *)
Fixpoint L (n : nat) : table X Y :=
match n with
| 0 => nil
| S n => flip (step (srev SXY) (R n) (flip (step SXY (R n) (L n))))
end.
Lemma L_tiso n :
tiso SXY (L n).
Proof.
induction n.
- intros x x' y y' [].
- rewrite <- srev_invol at 1. unfold L; fold L.
eapply flip_tiso, step_tiso, flip_tiso, step_tiso, IHn.
Qed.
(* Construction and verification of isomorphism F(orth) *)
Lemma L_tot x :
{ y | (x, y) el L (S (I x)) }.
Proof.
eexists. right. left. rewrite HIR. reflexivity.
Qed.
Lemma L_sur y :
{ x | (x, y) el L (S (I y)) }.
Proof.
eexists; cbn; rewrite HIR. now left.
Qed.
Definition Forth x :=
pi1 (L_tot x).
Definition Back y :=
pi1 (L_sur y).
Lemma L_cum n k :
n <= k -> L n <<= L k.
Proof.
induction 1.
- intuition.
- cbn. rewrite double_flip; intuition.
Qed.
Lemma L_iso n x y n' x' y' :
(x, y) el L n -> (x', y') el L n' -> iso SXY x x' y y' /\ iso SXY x' x y' y.
Proof.
intros H1 H2. split; apply (@L_tiso (n + n')).
all: eapply L_cum; try eassumption; lia.
Qed.
Lemma forth_iso x x' :
iso SXY x x' (Forth x) (Forth x').
Proof.
unfold Forth.
destruct (L_tot x) as [y H1], (L_tot x') as [y' H2]; cbn.
eapply L_iso; eassumption.
Qed.
Lemma back_forth x :
Back (Forth x) = x.
Proof.
unfold Forth, Back.
destruct L_tot as [y H1], L_sur as [x' H2]; cbn -[L] in *.
apply (@iso_eq _ _ SXY x' x y y); trivial.
eapply L_iso; eassumption.
Qed.
Lemma forth_back y :
Forth (Back y) = y.
Proof.
unfold Forth, Back.
destruct L_sur as [x H1], L_tot as [y' H2]; cbn -[L] in *.
apply (@iso_eq _ _ SXY x x y' y); trivial.
eapply L_iso; eassumption.
Qed.
Definition inverse (F : X -> Y) (G : Y -> X) :=
(forall x, G (F x) = x) /\ (forall y, F (G y) = y).
Theorem back_and_forth :
{ F & { G | inverse F G /\ forall x x', iso SXY x x' (F x) (F x') } }.
Proof.
exists Forth, Back.
split; try apply forth_iso.
split; try apply back_forth.
apply forth_back.
Qed.
End Abstract.
(* Definition of unbounded dense linear orders *)
Class dulo X :=
{
point : X;
rel : X -> X -> Prop;
rel_irref : forall x, ~ rel x x;
rel_trans : forall x y z, rel x y -> rel y z -> rel x z;
rel_trich : forall x y, { rel x y } + { x = y } + { rel y x };
rel_up : forall x, { y | rel x y };
rel_down : forall x, { y | rel y x };
rel_dense : forall x y, rel x y -> { z | rel x z /\ rel z y };
}.
Arguments rel {_ _} _ _, {_} _ _ _.
Lemma rel_asym X (OX : dulo X) :
forall x y, rel OX x y -> ~ rel OX y x.
Proof.
intros x y H1 H2. apply (@rel_irref X OX x).
eapply rel_trans; eauto.
Qed.
(* Note that in contrast to the paper we assume an informative proof rel_trich for trichotomy,
sparing the additional assumption of a decider for the relation rel and equality eq *)
Lemma rel_dec X (OX : dulo X) :
forall x y, { rel OX x y } + { ~ rel OX x y }.
Proof.
intros x y. destruct (rel_trich x y) as [[H|H]|H].
- left. apply H.
- right. rewrite H. apply rel_irref.
- right. intros H'. eapply rel_asym; eauto.
Qed.
Lemma dulo_disc X (OX : dulo X) :
discrete X.
Proof.
intros x y. destruct (rel_trich x y) as [[H|H]|H].
- right. intros ->. now apply rel_irref in H.
- now left.
- right. intros ->. now apply rel_irref in H.
Qed.
(* This section establishes the extension function for Cantor (Definition 4 and Lemma 5) *)
Section CantorStep.
Variables A B : Type.
Context (OA : dulo A) (OB : dulo B).
Notation "a <A a'" := (rel OA a a') (at level 70).
Notation "b <B b'" := (rel OB b b') (at level 70).
Hint Resolve rel_trans : core.
Definition morph' f :=
forall a c b d, (a, b) el f -> (c, d) el f -> a <A c <-> b <B d.
Definition matches f a b :=
forall c d, (c, d) el f -> a <A c <-> b <B d.
Lemma matches_down f a b c d :
a nel dom f -> b nel ran f -> matches f a b -> (c, d) el f -> c <A a <-> d <B b.
Proof.
intros Ha Hb Hf H1. split; intros H2.
- destruct (rel_trich d b) as [[H|<-]|H]; trivial.
+ contradict Hb. apply (ran_el H1).
+ apply (Hf c) in H; trivial. contradiction (rel_asym H H2).
- destruct (rel_trich c a) as [[H|<-]|H]; trivial.
+ contradict Ha. apply (dom_el H1).
+ apply (Hf c d) in H; trivial. contradiction (rel_asym H H2).
Qed.
Definition min_im f a :
{ min | (exists a', (a', min) el f /\ a <A a') /\ forall c d, (c, d) el f -> d <B min -> ~ a <A c }
+ { forall c d, (c, d) el f -> ~ a <A c }.
Proof.
induction f as [|[u v] f IH].
- right. intros c d [].
- destruct IH as [[min[H1 H2]]|H], (rel_dec OA a u) as [Ha|Ha].
+ destruct (rel_dec OB v min) as [Hv|Hv].
* left. exists v. split; try firstorder 0.
intros c d [[=]|H'] Hd; subst; eauto.
now apply rel_irref in Hd.
* left. firstorder congruence.
+ left. exists min. firstorder congruence.
+ left. exists v. split; try firstorder 0.
intros c d [[=]|H']; subst; eauto.
intros [] % rel_irref.
+ right. firstorder congruence.
Qed.
Definition max_im f a :
{ max | (exists a', (a', max) el f /\ a' <A a) /\ forall c d, (c, d) el f -> max <B d -> ~ c <A a }
+ { forall c d, (c, d) el f -> ~ c <A a }.
Proof.
induction f as [|[u v] f IH].
- right. intros c d [].
- destruct IH as [[max[H1 H2]]|H], (rel_dec OA u a) as [Ha|Ha].
+ destruct (rel_dec OB max v) as [Hv|Hv].
* left. exists v. split; try firstorder 0.
intros c d [[=]|H'] Hd; subst; eauto.
now apply rel_irref in Hd.
* left. firstorder congruence.
+ left. exists max. firstorder congruence.
+ left. exists v. split; try firstorder 0.
intros c d [[=]|H']; subst; eauto.
intros [] % rel_irref.
+ right. firstorder congruence.
Qed.
(* Definition and verification of mu_C *)
Definition partner a f :=
match min_im f a, max_im f a with
| inleft (exist _ min H1), inleft (exist _ max H2)
=> match rel_dec OB max min with left h => pi1 (@rel_dense _ OB max min h) | _ => @point _ OB end
| inleft (exist _ min _), _ => pi1 (@rel_down _ OB min)
| _, inleft (exist _ max _) => pi1 (@rel_up _ OB max)
| _, _ => @point _ OB
end.
Lemma partner_ran f a :
a nel dom f -> morph' f -> partner a f nel ran f.
Proof.
intros Ha Hf. unfold partner; destruct min_im as [[min H1]|H1], max_im as [[max H2]|H2].
try destruct rel_dec as [H|H]. all: intros [[c d][Heq H']] % in_map_iff; cbn in *; subst.
- destruct rel_dense as [x[H3 H4]]; cbn in *.
destruct (rel_trich a c) as [[|<-]|]; intuition eauto.
- destruct H1 as [[a1 Ha1]H1], H2 as [[a2 Ha2]H2].
apply H. apply (Hf a2 a1 max); try tauto. apply rel_trans with a; tauto.
- destruct rel_down as [x Hx]; cbn in *.
destruct (rel_trich a c) as [[|<-]|]; intuition eauto.
- edestruct rel_up as [x Hx]; cbn in *.
destruct (rel_trich a c) as [[|<-]|]; intuition eauto.
- apply Ha. apply dom_el with (@point _ OB).
destruct (rel_trich a c) as [[|<-]|]; trivial; exfalso; intuition eauto.
Qed.
Lemma partner_matches f a :
a nel dom f -> morph' f -> matches f a (partner a f).
Proof.
intros Ha Hf c d Hc. unfold partner.
destruct min_im as [[min[[u Hu]H1]]|H1], max_im as [[max[[v Hv]H2]]|H2].
- assert (Hm : max <B min). { eapply Hf; intuition eauto. }
destruct rel_dec as [H|H]; try tauto. destruct rel_dense as [x[H3 H4]]; cbn. clear H. split; intros H.
+ destruct (rel_trich x d) as [[|<-]|]; trivial; exfalso; intuition eauto.
+ destruct (rel_trich a c) as [[|<-]|]; trivial; exfalso; intuition eauto.
- destruct rel_down as [x Hx]; cbn in *. split; intros H.
+ destruct (rel_trich x d) as [[|<-]|]; trivial; exfalso; intuition eauto.
+ destruct (rel_trich a c) as [[|<-]|]; trivial; exfalso; intuition eauto.
- destruct rel_up as [x Hx]; cbn in *. split; intros H.
+ destruct (rel_trich x d) as [[|<-]|]; trivial; exfalso; intuition eauto.
+ destruct (rel_trich a c) as [[|<-]|]; trivial; exfalso; intuition eauto.
- assert (a = c) as <-.
+ destruct (rel_trich a c) as [[]|]; firstorder.
+ exfalso. intuition eauto.
Qed.
Lemma step_morph' f x :
x nel dom f -> morph' f -> morph' ((x, partner x f) :: f).
Proof.
intros Hx Hf a b c d [[=]|H] [[=]|H']; subst.
- split; now intros H % rel_irref.
- apply partner_matches; trivial.
- apply matches_down with f; trivial.
+ eapply partner_ran; trivial.
+ apply partner_matches; trivial.
- now apply Hf.
Qed.
Definition morph f :=
forall a c b d, (a, b) el f -> (c, d) el f -> ((a = c) <-> (b = d)) /\ (a <A c <-> b <B d).
Lemma morph_morph' f :
morph f -> morph' f.
Proof.
intros Hf. intros x y u v H1 H2. now apply Hf.
Qed.
Lemma step_morph f x :
x nel dom f -> morph f -> morph ((x, partner x f) :: f).
Proof.
intros Hx Hf a b c d [[=]|H] [[=]|H']; subst.
- split; try tauto. split; now intros H % rel_irref.
- split.
+ split; intros Heq; subst; try now apply dom_el in H'.
apply ran_el in H'. apply partner_ran in H'; try tauto.
now apply morph_morph'.
+ apply partner_matches; trivial. now apply morph_morph'.
- split.
+ split; intros Heq; subst; try now apply dom_el in H.
apply ran_el in H. apply partner_ran in H; try tauto.
now apply morph_morph'.
+ apply matches_down with f; trivial.
* eapply partner_ran; trivial. now apply morph_morph'.
* apply partner_matches; trivial. now apply morph_morph'.
- now apply Hf.
Qed.
End CantorStep.
(* Instantiation to Cantor's isomorphism theorem *)
Notation "x < y" := (rel x y).
Theorem Cantor X Y (OX : dulo X) (OY : dulo Y) (RX : retract X nat) (RY : retract Y nat) :
{ F : X -> Y & { G | inverse F G /\ forall x x', x < x' <-> (F x) < (F x') } }.
Proof.
unshelve edestruct back_and_forth as [F[G[H1 H2]]].
- intros A B. exact (dulo A * dulo B). (* structure *)
- intros A B [OA OB]. exact (OB, OA). (* srev *)
- intros A B [OA OB] a a' b b'. exact ((a = a' <-> b = b') /\ (a < a' <-> b < b')). (* iso *)
- cbn. intros A B [OA OB] f a. exact (partner OA OB f a). (* find *)
- exact X.
- exact Y.
- exact (OX, OY).
- intros A B [OA OB]. reflexivity. (* srev_invol *)
- cbn. tauto. (* iso_eq *)
- cbn. tauto. (* iso_rev *)
- cbn. intros A B [OA OB] f x. unfold step, tiso. now apply step_morph. (* find_iso *)
- exact RX.
- exact RY.
- cbn in *. exists F, G. split; try apply H1. apply H2.
Qed.
Print Assumptions Cantor. (* Closed under the global context *)
(* Import of the Equations package to support definition by well-founded recursion *)
From Equations Require Import Equations.
Unset Equations With Funext.
(* Definition of one-one interreducible predicates *)
Definition inj X Y (f : X -> Y) :=
forall x x', f x = f x' -> x = x'.
Definition reduction X Y (p : X -> Prop) (q : Y -> Prop) f :=
forall x, p x <-> q (f x).
Class bireduction X Y :=
{
eX : discrete X;
eY : discrete Y;
p : X -> Prop;
q : Y -> Prop;
f : X -> Y;
g : Y -> X;
f_inj : inj f;
g_inj : inj g;
f_red : reduction p q f;
g_red : reduction q p g;
}.
(* This section establishes the extension function for Myhill (Definition 8 and Lemma 9),
adapted from https://github.com/synthetic-reducibility-coq/paper/blob/main/Synthetic/myhill.v *)
Section MyhillStep.
Variables (X Y : Type).
Variable p : X -> Prop.
Variable q : Y -> Prop.
Variable f : X -> Y.
Hypothesis inj_f : inj f.
Hypothesis f_red : reduction p q f.
Variable eX : discrete X.
Variable eY : discrete Y.
Lemma ran_compute (y : Y) (L : table X Y) :
y el ran L -> {x : X | (x, y) el L}.
Proof.
induction L as [ | [x y'] L IH] in y |- *.
- inversion 1.
- cbn. destruct (eY y' y) as [-> | He].
+ exists x. eauto.
+ intros H. destruct (IH y) as (x' & IHx').
firstorder. exists x'. eauto.
Qed.
Lemma discrete_prod :
discrete (X * Y).
Proof.
intros [x y] [x' y']. destruct (eX x x'), (eY y y'); subst; try now left. all: right; congruence.
Qed.
(* Definition and verification of mu_C *)
Equations gamma (x : X) (C : table X Y) : X by wf (length C) lt :=
gamma x C with discrete_indec (f x) (ran C) eY => {
| left H with ran_compute H => {
| exist _ x' H' := gamma x' (remove discrete_prod (x', f x) C)
};
| right _ := x
}.
Next Obligation.
abstract (apply remove_length_lt; eauto).
Qed.
Definition mstep x C :=
f (gamma x C).
Arguments remove {_ _} _ _.
Definition correspondence (C : table X Y) :=
forall x x' y y', (x, y) el C -> (x', y') el C -> (x = x' <-> y = y') /\ (p x <-> q y).
Lemma correspondence_remove C x y :
correspondence C -> correspondence (@remove _ discrete_prod (x, y) C).
Proof.
intros HC. split. 1: split.
- intros <-. eapply HC; try reflexivity; eapply in_remove; eauto.
- intros <-. eapply HC; try reflexivity; eapply in_remove; eauto.
- eapply HC; eapply in_remove; eauto.
Qed.
Lemma gamma_spec (C : table X Y) x :
x nel dom C -> correspondence C -> (p x <-> p (gamma x C)) /\ (gamma x C) el (x :: dom C) /\ (mstep x C) nel ran C.
Proof.
intros Hx HC.
funelim (gamma x C); try rename H into IH; unfold mstep in *.
- rewrite <- Heqcall. cbn. intuition.
- specialize H0 as (IH1 & IH2 & IH3).
{ intros ([] & E & [] % in_remove) % in_map_iff; cbn in E; subst.
apply H0. f_equal. eapply HC; eauto. }
{ eapply correspondence_remove; eauto. }
split. 2: split.
+ etransitivity. eapply f_red. rewrite <- Heqcall. rewrite <- IH1. symmetry. eapply HC; eauto.
+ rewrite <- Heqcall. specialize IH2 as [EE | ([] & E & [] % in_remove) % in_map_iff]; eauto.
* rewrite <- EE. right. eauto.
* rewrite <- E. right. eauto.
+ rewrite Heqcall in IH3, IH2, IH1.
intros ([] & E & ?) % (in_map_iff). cbn in E. subst.
eapply IH3. eapply in_map_iff.
eexists (x0, _). split. cbn. reflexivity.
eapply in_in_remove. 2: exact H.
intros [= -> E % inj_f]. apply Hx. rewrite E in IH2.
specialize IH2 as [-> | ([] & EE & [] % in_remove) % in_map_iff]; cbn in *; subst; eauto.
Qed.
Lemma step_corr C x :
x nel dom C -> correspondence C -> correspondence ((x, mstep x C) :: C).
Proof.
intros Hx HC. split. 1: split.
- intros <-. destruct H as [[= <- <-] | ], H0 as [[= <-] | ]; eauto. 3: eapply HC; eauto.
+ exfalso. apply Hx. eauto.
+ exfalso. apply Hx. eauto.
- intros <-. destruct H as [[= <- <-] | ], H0 as [[= <-] | ]; eauto. 3: eapply HC; eauto.
+ exfalso. eapply gamma_spec; eauto.
+ subst. exfalso. eapply gamma_spec; eauto.
- destruct H as [[= <- <-] | ].
+ etransitivity. eapply gamma_spec; eauto. eapply f_red.
+ eapply HC; eauto.
Qed.
End MyhillStep.
(* Instantiation to Myhill's isomorphism theorem *)
Theorem Myhill X Y (SXY : bireduction X Y) (RX : retract X nat) (RY : retract Y nat) :
{ F : X -> Y & { G | inverse F G /\ reduction p q F } }.
Proof.
unshelve edestruct back_and_forth as [F[G[H1 H2]]].
- intros A B. exact (bireduction A B). (* structure *)
- intros A B S. cbn in *. apply (@Build_bireduction B A eY eX q p g f); apply S. (* srev *)
- intros A B S a a' b b'. cbn in S. exact ((a = a' <-> b = b') /\ (p a <-> q b)). (* iso *)
- cbn. intros A B S C a. exact (mstep f eX eY C a). (* find *)
- exact X.
- exact Y.
- exact SXY.
- cbn. intros A B []. reflexivity. (* srev_invol *)
- cbn. tauto. (* iso_eq *)
- cbn. tauto. (* iso_rev *)
- cbn. intros A B S C a. unfold step, tiso. apply step_corr; apply S. (* find_iso *)
- exact RX.
- exact RY.
- cbn in *. exists F, G. split; try apply H1. intros x. now apply H2.
Qed.
Print Assumptions Myhill. (* Closed under the global context *)
Theorem Cantor_Bernstein X Y (RX : retract X nat) (RY : retract Y nat) (f : X -> Y) (g : Y -> X) :
inj f -> inj g -> { F : X -> Y & { G | inverse F G } }.
Proof.
intros Hf Hg.
assert (SXY : bireduction X Y).
- unshelve esplit.
+ exact (fun _ => False).
+ exact (fun _ => False).
+ exact f.
+ exact g.
+ exact _.
+ exact _.
+ exact Hf.
+ exact Hg.
+ intros x. tauto.
+ intros x. tauto.
- destruct (Myhill SXY) as [F[G HFG]]; trivial.
exists F, G. apply HFG.
Qed.