Sierpinski.Hartogs
Section Hartogs.
Variable X : Type.
Implicit Types p q : powit X 1. (* subsets of X *)
Implicit Types P Q : powit X 2. (* sets of subsets of X, possibliy well-ordered by inclusion *)
Implicit Types alpha : powit X 3. (* equivalence classes of the previous *)
Definition worder P :=
forall Q, Q <<= P -> (exists p, Q p) -> exists p, Q p /\ forall q, Q q -> p <<= q.
Definition incl' P :=
fun ps qs : sig P => pi1 ps <<= pi1 qs.
Lemma worder_WO P :
worder P -> @WO (sig P) (@incl' P).
Proof.
intros H. split.
- firstorder.
- firstorder.
- intros ps qs H1 H2. now apply exist_pi1, incl_antisym.
- intros C [[x H1] H2]. destruct (@H (fun x => exists H : P x, C (exist _ x H))) as [p [[Hp1 Hp2] Hp3]].
+ intros y [Hy _]. exact Hy.
+ exists x, H1. exact H2.
+ exists (exist _ p Hp1). split; trivial. intros [y H3] H4. apply Hp3. exists H3. apply H4.
Qed.
Definition sincl P p q :=
P p /\ P q /\ p <<= q /\ ~ q <<= p.
Definition terminating P :=
forall p, P p -> Acc (sincl P) p.
Lemma worder_terminating P :
worder P -> terminating P.
Proof.
intros HP p Hp. edestruct XM as [H'|H']; eauto.
exfalso. destruct (@HP (fun p => P p /\ ~ Acc (sincl P) p)).
- firstorder.
- firstorder.
- clear Hp H' p. apply H. constructor.
intros y Hy. edestruct XM as [H'|H']; eauto. exfalso.
apply Hy, H. firstorder.
Qed.
Lemma worder_lin' P p q :
worder P -> P p -> P q -> p <<= q \/ q <<= p.
Proof.
intros H Hp Hq.
destruct (H (fun r => r = p \/ r = q)) as (r & [->| ->] & Hr).
- firstorder congruence.
- exists p. now left.
- left. apply Hr. now right.
- right. apply Hr. now left.
Qed.
Lemma worder_lin P p q :
worder P -> P p -> P q -> p <<= q \/ (q <<= p /\ ~ p <<= q).
Proof.
intros H Hp Hq.
destruct (H (fun r => r = p \/ r = q)) as (r & [->| ->] & Hr).
- firstorder congruence.
- exists p. now left.
- left. apply Hr. now right.
- destruct (XM (p <<= q)) as [H'|H']; try tauto.
right. split; trivial. apply Hr. now left.
Qed.
Definition morph P Q (f : sig P -> sig Q) :=
forall ps qs, pi1 ps <<= pi1 qs <-> pi1 (f ps) <<= pi1 (f qs).
Definition embed P Q :=
exists f : sig P -> sig Q, morph f.
Lemma embed_relation_embeddable P Q :
embed P Q -> @relation_embeddable (sig P) (sig Q) (@incl' P) (@incl' Q).
Proof.
intros [f Hf]. exists f. apply Hf.
Qed.
Lemma embed_refl P :
embed P P.
Proof.
exists (fun x => x). intros p q. tauto.
Qed.
Lemma embed_trans P Q R :
embed P Q -> embed Q R -> embed P R.
Proof.
intros [f Hf] [g Hg]. exists (fun x => g (f x)).
intros p q. rewrite (Hf p q). apply Hg.
Qed.
Lemma embed_worder P Q :
embed P Q -> worder Q -> worder P.
Proof.
intros [f Hf] H R HR [p Hp]. pose (p' := exist P p (HR p Hp)); cbn in p'.
destruct (@H (fun q => exists Hq ps, f ps = exist Q q Hq /\ R (pi1 ps))) as [q [[H1 [r[H2 H3]]] Hq]].
- firstorder.
- exists (pi1 (f p')), (pi2 (f p')), p'. split; trivial. now rewrite exist_eta.
- exists (pi1 r). split; trivial. intros s Hs. pose (s' := exist P s (HR s Hs)).
apply (Hf r s'). rewrite H2. apply Hq. exists (pi2 (f s')), s'.
split; trivial. now rewrite exist_eta.
Qed.
Lemma embed_inj P Q f :
@morph P Q f -> injective f.
Proof.
intros Hf p q H. apply exist_pi1. apply incl_antisym; apply Hf; now rewrite H.
Qed.
Lemma incl_embed P Q :
P <<= Q -> embed P Q.
Proof.
intros H. unshelve eexists.
- intros [p Hp]. exists p. now apply H.
- intros [p Hp] [q Hq]. cbn. tauto.
Qed.
Definition iso P Q :=
embed P Q /\ embed Q P.
Definition iso' P Q :=
exists f : sig P -> sig Q, morph f /\ exists g, inverse f g.
Lemma iso'_relation_isomorphic P Q :
iso' P Q -> @relation_isomorphic (sig P) (sig Q) (@incl' P) (@incl' Q).
Proof.
intros (f & Hf & g & Hg). exists f. split; try apply Hf. exists g. apply Hg.
Qed.
Lemma inverse_morph P Q (f : sig P -> sig Q) g :
morph f -> inverse f g -> morph g.
Proof.
intros H [H1 H2] q q'. rewrite <- (H2 q), <- (H2 q') at 1. symmetry. apply H.
Qed.
Lemma iso'_iso P Q :
iso' P Q -> iso P Q.
Proof.
intros (f & Hf & g & Hg). split.
- exists f. apply Hf.
- exists g. now apply (inverse_morph Hf).
Qed.
Lemma iso'_sym P Q :
iso' P Q -> iso' Q P.
Proof.
intros (f & Hf & g & Hg). exists g. split.
- now apply (inverse_morph Hf).
- exists f. split; apply Hg.
Qed.
Lemma iso_embed P Q :
iso P Q -> embed P Q.
Proof.
intros H. apply H.
Qed.
Lemma iso_refl P :
iso P P.
Proof.
split; apply embed_refl.
Qed.
Lemma iso_sym P Q :
iso P Q -> iso Q P.
Proof.
intros H. split; apply H.
Qed.
Lemma iso_trans P Q R :
iso P Q -> iso Q R -> iso P R.
Proof.
intros [H1 H2] [H3 H4]. split; eauto using embed_trans.
Qed.
Instance iso_equiv :
Equivalence iso.
Proof.
split.
- intros P. apply iso_refl.
- intros P Q. apply iso_sym.
- intros P Q R. apply iso_trans.
Qed.
Instance worder_proper :
Proper (iso ==> iff) worder.
Proof.
intros P Q [H1 H2]. split; now apply embed_worder.
Qed.
Instance embed_proper :
Proper (iso ==> iso ==> iff) embed.
Proof.
intros P P' [H1 H2] Q Q' [H3 H4]. split; eauto using embed_trans.
Qed.
Lemma iso_eq P Q :
iso P Q -> iso P = iso Q.
Proof.
intros H. apply incl_antisym; intros R <-; rewrite H; reflexivity.
Qed.
Definition morph_rel P Q (R : sig P -> sig Q -> Prop) :=
forall ps qs ps' qs', R ps qs -> R ps' qs' -> pi1 ps <<= pi1 ps' <-> pi1 qs <<= pi1 qs'.
Definition embed_rel P Q :=
exists (R : sig P -> sig Q -> Prop), total_rel R /\ morph_rel R.
Lemma embed_embed_rel P Q :
embed P Q -> embed_rel P Q.
Proof.
intros [f Hf]. exists (fun ps qs => qs = f ps). split.
- intros p. exists (f p). reflexivity.
- intros p q p' q' -> ->. apply Hf.
Qed.
Definition iso_rel P Q :=
exists R : sig P -> sig Q -> Prop, total_rel R /\ surjective_rel R /\ morph_rel R.
Lemma iso'_iso_rel P Q :
iso' P Q -> iso_rel P Q.
Proof.
intros (f & Hf & g & Hgf & Hfg). exists (fun ps qs => qs = f ps). split. 2: split.
- intros p. exists (f p). reflexivity.
- intros q. exists (g q). now rewrite Hfg.
- intros p q p' q' -> ->. apply Hf.
Qed.
Section Rel.
Variable P Q : powit X 2.
Variable R : sig P -> sig Q -> Prop.
Hypothesis R_total : total_rel R.
Hypothesis R_morph : morph_rel R.
Lemma R_functional ps qs qs' :
R ps qs -> R ps qs' -> qs = qs'.
Proof.
intros H1 H2. apply exist_pi1. apply incl_antisym.
- apply (R_morph H1 H2). apply incl_refl.
- apply (R_morph H2 H1). apply incl_refl.
Qed.
Lemma R_injective ps qs ps' :
R ps qs -> R ps' qs -> ps = ps'.
Proof.
intros H1 H2. apply exist_pi1. apply incl_antisym.
- apply (R_morph H1 H2). apply incl_refl.
- apply (R_morph H2 H1). apply incl_refl.
Qed.
Definition f' (p : sig P) :=
fun x => forall q (H : Q q), R p (exist Q q H) -> q x.
Lemma f_eq' ps qs :
R ps qs -> f' ps = pi1 qs.
Proof.
intros H. apply incl_antisym.
- intros x Hx. apply (Hx (pi1 qs) (pi2 qs)). now rewrite exist_eta.
- intros x Hx r H1 H2. specialize (R_functional H H2). intros ->. apply Hx.
Qed.
Lemma f_Q ps :
Q (f' ps).
Proof.
destruct (R_total ps) as [q Hq].
rewrite (f_eq' Hq). apply pi2.
Qed.
Definition f (p : sig P) :=
exist Q (f' p) (f_Q p).
Lemma f_eq ps qs :
R ps qs -> f ps = qs.
Proof.
intros H. apply exist_pi1. cbn. now apply f_eq'.
Qed.
Lemma f_R ps :
R ps (f ps).
Proof.
destruct (R_total ps) as [q Hq].
now rewrite (f_eq Hq).
Qed.
Lemma f_morph :
morph f.
Proof.
intros p q. apply R_morph; apply f_R.
Qed.
Hypothesis R_surjective : surjective_rel R.
Definition g' (q : sig Q) :=
fun x => forall p (H : P p), R (exist P p H) q -> p x.
Lemma g_eq' ps qs :
R ps qs -> g' qs = pi1 ps.
Proof.
intros H. apply incl_antisym.
- intros x Hx. apply (Hx (pi1 ps) (pi2 ps)). now rewrite exist_eta.
- intros x Hx r H1 H2. specialize (R_injective H H2). intros ->. apply Hx.
Qed.
Lemma g_P qs :
P (g' qs).
Proof.
destruct (R_surjective qs) as [p Hp].
rewrite (g_eq' Hp). apply pi2.
Qed.
Definition g (q : sig Q) :=
exist P (g' q) (g_P q).
Lemma g_eq ps qs :
R ps qs -> g qs = ps.
Proof.
intros H. apply exist_pi1. cbn. now apply g_eq'.
Qed.
Lemma g_R qs :
R (g qs) qs.
Proof.
destruct (R_surjective qs) as [p Hp].
now rewrite (g_eq Hp).
Qed.
End Rel.
Lemma embed_rel_embed P Q :
embed_rel P Q -> embed P Q.
Proof.
intros (R & H1 & H2). exists (f H1 H2). apply f_morph.
Qed.
Lemma iso_rel_iso' P Q :
iso_rel P Q -> iso' P Q.
Proof.
intros (R & H1 & H2 & H3).
exists (f H1 H3). split; try apply f_morph. exists (g H3 H2). split.
- intros p. erewrite g_eq; trivial. apply f_R.
- intros q. erewrite f_eq; trivial. apply g_R.
Qed.
Lemma rel_to_fun X' Y (R : X' -> (Y -> Prop) -> Prop) :
(forall x, exists! c, R x c) -> { f | forall x, R x (f x) }.
Proof.
intros HR. exists (fun x => fun y => exists c, R x c /\ c y).
intros x. destruct (HR x) as [p [Hp Hu]].
enough (p = (fun y : Y => exists p0 : Y -> Prop, R x p0 /\ p0 y)) as <- by apply Hp.
apply FE. intros y. apply PE. split; intros H.
- exists p. now split.
- destruct H as [q Hq]. now rewrite (Hu q).
Qed.
Definition segment P p :=
fun q => P q /\ q <<= p /\ ~ p <<= q.
Lemma segment_segment P p q :
p <<= q -> segment (segment P q) p = segment P p.
Proof.
intros H. apply incl_antisym; firstorder.
Qed.
Lemma segment_worder P p :
worder P -> worder (segment P p).
Proof.
intros H Q HQ [q Hq].
destruct (H Q) as [r Hr].
- firstorder.
- exists q. firstorder.
- exists r. firstorder.
Qed.
Lemma segment_embed P p :
embed (segment P p) P.
Proof.
unshelve eexists.
- intros [q Hq]. exists q. apply Hq.
- intros [q Hq] [r Hr]. cbn. tauto.
Qed.
Lemma segment_nembed P p :
worder P -> P p -> ~ embed P (segment P p).
Proof.
intros HP Hp1 Hp2.
destruct (HP (fun q => P q /\ embed P (segment P q))) as (q & [H1 H2] & H3).
- firstorder.
- firstorder.
- clear p Hp1 Hp2. destruct H2 as [f Hf].
pose (p := f (exist P q H1)). apply (pi2 p).
apply H3. split; try apply (pi2 p).
unshelve eexists.
+ intros [r Hr]. pose (r' := f (exist _ r Hr)).
assert (Hr' : P (pi1 r')) by apply (pi2 r').
exists (pi1 (f (exist _ (pi1 r') Hr'))). repeat split.
* eapply (pi2 (f (exist P (pi1 r') Hr'))).
* apply Hf. cbn. apply (pi2 r').
* intros H % Hf. cbn in H. now apply (pi2 r').
+ intros [r Hr] [s Hs]; cbn.
rewrite (Hf (exist _ r Hr) (exist _ s Hs)).
destruct (f (exist _ r Hr)) as [r'[Hr1 Hr2]], (f (exist _ s Hs)) as [s'[Hs1 Hs2]].
cbn. rewrite <- (Hf (exist _ r' Hr1) (exist _ s' Hs1)). tauto.
Qed.
Lemma segment_incl P p q :
worder P -> P p -> P q -> p <<= q <-> segment P p <<= segment P q.
Proof.
intros HP Hp Hq. split.
- intros Hs. firstorder.
- intros Hs. destruct (worder_lin HP Hp Hq) as [H|H]; firstorder.
Qed.
Lemma segment_incl_embed P p q :
worder P -> P p -> P q -> p <<= q <-> embed (segment P p) (segment P q).
Proof.
intros HP Hp Hq. split.
- intros H. now apply incl_embed, segment_incl.
- intros H. destruct (worder_lin HP Hp Hq) as [H'|[H1 H2]]; trivial.
exfalso. rewrite <- (segment_segment _ H1) in H.
refine (segment_nembed _ _ H).
+ now apply segment_worder.
+ split; tauto.
Qed.
Definition ordinal alpha :=
(exists P, alpha P /\ worder P /\ forall Q, alpha Q <-> iso P Q).
Lemma ordinal_eq alpha P :
ordinal alpha -> alpha P -> alpha = iso P.
Proof.
intros (Q & HQ) H. apply incl_antisym.
- intros R HR. apply HQ in HR. rewrite <- HR. symmetry. now apply HQ.
- intros R HR. apply HQ. rewrite <- HR. now apply HQ.
Qed.
Lemma ordinal_iso alpha P Q :
ordinal alpha -> alpha P -> alpha Q -> iso P Q.
Proof.
intros (R & _ & _ & HR) H1 H2. eapply iso_trans.
- apply iso_sym, (HR P), H1.
- apply (HR Q), H2.
Qed.
Lemma ordinal_iso' alpha P Q :
ordinal alpha -> alpha P -> iso P Q -> alpha Q.
Proof.
intros (R & _ & _ & HR) H1 H2. apply HR.
unshelve eapply (iso_trans _ H2).
apply (HR P), H1.
Qed.
Lemma ordinal_worder alpha P :
ordinal alpha -> alpha P -> worder P.
Proof.
intros (Q & H1 & H2 & H3) HP.
assert (iso P Q) as ->; trivial.
symmetry. now apply H3.
Qed.
Lemma worder_ordinal P :
worder P -> ordinal (iso P).
Proof.
exists P. intuition eauto using iso_refl.
Qed.
Definition le alpha beta :=
exists P Q, alpha P /\ beta Q /\ embed P Q.
Notation "alpha <= beta" := (le alpha beta) (at level 70).
Lemma le_refl alpha :
ordinal alpha -> alpha <= alpha.
Proof.
intros (P & H1 & H2 & H3). exists P, P.
repeat split; trivial.
apply embed_refl.
Qed.
Lemma le_trans alpha beta gamma :
ordinal beta -> alpha <= beta -> beta <= gamma -> alpha <= gamma.
Proof.
intros HB (P & Q & HP) (Q' & R & HQ).
exists P, R. split; try apply HP. split; try apply HQ.
eapply embed_trans; try apply HP.
eapply embed_trans; try apply HQ.
apply iso_embed. apply ordinal_iso with beta; tauto.
Qed.
Lemma le_antisym' alpha beta :
ordinal alpha -> ordinal beta -> alpha <= beta -> beta <= alpha -> alpha <<= beta.
Proof.
intros HA HB (P & Q & HP) (Q' & P' & HP') R HR.
apply ordinal_iso' with Q; try tauto. intuition. split.
- now rewrite (ordinal_iso HB H3 H1), (ordinal_iso HA HR H0).
- now rewrite (ordinal_iso HA HR H).
Qed.
Lemma le_antisym alpha beta :
ordinal alpha -> ordinal beta -> alpha <= beta -> beta <= alpha -> alpha = beta.
Proof.
intros H1 H2 H3 H4. apply incl_antisym; now apply le_antisym'.
Qed.
Lemma le_embed alpha beta P Q :
alpha <= beta -> ordinal alpha -> ordinal beta -> alpha P -> beta Q -> embed P Q.
Proof.
intros (P' & Q' & HP' & HQ' & H) HA HB HP HQ.
now rewrite (ordinal_iso HA HP HP'), (ordinal_iso HB HQ HQ').
Qed.
Lemma segment_incl_le P p q :
worder P -> P p -> P q -> p <<= q <-> iso (segment P p) <= iso (segment P q).
Proof.
intros HP Hp Hq. rewrite (segment_incl_embed HP Hp Hq). split.
- intros H. exists (segment P p), (segment P q).
now repeat split; try apply iso_refl.
- now intros (P' & Q' & -> & -> & H).
Qed.
Lemma embed_segment P Q (f : sig P -> sig Q) (p : sig P) :
morph f -> embed (segment P (pi1 p)) (segment Q (pi1 (f p))).
Proof.
intros Hf. unshelve eexists.
- intros (p' & Hp' & H1 & H2). exists (pi1 (f (exist P p' Hp'))).
split; try apply pi2. split.
+ now rewrite <- (Hf (exist P p' Hp') p).
+ now rewrite <- (Hf p (exist P p' Hp')).
- intros [p' [Hp' [H1 H2]]] [q' [Hq' [H3 H4]]]. cbn.
apply (Hf (exist P p' Hp') (exist P q' Hq')).
Qed.
Lemma iso'_segment P Q (f : sig P -> sig Q) g ps :
morph f -> inverse f g -> iso' (segment P (pi1 ps)) (segment Q (pi1 (f ps))).
Proof.
intros Hf [Hfg1 Hfg2]. assert (Hg : morph g) by now apply (inverse_morph Hf).
unshelve eexists. 2: split. 3: unshelve eexists. 4: split.
- intros (p' & Hp' & H1 & H2). exists (pi1 (f (exist P p' Hp'))).
split; try apply pi2. split.
+ now rewrite <- (Hf (exist P p' Hp') ps).
+ now rewrite <- (Hf ps (exist P p' Hp')).
- intros [p' [Hp' [H1 H2]]] [q' [Hq' [H3 H4]]]. cbn.
apply (Hf (exist P p' Hp') (exist P q' Hq')).
- intros (q & Hq & H1 & H2). exists (pi1 (g (exist Q q Hq))).
split; try apply pi2. split.
+ rewrite <- (Hfg1 ps). now rewrite <- (Hg (exist Q q Hq)).
+ rewrite <- (Hfg1 ps). now rewrite <- (Hg _ (exist Q q Hq)).
- intros (p' & Hp' & H1 & H2). apply exist_eq.
rewrite exist_eta, Hfg1. reflexivity.
- intros (q & Hq & H1 & H2). apply exist_eq.
rewrite exist_eta, Hfg2. reflexivity.
Qed.
Lemma morph_incl P Q (f : sig P -> sig Q) (g : sig Q -> sig P) ps :
worder P -> morph f -> morph g -> pi1 ps <<= pi1 (g (f ps)).
Proof.
intros HP Hf Hg. rewrite (segment_incl_embed HP); try apply pi2.
apply embed_trans with (segment Q (pi1 (f ps))); now apply embed_segment.
Qed.
Section Related.
Variable P Q : powit X 2.
Hypothesis HP : worder P.
Hypothesis HQ : worder Q.
Definition related p q :=
P p /\ Q q /\ iso' (segment P p) (segment Q q).
Lemma related_morph p q p' q' :
related p q -> related p' q' -> p <<= p' <-> q <<= q'.
Proof.
intros (H1 & H2 & H3 % iso'_iso) (H4 & H5 & H6 % iso'_iso). split; intros H.
- apply (@segment_incl_embed Q q q'); trivial. rewrite <- H3, <- H6. now apply segment_incl_embed.
- apply (@segment_incl_embed P p p'); trivial. rewrite H3, H6. now apply segment_incl_embed.
Qed.
Definition related_dom p :=
exists q, related p q.
Definition related_ran q :=
exists p, related p q.
Lemma related_iso :
iso' related_dom related_ran.
Proof.
apply iso_rel_iso'.
exists (fun ps qs => related (pi1 ps) (pi1 qs)). split. 2: split.
- intros (p & q & H). unshelve eexists.
+ now exists q, p.
+ cbn. exact H.
- intros (q & p & H). unshelve eexists.
+ now exists p, q.
+ cbn. exact H.
- intros p q p' q'. apply related_morph.
Qed.
Lemma dom_empty :
~ (exists p, P p /\ ~ related_dom p) -> related_dom = P.
Proof.
intros H. apply incl_antisym.
- firstorder.
- intros p Hp. destruct (XM (related_dom p)) as [H'|H']; trivial.
exfalso. apply H. now exists p.
Qed.
Lemma ran_empty :
~ (exists q, Q q /\ ~ related_ran q) -> related_ran = Q.
Proof.
intros H. apply incl_antisym.
- firstorder.
- intros q Hq. destruct (XM (related_ran q)) as [H'|H']; trivial.
exfalso. apply H. now exists q.
Qed.
Lemma dom_down p p' :
related_dom p -> segment P p p' -> related_dom p'.
Proof.
intros (q & Hp & Hq & f & Hf & g & Hfg) Hp'. exists (pi1 (f (exist _ p' Hp'))).
split; try apply Hp'. split. { destruct f. cbn. apply s. }
specialize (@iso'_segment _ _ f g (exist _ p' Hp') Hf Hfg).
rewrite !segment_segment; cbn; trivial; try apply Hp'.
destruct f. cbn. apply s.
Qed.
Lemma ran_down q q' :
related_ran q -> segment Q q q' -> related_ran q'.
Proof.
intros (p & Hq & Hp & f & Hf & g & Hfg) Hq'. exists (pi1 (g (exist _ q' Hq'))).
split. { destruct g. cbn. apply s. } split; try apply Hq'.
apply iso'_sym. assert (Hgf : inverse g f) by (split; apply Hfg).
specialize (@iso'_segment _ _ g f (exist _ q' Hq') (inverse_morph Hf Hfg) Hgf).
rewrite !segment_segment; cbn; trivial; try apply Hq'.
destruct g. cbn. apply s.
Qed.
Lemma dom_least p :
P p -> ~ related_dom p -> (forall p', P p' /\ ~ related_dom p' -> p <<= p') -> related_dom = segment P p.
Proof.
intros H1 H2 H3. apply incl_antisym.
- intros p' Hp. split. 1: firstorder. assert (H : p' <<= p).
+ destruct (@worder_lin P p' p) as [H|H]; trivial. firstorder.
exfalso. apply H2, dom_down with p'; firstorder.
+ split; trivial. intros H'. apply H2.
enough (p = p') as -> by contradiction.
now apply incl_antisym.
- intros p' [Hp Hp']. destruct (XM (related_dom p')) as [H|H]; trivial.
exfalso. now apply Hp', H3.
Qed.
Lemma ran_least q :
Q q -> ~ related_ran q -> (forall q', Q q' /\ ~ related_ran q' -> q <<= q') -> related_ran = segment Q q.
Proof.
intros H1 H2 H3. apply incl_antisym.
- intros q' Hq. split. 1: firstorder. assert (H : q' <<= q).
+ destruct (@worder_lin Q q' q) as [H|H]; trivial. firstorder.
exfalso. apply H2, ran_down with q'; firstorder.
+ split; trivial. intros H'. apply H2.
enough (q = q') as -> by contradiction.
now apply incl_antisym.
- intros q' [Hq Hq']. destruct (XM (related_ran q')) as [H|H]; trivial.
exfalso. now apply Hq', H3.
Qed.
Lemma related_tricho :
(exists q, Q q /\ iso' P (segment Q q)) \/ (exists p, P p /\ iso' Q (segment P p)) \/ iso' P Q.
Proof.
destruct (XM (exists p, P p /\ ~ related_dom p)) as [H|H], (XM (exists q, Q q /\ ~ related_ran q)) as [H'|H'].
- destruct (@HP (fun p => P p /\ ~ related_dom p)) as (p&[H1 H2]&H3); trivial. firstorder.
destruct (@HQ (fun q => Q q /\ ~ related_ran q)) as (q&[H4 H5]&H6); trivial. firstorder.
exfalso. apply H2. exists q. split; trivial. split; trivial.
rewrite <- (dom_least H1 H2 H3), <- (ran_least H4 H5 H6).
apply related_iso.
- right. left. rewrite <- (ran_empty H').
destruct (@HP (fun p => P p /\ ~ related_dom p)) as (p&[H1 H2]&H3); trivial. firstorder.
exists p. split; trivial. rewrite <- (dom_least H1 H2 H3). apply iso'_sym, related_iso.
- left. rewrite <- (dom_empty H).
destruct (@HQ (fun q => Q q /\ ~ related_ran q)) as (q&[H1 H2]&H3); trivial. firstorder.
exists q. split; trivial. rewrite <- (ran_least H1 H2 H3). apply related_iso.
- right. right. rewrite <- (dom_empty H), <- (ran_empty H'). apply related_iso.
Qed.
Lemma iso_iso' :
iso P Q -> iso' P Q.
Proof.
intros [H1 H2]. destruct related_tricho as [[q Hq]|[[p Hp]|H]]; trivial.
- exfalso. eapply (segment_nembed HQ); try apply Hq.
apply (embed_trans H2), iso'_iso, iso'_sym, Hq.
- exfalso. eapply (segment_nembed HP); try apply Hp.
apply (embed_trans H1), iso'_iso, iso'_sym, Hp.
Qed.
End Related.
Lemma nembed_segment' P Q :
worder P -> worder Q -> ~ embed Q P -> exists q, Q q /\ iso' P (segment Q q).
Proof.
intros HP HQ HPQ. destruct (related_tricho HP HQ) as [H|[H|H]]; trivial; exfalso.
- apply HPQ. destruct H as [p[_ Hp % iso'_iso]]. eapply embed_trans; try apply Hp. apply segment_embed.
- apply iso'_iso in H. apply HPQ, H.
Qed.
Lemma nembed_segment P Q :
worder P -> worder Q -> ~ embed Q P -> exists q, Q q /\ iso P (segment Q q).
Proof.
intros HP HQ HPQ. destruct (nembed_segment' HP HQ HPQ) as (q & H1 & H2).
apply iso'_iso in H2. now exists q.
Qed.
Lemma embed_wf (A : powit X 3) :
A <<= worder -> (forall P Q, iso P Q -> A P -> A Q) -> (exists P, A P) -> exists P, A P /\ forall Q, A Q -> embed P Q.
Proof.
intros HA HA' [P HP]. destruct (XM (exists Q, A Q /\ ~ embed P Q)) as [[Q[H1 H2]]|H'].
- destruct (HA P HP (fun p => P p /\ A (segment P p))) as [q[Hq1 Hq2]].
+ firstorder.
+ destruct (nembed_segment (HA Q H1) (HA P HP) H2) as [p Hp].
exists p. split; try apply Hp. apply HA' with Q; tauto.
+ exists (segment P q). split; try apply Hq1. intros R HR.
destruct (XM (embed (segment P q) R)) as [H'|[r Hr] % nembed_segment]; trivial.
* exfalso. apply Hr, Hq2. split; try apply Hr. apply HA' with R; trivial.
rewrite segment_segment in Hr; apply Hr.
* now apply HA.
* now apply segment_worder, HA.
- exists P. split; trivial. intros Q HQ. destruct (XM (embed P Q)); firstorder.
Qed.
Lemma le_wf (A : powit X 4) :
A <<= ordinal -> (exists alpha, A alpha) -> exists alpha, A alpha /\ forall beta, A beta -> alpha <= beta.
Proof.
intros H [alpha Ha]. destruct (H alpha Ha) as (P & H1 & H2 & H3).
destruct (@embed_wf (fun P => worder P /\ A (iso P))) as [Q HQ].
- now intros Q [HQ _].
- intros Q R HPQ [HP1 HP2]. split; try now rewrite <- HPQ. now rewrite <- (iso_eq HPQ).
- exists P. split; trivial. erewrite <- ordinal_eq; eauto.
- exists (iso Q). split; try apply HQ. intros beta Hb.
destruct (H beta Hb) as [R HR].
exists Q, R. split; try apply iso_refl. split; try now apply HR.
apply HQ. split; try apply HR. erewrite <- ordinal_eq; firstorder eauto.
Qed.
Lemma embed_linear_classical' (phi : Prop) :
(forall P Q, worder P -> worder Q -> embed P Q \/ embed Q P) -> ~ phi \/ ~ ~ phi.
Proof.
intros HE. pose (e := fun x : X => False).
pose (U p := phi /\ p = e).
pose (V p := ~ phi /\ p = e).
destruct (HE U V) as [[f Hf]|[f Hf]].
- intros A HA [p Hp]. exists e. firstorder congruence.
- intros A HA [p Hp]. exists e. firstorder congruence.
- left. intros H. edestruct f as [p Hp].
+ exists e. split; trivial.
+ apply Hp, H.
- right. intros H. edestruct f as [p Hp].
+ exists e. split; trivial.
+ apply H, Hp.
Qed.
Lemma embed_dec_classical (phi : Prop) :
(forall P Q, worder P -> worder Q -> embed P Q \/ ~ embed P Q) -> phi \/ ~ phi.
Proof.
intros HE. pose (e := fun x : X => False).
pose (U p := phi /\ p = e).
pose (V p := p = e).
destruct (HE V U) as [[f Hf]|HUV].
- intros A HA [p Hp]. exists e. firstorder congruence.
- intros A HA [p Hp]. exists e. firstorder congruence.
- left. edestruct f as [p H].
+ exists e. reflexivity.
+ apply H.
- right. intros H. apply HUV. enough (U = V) as -> by apply embed_refl.
apply incl_antisym; firstorder.
Qed.
Definition HN := sig ordinal.
Notation "alpha <=' beta" := (pi1 alpha <= pi1 beta) (at level 70).
Lemma HN_refl (a : HN) :
a <=' a.
Proof.
apply le_refl, pi2.
Qed.
Lemma HN_trans (a b c : HN) :
a <=' b -> b <=' c -> a <=' c.
Proof.
apply le_trans, pi2.
Qed.
Lemma HN_antisym (a b : HN) :
a <=' b -> b <=' a -> a = b.
Proof.
intros H1 H2. apply exist_pi1.
apply le_antisym; trivial; apply pi2.
Qed.
Lemma HN_wf (A : HN -> Prop) :
(exists a, A a) -> exists a, A a /\ forall b, A b -> a <=' b.
Proof.
intros [[alpha H] H'].
destruct (@le_wf (fun alpha => exists (Ha : ordinal alpha), A (exist _ alpha Ha))) as [beta[[H1 H2] H3]].
- now intros beta [Hb _].
- now exists alpha, H.
- exists (exist _ beta H1). split; trivial. intros [gamma Hc] H4. apply H3. now exists Hc.
Qed.
Lemma HN_inject :
inject HN (powit X 3).
Proof.
apply inject_subtype.
Qed.
Section Inject.
Variable R : HN -> X -> Prop.
Hypothesis R_tot : total_rel R.
Hypothesis R_inj : injective_rel R.
Definition down (a : HN) : X -> Prop :=
fun x => forall b, R b x -> b <=' a.
Definition hn : powit X 2 :=
fun p => exists a : HN, p = down a.
Lemma hn_worder :
worder hn.
Proof.
intros P HP [p Hp].
pose (A a := P (down a)).
destruct (HP p Hp) as [a ->].
destruct (@HN_wf A) as [a0 Ha].
- exists a. apply Hp.
- exists (down a0). split; try apply Ha.
intros q Hq. destruct (HP q Hq) as [b ->]. intros x Hx c Hc.
eapply le_trans; try apply Ha; try apply proj2_sig; intuition.
Qed.
Definition hno := iso hn.
Lemma hno_ordinal :
ordinal hno.
Proof.
apply worder_ordinal, hn_worder.
Qed.
Definition morph' (P : powit X 2) (f : HN -> sig P) :=
forall a b, a <=' b <-> pi1 (f a) <<= pi1 (f b).
Definition full alpha :=
exists P, alpha P /\ exists f : HN -> sig P, morph' f.
Definition G :
HN -> sig hn.
Proof.
intros a. exists (down a). now exists a.
Defined.
Lemma le_down a b :
a <=' b -> down a <<= down b.
Proof.
intros H x Hx c Hc % (Hx c); cbn in *.
apply le_trans with (pi1 a); trivial. apply pi2.
Qed.
Lemma down_le a b :
down a <<= down b -> a <=' b.
Proof.
intros H. destruct (R_tot a) as [x Hx].
assert (H' : down a x).
- intros c Hc. rewrite (R_inj Hx Hc). apply HN_refl.
- apply H in H'. apply H', Hx.
Qed.
Lemma G_morph' :
morph' G.
Proof.
intros a b; cbn. split.
- apply le_down.
- apply down_le.
Qed.
Lemma hno_full :
full hno.
Proof.
exists hn. split; try apply iso_refl.
exists G. apply G_morph'.
Qed.
Definition segord P (p : X -> Prop) :
worder P -> HN.
Proof.
intros H. exists (iso (segment P p)).
apply worder_ordinal, segment_worder, H.
Defined.
Lemma no_full alpha :
ordinal alpha -> ~ full alpha.
Proof.
intros Ha [P[HP[f Hf]]].
assert (HP' : worder P) by now apply ordinal_worder with alpha.
pose (pa := f (exist _ alpha Ha)).
apply (@segment_nembed P (pi1 pa)).
- now apply ordinal_worder with alpha.
- apply pi2.
- unshelve eexists.
+ intros [p Hp].
exists (pi1 (f (segord p HP'))). repeat split.
* apply pi2.
* apply Hf. cbn. exists (segment P p), P.
split; try apply iso_refl. split; trivial. apply segment_embed.
* intros H % Hf. cbn in H. apply (segment_nembed (ordinal_worder Ha HP) Hp).
apply (le_embed H); trivial; try apply iso_refl.
now apply worder_ordinal, segment_worder.
+ intros [r Hr] [s Hs]; cbn. rewrite (segment_incl_le HP' Hr Hs).
now rewrite (Hf (segord r HP') (segord s HP')).
Qed.
Lemma HN_ninject' :
False.
Proof.
apply (no_full hno_ordinal hno_full).
Qed.
End Inject.
Lemma HN_ninject_rel :
~ inject_rel HN X.
Proof.
intros (R & H1 & H2 & H3). apply (HN_ninject' H1 H3).
Qed.
Lemma HN_ninject :
~ inject HN X.
Proof.
intros H. apply HN_ninject_rel, inject_inject_rel, H.
Qed.
End Hartogs.