(** * Computational Back-and-Forth Arguments ***) 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. (** ** Preliminary Definitions ***) (* 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. (** ** Abstract Back-and-Forth Argument ***) 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. (** ** Cantor's Isomorphism Theorem ***) (* 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 (c, d) el f -> a b a b b nel ran f -> matches f a b -> (c, d) el f -> c d d ~ a ~ a max ~ c ~ c 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 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 b 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 *) (** ** Myhills's Isomorphism Theorem ***) (* 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.