(** * Theory of Sets EIII-2 Well ordered sets
Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm). *)
(* $Id: sset6.v,v 1.80 2016/05/18 14:54:53 grimm Exp $ *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset5.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Worder.
(** ** EIII-2-1 Segments of a well-ordered set *)
(** Well ordering *)
Definition worder r :=
order r /\ forall x, sub x (substrate r) -> nonempty x ->
has_least (induced_order r x).
Definition worder_r (r: relation) :=
order_r r /\ forall x, {inc x, reflexive_r r} -> nonempty x ->
has_least (graph_on r x).
Definition worder_on G E := worder G /\ substrate G = E.
Lemma worder_or r: worder r -> order r.
Proof. move=> [or _]; exact or. Qed.
Hint Resolve worder_or: fprops.
Lemma wordering_pr r x:
worder_r r -> {inc x, reflexive_r r} ->
worder_on (graph_on r x) x.
Proof.
move=> [or wo] ar.
have sg: (substrate (graph_on r x) = x) by bw.
have gor: order (graph_on r x) by apply: order_from_rel.
split=>//; split=>//.
rewrite sg => s sx nes.
have rs: {inc s, reflexive_r r} by move=> a /sx/ar.
have sgs: substrate (graph_on r s) = s by bw.
move: (wo _ rs nes)=> [a []]; rewrite sgs => ais lea.
have ss:sub s (substrate (graph_on r x)) by rewrite sg.
exists a; split; first by aw; ue.
rewrite (iorder_sr gor ss) => y ys; aw.
move: (lea _ ys) => /graph_on_P1 [pa pb pc]; apply/iorder_gleP => //.
by apply/graph_on_P1;split => //; apply: sx.
Qed.
Lemma worder_prop r x: worder r -> sub x (substrate r) -> nonempty x ->
exists2 a, inc a x & (forall b, inc b x -> gle r a b).
Proof.
move => [or wor] xsr nex; move:(wor _ xsr nex) => [a []]; aw.
by move=> ax ap; ex_tac => b /ap /iorder_gle1.
Qed.
Lemma worder_prop_rev r: order r ->
(forall x, sub x (substrate r) -> nonempty x ->
exists2 a, inc a x & (forall b, inc b x -> gle r a b)) ->
worder r.
Proof.
move => h1 h2; split => // x xsr nex; move: (h2 x xsr nex) => [a ax ap].
by exists a; split; aw => b bx; apply/iorder_gleP => //; apply: ap.
Qed.
Lemma worder_invariance r r':
r \Is r' -> worder r -> worder r'.
Proof.
move=> [f [or or' [bf sf tf] sif]] wor.
apply:(worder_prop_rev or') =>// x xsr [y yx].
set A := Vfs (inverse_fun f) x.
have bif := (inverse_bij_fb bf).
have fi: function (inverse_fun f) by fct_tac.
have sxt: (sub x (target f)) by rewrite tf.
have sxs: (sub x (source (inverse_fun f))) by aw.
have sx :source f = (target (inverse_fun f)) by aw.
have Asx: sub A (substrate r).
rewrite - sf sx; apply: sub_trans (fun_image_Starget fi).
by apply: dirim_S.
have neA: (nonempty A).
exists (Vf (inverse_fun f) y); apply /(Vf_image_P fi sxs); ex_tac.
move: (worder_prop wor Asx neA) => [z zA zle].
move: (zA) => /(Vf_image_P fi sxs) [u ux Wu].
ex_tac; move =>// v vx.
have utx: inc u (target f) by apply: sxt.
have uW :=inverse_V bf utx.
have vt: inc v (target f) by apply: sxt.
set v':= Vf (inverse_fun f) v.
have vA: inc v' A by apply /(Vf_image_P fi sxs); ex_tac.
rewrite - (inverse_V bf vt) - uW - sif.
- by rewrite -Wu; move:(zle _ vA).
- rewrite sx; fprops.
- rewrite sx; fprops.
Qed.
(** The empty set is well-ordered *)
Lemma set0_or: order emptyset.
Proof. by rewrite - setI_0; apply: setIrel_or => t /in_set0. Qed.
Lemma set0_wor: worder_on emptyset emptyset.
Proof.
have aux: substrate emptyset = emptyset.
by rewrite /substrate domain_set0 range_set0 setU2_id.
split; [ split; [apply: set0_or | rewrite aux ] | exact: aux].
move=> x xs [y yx]; case: (in_set0 (xs _ yx)).
Qed.
Lemma empty_substrate_zero x: substrate x = emptyset -> x = emptyset.
Proof. by move /setU2_eq0P => [/domain_set0_P ]. Qed.
(** Singletons are well-ordered, and isomorphic *)
Lemma set1_wor x: worder_on (singleton (J x x)) (singleton x).
Proof.
set G := (singleton (J x x)).
have Ei: diagonal (singleton x) = G.
apply: set1_pr; first by apply/diagonal_pi_P;fprops.
by move => z /diagonal_i_P [pa /set1_P]; rewrite - {4} pa => -> <-.
have [pa pb] := diagonal_osr (singleton x).
have oE: (order G) by rewrite -Ei.
have sE: (substrate G = singleton x) by rewrite - Ei pb.
split =>//; apply: (worder_prop_rev oE) => y yE [z zy]; ex_tac => t ty.
rewrite sE in yE.
by rewrite (set1_eq (yE _ zy)) (set1_eq (yE _ ty)); apply/set1_P.
Qed.
Lemma set1_order_is x y:
(singleton (J x x)) \Is (singleton (J y y)).
Proof.
have [[o1 _] s1] := (set1_wor x).
have [[o2 _] s2] := (set1_wor y).
have ta: lf_axiom (fun _ => y) (singleton x) (singleton y).
by move=> t;fprops.
exists (Lf (fun _ => y) (singleton x) (singleton y)).
split => //.
rewrite s1 s2; split; aw => //.
apply lf_bijective => //.
by move=> u v /set1_P -> /set1_P ->.
move=> t /set1_P ->; exists x;fprops.
hnf; rewrite lf_source => a b pa pb; aw.
split; move => _; first by apply/set1_P.
move /set1_P: pa => ->; move /set1_P: pb => ->; by apply/set1_P.
Qed.
Lemma set1_order_is0 r x:
order r -> substrate r = singleton x -> r = singleton (J x x).
Proof.
move=> or sxsu.
apply: set1_pr; first by order_tac;rewrite sxsu; fprops.
move=> v vx; move: (pr1_sr vx) (pr2_sr vx); rewrite sxsu.
move => /set1_P {2} <- /set1_P <-.
by rewrite ((order_sgraph or) _ vx).
Qed.
Lemma set1_order_is1 r:
order r -> singletonp (substrate r) ->
exists x, r = singleton (J x x).
Proof. by move=> or [x xa]; exists x; apply:set1_order_is0. Qed.
Lemma set1_order_is2 r r':
order r -> order r' ->
singletonp (substrate r) -> singletonp (substrate r') ->
r \Is r'.
Proof.
move=> ox oy ssx ssy.
move: (set1_order_is1 ox ssx)=> [u ->].
move: (set1_order_is1 oy ssy)=> [v ->].
apply: set1_order_is.
Qed.
Lemma worder_set1 r e: order_on r (singleton e) -> worder r.
Proof.
move=> [or sr].
rewrite(set1_order_is0 or sr); exact: (proj1(set1_wor e)).
Qed.
(** We sometimes need an ordered set with two elements; It is well-ordered *)
Definition canonical_doubleton_order :=
(tripleton (J C0 C0) (J C1 C1) (J C0 C1)).
Lemma cdo_gleP x y:
gle canonical_doubleton_order x y <->
[\/ (x = C0 /\ y = C0), (x = C1 /\ y = C1) | (x = C0 /\ y = C1)].
Proof.
split; first by case/set3_P; move => h;rewrite(pr1_def h)(pr2_def h); in_TP4.
case; move=> [-> ->]; apply /set3_P; in_TP4.
Qed.
Lemma cdo_glt1: glt canonical_doubleton_order C0 C1.
Proof. split; [ apply /cdo_gleP; in_TP4 | fprops]. Qed.
Lemma cdo_wor: worder_on canonical_doubleton_order C2.
Proof.
have cg: sgraph canonical_doubleton_order.
by move => t /set3_P; case => ->; fprops.
have subs: substrate canonical_doubleton_order = C2.
set_extens x.
case/(substrate_P cg) => [] [y] /cdo_gleP.
case;case => ->; fprops.
case;case => _ ->; fprops.
case /C2_P => ->; apply: (@arg1_sr _ _ C1); apply /cdo_gleP; in_TP4.
have oc: (order canonical_doubleton_order).
split => //.
move => y;rewrite subs; case /C2_P => ->; apply /cdo_gleP; in_TP4.
move=> x y z /cdo_gleP pa /cdo_gleP pb; apply /cdo_gleP.
have aux: z = C0 \/ z = C1 by case: pb;move => [_ ->]; [left |right |right].
case: (equal_or_not y C0); first by move => ->; case :aux => ->; in_TP4.
case: pa; move => [-> pa] //.
move: pa; case: pb; move => [-> ->]; in_TP4.
move=> x y /cdo_gleP pa /cdo_gleP.
by case: pa; move=> [-> ->] //; case; try move => [ aa bb].
split; [ apply:(worder_prop_rev oc); rewrite subs => x xt nex | exact].
case: (inc_or_not C0 x)=> hyp.
ex_tac => y yx; apply /cdo_gleP; case /C2_P: (xt _ yx) => ->; in_TP4.
move: nex=> [y yx]; ex_tac.
have p: forall t, inc t x -> t = C1.
by move=> t tx; case/C2_P: (xt _ tx) => // ta;case: hyp; rewrite - ta.
by move => t tx; apply /cdo_gleP;rewrite (p _ yx)(p _ tx); constructor 2.
Qed.
(** A well ordering is total; bounded sets have a supremum *)
Lemma worder_total r: worder r -> total_order r.
Proof.
move=> wor; move: (proj1 wor) => or; split=> // x y xs ys.
move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu.
have ur: sub u (substrate r) by apply: sub_set2.
have si: substrate (induced_order r u) = u by aw.
have neu: nonempty u by ex_tac.
move: (worder_prop wor ur neu)=> [z zu zle].
move: (zle _ xu)(zle _ yu) => p1 p2.
by case /set2_P: zu => <-; [left | right].
Qed.
Lemma worderr_total r x y: worder_r r -> r x x -> r y y ->
(r x y \/ r y x).
Proof.
move => [p1 p2] rxx ryy.
move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu.
have p3: (forall a, inc a u -> r a a).
by move => a /set2_P; case => ->.
have p4: nonempty u by ex_tac.
have p5:(substrate (graph_on r u)) = u by apply: graph_on_sr.
move: (p2 _ p3 p4)=> [z []]; rewrite p5 => zu zle.
move: (zle _ xu) => /graph_on_P1 [_ _ zx].
move: (zle _ yu) => /graph_on_P1 [_ _ zy].
by case /set2_P: zu => <-; [left | right].
Qed.
Lemma worder_hassup r A: worder r -> sub A (substrate r) ->
bounded_above r A -> has_supremum r A.
Proof.
move=> H As [t tA].
rewrite /has_supremum /least_upper_bound.
set X:= (Zo _ _).
have Xs: sub X (substrate r) by apply: Zo_S.
have nX: (nonempty X) by exists t; apply: Zo_i => //; exact: (proj1 tA).
by move: ((proj2 H) _ Xs nX)=> [x leX]; exists x.
Qed.
Lemma induced_wor r A: worder r -> sub A (substrate r) ->
worder (induced_order r A).
Proof.
move=> [or wo] As; move: (iorder_osr or As) => [pa pb].
split; [exact | rewrite pb => x sx nex].
rewrite (iorder_trans _ sx).
by apply: wo=>//; apply: sub_trans As.
Qed.
Lemma worder_least r: worder r -> nonempty (substrate r) ->
has_least r.
Proof.
move=> [or wo] ne.
move: (wo _ (@sub_refl (substrate r)) ne)=> [x].
by rewrite iorder_substrate //; exists x.
Qed.
(** A set remains well-ordered after adjoining a greatest element *)
Lemma worder_adjoin_greatest r a: worder r -> ~ (inc a (substrate r)) ->
worder (order_with_greatest r a).
Proof.
move=> wor nas.
have [[on sn] rd [ _ gna]]:= (order_with_greatest_pr (proj1 wor) nas).
apply:(worder_prop_rev on) => x xs nex.
set (y := x \cap (substrate r)).
case: (emptyset_dichot y) => ye.
have xa: x = singleton a.
apply: set1_pr1 => //.
move=> z zx; move: (xs _ zx); rewrite sn; case /setU1_P => // zr.
by empty_tac1 z; apply:setI2_i.
have ax: inc a x by rewrite xa; fprops.
by ex_tac; rewrite xa => t /set1_P ->; order_tac; apply: xs.
have sys:sub y (substrate r) by apply: subsetI2r.
move: (worder_prop wor sys ye)=> [z zy lez].
have zx:= (setI2_1 zy).
exists z => // t tx.
move: (xs _ tx); rewrite sn; case /setU1_P => p.
have ty: inc t y by apply: setI2_i.
by move: (lez _ ty) => pa; apply:setU2_1.
by rewrite p; apply: gna; apply: xs.
Qed.
(** Every set can be well-ordered;
We assume here [inc (rep a) a] for any non-empty subset of [E] *)
Definition Zermelo_chain E F :=
let p := fun a => a -s1 (rep a) in
[/\ sub F (powerset E), inc E F,
(forall A, inc A F -> inc (p A) F)
& (forall A, sub A F -> nonempty A -> inc (intersection A) F)].
Definition worder_of E :=
let om := intersection (Zo (powerset (powerset E)) (Zermelo_chain E)) in
let d:= fun x => intersection (Zo om (sub x)) in
let R := fun x => d (singleton x) in
graph_on (fun x y => (sub (R y) (R x))) E.
Definition segment_r r x:= interval_cu r x.
Definition Zermelo_like r:= worder r /\
forall x, inc x (substrate r) -> rep (segment_r r x) = x.
Lemma segment_rP r x y: inc y (segment_r r x) <-> gle r x y.
Proof.
split; first by move /Zo_P => [].
move => h; apply: Zo_i => //; order_tac.
Qed.
Lemma Zermelo_ter E (r := worder_of E):
worder_on r E /\ Zermelo_like r.
Proof.
rewrite /r /worder_of; clear r.
set chain := (Zermelo_chain E).
set om := intersection (Zo (powerset (powerset E)) chain).
pose d p := intersection (Zo om (sub p)).
pose R x := d (singleton x).
set res:= graph_on (fun x y => (sub (R y) (R x))) E.
pose p a:= a -s1 (rep a).
have pe: p emptyset = emptyset by apply /set0_P => x /setC_P [/in_set0].
have sp: forall a, sub (p a) a by move=> t; apply:sub_setC.
have cp: chain (powerset E).
split; fprops; first by apply /setP_P.
move=> A /setP_P AE;apply/setP_P /(sub_trans (sp A) AE).
move=> A AP [x xA]; move: (AP _ xA) => /setP_P xE; apply/setP_P.
move=> t ti; exact: (xE _ (setI_hi ti xA)).
have co :chain om.
have aux: nonempty (Zo (powerset (powerset E)) chain).
by exists (powerset E); apply: Zo_i; aw; apply: setP_Ti.
split.
+ by apply:setI_s1; apply: Zo_i=> //; apply: setP_Ti.
+ by apply: (setI_i aux) =>y /Zo_hi [_].
+ move=> A Ai; apply:(setI_i aux) => y yi.
move/Zo_hi: (yi) => / proj43;apply;apply: (setI_hi Ai yi).
+ move=> A sAi neA; apply: (setI_i aux) => y yi.
by move/Zo_hi: (yi) => /proj44; apply => // t /sAi /setI_hi; apply.
move: (co)=> [sop Eo po io].
have cio: forall x, chain x -> sub om x.
by move=> x [ha hb hc hd]; apply: setI_s1; apply: Zo_i =>//;apply /setP_P.
pose m a:= forall x, inc x om -> sub x a \/ sub a x.
have am: om = Zo om m.
apply: extensionality; last by apply: Zo_S.
apply: (cio); split => //.
+ by apply: sub_trans sop; apply: Zo_S.
+ by apply: Zo_i=>//; move=> x xom; left;move: (sop _ xom); move/setP_P.
+ move=> A /Zo_P [Aom mA]; apply: Zo_i; first by apply: (po _ Aom).
suff aux: sub om (Zo om (fun x=> sub x (p A) \/ sub A x)).
move=> x xom; case: (mA _ xom) => hyp.
move: (aux _ xom) => /Zo_hi; case =>xpB; first by left.
rewrite (extensionality xpB hyp); right; apply: sp.
right; apply: (sub_trans (sp A) hyp).
apply: cio; split.
- by apply: (@sub_trans om); first by apply: Zo_S.
- by apply: Zo_i=>//; right; move: (sop _ Aom);move/setP_P.
- move => B /Zo_P [Bom ors]; apply: Zo_i; first by apply: (po _ Bom).
case: ors => orsi; first by left; apply: sub_trans orsi; apply: sp.
case: (mA _ (po _ Bom)) => aux; last by right.
case: (inc_or_not (rep B) A)=> aux2.
rewrite (extensionality orsi _); first by left.
move=> t tB; case: (equal_or_not t (rep B)); first by move=> ->.
by move=> trB; apply: aux; apply/setC1_P; split.
right; move=> t tA;apply/setC1_P;split; [ by apply: orsi| dneg trB; ue].
- move=> B sB neB; apply: Zo_i.
apply: io =>//; apply: (sub_trans sB) ; apply: Zo_S.
case: (p_or_not_p (exists x, inc x B /\ sub x (p A))) => H.
move: H=> [x [xB xp]]; left; move=> t ti; apply:(xp _ (setI_hi ti xB)).
right; move=> t tA; apply: setI_i=>//.
move=> y yB; move: (sB _ yB) => /Zo_P [yom ]; case; last by apply.
by move => sy; case: H; exists y.
+ move=> A sAZ neA; apply: Zo_i.
apply: io =>//; apply: (sub_trans sAZ); apply: Zo_S.
move=> x xom.
case: (p_or_not_p (exists2 y, inc y A & sub y x)) => H.
move: H=> [y yA yx]; right; move => t ti;apply: (yx _ (setI_hi ti yA)).
left; move=> t tx; apply: setI_i=>//.
move=> y yA; move: (sAZ _ yA)=> /Zo_P [yom my].
case: (my _ xom);[ by apply| move=> yx; case: H;ex_tac; apply: Zo_S].
have st: forall a b, inc a om -> inc b om -> sub a b \/ sub b a.
move=> a b; rewrite {2} am; move => aom /Zo_P [bom ba]; apply: (ba _ aom).
have dpo: forall X, sub X E -> inc (d X) om.
by move=> X XE; rewrite /d; apply: io;[ apply:Zo_S | exists E;apply: Zo_i].
have pdp: forall X, sub X E -> sub X (d X).
rewrite /d=> X XE t tX; apply: setI_i; first by exists E; apply: Zo_i.
by move => y /Zo_hi; apply.
have dpq: forall X Y, inc Y om -> sub X Y -> sub X E -> sub (d X) Y.
by rewrite /d=> X Y Yom XY XE; apply: setI_s1; apply: Zo_i.
have rdq: forall X, sub X E -> nonempty X -> inc (rep (d X)) X.
move=> X XE neX; case: (inc_or_not (rep (d X)) X)=>// ni.
have aux: (sub X (p (d X))).
move=> t tX;apply /setC1_P; split; [ by apply: (pdp _ XE)|].
move => h;case: ni; ue.
move: (dpq _ _ (po _ (dpo _ XE)) aux XE).
rewrite /p; case: (emptyset_dichot (d X)).
by move => dqe; case /nonemptyP: neX; apply/sub_set0;rewrite - pe - dqe.
by move=> ned; move: (rep_i ned) => rd dc; move: (dc _ rd) => /setC1_P [_].
have qdp: forall X Y, inc Y om -> sub X Y -> inc (rep Y) X -> Y = d X.
move => X Y Yom sXY YX.
have sXE: sub X E by apply: (sub_trans sXY); apply /setP_P; apply: sop.
apply: extensionality =>// t tr; last by apply: (dpq _ _ Yom sXY sXE).
case: (st _ _ (dpo _ sXE) (po _ Yom)) => ch.
by case /setC1_P: (ch _ ( (pdp _ sXE) _ YX)) => _.
case: (equal_or_not t (rep Y)); first by move=> ->; apply: (pdp _ sXE).
by move=> tnr; apply: ch; apply /setC1_P.
have Rp: forall x, inc x E ->
[/\ inc (R x) om, inc x (R x) & rep (R x) = x].
move => x xE.
have p1: sub (singleton x) E by apply: set1_sub.
split; [ by apply: dpo | exact:(pdp _ p1 _ (set1_1 x)) | ].
exact:(set1_eq (rdq _ p1 (set1_ne x))).
have Ri:forall x y, inc x E -> inc y E -> R x = R y -> x = y.
move=> x y xE yE; move: (Rp _ xE)(Rp _ yE).
by move=> [_ _ p1][_ _ p2] p3; rewrite -p3 in p2; rewrite -p1 -p2.
have Rrq: forall X, inc X om -> nonempty X -> R (rep X) = X.
move=> X Xom neX; symmetry; apply: qdp =>//; last by fprops.
by move=> t /set1_P ->; apply: rep_i.
have sRR: forall x y, inc x E -> inc y E -> inc x (R y) -> (sub (R x) (R y)).
move=> x y xE yE xRy.
move: (Rp _ xE)(Rp _ yE) => [Rom xRx rR] [Rom' yRy rR'].
case: (st _ _ Rom Rom') =>// hyp.
move: (sub_set2 xRy yRy) => p1; move: (sub_trans p1 hyp) => p2.
have p3: (inc (rep (R x)) (doubleton x y)) by rewrite rR; fprops.
have p4: (inc (rep (R y)) (doubleton x y)) by rewrite rR'; fprops.
by rewrite (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4).
have [or sr]:order_on res E.
split; last by apply: graph_on_sr => a _.
apply: order_from_rel1.
+ by move=> x y z /= xy yz; apply: sub_trans yz xy.
+ by move=> u v uE vE vu uv; apply: Ri=>//; apply: extensionality.
+ by move => u ue.
have wor:worder res.
apply:(worder_prop_rev or)=> x; rewrite sr => xsr nex.
move:(rdq x xsr nex) => rdx.
ex_tac=> a ax; apply/graph_on_P1; split => //; try apply: xsr => //.
move: ((pdp _ xsr) _ ax)=> adx; apply: sRR; fprops.
have ne: (nonempty (d x)) by exists a.
by rewrite (Rrq _ (dpo _ xsr) ne).
split=>//;split=>//; rewrite sr -/res => x xE.
suff: (segment_r res x) = R x by move => ->; exact:(proj33 (Rp _ xE)).
set_extens t.
move /segment_rP /(graph_on_P0 (fun x y=> sub (R y) (R x)) E x t).
move => [_ tE ]; apply; exact (proj32 (Rp _ tE)).
move => tR; move: ((setP_hi (sop _ (proj31 (Rp _ xE)))) _ tR) => tE.
by apply/segment_rP; apply/graph_on_P1; split => //; apply: sRR.
Qed.
(** Two stricly increasing functions with the same range are equal if the source is well-ordered *)
Lemma strict_increasing_extens f g r r':
strict_increasing_fun f r r'-> strict_increasing_fun g r r' -> worder r ->
range (graph f) = range (graph g) -> f = g.
Proof.
move=> sif sig wo.
have to: total_order r by apply: worder_total.
have sm: (strict_monotone_fun f r r') by left.
have smg: (strict_monotone_fun g r r') by left.
have injf:= (total_order_monotone_injective to sm).
have injg:= (total_order_monotone_injective to smg).
move:sif sig=> [or or' [ff sr sr'] si] [_ _ [fg srg sr'g] sig] rr {sm smg}.
set (A:=Zo (source f)(fun x=> Vf f x <> Vf g x)).
case: (emptyset_dichot A) => eA.
apply: function_exten=>//; try ue.
by move=> x xsf; ex_middle sg; empty_tac1 x;rewrite /A; apply: Zo_i.
have Asf: (sub A (substrate r)) by rewrite- sr /A;apply: Zo_S.
move:(worder_prop wo Asf eA)=> [x xA xl].
have xsf: inc x (source f) by rewrite sr; apply: Asf.
have xsg: inc x (source g) by rewrite srg - sr.
have: inc (Vf f x) (range (graph g)) by rewrite -rr; apply: Vf_range_g.
move/(range_fP fg) => [y ysg WW].
move:(ysg); rewrite srg - sr=> ysf.
have: inc (Vf g x) (range (graph f)) by rewrite rr; apply: Vf_range_g.
move/(range_fP ff) => [z zsf WWw].
move:(zsf); rewrite sr - srg=> zsg.
have xsr: inc x (substrate r) by apply: Asf.
have ysr: inc y (substrate r) by rewrite srg in ysg.
have zsr: inc z (substrate r) by rewrite sr in zsf.
have p1: glt r' (Vf g x) (Vf f x).
have a0: x <> y by move=> h; move: xA WW; rewrite -h; move /Zo_P => [].
rewrite WW; case: (total_order_pr1 to xsr ysr) => // h;first by apply: sig.
move: (sig _ _ h) => [le ne].
suff: inc y A by move=> /xl hh; order_tac.
by apply: Zo_i=>//;rewrite -WW => aux;case: a0; symmetry; apply: (proj2 injf).
have p2: glt r' (Vf f x) (Vf g x).
have a0: x <> z by move=> h; move: xA WWw;rewrite -h;move /Zo_P => []; fprops.
rewrite WWw; case: (total_order_pr1 to xsr zsr) => h //; first by apply: si.
move: (si _ _ h) => [le _].
suff: inc z A by move=> /xl h'; order_tac.
by apply: Zo_i=>//; rewrite -WWw; dneg xx; apply: (proj2 injg).
order_tac.
Qed.
Lemma iso_unique r r' f f':
worder r -> order_isomorphism f r r' -> order_isomorphism f' r r' ->
f = f'.
Proof.
move => wor ha hb.
have ha':= (order_isomorphism_increasing ha).
have hb':= (order_isomorphism_increasing hb).
have hd: range (graph f) = range (graph f').
move: ha => [_ _ [[_ /surjective_pr3 ->] _ ->] _].
by move: hb => [_ _ [[_ /surjective_pr3 ->] _ ->] _].
apply(strict_increasing_extens ha' hb' wor hd).
Qed.
(** A segment is a set such that if if contains [x],
it contains all elements less than [x]. Left-unbounded intervals are segments. *)
Definition segmentp r s :=
sub s (substrate r) /\ forall x y, inc x s -> gle r y x -> inc y s.
Definition segment r s := interval_uo r s.
Definition segmentc r s := interval_uc r s.
Lemma lt_in_segment r s x y:
segmentp r s -> inc x s -> glt r y x -> inc y s.
Proof. move=> [ss sp] xs [le ne]; apply: sp xs le. Qed.
Lemma inc_segment r x y:
inc y (segment r x) -> glt r y x.
Proof. by move /Zo_hi. Qed.
Lemma not_in_segment r x: ~ inc x (segment r x).
Proof. by move=> h; move: (inc_segment h) =>[_ h']. Qed.
Lemma sub_segment r x: sub (segment r x) (substrate r).
Proof. by move=> t /Zo_S. Qed.
Lemma sub_segment1 r s: segmentp r s -> sub s (substrate r).
Proof. by move=> [ss sp] t ts; apply: ss. Qed.
Lemma sub_segment2 r x y: sub (segment (induced_order r x) y) x.
Proof. by move=> t /Zo_hi [/setI2_2 /setXp_P [] ]. Qed.
Lemma segment_inc r x y: glt r y x -> inc y (segment r x).
Proof. move=> xy;apply /Zo_i =>//;order_tac. Qed.
Lemma segmentP r x y: inc y (segment r x) <-> glt r y x.
Proof. by split; [ apply: inc_segment | apply: segment_inc]. Qed.
Lemma segmentcP r x y: inc y (segmentc r x) <-> gle r y x.
Proof.
split; [ by move/Zo_P => [] | move =>h;apply: Zo_i =>//; order_tac ].
Qed.
Lemma inc_bound_segmentc r x: order r -> inc x (substrate r) ->
inc x (segmentc r x).
Proof. by move=> or xs;apply/segmentcP =>//; order_tac. Qed.
Lemma sub_segmentc r x: sub (segmentc r x) (substrate r).
Proof. by move=> t /Zo_S. Qed.
Hint Resolve inc_bound_segmentc: fprops.
Lemma segmentc_pr r x: order r -> inc x (substrate r) ->
(segment r x) +s1 x = segmentc r x.
Proof.
move=> or xsr;set_extens y.
case /setU1_P; first by move/segmentP => [pa _]; apply/segmentcP.
by move => -> ; apply inc_bound_segmentc.
move/segmentcP => h; case: (equal_or_not y x)=> h1.
by apply/setU1_P; right.
by apply/setU1_P; left; apply/segmentP; split.
Qed.
(** Examples of segments. Empty set, whole substrate, union, intersection, subsegments*)
Lemma set0_segment r: segmentp r emptyset.
Proof. by split; [ fprops | move=> x y /in_set0 ]. Qed.
Lemma substrate_segment r: order r -> segmentp r (substrate r).
Proof. move=> or; split => // x y xst xy; order_tac. Qed.
Lemma segment_segment r x: order r ->
inc x (substrate r) -> segmentp r (segment r x).
Proof.
move=> or xs; rewrite /segment/interval_uo.
split; first by apply: Zo_S.
move=> a b /Zo_P [asr ax] ba; apply: Zo_i; order_tac.
Qed.
Lemma segmentc_segment r x:
order r -> inc x (substrate r) ->
segmentp r (segmentc r x).
Proof.
move=> or xs; split; first by apply: Zo_S.
move=> a b /Zo_P [asr ax] ba; apply: Zo_i; order_tac.
Qed.
Lemma subsegment_segment r s s': order r ->
segmentp r s -> segmentp (induced_order r s) s' -> segmentp r s'.
Proof.
move=> or srs sis.
move: (sub_segment1 srs)=>ssr.
hnf; move: sis; rewrite /segmentp; aw.
move=> [s's hyp]; split; first by apply: sub_trans s's ssr.
move=> x y xs' yx; move: (s's _ xs')=> xs; move: srs=> [_ h].
apply: (hyp _ _ xs'); apply /iorder_gleP => //; apply: h xs yx.
Qed.
Lemma setI_segment r s: order r -> nonempty s ->
(alls s (segmentp r)) -> segmentp r (intersection s).
Proof.
move=> or nes als; split.
move :nes => [y ys] x xs; move: (als _ ys) => [yss _].
exact (yss _ (setI_hi xs ys)).
move=> x y xi yx; apply: (setI_i nes) => z zs; move: (als _ zs) => [_ p].
apply : p (setI_hi xi zs) yx.
Qed.
Lemma setUf_segment r j s: order r ->
(alls j (fun x => segmentp r (s x))) -> segmentp r (unionf j s).
Proof.
move=> or als; split.
move=> t tu;move: (setUf_hi tu)=> [y yj ts].
by move:(als _ yj) => [ss _]; apply: ss.
move=> x y xu xy;move: (setUf_hi xu)=> [z zj ts].
move:(als _ zj) => [_ ss]; move: (ss _ _ ts xy) =>h; union_tac.
Qed.
Lemma setU_segment r s: order r ->
(alls s (segmentp r)) -> segmentp r (union s).
Proof. by move=> or als; rewrite setU_prop; apply: setUf_segment. Qed.
(** Any segment is [ segment r x] or the whole set *)
Theorem well_ordered_segment r s: worder r -> segmentp r s ->
s = substrate r \/ (exists2 x, inc x (substrate r)& s = segment r x).
Proof.
move=> wor sr.
case: (equal_or_not s (substrate r));[by left | move=> snr; right].
set y:= (substrate r) -s s.
have ney: nonempty y by move: sr=> [sr _] ; apply: setC_ne.
have tor := (worder_total wor); have or := proj1 tor.
have sys: (sub y (substrate r)) by apply: sub_setC.
move: (worder_prop wor sys ney)=> [x xy xle].
have xis: inc x (substrate r) by apply: sys.
ex_tac;set_extens z => zs.
apply/segmentP.
have zsr: inc z (substrate r) by apply: (sub_segment1 sr).
case: (total_order_pr2 tor zsr xis) => //.
by case /setC_P: xy => [_ bad] /(proj2 sr _ _ zs).
ex_middle zis.
have zy: (inc z y) by apply/setC_P; split => // ;apply: (sub_segment zs).
move: (xle _ zy) (inc_segment zs)=> p1 p2; order_tac.
Qed.
Lemma segment_alt r x a: order r -> least r a ->
segment r x = interval_co r a x.
Proof.
move => or [ais lea]; set_extens t; move /Zo_P => [pa pb]; apply/Zo_P;fprops.
by move: pb => [_].
Qed.
Lemma segment_alt1 r s: worder r -> segmentp r s ->
s = substrate r \/ (exists x, exists a, s = interval_co r a x).
Proof.
move => wo iss.
case: (emptyset_dichot (substrate r)) => sre.
left; move: iss=> [p _].
apply: extensionality=>//;rewrite sre; fprops.
case: (well_ordered_segment wo iss); first by left.
move: (worder_least wo sre) => [a lea] [x xsr p].
right; exists x, a; rewrite - segment_alt //.
by move: wo=> [].
Qed.
Lemma segment_monotone r x y: order r -> gle r x y ->
sub (segment r x) (segment r y).
Proof.
move=> or xy t ts; move: (inc_segment ts) => h.
apply: segment_inc; order_tac.
Qed.
Lemma segment_dichot_sub r x y:
worder r -> segmentp r x -> segmentp r y ->
(sub x y \/ sub y x).
Proof.
move=> wo sx sy.
case: (well_ordered_segment wo sx).
by move=> ->; right; apply: sub_segment1.
move=> [a ar xsa];case: (well_ordered_segment wo sy).
by move=> ->; left; apply: sub_segment1.
move=>[b br ysb].
move:(worder_total wo) => [or h].
by rewrite xsa ysb;case: (h _ _ ar br); [left | right]; apply: segment_monotone.
Qed.
Lemma le_in_segment r x y z: order r -> inc x (substrate r) ->
inc y (segment r x) -> gle r z y -> inc z (segment r x).
Proof.
move=> or xsr ysr zy; apply: segment_inc=>//.
move: (inc_segment ysr)=> aux; order_tac.
Qed.
Lemma coarse_segment_monotone r x y: order r -> gle r x y ->
sub (coarse (segment r x)) (coarse (segment r y)).
Proof.
by move=> or xy;move: (segment_monotone or xy) =>sm; apply: setX_Slr.
Qed.
Lemma segment_induced_a r s x:
order r -> segmentp r s -> inc x s ->
segment (induced_order r s) x = segment r x.
Proof.
move=> or srs xs; set_extens t=> ys.
move: (inc_segment ys)=> iys; move: (iorder_gle2 iys)=> tx.
apply: segment_inc=>//; order_tac.
apply: segment_inc.
move: (inc_segment ys)=> [tx nxy]; split => //; apply /iorder_gleP=> //.
apply (proj2 srs _ _ xs tx).
Qed.
Lemma segment_induced r a b: order r -> glt r b a ->
segment (induced_order r (segment r a)) b = segment r b.
Proof.
move=> or ab.
have h: inc a (substrate r) by order_tac.
rewrite segment_induced_a //; last by apply /segmentP.
by apply: segment_segment.
Qed.
Lemma segment_induced1 r a b: order r -> glt r b a ->
segment (induced_order r (segmentc r a)) b = segment r b.
Proof.
move=> or ab.
have h: inc a (substrate r) by order_tac.
rewrite segment_induced_a =>//; last by apply/segmentcP; order_tac.
by apply: segmentc_segment.
Qed.
(** The union of all segments of [E], distinct from [E],
is [E] when it has no gratest element, [E] minus its greatest element otherwise.
Assumes the set totally ordered *)
Definition segmentss r:=
fun_image (substrate r) (segment r).
Lemma union_segments r (E := substrate r)(A := union (segmentss r)):
total_order r ->
( (forall x, ~ (greatest r x)) -> A = E)
/\ (forall x, greatest r x -> A = E -s1 x).
Proof.
move=> tor.
have Ap: forall x, inc x A <-> exists y, glt r x y.
move=> x;split.
move/setU_P => [y xy /funI_P [z zE sy]].
exists z; apply: inc_segment;ue.
move=> [y xy]; apply/setU_P;exists (segment r y).
by apply: segment_inc=>//; order_tac.
apply/funI_P; exists y => //; rewrite /E; order_tac.
have AE: sub A E by move=> t /Ap [y xy]; rewrite /E;order_tac.
split.
move=> p; apply: extensionality=>// t tE.
apply /Ap; ex_middle bad; case: (p t); split =>//.
move=> y ysr; case: (total_order_pr2 tor tE ysr)=>//.
by move=> ty; case: bad; exists y.
move=> x [xs gr]; set_extens y => ys.
apply/setC_P;split; first by apply: AE.
move=> /set1_P xy; move: ys => /Ap [z yz].
have zc: inc z (substrate r) by order_tac.
move: (gr _ zc) => aux.
rewrite xy in yz; move:tor=> [or _];order_tac.
move /setC_P: ys => [yE] /set1_P yx.
by apply/Ap; exists x; split=>//; apply: gr.
Qed.
(** The mapping that associates to each [x] the segment with endpoint [x] is a
bijection from [E] to the set of segments of [E], different from [E].
It is an order isomorphism (target ordered by inclusion), for any well-ordering.
The set of all segments is thus well-ordered *)
Definition segments r:=
(segmentss r) +s1 (substrate r).
Definition segments_iso r:=
Lf (segment r) (substrate r) (segmentss r).
Lemma inc_segmentsP r: worder r -> forall x,
(segmentp r x <-> inc x (segments r)).
Proof.
move => wor x; split=> hyp.
case: (well_ordered_segment wor hyp).
by move => ->; apply /setU1_P; right.
move=> [y ysr ->]; apply /setU1_P; left; apply/funI_P; ex_tac.
move:wor=> [or wor].
case /setU1_P: hyp.
move/funI_P => [z zr ->]; apply: segment_segment=>//.
by move=> ->; apply: substrate_segment.
Qed.
Lemma segment_insetof r x: worder r -> inc x (substrate r) ->
inc (segment r x) (segments r).
Proof.
move=> wo xsr; apply/(inc_segmentsP wo).
apply: segment_segment; fprops.
Qed.
Lemma segmentc_insetof r x: worder r -> inc x (substrate r) ->
inc (segmentc r x) (segments r).
Proof.
move=> wo xsr; apply/(inc_segmentsP wo).
apply: segmentc_segment; fprops.
Qed.
Lemma sub_segments r x: worder r ->
inc x (segments r) -> sub x (substrate r).
Proof. move=> wor /(inc_segmentsP wor) ;apply: sub_segment1. Qed.
Lemma segment_monotone1 r x y: total_order r ->
inc x (substrate r) -> inc y (substrate r) ->
sub (segment r x)(segment r y) -> gle r x y.
Proof.
move=> tor xsr ysr sxy.
case: (total_order_pr2 tor ysr xsr)=>//.
by move/segmentP=> yis; move: (sxy _ yis) => /segmentP [].
Qed.
Lemma segment_injective r : total_order r ->
{inc (substrate r) &, injective (segment r) }.
Proof.
move=> tor x y xsr ysr sxy.
have p1: (sub (segment r x)(segment r y)) by rewrite sxy.
have p2: (sub (segment r y)(segment r x)) by rewrite sxy.
have p3:= (segment_monotone1 tor xsr ysr p1).
have p4:= (segment_monotone1 tor ysr xsr p2).
move: tor=> [or _]; order_tac.
Qed.
Theorem segments_iso_is r: worder r ->
order_isomorphism (segments_iso r) r (sub_order (segmentss r)).
Proof.
move=> wor;move: (wor)=> [or worp].
have ta: lf_axiom (segment r) (substrate r) (segmentss r).
by move => t ts; apply /funI_P; ex_tac.
move: (sub_osr (segmentss r)) => [pa pb].
hnf; rewrite /segments_iso;split => //.
split; aw => //;apply: lf_bijective=> //.
+ move=> u v; apply: (segment_injective (worder_total wor)).
+ move=> y /funI_P [z za ->];ex_tac.
hnf; aw;move=> x y xsr ysr; aw; split.
move=> hyp; apply/sub_gleP;split => //; fprops.
by apply: segment_monotone.
move /sub_gleP=> [_ _ ss].
exact: (segment_monotone1 (worder_total wor) xsr ysr ss).
Qed.
Theorem segments_worder r: worder r ->
worder (sub_order (segments r)).
Proof.
move=> wor; move: (wor)=> [or _];move: (worder_total wor)=> tor.
have [oi sr] := (sub_osr (segments r)).
apply:(worder_prop_rev oi); rewrite sr => x xsr nex.
set y := x \cap (segmentss r).
case: (emptyset_dichot y) => hy.
have xv: x = singleton (substrate r).
apply: set1_pr1=>// z zx.
case /setU1_P: (xsr _ zx) => //.
by move=> aux; empty_tac1 z; apply: setI2_i.
have srx: inc (substrate r) x by rewrite xv; fprops.
by ex_tac; rewrite xv; move=> z /set1_P ->; order_tac;rewrite sr; apply:xsr.
have ysr: sub y (segmentss r) by move => t ty; apply: (setI2_2 ty).
have segp a: inc a y -> exists2 u, inc u (substrate r) & a = segment r u.
by move=> /ysr /funI_P.
pose cf a := select(fun u => a = segment r u) (substrate r).
have cfp: forall a, inc a y ->
(inc (cf a) (substrate r) /\ a = segment r (cf a)).
move=> a ay; move: (segp _ ay) => [u us uv].
have <- //: u = cf a.
apply: (select_uniq _ us uv); move => c b csr sc bsr sb.
by apply: (segment_injective (worder_total wor) csr bsr); rewrite - sb - sc.
set (z:= fun_image y cf).
have nez: nonempty z by move:hy=> [w wy];exists (cf w); apply/funI_P; ex_tac.
have zsr: sub z (substrate r).
by move => t /funI_P [u uy ->]; move: (cfp _ uy)=> [res _].
move: (worder_prop wor zsr nez) => [a asr lea].
have sax: (inc (segment r a) x).
move: asr => /funI_P [u uy ->].
move: (cfp _ uy)=> [h <-]; apply: (setI2_1 uy).
ex_tac;move=> b bx; apply/sub_gleP; split; fprops.
case /setU1_P: (xsr _ bx); [ move => h | by move=>->; apply: sub_segment ].
have biy: (inc b y) by apply: setI2_i.
have cbz: (inc (cf b) z) by apply /funI_P; ex_tac.
move: (lea _ cbz).
by move: (cfp _ biy)=> [p1 {2} ->]; apply: segment_monotone.
Qed.
(** Assume that [G] is a family such that (a) each [G(i)] is a well-ordering
on [E(i)]; (b) if [E(i)] is a subset of [E(j)], then [G(j)] agrees with [G(i)] on [E(i)], and (c) for any [i] and [j] there is [k] such that [E(k)] is a
subset of [E(i)] and [E(j)]. Instead of (c) we may assume (d) that one
[E(i)] of [E(j)] is a segment of the order.
Then the union of [G] is a well-ordering; moreover
segments of the union are segments of [G(i)]. *)
Definition worder_fam g := allf g worder.
Definition order_extends r r' := r = induced_order r' (substrate r).
Definition monotone_order_fam g :=
forall a b, inc a (domain g) -> inc b (domain g) ->
sub (substrate (Vg g a)) (substrate (Vg g b)) ->
order_extends (Vg g a) (Vg g b).
Definition common_extension_order g h:=
[/\ order h, substrate h = unionf (domain g) (fun a => substrate (Vg g a))
& (forall a, inc a (domain g) -> order_extends (Vg g a) h)].
Definition common_extension_order_axiom g :=
[/\ order_fam g,
(forall a b, inc a (domain g) -> inc b (domain g )-> exists c,
[/\ inc c (domain g), sub (substrate (Vg g a)) (substrate (Vg g c))
& sub (substrate (Vg g b)) (substrate (Vg g c))])
& monotone_order_fam g].
Definition common_worder_axiom g:=
[/\ worder_fam g,
(forall a b, inc a (domain g) -> inc b (domain g) ->
segmentp (Vg g a) (substrate (Vg g b))
\/ segmentp (Vg g b) (substrate (Vg g a)))
& monotone_order_fam g].
(** We first show that we have an ordering that extends [G(i)] *)
Lemma order_merge1 g:
common_extension_order_axiom g -> common_extension_order g (unionb g).
Proof.
set G := (unionb g); move=> [alo eVVg pVV].
have gu: sgraph G.
move=> t tu; move: (setUb_hi tu)=> [x xdg xp].
by move: (alo _ xdg); fprops=> h; apply: (order_sgraph h).
set (E:=unionf (domain g) (fun a => substrate (Vg g a))).
have ur: forall y,inc y E -> related (unionb g) y y.
rewrite /E=> y yE; move: (setUf_hi yE)=> [x xdg xp].
by move: (alo _ xdg); fprops=> h; apply: (setUb_i xdg); order_tac.
have su: substrate G = E.
set_extens x; last by move=> xE; move: (ur _ xE)=> h; substr_tac.
rewrite /E;case /(substrate_P gu) => [] [y Ju];
move: (setUf_hi Ju)=> [z zdg zp]; union_tac;
move: (alo _ zdg)=> h; substr_tac.
have cov: forall x y, inc x G -> inc y G ->
exists u, [/\ inc u (domain g), inc x (Vg g u)& inc y (Vg g u)].
move=> x y xu yu.
move: (setUf_hi xu) (setUf_hi yu)=> [a adg ap][b bdg bp].
move: (eVVg _ _ adg bdg)=> [c [cdg sac sbc]].
move:(pVV _ _ adg cdg sac)(pVV _ _ bdg cdg sbc)=> Vag Vbg.
move: ap bp; rewrite Vag Vbg /induced_order; aw.
by move /setI2_P => [p1 _] /setI2_P [p2 _]; exists c.
have oG: order G.
split => //.
by hnf; rewrite su.
rewrite /related => x y z p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
move: (alo _ cdg) => or; rewrite /G /related; union_tac; order_tac.
rewrite /related => x y p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
move: (alo _ cdg)=> or; order_tac.
split=>// a adg;set_extens x => xs.
apply/setI2_P; split; first by rewrite /G; union_tac.
move: (alo _ adg)=> [ga _ _ _].
by apply:(sub_graph_coarse_substrate ga).
move: (setUb_hi (setI2_1 xs))=> [z zdg zpr].
move: (eVVg _ _ adg zdg)=> [t [tdg sa sz]].
rewrite (pVV _ _ adg tdg sa); apply/setI2_P;split;last by apply: (setI2_2 xs).
by move: zpr; rewrite(pVV _ _ zdg tdg sz); move/setI2_P => [].
Qed.
(** There is at most one extension *)
Lemma order_merge2 g: common_extension_order_axiom g ->
uniqueness (common_extension_order g).
Proof.
move => [alo eVVg pVV] h1 h2 c1 c2.
suff: (forall h1 h2, common_extension_order g h1 ->
common_extension_order g h2 -> sub h1 h2).
by move=> aux; apply: extensionality; apply: aux.
move => r r' [or sr vr][or' sr' vr'].
move=> x xr.
have ppx:= (proj41 or _ xr).
move:(pr1_sr xr)(pr2_sr xr); rewrite sr => pxs pys.
move: (setUf_hi pxs) (setUf_hi pys)=> [u udg psu][v vdg qsv].
move:(eVVg _ _ udg vdg)=> [w [wdg wu wv]].
have: (inc x (Vg g w)).
rewrite (vr _ wdg); apply /setI2_i => //;apply/setX_P;split;fprops.
by rewrite (vr' _ wdg) ; move /setI2_P => [].
Qed.
(** Property (d) implies (c); in this case, the unique extension is the union *)
Lemma order_merge3 g:
common_worder_axiom g -> common_extension_order_axiom g.
Proof.
move=> [alwo pa pb];split => //.
by move => w xdg; move: (alwo _ xdg) => [ok _].
move => a b adg bdg;case: (pa _ _ adg bdg); rewrite /segmentp;
move => [ss _]; [ exists a | exists b]; split=> //.
Qed.
Lemma order_merge4 g:
common_worder_axiom g -> common_extension_order g (unionb g).
Proof. by move=> ga; apply: order_merge1; apply: order_merge3. Qed.
Lemma order_merge5 g: common_worder_axiom g ->
uniqueness (common_extension_order g).
Proof.
move=> ca h1 h2 a1 a2;apply: (order_merge2 (order_merge3 ca) a1 a2).
Qed.
(** This is the main result *)
Theorem worder_merge g (G := unionb g):
common_worder_axiom g ->
[/\ (common_extension_order g G),
worder G,
(forall a x, inc a (domain g) -> segmentp (Vg g a) x
-> segmentp G x),
(forall a x, inc a (domain g) -> inc x (substrate (Vg g a)) ->
segment (Vg g a) x = segment G x)
& (forall x, segmentp G x ->
x = substrate G \/ exists2 a, inc a (domain g) & segmentp (Vg g a) x)].
Proof.
move=> co.
move: (order_merge4 co)=>coe.
move: coe=> [oh sh Vag].
move: co => [pb pc pd].
have p1: (forall a, inc a (domain g) -> sub (substrate (Vg g a)) (substrate G)).
by move=> a adg; rewrite sh; move=> t ts; apply: (setUf_i adg).
have p0 a x y: inc x (substrate (Vg g a)) -> gle G y x -> inc y (substrate G)
-> inc a (domain g) -> inc y (substrate (Vg g a)).
move => xs yx ys adg.
move: (setUf_hi yx) => [u udg Jv].
case: (pc _ _ adg udg) => h; first by apply:(proj1 h); substr_tac.
exact: (proj2 h _ _ xs Jv).
have p2: (forall a, inc a (domain g) -> segmentp G (substrate(Vg g a))).
move=> a adg;split; first by apply: p1.
move=> x y xs yx;exact: (p0 a _ _ xs yx (arg1_sr yx) adg).
have p3:(forall a x, inc a (domain g) -> inc x (substrate (Vg g a))
-> segment (Vg g a) x = segment G x).
move=> a x adg xs; set_extens y => ys; move: (inc_segment ys) => [yx nyx].
apply /segmentP; split=>//; apply: setUb_i adg yx.
apply/segmentP; split => //;rewrite (Vag _ adg);apply/iorder_gleP => //.
exact: (p0 a _ _ xs yx (arg1_sr yx) adg).
have p4: (forall a x, inc a (domain g) -> segmentp (Vg g a) x ->
segmentp G x).
move=> a x adg sa; case: (well_ordered_segment (pb _ adg) sa).
by move=> ->; apply: p2.
move=> [y ysV ->]; rewrite (p3 _ _ adg ysV); apply: segment_segment=>//.
by apply: (p1 _ adg).
have p5: worder G.
apply:(worder_prop_rev oh) => x xsr [y yx].
move: (xsr _ yx)=> ysr; rewrite sh in ysr.
move: (setUf_hi ysr) => [a adg ysVa].
set (x1:= x \cap (substrate (Vg g a))).
have sx1s: (sub x1 (substrate (Vg g a))) by apply: subsetI2r.
have nx1: nonempty x1 by exists y; apply: setI2_i.
move: (worder_prop (pb _ adg) sx1s nx1)=> [z zs zle].
have zx: inc z x by apply: (setI2_1 zs).
have zVa: inc z (substrate (Vg g a)) by apply: (setI2_2 zs).
exists z => // t tx.
move: (xsr _ tx); rewrite sh => tu; move: (setUf_hi tu)=> [b bdg bV].
have aux: inc t (substrate (Vg g a)) -> gle G z t.
move=> hyp.
by move:(zle _ (setI2_i tx hyp));rewrite (Vag _ adg) => /iorder_gle1.
case: (pc _ _ adg bdg); move => [p p']; first by apply: (aux (p _ bV)).
move: (p _ zVa)=> zVb.
case: (total_order_pr2 (worder_total (pb _ bdg)) bV zVb).
move=> [tz ntz]; apply: (aux (p' _ _ zVa tz)).
rewrite Vag // => h; exact:(iorder_gle1 h).
split => //.
move=> x seg.
case: (well_ordered_segment p5 seg); [ by left | move=>[y ysr ->]; right ].
rewrite sh in ysr; move: (setUf_hi ysr)=> [a adg ap]; ex_tac.
rewrite -(p3 _ _ adg ap); apply: segment_segment => //.
exact (proj1 (pb _ adg)).
Qed.
(** ** EIII-2-2 The principle of transfinite induction *)
(** Let [O(x)] and [C(x)] be the set of all elements less than (resp. less or
equal than) [x]. These are segments, and [C(x)] is the union of [O(x)] and the
singleton [x]. In a well-ordered set every segment [S] is of the form [C(x)] or
the union of all segments of [S], distinct from [S].
Consequence: a set of segments, stable by union,
and stable by the mapping [O->C] contains all segments.*)
Section TransfinitePrinciple.
Variables r s: Set.
Hypothesis wor: worder r.
Hypothesis u_stable: forall s', sub s' s -> inc (union s') s.
Hypothesis adj_stable:
(forall x, inc x (substrate r) -> inc (segment r x) s -> inc (segmentc r x) s).
Lemma transfinite_principle1 x: segmentp r x -> inc x s.
Proof.
move=> sx.
have or: order r by case: wor.
move: (segments_worder wor) => woi.
set (cs:= (segments r) -s s).
case: (emptyset_dichot cs) => necs.
have nc: (~ inc x cs) by rewrite necs; case; case.
move: sx => /(inc_segmentsP wor) sx.
apply: (nin_setC sx nc).
have scs: sub cs (segments r) by rewrite /cs; apply: sub_setC.
move:(proj2 (sub_osr (segments r))) => sr1.
move: (scs); rewrite - {1} sr1 => src1.
move:(worder_prop woi src1 necs) => [y ycs hyp].
move/setC_P:(ycs) => [yssr nys].
have ysr:(sub y (substrate r)) by apply: sub_segments=>//.
have woi': worder (induced_order r y) by apply: induced_wor.
case: (p_or_not_p (exists a, greatest (induced_order r y) a)).
move=> [a []]; aw => [ay pa].
move: (ysr _ ay)=> asr.
have ysc: (y = segmentc r a).
set_extens t => ts; first by move: (iorder_gle1 (pa _ ts)) => /segmentcP.
move: ts => /segmentcP ta.
move: yssr => /(inc_segmentsP wor) [_ aux]; apply: (aux _ _ ay ta).
case: (p_or_not_p (inc (segment r a) cs))=> h.
move: (hyp _ h) => /sub_gleP [_ _ ysa].
case: (not_in_segment (ysa _ ay)).
have p1: (inc (segment r a) (segments r)) by apply: segment_insetof.
by case: nys; rewrite ysc; apply: adj_stable =>//; apply: (nin_setC p1 h).
move=> nge.
have aux: (forall x, ~ greatest (induced_order r y) x).
by move=> b ngeb; case: nge; exists b.
move: (union_segments (worder_total woi'))=> [unm _].
move: (unm aux); aw => us; clear aux unm.
case: nys; rewrite -us; apply: u_stable.
move => z /funI_P [u uy zv].
case: (inc_or_not z cs) => zcs.
move: (hyp _ zcs) => /sub_gleP [_ _ yz].
move: uy; aw => uy; move: (yz _ uy).
by rewrite zv=>/not_in_segment.
have siu: (segmentp (induced_order r y) z).
rewrite zv; apply: segment_segment; fprops; aw.
have zsr: (inc z (segments r)).
apply /(inc_segmentsP wor).
move: yssr => /(inc_segmentsP wor) yssr.
apply: (subsegment_segment or yssr siu).
by apply: (nin_setC zsr zcs).
Qed.
Lemma transfinite_principle2: inc (substrate r) s.
Proof.
apply: (transfinite_principle1); apply: substrate_segment; fprops.
Qed.
End TransfinitePrinciple.
(** Two proofs of the transfinite principle; either by application of the
previous lemma or direct proof (in ssete2) *)
Theorem transfinite_principle r (p:property):
worder r ->
(forall x, inc x (substrate r) ->
(forall y, inc y (substrate r) -> glt r y x -> p y) -> p x) ->
forall x, inc x (substrate r) -> p x.
Proof.
move => wor hyp x xsr.
have or: order r by case: wor.
set (s:= Zo (segments r)(fun z => forall y, inc y z -> p y)).
have alseg: forall x, inc x s -> segmentp r x.
by move=> t /Zo_P [] /(inc_segmentsP wor).
have su:forall s', sub s' s -> inc (union s') s.
move=> s' s's; apply /Zo_P; split.
apply /(inc_segmentsP wor);apply: setU_segment =>//.
by move=> t ts'; apply: alseg; apply: s's.
move=> y yu; move: (setU_hi yu)=> [v yv vs].
by move: (s's _ vs) => /Zo_hi; apply.
have seg: forall x, inc x (substrate r) -> inc (segment r x) s ->
inc (segmentc r x) s.
move=> y ysr yxs; rewrite /s; apply: Zo_i.
apply /(inc_segmentsP wor); apply: segmentc_segment =>//.
move: yxs => /Zo_P [p1 p2].
move=> z; rewrite - segmentc_pr //; case /setU1_P; first by apply: p2.
move=> ->; apply: hyp =>//; move=> t tsr ty; apply: p2; fprops.
by apply: segment_inc.
move: (transfinite_principle2 wor su seg).
by move => /Zo_hi; apply.
Qed.
(** Let [r] be a well-ordering, [x] in the substrate, [S(x)] the segment with
endpoint [x], and [g] a function, whose source contains [S(x)].
We define [gx] to be the restriction of [g] to [Sx];
and study some properties. *)
Definition restriction_to_segment r x g :=
restriction1 g (segment r x).
Lemma rts_fs r x g: function g -> sub (segment r x) (source g) ->
surjection (restriction_to_segment r x g).
Proof. by move=> p3 p4; apply: restriction1_fs. Qed.
Lemma rts_extensionality r s x f g:
segment r x = segment s x ->
function f -> sub (segment r x) (source f) ->
function g -> sub (segment s x) (source g) ->
{inc (segment r x), f =1f g} ->
restriction_to_segment r x f = restriction_to_segment s x g.
Proof.
move=> srsx ff srf fg ssg sv.
have pa: source (restriction_to_segment r x f) = segment r x by apply:corresp_s.
apply: function_exten4.
- rewrite /restriction_to_segment /restriction1; aw.
- by apply restriction1_fs.
- by apply restriction1_fs.
- rewrite pa => t ts.
rewrite (restriction1_V ff srf ts) (sv _ ts).
by rewrite srsx in ts; rewrite (restriction1_V fg ssg ts).
Qed.
(** A function [f] is defined by transfinite induction by [p] if [f(x)] is
[p(fx)], where [fx] is as above. It exists, its graph is unique.
The value [f(x)] is in a set [F] if, for all [g] whose source is a segment and
target is a subset of [F], [p(g)] is in [F]. We start with some uniqueness
properties *)
Definition transfinite_def r (p: fterm) f :=
[/\ surjection f, source f = substrate r &
forall x, inc x (substrate r) -> Vf f x = p (restriction_to_segment r x f)].
Lemma transfinite_unique1 r p f f' z:
transfinite_def r p f -> transfinite_def r p f' ->
{inc (segment r z), f =1f f'} ->
restriction_to_segment r z f = restriction_to_segment r z f'.
Proof.
move=> [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW.
have ss: sub (segment r z) (substrate r) by apply: sub_segment.
apply: rts_extensionality => //; ue.
Qed.
Lemma transfinite_unique r p : worder r ->
uniqueness (transfinite_def r p).
Proof.
move=> wo f f' tf tf'.
set (s:=Zo(segments r) (fun z => {inc z, f =1f f'})).
move: (wo)=> [or _].
have alse:forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(inc_segmentsP wo).
have su: forall s', sub s' s -> inc (union s') s.
move=> s' s's; apply /Zo_P; split.
apply/(inc_segmentsP wo); apply /(setU_segment or).
move=> x xs'; move: (s's _ xs'); apply: alse.
move=> x xu; move: (setU_hi xu)=> [y xy ys'].
by move: (s's _ ys') => /Zo_hi;apply.
have sc: forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segmentc r x) s.
move=> x xsr => /Zo_P [] /(inc_segmentsP wo) pa pb.
apply Zo_i;first by apply: segmentc_insetof.
move=> y; rewrite - (segmentc_pr or xsr); case/setU1_P; first apply: pb.
move: (transfinite_unique1 tf tf' pb) => sWx ->.
by move: tf tf'=> [_ _ pf] [_ _ pf']; rewrite (pf _ xsr)(pf' _ xsr) sWx.
move: (transfinite_principle2 wo su sc); move /Zo_P => [_ asW].
move:tf tf'=> [suf sf _][suf' sf' _ ].
apply: function_exten4 => //; [ by rewrite sf sf' | by rewrite sf].
Qed.
Lemma transfinite_aux1 r p s' s'' f' f'':
worder r -> segmentp r s' -> segmentp r s'' -> sub s' s'' ->
transfinite_def (induced_order r s') p f' ->
transfinite_def (induced_order r s'') p f'' ->
f' = restriction1 f'' s'.
Proof.
move=> wo ss' ss'' is'' tf' tf''.
set (f:=restriction1 f'' s').
have or:order r by fprops.
move: tf''=> [[ff'' _] sf'' pb].
have s''s: sub s'' (substrate r) by move: ss''=>[q _]; exact q.
have s's: sub s' (substrate r) by move: ss'=>[q _]; exact q.
have woi: worder (induced_order r s') by apply: induced_wor.
have s'sf'': sub s' (source f'') by rewrite sf''; aw.
have sf: source f = s' by rewrite /f/restriction1; aw.
have suf: surjection f by rewrite /f; apply: restriction1_fs=>//.
have ff: function f by fct_tac.
suff: transfinite_def (induced_order r s') p f.
by apply: (transfinite_unique woi tf').
split => //; aw.
move=> x xs'.
have p1: sub (segment (induced_order r s') x) s' by apply: sub_segment2.
have p2: sub (segment (induced_order r s'') x) (source f'').
by rewrite sf''; apply: sub_segment.
have p3: {inc s', f =1f f''} by move=> a as''; rewrite /f restriction1_V //.
move: (is'' _ xs') => xs''.
have xsi: inc x (substrate (induced_order r s'')) by aw.
have ->: (restriction_to_segment (induced_order r s') x f =
restriction_to_segment (induced_order r s'') x f'').
rewrite -{2} sf in p1.
apply: rts_extensionality =>//; aw.
do 2 rewrite segment_induced_a //.
by move=> a asi; apply: p3; rewrite - sf; apply: p1.
by rewrite - (pb _ xsi); apply: p3.
Qed.
(** Existence follows from two extension properties *)
Definition change_target_fun f t := triple (source f) t (graph f).
Lemma transfinite_aux2 r p s tdf: worder r ->
(alls s (segmentp r)) ->
(forall z, inc z s -> transfinite_def (induced_order r z) p (tdf z)) ->
let t := unionf s (fun z => target (tdf z)) in
let f := (common_ext (Lg s id) (fun z => change_target_fun (tdf z) t) t) in
(transfinite_def (induced_order r (union s)) p f /\ target f = t).
Proof.
move=> wo alseg altd /=.
set si := Lg s id.
set t:= unionf _ _.
have or: order r by fprops.
have alfun:forall i, inc i s -> function (tdf i).
move=> i ins; move: (altd _ ins)=> [sf _ _ ]; fct_tac.
have slso:forall i, inc i s -> source (tdf i) = i.
move=> i ins; move: (altd _ ins)=> [_ so _]; move: so; aw.
by move: (alseg _ ins)=> [q _].
pose tde z := change_target_fun (tdf z) t.
have fpe:forall i, inc i s -> function_prop (tde i) (Vg si i) t.
rewrite /si/tde/change_target_fun; bw;move=>i ins;bw.
move: (alfun _ ins)=> fd.
hnf; rewrite (slso _ ins); aw; split => //.
apply: function_pr; fprops.
apply: (@sub_trans (target (tdf i))); first by apply: f_range_graph.
rewrite /t => x xt; union_tac.
by rewrite (f_domain_graph fd) (slso _ ins).
have Wfe:forall i a, inc i s-> inc a i -> Vf (tdf i) a = Vf (tde i) a.
move=> i a ins ai; symmetry.
set (x:= Vf (tde i) a).
have : (inc (J a x) (graph (tde i))).
move: (fpe _ ins)=> [fu st tg]; apply: Vf_pr3 =>//.
rewrite st /si; bw.
by rewrite /tde /change_target_fun; aw;apply: Vf_pr; apply: alfun.
have agr: (forall i j, inc i s -> inc j s -> sub i j ->
agrees_on (i \cap j) (tde i) (tde j)).
move=> i j ins jns ij.
have ->: (i \cap j = i) by apply/setI2id_Pl.
move: (fpe _ ins)(fpe _ jns)=> [ffi sfi tfi][ffj sfj tfj].
hnf; rewrite sfi sfj /si; bw; split => //.
move=> a ai /=; rewrite -(Wfe _ _ ins ai) -(Wfe _ _ jns (ij _ ai)).
rewrite (transfinite_aux1 wo (alseg _ ins) (alseg _ jns)
ij (altd _ ins) (altd _ jns)).
rewrite restriction1_V =>//; [ by apply: alfun | by rewrite slso].
have agr':forall i j, inc i s -> inc j s ->
agrees_on ((Vg si i) \cap (Vg si j)) (tde i) (tde j).
move=> i j ins jns; rewrite /si; bw.
case: (segment_dichot_sub wo (alseg _ ins) (alseg _ jns)).
by apply: agr.
rewrite setI2_C.
move=> ji; move: (agr _ _ jns ins ji); rewrite /agrees_on.
by move => [s1 s2 sv]; split => //; move => a ai; symmetry; apply: sv.
have su:sub (union s) (substrate r).
move=> v vu; move: (setU_hi vu)=> [i vi ins].
by move: (alseg _ ins)=> [q _]; apply: q.
have dsi: domain si = s by rewrite /si; bw.
rewrite - dsi in fpe agr'.
have aux:forall x0 x1, inc x0 x1 -> inc x1 s ->
sub (segment (induced_order r (union s)) x0) x1.
move=> x0 x1 x0x1 x1s u us; move: (alseg _ x1s)=> [_ spr].
move: (inc_segment us); rewrite /glt; move => [ux0 nux0].
move: (iorder_gle1 ux0); apply: (spr _ _ x0x1).
move: (extension_covering fpe agr'); set f := (common_ext si tde t).
rewrite dsi;move => [[sf tf gf] _ _ agf].
have sjf: surjection f.
split => //; rewrite gf /t => y yt; move: (setUf_hi yt)=> [i ins ti].
move: (altd _ ins)=> [sfi sofi vfi].
move:((proj2 sfi) _ ti)=> [z zs Wz].
rewrite (slso _ ins) in zs.
move: (agf _ ins)=> [sis _ prop].
have zf: inc z (source f) by apply: sis; rewrite /si;bw.
ex_tac; rewrite -Wz Wfe //; apply: prop; rewrite /si;bw.
split => //; split => //; first by aw; rewrite tf - setUb_identity.
aw;move=> x xu; move: (setU_hi xu)=> [i xi ins].
have ap: {inc i, f =1f (tdf i)}.
move=> a ai; move: (agf _ ins)=> [sis _ prop]; rewrite Wfe // prop/si; bw.
have p1: (sub i (substrate r)) by move: (alseg _ ins) => [q _]; apply: q.
have p2: (segment (induced_order r i) x = segment r x).
by rewrite segment_induced_a //; apply: alseg.
have ->: (restriction_to_segment (induced_order r (union s)) x f =
restriction_to_segment (induced_order r i) x (tdf i)).
have p3: (segment (induced_order r (union s)) x = segment r x).
rewrite segment_induced_a//; apply: setU_segment =>//.
have p4: sub (segment r x) i.
move: (alseg _ ins) => [_ nsi] y /segmentP [xle _]; apply: (nsi _ _ xi xle).
apply: rts_extensionality =>//; rewrite ? p2 ? p3;
try apply: induced_wor=>//; aw.
rewrite tf/si; move=> u us; move: (p4 _ us)=> ui; apply/setUb_P; bw.
ex_tac; bw.
by apply: alfun.
by rewrite slso.
move=> a asr; apply: (ap _ (p4 _ asr)).
move: (altd _ ins)=> [_ _]; rewrite ap=>//;apply; aw.
Qed.
Lemma transfinite_aux3 r p x g:
worder r -> inc x (substrate r) ->
transfinite_def (induced_order r (segment r x)) p g ->
transfinite_def (induced_order r (segmentc r x)) p
(extension g x (p (restriction_to_segment r x g))).
Proof.
move=> wo xsr tdo.
have or: order r by fprops.
move: (tdo)=> [sug sog Wg].
have ssr: sub (segment r x) (substrate r) by apply: sub_segment.
have sio: substrate (induced_order r (segment r x)) = segment r x by aw.
rewrite sio in sog Wg.
set (tsx:= segmentc r x).
have stsx: (sub tsx (substrate r)) by apply: sub_segmentc.
have sioc: substrate (induced_order r tsx) = tsx by aw.
have nxsg: ~ (inc x (source g)).
by rewrite sog; aw; hnf; apply: not_in_segment.
set (h:= (restriction_to_segment r x g)).
have sto := (extension_fs (p h) (proj1 sug) nxsg sug).
have tos:(segment r x) +s1 x = tsx by rewrite /tsx segmentc_pr//.
have soto: source (extension g x (p h)) = tsx.
by rewrite/extension; aw; rewrite sog.
hnf;rewrite sioc; split => // y ytsx.
have syx: (sub (segment r y) (segment r x)).
by move: ytsx => /segmentcP; apply: segment_monotone.
have fto: function (extension g x (p h)) by fct_tac.
have fg: function g by fct_tac.
have p2: segment (induced_order r tsx) y = segment r y.
apply: segment_induced_a =>//.
rewrite /tsx; apply: segmentc_segment=>//.
case: (equal_or_not y x) => yx.
rewrite yx extension_Vf_out //.
rewrite yx in ytsx p2.
have p1: sub (segment r x) tsx by rewrite -tos; fprops.
congr p.
apply: rts_extensionality =>//; aw; try ue.
rewrite soto p2; fprops.
hnf; aw; move=> a asr /=; rewrite extension_Vf_in //; ue.
have ysx: inc y (segment r x).
by move: ytsx; rewrite -tos; case/setU1_P.
have p1: {inc (segment r x), g =1f (extension g x (p h))}.
move=> u usx /=; rewrite extension_Vf_in //; ue.
have p3: segment (induced_order r (segment r x)) y = segment r y.
by apply: segment_induced_a =>//; apply: segment_segment =>//.
rewrite -p1 // Wg //.
congr p.
apply: rts_extensionality =>//; rewrite ? p2 ? p3 ? soto ? sog;
try apply: induced_wor=>//;aw.
apply: (sub_trans syx); rewrite -tos; fprops.
move=> a asr; apply: (p1 _ (syx _ asr)).
Qed.
Definition transfinite_defined r p:= choose (fun f => transfinite_def r p f).
Theorem transfinite_definition r p:
worder r -> exists! f, (transfinite_def r p f).
Proof.
move=> wo; apply /unique_existence.
split; last by move=> x y;apply: (transfinite_unique wo).
set (s:=Zo (segments r) (fun z =>
exists f, transfinite_def (induced_order r z) p f)).
have or: order r by fprops.
have als: forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(inc_segmentsP wo).
have ssu: forall s', sub s' s -> inc (union s') s.
move=> s' s's.
have als': (alls s' (segmentp r)).
by move=> x xs'; apply: (als _ (s's _ xs')).
apply: Zo_i.
apply /(inc_segmentsP wo); apply: setU_segment =>//.
pose tdf z:= transfinite_defined (induced_order r z) p.
have atdf: forall z, inc z s' ->
transfinite_def (induced_order r z) p (tdf z).
move=> z zs'; move: (s's _ zs') => /Zo_P [p1 p2].
apply: (choose_pr p2).
move: (transfinite_aux2 wo als' atdf) => [].
set f:= common_ext _ _ _; move=> p1 p2; by exists f.
have sss: forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segmentc r x) s.
move=> x xst /Zo_hi [f tdf]; apply: Zo_i.
by apply: segmentc_insetof.
exists (extension f x (p (restriction_to_segment r x f))).
apply: (transfinite_aux3 wo xst tdf).
move: (transfinite_principle2 wo ssu sss).
by move /Zo_P; rewrite iorder_substrate //; move=> [_].
Qed.
Lemma transfinite_pr r x p:
worder r -> transfinite_def r p x -> transfinite_defined r p = x.
Proof.
move=> wo td.
have tdt: (transfinite_def r p (transfinite_defined r p)).
by apply: choose_pr; exists x.
apply: (transfinite_unique wo tdt td).
Qed.
Lemma transfinite_defined_pr r p: worder r ->
transfinite_def r p (transfinite_defined r p).
Proof.
move=> wo; rewrite /transfinite_defined.
move: (transfinite_definition p wo) => /unique_existence [ ext _].
by apply:choose_pr.
Qed.
(** if [p] sends some functions to [E], then the target of function defined by
transfinite induction is a subset of [E] *)
Theorem transfinite_definition_stable r p F:
worder r ->
(forall f, function f -> segmentp r (source f) -> sub (target f) F ->
inc (p f) F) ->
sub (target (transfinite_defined r p)) F.
Proof.
move => wor hb t.
have or := proj1 wor.
move:(transfinite_defined_pr p wor); set f := transfinite_defined r p.
move => [sfj sf frec]; move/(proj2 sfj); rewrite sf; move => [x xsf <-].
move: x xsf.
apply:(transfinite_principle wor) => x xsr xrec; rewrite (frec _ xsr).
have ssa: sub (segment r x) (source f) by rewrite sf; apply:sub_segment.
move:(rts_fs (proj1 sfj) ssa) => [fg _].
apply: hb => //.
by rewrite /restriction_to_segment/restriction1; aw; apply:segment_segment.
rewrite /restriction_to_segment/restriction1; aw.
move => y /(Vf_image_P (proj1 sfj) ssa) [u /segmentP ua ->]; apply: xrec => //.
order_tac.
Qed.
Theorem transfinite_definition_stable_orig r p F:
worder r ->
(forall f, function f -> segmentp r (source f) -> sub (target f) F ->
inc (p f) F) ->
sub (target (transfinite_defined r p)) F.
Proof.
move=> wo hyp.
set (s:=Zo(segments r) (fun z =>
exists2 f, (transfinite_def (induced_order r z) p f) &(sub (target f) F))).
have or: order r by fprops.
have als x: inc x s -> segmentp r x by move/Zo_S /(inc_segmentsP wo).
suff: inc (substrate r) s.
move /Zo_P => [p1 [f tdf tfF]].
have aux: (induced_order r (substrate r) = r) by apply: iorder_substrate.
rewrite aux in tdf.
have -> //: (transfinite_defined r p = f) by apply: (transfinite_pr wo tdf).
apply: transfinite_principle2=>//.
move=> s' s's.
have als': (alls s' (segmentp r))
by move=> x xs'; apply: (als _ (s's _ xs')).
apply: Zo_i.
apply/(inc_segmentsP wo); apply: setU_segment =>//.
pose tdf z := transfinite_defined (induced_order r z) p.
have atdf: forall z, inc z s' ->
transfinite_def (induced_order r z) p (tdf z).
move=> z zs'; move: (s's _ zs') => /Zo_P [p1 [f p2 _]].
have aux: (exists f, transfinite_def (induced_order r z) p f).
by exists f.
apply: (choose_pr aux).
move: (transfinite_aux2 wo als' atdf) => [].
set f:= common_ext _ _ _ ; move=> p1 p2; exists f => //.
rewrite p2.
move => u uu; move: (setUf_hi uu)=> [v vs' uv].
move: (s's _ vs') => /Zo_P [vs [g tdg tg]].
move: (atdf _ vs') => tdf1.
have wa: (worder (induced_order r v)).
apply: induced_wor =>//; apply: sub_segment1; apply: (als' _ vs').
rewrite (transfinite_unique wa tdg tdf1) in tg.
by apply: tg.
move=> x xst => /Zo_P [_ [f tdf tfF]]; apply: Zo_i.
by apply: segmentc_insetof.
exists (extension f x (p (restriction_to_segment r x f))).
by apply: (transfinite_aux3 wo xst tdf).
have srx: (sub (segment r x) (substrate r)) by apply: sub_segment.
rewrite /extension; move=> t;aw; case /setU1_P; first by apply: tfF.
move: (tdf)=> [sf sof Wf].
have ff: function f by fct_tac.
have ssf: sub (segment r x) (source f) by rewrite sof; aw; fprops.
move => ->; apply: hyp.
exact (proj1 (restriction1_fs (proj1 sf) ssf)).
rewrite /restriction_to_segment/restriction1; aw.
apply: segment_segment=>//.
rewrite /restriction_to_segment/restriction1; aw.
move=> v /(Vf_image_P ff ssf) [u us ->]; apply: tfF;Wtac.
Qed.
Definition ordinal_iso r := transfinite_defined r target.
Lemma transdef_tg1 r (f := ordinal_iso r): worder r ->
forall x, inc x (substrate r) ->
Vf f x = Vfs f (segment r x).
Proof.
move => wor x xsr.
move: (transfinite_defined_pr target wor)=> [pa pb pc].
by rewrite (pc _ xsr) corresp_t.
Qed.
Lemma transdef_tg2 r f:
worder r -> surjection f -> source f = substrate r ->
(forall x, inc x (substrate r) -> Vf f x = Vfs f (segment r x)) ->
f = ordinal_iso r.
Proof.
move => wor pa pb pc.
have pd: transfinite_def r target f by split => // x /pc ->; rewrite corresp_t.
by move: (transfinite_pr wor pd).
Qed.
Lemma transdef_tg3 r X (f: fterm):
worder r -> segmentp r X ->
(forall x, inc x X -> f x = fun_image (segment r x) f) ->
forall x, inc x X -> f x = Vf (ordinal_iso r) x.
Proof.
move => wor pa pb x xX.
have srr: sub (substrate r) (substrate r) by [].
move: (wor) => [or _].
set A:= fun_image X f.
have ta: forall t, inc t X -> inc (f t) A by move => t tx; apply/funI_P; ex_tac.
set g := Lf f X A.
have sg: surjection g by apply: lf_surjective => // y /funI_P.
have fg: function g by fct_tac.
have -> : f x = Vf g x by rewrite /g; aw.
have pc:= (substrate_segment or).
have pd := (sub_segment1 pa).
have pe: transfinite_def (induced_order r X) target g.
rewrite/g;split; aw => t tX; aw; rewrite corresp_t segment_induced_a //.
have ssg': sub (segment r t) X.
move => s /segmentP [st _]; exact: (proj2 pa _ _ tX st).
have ssg: sub (segment r t) (source g) by rewrite /g;aw.
rewrite (pb _ tX); set_extens w.
move /funI_P => [z za zb]; apply /(Vf_image_P fg ssg); ex_tac.
by rewrite /g; aw;apply: ssg'.
move /(Vf_image_P fg ssg)=> [u us]; rewrite /g; aw; last by apply: ssg'.
move => ->; apply/funI_P; ex_tac.
have pf: transfinite_def (induced_order r (substrate r)) target (ordinal_iso r).
rewrite (iorder_substrate or); exact:(transfinite_defined_pr target wor).
move: (pf) =>[[fs _] ]; rewrite (iorder_sr (proj1 wor) srr) => ss _.
move: (transfinite_aux1 wor pa pc pd pe pf) => ->.
by rewrite restriction1_V // ss.
Qed.
(** ** EIII-2-3 Zermelo's theorem *)
(** Given an ordering, let [Sx] be the segment with endpoint [x],
considered as an ordered set. Given two orderings, we consider the set of
all [x] with [Sx=Sx'].
This is a segment, ordered by any of the two induced orders. *)
Definition common_ordering_set r r' :=
Zo ((substrate r) \cap (substrate r'))
(fun x => segment r x = segment r' x /\
induced_order r (segment r x) = induced_order r' (segment r' x)).
Lemma Zermelo_aux0 r r':
common_ordering_set r r' = common_ordering_set r' r.
Proof.
rewrite /common_ordering_set setI2_C.
set_extens t; move/Zo_P => [pa [pb pc]]; apply: Zo_i => //.
Qed.
Lemma Zermelo_aux1 r r': worder r -> worder r' ->
segmentp r (common_ordering_set r r').
Proof.
rewrite /common_ordering_set=> wor wor'.
split; first by move=> t /Zo_P [] /setI2_P [].
move=> x y.
case: (equal_or_not y x); first by move=> ->.
move => nyx /Zo_P [pa [pb pc]] pd.
have ltyx:glt r y x by split.
have sry: inc y (segment r x) by apply /segmentP.
have sry': inc y (segment r' x) by rewrite - pb.
have syr: inc y (substrate r) by apply: (sub_segment sry).
have syr': inc y (substrate r') by apply: (sub_segment sry').
rewrite /induced_order - pb in pc.
have or: order r by fprops.
have or': order r' by fprops.
have sryy': (segment r y = segment r' y).
set_extens t; move/segmentP => [ty nty]; apply /segmentP; split=>//;
suff: (inc (J t y) (r \cap (coarse (segment r x)))).
- rewrite pc; move/setI2_P => [] //.
- apply/setI2_i => //; apply/setXp_i => //; apply/segmentP; order_tac.
- move /setI2_P => [] //.
- have aux: glt r' y x by apply/segmentP; rewrite -pb; apply/segmentP.
rewrite pc pb;apply:setI2_i => //; apply:setXp_i;apply/segmentP =>//.
order_tac.
apply: Zo_i; [ fprops | split=>// ].
rewrite /induced_order - sryy'.
move: (coarse_segment_monotone or pd)=> p1.
set_extens z; move/setI2_P =>[zr zc];
suff: (inc z (r \cap (coarse (segment r x)))).
rewrite pc; move/setI2_P => [] //.
- by move => qa qb; apply: setI2_i => //; apply: p1.
- by apply /setI2_i => //; apply: p1.
- by move /setI2_P => [qa qb]; apply :setI2_i.
- by rewrite pc;apply/setI2_i => //; apply: p1.
Qed.
Lemma Zermelo_aux2 r r' v: worder r -> worder r' ->
v = common_ordering_set r r' -> sub (induced_order r v) (induced_order r' v).
Proof.
rewrite /induced_order /coarse /common_ordering_set.
move=> wor wor' vd.
have or: order r' by fprops.
move=> t /setI2_P [tr] /setX_P [pt Pt Qt].
apply/setI2_P; split; last by apply /setX_P.
move: Qt; rewrite vd => /Zo_P [] /setI2_P [Qtr Qtr'] [ss io].
case: (equal_or_not (P t) (Q t)).
by move=> eq; rewrite -pt eq; order_tac.
move=> neq; rewrite -pt in tr.
have: inc (P t) (segment r (Q t)) by apply: segment_inc.
rewrite ss -{3} pt => aux.
exact: (proj1 (inc_segment aux)).
Qed.
(** We prove Zermelo's theorem by considering well-orderings r,
and sets [S] such that
the segment [Sx] with endpoint [x] is in [S], and [P(Sx)=x].
*)
Definition Zermelo_axioms E p s r:=
[/\ worder r,
sub (substrate r) E,
(forall x, inc x (substrate r) -> inc (segment r x) s) &
(forall x, inc x (substrate r) -> p (segment r x) = x)].
Lemma Zermelo_aux3 E s p r r':
let q := fun r r' => [/\ sub (substrate r) (substrate r'),
r = induced_order r' (substrate r) & segmentp r' (substrate r)] in
Zermelo_axioms E p s r -> Zermelo_axioms E p s r' ->
q r r' \/ q r' r.
Proof.
move=> q [wor srE alseg pr][wor' srE' alseg' pr'].
move: (Zermelo_aux1 wor' wor)(Zermelo_aux1 wor wor').
rewrite Zermelo_aux0.
set (v:= common_ordering_set r r').
move=> svr' svr.
have io: (induced_order r v = induced_order r' v).
by apply: extensionality; apply: Zermelo_aux2=>//; rewrite Zermelo_aux0.
move: (sub_segment1 svr)(sub_segment1 svr')=> vsr vsr'.
case: (equal_or_not v (substrate r)) => evr.
left; rewrite /q -evr; split => //.
rewrite -io evr;symmetry; apply: iorder_substrate; fprops.
case: (equal_or_not v (substrate r')) => evr'.
right; rewrite /q -evr'; split => //.
rewrite io evr';symmetry; apply: iorder_substrate; fprops.
case: (emptyset_dichot ((substrate r) -s v)) => co.
by case: evr; apply: extensionality=>//; apply: empty_setC.
case: (emptyset_dichot (complement (substrate r') v)) => co'.
by case: evr'; apply: extensionality=>//; apply: empty_setC.
have sc: (sub ((substrate r) -s v) (substrate r)).
by apply: sub_setC.
have sc': (sub ((substrate r') -s v) (substrate r')).
by apply: sub_setC.
move:(worder_total wor) (worder_total wor')=> tor tor'.
move:wor=> [or wo]; move: (wo _ sc co)=> [x []]; aw => /setC_P [xs xc] px.
move:wor'=> [or' wo']; move: (wo' _ sc' co')=> [y []]; aw => /setC_P [ys yc] py.
have p1: (segment r x = v).
set_extens z => zs.
ex_middle aux.
move: (inc_segment zs) => zx.
have zc: inc z ((substrate r) -s v) by apply/setC_P; split=>//; order_tac.
move: (iorder_gle1 (px _ zc)) => h; order_tac.
apply /segmentP.
case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz.
case: xc; exact: ((proj2 svr) _ _ zs xz).
have p2: (segment r' y = v).
set_extens z => zs.
ex_middle aux.
move: (inc_segment zs) => zx.
have zc: inc z ((substrate r') -s v) by apply/setC_P; split=>//; order_tac.
move: (iorder_gle1 (py _ zc)) => h; order_tac.
apply /segmentP.
case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz.
case: yc; exact: ((proj2 svr') _ _ zs yz).
have xy: x = y by rewrite - (pr _ xs) -(pr' _ ys) p1 p2.
case: xc.
apply: Zo_i; first by apply :setI2_i => //; ue.
by rewrite p1 xy p2.
Qed.
Lemma Zermelo_aux4 r a (owg := order_with_greatest r a):
worder r -> ~ (inc a (substrate r)) ->
[/\ worder owg, segment owg a = (substrate r) &
forall x, inc x (substrate owg) -> x = a \/
segment owg x = segment r x].
Proof.
move=> wor nas.
move:(worder_adjoin_greatest wor nas) => woe.
move: (order_with_greatest_pr (worder_or wor) nas)=> [[oe se] rv ge].
move: ge=>[asr prop].
split=>//.
set_extens x => xs.
move:(inc_segment xs)=> [xa xna].
have: inc x (substrate owg) by order_tac.
by rewrite se => /setU1_P;case.
have ax: x <> a by dneg ax; rewrite -ax.
apply /segmentP; split=>//; apply: prop; rewrite se; fprops.
move=> x; rewrite se => /setU1_P; case; last by left.
move=> xsr; right.
have xsre: inc x (substrate owg) by rewrite se; aw; fprops.
set_extens y; move /segmentP=> [yx nyx]; apply/segmentP; split => //;last first.
by move: yx; rewrite rv; apply: iorder_gle1.
rewrite rv; apply/iorder_gleP => //.
move: (arg1_sr yx); rewrite se => /setU1_P; case => // eya.
move: (prop _ xsre); rewrite -/owg - eya => xy; case: nyx; order_tac.
Qed.
Lemma Zermelo_aux E s p: sub s (powerset E) ->
(forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x))) ->
exists2 r, Zermelo_axioms E p s r & (~ (inc (substrate r) s)).
Proof.
move=> sp pp.
set (m:= Zo (powerset (coarse E)) (fun r => Zermelo_axioms E p s r)).
pose q r r' := [/\ sub (substrate r) (substrate r'),
r = induced_order r' (substrate r) & segmentp r' (substrate r)].
have qq:(forall r r', inc r m -> inc r' m -> q r r' \/ q r' r).
move=> r r' /Zo_P [rp za] /Zo_P [rp' za'].
apply: (Zermelo_aux3 za za').
set (g:= Lg m id).
have cog: common_worder_axiom g.
rewrite /g / common_worder_axiom/worder_fam;bw;split; fprops.
by hnf; bw; move=> x xm; bw; move: xm => /Zo_hi [a _].
move=> a b am bm; bw.
move: am bm => /Zo_P [ac za] /Zo_P [bc zb].
by case: (Zermelo_aux3 za zb); move => [_ _]; [right | left ].
hnf; bw;move=> a b am bm; bw.
move: am bm => /Zo_P [ac za] /Zo_P [bc zb].
case: (Zermelo_aux3 za zb); first by move => [_].
move=> [sba bi siab] sab.
have ssab: (substrate a = substrate b) by apply: extensionality=>//.
have oa: order a by move: za=> [woa _]; fprops.
have ob: order b by move: zb=> [wob _ ]; fprops.
hnf;rewrite ssab iorder_substrate // bi - ssab iorder_substrate //.
move: (worder_merge cog) => [coex wou alsu ssu ssup].
have dg: domain g = m by rewrite /g; bw.
have Vga a: inc a m -> Vg g a = a by move=> am; rewrite /g; bw.
move: coex => [om0 som0 pom0].
rewrite dg in alsu ssu ssup som0 pom0.
set (m0:= unionb g).
have Za: (Zermelo_axioms E p s m0).
hnf; split => //; rewrite som0=> t tu;move: (setUf_hi tu)=> [u ud ts];
move: (ud) => /Zo_P [_ [_ p1 p2 p3]];
move: (ts); rewrite Vga // => tb.
by apply: p1.
by rewrite -(ssu _ _ ud ts); rewrite Vga //; apply: p2.
by rewrite -(ssu _ _ ud ts); rewrite Vga //; apply: p3.
exists m0 => // sm0s.
move:(pp _ sm0s)=> [pE nps].
move: (Zermelo_aux4 wou nps) => [woe seu asu].
set (a:= p (substrate m0)).
move: (order_with_greatest_pr om0 nps) =>[[ou su] up geu].
have Zae: (Zermelo_axioms E p s (order_with_greatest m0 a)).
move: Za=> [p1 p2 p3 p4].
have H t: inc t (substrate m0) ->
segment (order_with_greatest (unionb g) a) t = segment (unionb g) t.
move => ts; move: (setU1_r (p (substrate m0)) ts); rewrite - su => /asu.
by case => // hyp; case: nps; rewrite - hyp.
split=>//; rewrite su => t /setU1_P; case.
- apply: p2.
- by move=> ->.
- by move=> ts; rewrite (H _ ts); apply: p3.
- by move => ->; rewrite seu.
- by move=> ts;rewrite (H _ ts); apply: p4.
- by move=> ->; rewrite seu.
have um:inc (order_with_greatest m0 a) m.
apply: Zo_i =>//;apply /setP_P.
apply: sub_trans (setX_Sll (proj42 Zae)).
apply: sub_graph_coarse_substrate; fprops.
case: nps; rewrite {2} som0.
apply: (setUf_i um); rewrite (Vga _ um) su; fprops.
Qed.
(** The axiom of choice asserts existence of an element [p(x)] of [E] not
in [x], if [x] is not [E]. From this we deduce a well-ordering on [E] *)
Theorem Zermelo E: exists r, worder_on r E.
Proof.
set (s:=(powerset E) -s1 E).
have p1: sub s (powerset E) by rewrite /s; apply: sub_setC.
set (p:= fun x => rep (E -s x)).
have p2: forall x, inc x s -> inc (p x) (E -s x).
move=> x xs; rewrite /p; apply: rep_i.
apply: setC_ne.
by move: xs => /setC_P [] /setP_P pa /set1_P xe.
have p3: forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x)).
by move => x xs; move: (p2 _ xs) => /setC_P.
move: (Zermelo_aux p1 p3) => [r [xor so alse ps ns]].
exists r; split=> //;ex_middle h; case: ns.
by apply/setC_P; split; [ apply /setP_P | move/set1_P].
Qed.
(** ** EIII-2-4 Inductive sets *)
Definition inductive r :=
forall X, sub X (substrate r) -> total_order (induced_order r X) ->
exists x, upper_bound r X x.
(** Examples of inductive set *)
Lemma inductive_graphs a b:
inductive (opp_order (extension_order a b)).
Proof.
move: (extension_osr a b)=> [or sr].
move: (opp_osr or) => [ooi osr] X XX.
move: (XX); rewrite osr sr => Xs toX.
have Ha:forall i, inc i X -> function i.
by move=> i iX; move: (Xs _ iX) => /sfunctionsP [].
have Hb:forall i, inc i X -> target i = b.
by move=> i iX; move: (Xs _ iX) => /sfunctionsP [_ ].
move: toX=> [orX]; aw => tor.
set si:= Lg X source.
have Hd: forall i j, inc i (domain si) -> inc j (domain si) ->
agrees_on ((Vg si i) \cap (Vg si j)) i j.
rewrite /si; bw; move=> i j iX jX; bw.
split; [by apply: subsetI2l | by apply: subsetI2r | ].
move=> t /setI2_P [ti tj].
case: (tor _ _ iX jX)=> h; move: (iorder_gle1 h)=> h'.
apply: (extension_order_pr h' ti).
symmetry; apply: (extension_order_pr h' tj).
have He:forall i, inc i (domain si) -> function_prop i (Vg si i) b.
rewrite /si; bw; move=> i iX; hnf; bw;split; fprops.
move: (extension_covering He Hd) => [[fg sg tg] _ _ agg].
set g:= (common_ext si id b).
have gs: (inc g (sub_functions a b)).
apply /sfunctionsP;split => // t tsg.
rewrite sg in tsg; move: (setUf_hi tsg)=> [v].
rewrite {1}/si; bw => vx; rewrite /si; bw => tv.
by move: (Xs _ vx) => /sfunctionsP [_ sv _]; apply: sv.
rewrite /upper_bound osr sr; ex_tac.
move: agg; rewrite /si; bw => agg.
move=> y yX; move: (Xs _ yX)=> ys; move: (agg _ yX)=> ag.
have fy: (function y) by move: ys; fprops.
apply /igraph_pP; apply/extension_order_P1;split => //.
apply/(sub_functionP fy fg).
move: ag; rewrite /agrees_on; bw;move=> [p1 p2 p3]; split => //.
by move=> u; symmetry; apply: p3.
Qed.
(** Full and short version of Zorn's lemma *)
Theorem Zorn_aux r: order r ->
(forall s, sub s (substrate r) -> worder (induced_order r s) ->
(bounded_above r s)) ->
exists a, maximal r a.
Proof.
move=> or zaux.
pose px X v := upper_bound r X v /\ ~ (inc v X).
set (p := fun X => choose (fun v => px X v)).
set (E:= substrate r).
set (s:= Zo (powerset E) (fun X => exists v, px X v)).
have apx: forall X, inc X s -> px X (p X).
by move=> X /Zo_P [_ ev]; apply: choose_pr.
have sp: sub s (powerset E) by rewrite /s; apply: Zo_S.
have zp: forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x)).
by move=> x xs; move: (apx _ xs); rewrite /px; move=> [[h1 h2] h3].
move: (Zermelo_aux sp zp)=> [r' [xor so alse ps ns]].
move: (iorder_osr or so) => [oi sr1].
have ext: sub r' (induced_order r (substrate r')).
move=> x xr.
move:(pr1_sr xr)(pr2_sr xr) => Ps Qs.
have gr: sgraph r' by fprops.
move: (gr _ xr) => xp; rewrite -xp; rewrite - xp in xr.
case: (equal_or_not (P x) (Q x)) => aux.
rewrite aux; order_tac; aw.
have ltPQ: glt r' (P x) (Q x) by split.
have Pse: (inc (P x) (segment r' (Q x))) by apply/segmentP.
apply /iorder_gleP => //.
by move: (alse _ Qs)(ps _ Qs) => p1 <-; apply: (proj2 (proj1 (apx _ p1))).
have r'v: r' = induced_order r (substrate r').
apply: extensionality => // t tio.
have p1: order (induced_order r (substrate r')) by fprops.
have p2: sgraph (induced_order r (substrate r')) by fprops.
move: (p2 _ tio) => pt.
move:(pr1_sr tio)(pr2_sr tio); rewrite sr1 => Ps Qs.
rewrite -pt in tio |- *.
case: (total_order_pr2 (worder_total xor) Qs Ps) =>//.
move=> [lePQ nPQ]; move: (ext _ lePQ)=>tio'; case: nPQ; order_tac.
rewrite r'v in xor.
move: (zaux _ so xor) => [u [us ub]].
exists u.
split => // x ux.
ex_middle h.
have xu: (glt r u x) by split => //; apply: nesym.
case: ns; apply: Zo_i; [ by apply/setP_P | exists x; split].
split; first by order_tac.
move=> y ys'; move: (ub _ ys')=> yu; order_tac.
move=> xs'; move: (ub _ xs')=> xu'; order_tac.
Qed.
Theorem Zorn_lemma r: order r -> inductive r ->
exists a, maximal r a.
Proof.
move=> or isr; apply: Zorn_aux =>//.
by move=> s ssr wo; hnf; apply: isr =>//; apply: worder_total.
Qed.
(** Consequences *)
Lemma inductive_max_greater r a: order r -> inductive r ->
inc a (substrate r) -> exists2 m, maximal r m & gle r a m.
Proof.
move=> or isr asr.
set (F:= Zo (substrate r)(gle r a)).
have Fs: sub F (substrate r) by rewrite /F; apply: Zo_S.
move: (iorder_osr or Fs) => [oi sr].
have aF: inc a F by rewrite /F; apply: Zo_i=> //; order_tac.
suff isF: inductive (induced_order r F).
move:(Zorn_lemma oi isF)=> [b []]; aw => bF bm.
move: (bF) => /Zo_P [bs ab].
exists b => //; split =>// x h.
apply: bm; apply/iorder_gleP => //; apply: Zo_i; order_tac.
move=> u; aw=> uF; rewrite iorder_trans // => toi.
have tos: (sub (u +s1 a) (substrate r)).
by apply: sub_trans Fs => t; case /setU1_P ; [ apply: uF| move=> ->].
move: (iorder_osr or tos) => [oit sit].
have toit: total_order (induced_order r (u +s1 a)).
split=>//; rewrite sit.
have susr: sub u (substrate r) by apply: sub_trans Fs.
move=> x y; case /setU1_P=> hx; case /setU1_P => hy.
- move: toi => [_]; aw => h.
move: (h _ _ hx hy); case => xx; [left | right];
apply/iorder_gleP; fprops; apply (iorder_gle1 xx).
- rewrite hy;right; apply/iorder_gleP; fprops.
by move: (uF _ hx); move /Zo_P => [].
- rewrite hx;left; apply/iorder_gleP; fprops.
by move: (uF _ hy); move /Zo_P => [].
- rewrite hx hy; left;apply/iorder_gleP; fprops.
by move: aF; move /Zo_P => [].
move: (isr _ tos toit) => [b [bs bub]].
move: (bub _ (setU1_1 u a)) => ab.
have bF: inc b F by rewrite /F; apply: Zo_i.
exists b; split; aw=>// y yu.
by move: (bub _ (setU1_r a yu)) => yb; apply/iorder_gleP => //; apply: uF.
Qed.
Lemma inductive_powerset A F: sub A (powerset F) ->
(forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) ->
sub S A ->inc (union S) A) ->
inductive (sub_order A).
Proof.
move=> sp Sp X XA [oX tX].
move: (sub_osr A) => [or1 sr1].
rewrite iorder_sr in tX; fprops; rewrite sr1 in XA.
have p1: inc (union X) A.
apply: Sp =>// x y xX yX.
case: (tX _ _ xX yX).
by move/iorder_gle1 => /sub_gleP [_ _ h]; left.
by move/iorder_gle1 => /sub_gleP [_ _ h]; right.
exists (union X);split; first by ue.
by move=> y yX; apply /sub_gleP;split => //;fprops; apply: setU_s1.
Qed.
Lemma maximal_in_powerset A F: sub A (powerset F) ->
(forall So, (forall x y, inc x So -> inc y So -> sub x y \/ sub y x) ->
sub So A -> inc (union So) A) ->
exists a, maximal (sub_order A) a.
Proof.
move=> Ap /(inductive_powerset Ap).
by move: (sub_osr A) => [oA sr1];apply: Zorn_lemma.
Qed.
Lemma minimal_in_powerset A F: sub A (powerset F) -> nonempty A ->
(forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) ->
sub S A -> nonempty S -> inc (intersection S) A) ->
exists a, minimal (sub_order A) a.
Proof.
move=> Ap [x xA] pA.
move: (sub_osr A) => [oA sr1].
move: (opp_osr oA) => [ooA soA].
have ioA: inductive (opp_order (sub_order A)).
move => X; rewrite soA sr1 => XA;rewrite /total_order.
rewrite iorder_sr // ? soA ? sr1 //.
move=> [pb pc]; rewrite /upper_bound soA sr1.
case: (emptyset_dichot X) => neX.
exists x; rewrite neX;split => // y; case; case.
have iXA:inc (intersection X) A.
apply: pA =>// a b aX bX.
by move: (pc _ _ aX bX); case => h; move: (iorder_gle1 h) =>
/igraph_pP /sub_gleP [_ _]; [right | left].
exists (intersection X); split; first by aw; ue.
move=> y yX;apply /igraph_pP; apply /sub_gleP;split; fprops.
by apply: setI_s1.
move: (Zorn_lemma ooA ioA)=> [a ] /(maximal_opp oA) ha.
by exists a.
Qed.
(** ** EIII-2-5 Isomorphisms of well-ordered sets *)
(** Uniqueness of morphism between segments of well-ordered sets *)
Lemma increasing_function_segments r r' f g:
worder r -> worder r' ->
increasing_fun f r r' -> strict_increasing_fun g r r'->
segmentp r' (range (graph f)) ->
forall x, inc x (source f) -> gle r' (Vf f x) (Vf g x).
Proof.
move=> wor wor'
[or or' [ff sf tf] incf] [_ _ [fg sg tg] sing] sr x xsf.
set (s :=Zo (source f) (fun x => (glt r' (Vf g x) (Vf f x)))).
have sfsg: source f = source g by ue.
move: (worder_total wor) => tor.
move: (worder_total wor') => tor'.
have Wfsr': inc (Vf f x) (substrate r') by rewrite - tf; fprops.
have Wgsr': inc (Vf g x) (substrate r').
by rewrite sfsg in xsf;rewrite - tg; fprops.
case: (total_order_pr2 tor' Wgsr' Wfsr') =>// Wlt.
have nes: nonempty s by exists x; rewrite /s; apply: Zo_i.
have ssf: sub s (substrate r) by rewrite /s sf; apply: Zo_S.
move:(worder_prop wor ssf nes)=> [y ys yle].
move: ys => /Zo_P [ysf [leWy neWy]].
have Wrg: inc (Vf f y) (range (graph f)) by Wtac.
move: ((proj2 sr) _ _ Wrg leWy).
move/(range_fP ff) => [z zf vv].
have lt1: glt r' (Vf f z) (Vf f y) by rewrite - vv.
have lt2: glt r z y.
have: (glt r z y \/ gle r y z).
rewrite sf in ysf zf; apply: (total_order_pr2 tor zf ysf).
case =>// yz; move: (incf _ _ yz)=> lt4; order_tac.
have Wzf: inc (Vf f z) (substrate r') by rewrite - tf; fprops.
have Wzg: inc (Vf g z) (substrate r')
by rewrite sfsg in zf;rewrite- tg; fprops.
case: (total_order_pr2 tor' Wzg Wzf) => h.
have zs: (inc z s) by apply: Zo_i.
case: (not_le_gt or (yle _ zs) lt2).
move: (sing _ _ lt2); rewrite vv => lt3; order_tac.
Qed.
Lemma isomorphism_worder_unique r r' x y:
worder r -> worder r' -> segmentp r' (range (graph x)) ->
segmentp r' (range (graph y)) ->
order_morphism x r r' -> order_morphism y r r' ->
x = y.
Proof.
move=> wor wor' srx sry mx my.
move:(order_morphism_increasing mx) => six.
move:(order_morphism_increasing my) => siy.
move: (strict_increasing_w six)=> sx.
move: (strict_increasing_w siy)=> sy.
move: mx my=> [_ or' [fx srcx tx] _][_ _ [fy srcy ty] _].
apply: function_exten =>//; try ue.
move=> a asx.
move: (increasing_function_segments wor wor' sx siy srx asx) => p1.
rewrite srcx - srcy in asx.
move: (increasing_function_segments wor wor' sy six sry asx) => p2.
order_tac.
Qed.
Theorem isomorphism_worder r r': worder r -> worder r' ->
let iso:= (fun u v f =>
segmentp v (range (graph f)) /\ order_morphism f u v) in
(exists! f,iso r r' f) \/ (exists! f, iso r' r f).
Proof.
move=> wor wor' iso.
set (E:= substrate r).
set (E':= substrate r').
have or: order r by fprops.
have or': order r' by fprops.
move: (extension_osr E E').
set o1:= (extension_order E E'); set o2:= opp_order o1.
move => [oe soe1]; move: (opp_osr oe) => [ooe osr].
have soe: sub_functions E E' = substrate o2 by ue.
set (s:= (Zo (sub_functions E E') (fun z => exists2 u,
segmentp r u & iso (induced_order r u) r' z))).
have ssee: sub s (sub_functions E E') by rewrite /s; apply: Zo_S.
have sse: sub s (substrate o1) by ue.
have ssoxee: sub s (substrate o2) by ue.
have ins:inductive (induced_order o2 s).
move=> X;rewrite (iorder_sr ooe ssoxee) => Xs;rewrite(iorder_trans _ Xs)=> pX.
have Xse:sub X (sub_functions E E') by apply: (sub_trans Xs ssee).
have Xsoe:sub X (substrate o2) by ue.
have alseg: forall x, inc x s -> segmentp r (source x).
move=> x /Zo_hi [u ru [_ bb]]; move: bb => [_ _ [_ -> _] _].
by aw;apply: sub_segment1.
have alsegr: forall x, inc x s -> segmentp r' (range (graph x)).
by move=> x /Zo_hi [u _ [sv _]].
have Xso: sub X (substrate o1) by ue.
move: pX => [_ ]; aw => ppX.
have cov: forall u v x, inc u X -> inc v X -> inc x (source u) ->
inc x (source v) -> Vf u x = Vf v x.
move=> u v x uX vX xsu xsv.
move: (ppX _ _ uX vX); case => h; move: (iorder_gle1 h);
move/igraph_pP/ extension_orderP => [_ _ h0];
[ | symmetry];apply: extends_sV => //.
move:(sup_extension_order2 Xse cov)=> [x [lubx sx rgx gx]].
move: lubx => /(lubP ooe Xsoe) [[xsoe xb] lub]; rewrite - soe in xsoe.
have xs: inc x s.
have ssx: segmentp r (source x).
rewrite sx; apply: setUf_segment =>//.
by hnf; bw;move=> a aX; bw;apply: alseg; apply: Xs.
rewrite /s; apply: Zo_i=>//; exists (source x) => //.
have srgx: segmentp r' (range (graph x)).
rewrite rgx; apply: setUf_segment =>//.
by hnf;bw;move=> a aX; bw;apply: alsegr; apply: Xs.
have sxsr: sub (source x) (substrate r) by move: ssx=> [].
have srxs: sub (range (graph x)) (substrate r') by move: srgx => [].
have xi: (forall a b,
inc a (source x) -> inc b (source x) ->
(gle (induced_order r (source x)) a b <->
gle r' (Vf x a) (Vf x b))).
move=> a b; rewrite sx => asX bsX.
apply: (iff_trans(iorder_gleP r asX bsX)).
move: (setUf_hi asX)=> [u uX].
move: (setUf_hi bsX)=> [v vX].
rewrite Lg_domain in uX vX; bw => bv au.
have [w [wX asw bsw]] :exists z,
[/\ inc z X, inc a (source z) & inc b (source z)].
move: (ppX _ _ uX vX) ; case => h; move: (iorder_gle1 h);
move/igraph_pP/ extension_orderP => [_ _ ext];
move: (extends_Ssource ext)=> sext.
by move: (sext _ au) => ax; exists v.
by move: (sext _ bv) => ax; exists u.
rewrite - (extension_order_pr (xb _ wX) asw).
rewrite - (extension_order_pr (xb _ wX) bsw).
move:(Xs _ wX) => /Zo_hi [z [sz _ [_ [_ _ [_ sf _] ifz]]]].
rewrite (iorder_sr or sz) in sf; rewrite - sf in ifz.
split; last by move /(ifz _ _ asw bsw);apply:iorder_gle1.
move => lab; apply /(ifz _ _ asw bsw);apply/(iorder_gleP ) => //.
move: xsoe => /sfunctionsP [fx srcx tx].
move: (iorder_osr or srcx) => [pa pb].
split => //.
exists x.
split; first by rewrite iorder_sr //.
move=> y yX; move: (Xs _ yX)=> ys.
by apply /iorder_gleP => //; apply: xb.
move:(iorder_osr ooe ssoxee) => [oio sio].
move: (Zorn_lemma oio ins) => [f []]; aw =>fis fmax.
move: (fis) => /Zo_P [fee [x sx xiso]].
(* maybe f is the answer *)
case: (equal_or_not x (substrate r)) => h.
move: xiso; rewrite h iorder_substrate //; move=> xiso.
left; apply /unique_existence;split; first by exists f.
move=> a b [s1 m1][s2 m2].
by apply: (isomorphism_worder_unique (r:=r) (r':=r')).
(* first case is excluded; uniqueness is trivial *)
right; apply /unique_existence;split; last first.
move=> a b [s1 m1][s2 m2].
by apply: (isomorphism_worder_unique (r:=r') (r':=r)) =>//.
(* maybe the inverse of f is the answer *)
case: (equal_or_not (range (graph f)) (substrate r'))=> h'.
move: xiso => [_ xiso]; move: (order_morphism_fi xiso) => injf.
set (g:= triple E' E (inverse_graph (graph f))).
move: xiso=> [_ _ [ff sf tf] vf].
have gf: sgraph (graph f) by fprops.
have sf': source f = x by rewrite sf; aw; apply: sub_segment1.
have rgg: range (graph g) = x by rewrite /g; aw; rewrite igraph_range; aw.
have fg: function g.
rewrite /g; apply: function_pr.
split;fprops; move=> a b /=.
move/igraphP=> [pa J1g] /igraphP [pb J2g] sv.
rewrite - sv in J2g; move: (injective_pr3 injf J1g J2g).
by apply: pair_exten.
by move: rgg; rewrite /g; aw; move=> ->;move: sx=> [xe _].
rewrite igraph_domain =>//.
exists g.
hnf; rewrite rgg /order_morphism;split => //.
split => //; first by split => //;try solve [ rewrite /g; aw].
move=> a b asg bsg.
have fgp: (forall u, inc u (source g) ->
(inc (Vf g u) (source f) /\ Vf f (Vf g u) = u)).
move=> u usg; move: (Vf_pr3 fg usg); rewrite {2} /g; aw.
move/igraph_pP => Jg; split; [ Wtac | symmetry;apply: (Vf_pr ff Jg)].
move: (fgp _ asg)(fgp _ bsg)=> [W1s va][W2s vb].
rewrite -{1} va -{1} vb.
rewrite - (vf _ _ W1s W2s); split; first (by apply:iorder_gle1).
move => lab; apply/iorder_gleP => //; ue.
(* Here f is not maximal, we construct an extension *)
case: (well_ordered_segment wor sx)=> aux; first by contradiction.
move: aux=> [a asr xa].
move: xiso=> [st [_ _ [ff sf tf] isf]].
case: (well_ordered_segment wor' st)=> aux; first by contradiction.
move: aux=> [b vsr tb].
set (g:=extension f a b).
have sfx: source f = x by rewrite sf; aw;rewrite xa; apply: sub_segment.
have asf: ~ (inc a (source f)) by rewrite sfx xa; move;apply: not_in_segment.
have fg:function g by apply: extension_f.
have tg: target g = E'.
rewrite/g /extension; aw; rewrite tf; by apply: setU1_eq.
have sg: source g = segmentc r a.
by rewrite /g/extension; aw; rewrite sfx xa; apply: segmentc_pr.
have sap t: sub (segmentc r t) (substrate r) by apply: Zo_S.
have rgg: (range (graph g) = segmentc r' b).
rewrite/g/extension; aw; rewrite - segmentc_pr // range_setU1; ue.
have gs: inc g s.
rewrite /s; apply: Zo_i.
by apply/sfunctionsP;split => //; rewrite sg; apply: sap.
exists (segmentc r a).
by apply: segmentc_segment.
split; first by rewrite rgg; apply: segmentc_segment.
move: (iorder_osr or (sap a)) => []; rewrite - sg => pa pb.
hnf;split => // u v; rewrite sg - segmentc_pr //.
move => qa qb; apply: (iff_trans (iorder_gleP r qa qb)).
move: qa qb; rewrite - xa - sfx => /setU1_P ut /setU1_P vt.
have p1: forall w, inc w (source f) -> glt r' (Vf f w) b.
move=> w wsf.
have: inc (Vf f w) (range (graph f)) by Wtac.
by rewrite tb; move/segmentP.
have p2: forall w, inc w (source f) -> glt r w a.
by move=> w; rewrite sfx xa; move/segmentP.
case: ut => hu; [rewrite extension_Vf_in // | rewrite hu extension_Vf_out //].
case:vt => hv;[rewrite extension_Vf_in // | rewrite hv extension_Vf_out //].
move:(isf u v hu hv). move:(iff_sym(iorder_gleP r hu hv)); rewrite sfx.
move => qa qb; exact: (iff_trans qa qb).
by move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _].
case:vt => hv; [rewrite extension_Vf_in // | rewrite hv extension_Vf_out //].
move: (p1 _ hv)(p2 _ hv)=> [e1 ne1][e2 ne2].
split => h'';[ case: ne2 | case: ne1];order_tac.
by split => _; order_tac.
(* We express maximality *)
have eqfg: g = f.
have pa: inc g (sub_functions E E') by rewrite /g/extension; fprops.
have pb: sub (graph f) (graph g) by rewrite corresp_g;fprops.
have pc: sub (target f) (target g) by rewrite corresp_t ; fprops.
apply: fmax; apply /iorder_gleP => //; apply /igraph_pP.
by apply /extension_orderP.
case: asf; rewrite -eqfg sg.
by apply: inc_bound_segmentc.
Qed.
(** Consequences *)
Lemma unique_isomorphism_onto_segment r f: worder r ->
segmentp r (range (graph f)) -> order_morphism f r r ->
f = identity (substrate r).
Proof.
move=> wor seg mor.
have [pa pb]: segmentp r (range (graph (identity (substrate r)))) /\
order_morphism (identity (substrate r)) r r.
split.
have [_ si]:(bijection (identity (substrate r))) by apply: identity_fb.
rewrite (surjective_pr3 si); aw; apply: substrate_segment; fprops.
apply: identity_morphism; fprops.
by case: (isomorphism_worder wor wor); move /unique_existence=> [_]; apply.
Qed.
Lemma bij_pair_isomorphism_onto_segment r r' f f':
worder r -> worder r' ->
segmentp r' (range (graph f)) -> order_morphism f r r' ->
segmentp r (range (graph f')) -> order_morphism f' r' r ->
(order_isomorphism f r r' /\ order_isomorphism f' r' r /\
f = inverse_fun f').
Proof.
move=> wor wor' sr1 om sr2 om'.
move: (om)(om')=>[or or' [ff sf tf] fp] [_ _ [ff' sf' tf'] fp'].
have gf: sgraph (graph f) by fprops.
have gf': sgraph (graph f') by fprops.
have cff': (f \coP f') by split => //; ue.
have cf'f: (f' \coP f) by split => //; ue.
have mor1 := (compose_order_morphism om' om).
have mor2 := (compose_order_morphism om om').
have fc: function (f' \co f) by fct_tac.
have srg: segmentp r (range (graph (f'\co f))).
split.
have <-: target (f' \co f) = substrate r by aw.
by apply: f_range_graph.
move=> x y.
rewrite /compose; aw; rewrite (compg_range _ gf).
move/dirim_P=> [u urg p2] yx.
have xrg: (inc x (range (graph f'))) by ex_tac.
have usr: inc u (source f') by Wtac.
move: ((proj2 sr2) _ _ xrg yx) => /(range_fP ff') [v vsf' vp].
move: yx; rewrite (Vf_pr ff' p2) vp -fp'// => yr.
move: ((proj2 sr1) _ _ urg yr) => va; apply /dirim_P; ex_tac; Wtac.
have srg': segmentp r' (range (graph (f \co f'))).
have fc': function (f \co f') by fct_tac.
split.
have <-: target (f \co f') = substrate r' by aw.
by apply: f_range_graph.
move => x y.
rewrite /compose; aw; rewrite (compg_range _ gf').
move/dirim_P=> [u urg p2] yx.
have xrg: (inc x (range (graph f))) by ex_tac.
have usr: inc u (source f) by Wtac.
move: ((proj2 sr1) _ _ xrg yx) => /(range_fP ff) [v vsf' vp].
move: yx; rewrite (Vf_pr ff p2) vp -fp// => yr.
move: ((proj2 sr2) _ _ urg yr) => va; apply /dirim_P; ex_tac; Wtac.
have p1 := (unique_isomorphism_onto_segment wor srg mor2).
have p2 := (unique_isomorphism_onto_segment wor' srg' mor1).
rewrite - sf in p1; rewrite - sf' in p2.
have [p3 p4 p5] := (bijective_from_compose cff' cf'f p2 p1).
by split.
Qed.
Lemma isomorphic_subset_segment r a:
worder r -> sub a (substrate r) ->
exists w, exists f, segmentp r w /\
order_isomorphism f (induced_order r a) (induced_order r w).
Proof.
move=> wo asr.
have woi :=(induced_wor wo asr).
move: (isomorphism_worder woi wo).
case; move/unique_existence=> [[f [sr h]] _];
move: (order_morphism_fi h) => [ff injf];
move: h => [oir or [_ sf tf] fp].
move: sf; aw => sf.
have ta: lf_axiom (Vf f) (source f) (range (graph f)).
by move=> c csf /=; Wtac.
set (g := Lf (Vf f) (source f) (range (graph f))).
exists (range (graph f)); exists g.
have aux:sub (range (graph f)) (substrate r) by case:sr.
have gf: sgraph (graph f) by fprops.
rewrite /order_isomorphism /g;split => //; split => //.
apply: (proj1 (iorder_osr or aux)).
split; aw;fprops;apply: lf_bijective =>//.
move=> y /(range_fP ff) [x pa pb]; ex_tac.
hnf; aw;move=> x y xsf ysf; aw;apply: (iff_trans (fp _ _ xsf ysf)).
split; [ move => aux1; apply/iorder_gleP => //; Wtac | apply: iorder_gle1].
case: (well_ordered_segment woi sr)=> hyp.
rewrite -hyp in tf.
have oi: order_isomorphism f r (induced_order r a).
split => //; split => //;last by rewrite -hyp tf.
split=>//; apply: surjective_pr4 =>//.
have ioi :=(inverse_order_is oi).
exists (substrate r); exists (inverse_fun f).
split; first by apply: substrate_segment.
by rewrite iorder_substrate.
move: hyp=>[x xsr rgf].
move: xsr; aw => xsr.
have xsf: inc x (source f) by rewrite sf; apply: asr.
have Ws: inc (Vf f x) (segment (induced_order r a) x).
by rewrite -rgf; Wtac.
set (s :=Zo (source f) (fun a => (glt r (Vf f a) a))).
have nes: nonempty s.
exists x; apply: Zo_i => //.
apply:iorder_gle2 (inc_segment Ws).
have ssf: sub s (substrate r) by rewrite - sf;apply: Zo_S.
move: (worder_prop wo ssf nes) => [y ys ley].
move: ys => /Zo_P [ysf [leW neW]].
have p1: inc (Vf f y) (source f) by rewrite sf; order_tac.
have p2: inc (Vf f y) s.
apply: Zo_i =>//; split; last by dneg h; apply: injf.
move: leW;rewrite (fp _ _ p1 ysf) => leW; apply: (iorder_gle1 leW).
move: (ley _ p2) => geW.
case: neW; order_tac.
Qed.
(** Two isomorphic segments of a well-ordered set are equal *)
Lemma segments_iso1 r A B: worder r -> sub A B ->
segmentp r A -> segmentp r B ->
(induced_order r B) \Is (induced_order r A) -> A = B.
Proof.
move => woa AB sA sB.
move => [f [ora orb [ [[ff injf] sjf] sf tf] isf]].
have oa: order r by move: woa => [o _].
have As: sub A (substrate r) by apply: sub_segment1.
have Bs: sub B (substrate r) by apply: sub_segment1.
move: sf tf; aw=> sf tf.
rewrite - sf in injf isf.
have ta: lf_axiom (Vf f) B B.
move=> t tx; apply: AB; rewrite - tf; Wtac; ue.
set g := Lf (Vf f) B B.
have fg: function g by apply: lf_function.
have rg: (range (graph g) = A).
rewrite - tf;set_extens t.
move /(range_fP fg)=> [u];rewrite /g lf_source => uc; aw => ->; Wtac; ue.
move/(proj2 sjf) =>[u usf].
rewrite sf in usf;move=> <-; apply /(range_fP fg).
exists u; rewrite /g; aw; split => //.
have sr: segmentp (induced_order r B) (range (graph g)).
rewrite rg; hnf; aw;split => //.
move => x y xA leyx; move: (iorder_gle1 leyx).
move: sA xA; rewrite /segmentp; move=>[_]; apply.
have om: order_morphism g (induced_order r B)(induced_order r B).
hnf; split => //; rewrite /g; aw.
split; aw.
hnf; aw; move=> x y xB yB /=; aw.
move:(iorder_gleP r (ta _ xB) (ta _ yB)) => xx.
hnf in isf; rewrite sf in isf.
apply: (iff_trans (isf _ _ xB yB)).
rewrite - sf in xB yB.
move: (Vf_target ff xB) (Vf_target ff yB); rewrite tf => f1a f2a.
apply: (iff_trans (iorder_gleP r f1a f2a)).
by symmetry.
have wob:= (induced_wor woa Bs).
have gi:= (unique_isomorphism_onto_segment wob sr om).
symmetry;move: rg; rewrite gi; aw; rewrite surjective_pr3 //; aw.
by move: (identity_fb B) => [_ ok].
Qed.
Lemma segments_iso2 a A B: worder a ->
inc A (segments a) -> inc B (segments a) ->
(induced_order a A) \Is (induced_order a B) -> A = B.
Proof.
move=> woa As Bs.
move: (worder_total (segments_worder woa)) => [or].
rewrite (proj2 (sub_osr _)) => tor; move: (tor _ _ As Bs).
move: As Bs;move/(inc_segmentsP woa)=> As /(inc_segmentsP woa) Bs.
case; move /sub_gleP=> [_ _ sAB] oi.
move: (orderIS oi) => oi'; apply: (segments_iso1 woa)=>//.
symmetry; apply: (segments_iso1 woa)=>//.
Qed.
(** We rewrite [isomorphism_worder]: two well-ordered sets is isomorphic,
or one is isomorphic to a segment of the other *)
Lemma isomorphism_worder2 r r': worder r -> worder r' ->
[\/ r \Is r',
(exists2 x, inc x (substrate r) & (induced_order r (segment r x)) \Is r') |
(exists2 x, inc x (substrate r') & (induced_order r' (segment r' x)) \Is r)].
Proof.
move => wor wor'.
case: (isomorphism_worder wor wor'); move /unique_existence=> [[f [fp1 fp2]] _];
move: (order_morphism_fi fp2) => injf;
move: fp2 => [pa pb [pc pd pe] pf].
case : (well_ordered_segment wor' fp1) => eq1.
constructor 1;exists f; split => //; split => //.
split =>//; apply: surjective_pr4 => //;apply: extensionality.
fct_tac.
rewrite eq1 pe; fprops.
move: eq1 => [x xsr' rgx].
constructor 3; ex_tac; apply: orderIS.
move: (@sub_segment r' x) => p1.
move: (iorder_osr pb p1) => [qa qb].
exists (restriction1 f (source f)); split => //.
hnf; rewrite qb /restriction1; aw; split => //.
by apply: restriction1_fb.
by rewrite -rgx - image_by_fun_source.
hnf; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V pc ssf ax) (restriction1_V pc ssf bx); split.
move/(pf _ _ ax bx) => e1; apply/iorder_gleP =>//; rewrite -rgx; Wtac.
by move/iorder_gle1 => /(pf _ _ ax bx).
case : (well_ordered_segment wor fp1) => eq1.
constructor 1;apply: orderIS; exists f; split => //.
split => //;split =>//; apply: surjective_pr4 => //;apply: extensionality.
fct_tac.
rewrite eq1 pe; fprops.
move: eq1 => [x xsr rgx].
constructor 2;ex_tac; apply: orderIS.
move: (@sub_segment r x) => p1.
move: (iorder_osr pb p1) => [qa qb].
exists (restriction1 f (source f)); split => //.
rewrite qb /restriction1; split; aw; first by apply: restriction1_fb => //.
by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
hnf; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V pc ssf ax) (restriction1_V pc ssf bx); split.
move/(pf _ _ ax bx) => e1; apply/iorder_gleP =>//; rewrite -rgx; Wtac.
by move/iorder_gle1 => /(pf _ _ ax bx).
Qed.
Lemma isomorphism_worder3 r r': worder r -> worder r' ->
(exists f, segmentp r' (range (graph f)) /\ order_morphism f r r')
\/ (exists2 x, inc x (substrate r) & (induced_order r (segment r x)) \Is r').
Proof.
move => wor wor'.
case: (isomorphism_worder wor wor').
by move => [f [fa _ ]]; left; exists f.
move=> [f [[fa fb] _ ]].
move: (order_morphism_fi fb) => injf.
move: fb => [or' or [ff pd pe] pf].
case : (well_ordered_segment wor fa) => eq1.
left; exists (inverse_fun f).
have bf: bijection f.
by split => //; apply: (surjective_pr4 ff); rewrite pe.
rewrite {1} /inverse_fun corresp_g (igraph_range (function_sgraph ff)).
rewrite(f_domain_graph ff) pd; split; first by apply: substrate_segment.
have fif:= (bijective_inv_f bf).
have sfi: source f = target (inverse_fun f) by aw.
have tfi: target f = source (inverse_fun f) by aw.
split => //; [ by split; aw | move => x y; aw => xtf ytf ].
rewrite - {1} (inverse_V bf xtf) - {1} (inverse_V bf ytf).
apply: iff_sym;apply: pf; rewrite sfi; Wtac; aw.
move: eq1 => [x xsr rgx]; right;ex_tac; apply: orderIS.
move: (@sub_segment r x) => p1.
move: (iorder_osr or p1) => [qa qb].
exists (restriction1 f (source f)); split => //.
rewrite qb /restriction1; split; aw;first by apply: restriction1_fb => //.
by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
hnf; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V ff ssf ax) (restriction1_V ff ssf bx); split.
move/(pf _ _ ax bx) => e1; apply/iorder_gleP =>//; rewrite -rgx; Wtac.
by move/iorder_gle1 => /(pf _ _ ax bx).
Qed.
(** ** EIII-2-6 Lexicographic Products *)
(** Given a family of orders [g] and an ordering [r] on the index, we compare
two elements [x] and [x'] of the product by comparing [x(i)] and [x'(i)]
where [i] is the least index where the quantities differ *)
Definition order_prod_r r g :=
fun x x' =>
forall j, least (induced_order r (Zo (domain g)
(fun i => Vg x i <> Vg x' i))) j -> glt (Vg g j) (Vg x j)(Vg x' j).
Definition orprod_ax r g:=
[/\ worder r, substrate r = domain g & order_fam g].
Definition order_prod r g :=
graph_on (order_prod_r r g)(prod_of_substrates g).
(** Alternate formulation without [least_element] *)
Lemma orprod_gle1P r g:
orprod_ax r g -> forall x x',
(related (order_prod r g) x x' <->
[/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) &
forall j, least (induced_order r (Zo (domain g)
(fun i => Vg x i <> Vg x' i))) j -> glt (Vg g j) (Vg x j)(Vg x' j)]).
Proof. move=> ax x x';apply/graph_on_P1. Qed.
Lemma orprod_gleP r g : orprod_ax r g -> forall x x',
(gle (order_prod r g) x x' <->
[/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) &
(x= x' \/ exists j, [/\ inc j (substrate r),
glt (Vg g j) (Vg x j) (Vg x' j) &
forall i, glt r i j -> Vg x i = Vg x' i])]).
Proof.
move=> la x x'.
move: (la) => [wor sr alo]; move: (proj1 wor) => or.
have He: domain (fam_of_substrates g) = domain g.
by rewrite /fam_of_substrates; bw.
have Hf: fgraph(fam_of_substrates g) by rewrite /fam_of_substrates; fprops.
split.
move/(orprod_gle1P la) => [xp x'p aux]; split => //.
set (s := (Zo (domain g) (fun i => Vg x i <> Vg x' i))) in aux.
have ssr: sub s (substrate r) by rewrite sr; apply: Zo_S.
case: (emptyset_dichot s)=> nse.
left; apply: (setXb_exten xp x'p).
move=> i idf; ex_middle h; empty_tac1 i.
by rewrite /s; apply: Zo_i; move: idf; rewrite /fam_of_substrates; bw.
have [j jle] := (proj2 wor _ ssr nse).
have jp :=(aux _ jle).
move: jle => []; aw;move=> js jmin.
have jsr: inc j (substrate r) by apply: ssr.
right; exists j; split => //; move=> i ij; ex_middle v.
have iis : (inc i s) by rewrite /s; apply: Zo_i =>//;rewrite - sr;order_tac.
move: (iorder_gle1 (jmin _ iis)) => aux'; order_tac.
move => [xp x'p aux]; apply /(orprod_gle1P la);split => //.
set s := (Zo (domain g) (fun i => Vg x i <> Vg x' i)).
have ssr: (sub s (substrate r)) by rewrite sr; apply: Zo_S.
move=> j []; aw; move => js jmin.
move /Zo_P: js =>[jdg Vj].
case: aux => haux; first by rewrite haux in Vj.
have [i [isr lti aeq]] := haux.
have iis: inc i s by move:lti => [_ ok];apply: Zo_i =>//; ue.
have ij := (iorder_gle1 (jmin _ iis)).
case: (equal_or_not j i) => ji; first by ue.
have ltji: glt r j i by split.
by case: Vj; apply: aeq.
Qed.
Lemma orprod_osr r g:
orprod_ax r g -> order_on (order_prod r g) (prod_of_substrates g).
Proof.
move => ax; move: (ax)=> [wor sr ao].
have osr: substrate (order_prod r g) = prod_of_substrates g.
rewrite /order_prod graph_on_sr //.
move=> x _ j [js _]; move: js; aw; fprops; last by rewrite sr; apply: Zo_S.
by move /Zo_hi; case.
split => //.
have tor: total_order r by apply: worder_total.
split.
+ by apply: graph_on_graph.
+ by hnf; rewrite osr => y ya; apply/(orprod_gleP ax); split => //; left.
+ move => v u w ha.
move/(orprod_gleP ax): (ha) => [ux _]; case; first by move ->.
move => [j1 [j1sr hu1 hu2]].
move/(orprod_gleP ax) => [_ wx]; case;first by move <-.
move => [j2 [j2sr hv1 hv2]]; apply/(orprod_gleP ax); split => //; right.
case (equal_or_not j1 j2) => j12.
exists j1; rewrite - j12 in hv1 hv2; split => //.
rewrite sr in j1sr; exact:(lt_leq_trans (ao j1 j1sr) hu1 (proj1 hv1)).
by move => i ha1; rewrite (hu2 _ ha1) (hv2 _ ha1).
case:(proj2 tor _ _ j1sr j2sr) => h.
exists j1; split => //; first by rewrite - (hv2 _ (conj h j12)).
by move => i ia;rewrite (hu2 _ ia) (hv2 _ (lt_leq_trans (proj1 wor) ia h)).
exists j2; split => //; first by rewrite (hu2 _ (conj h (nesym j12))).
by move => i ia; rewrite - (hv2 _ ia) (hu2 _ (lt_leq_trans (proj1 wor) ia h)).
move => u v.
move/(orprod_gleP ax) => [_ _]; case => // [[j1 [j1sr hu1 hu2]]].
move/(orprod_gleP ax) => [_ _]; case => // [[j2 [j2sr hv1 hv2]]].
case: (equal_or_not j1 j2) => sj.
move: hv1 => []; rewrite - sj => hv11; rewrite sr in j1sr.
by rewrite(order_antisymmetry (ao j1 j1sr) (proj1 hu1) hv11).
case:(proj2 tor _ _ j1sr j2sr) => h.
by move: (hv2 _ (conj h sj)) (proj2 hu1) => ->.
by move:(hu2 _ (conj h (nesym sj))) (proj2 hv1) => ->.
Qed.
Lemma orprod_sr r g:
orprod_ax r g -> substrate(order_prod r g) = prod_of_substrates g.
Proof. move => h;exact: (proj2 (orprod_osr h)). Qed.
Lemma orprod_or r g:
orprod_ax r g -> order (order_prod r g).
Proof. move => h;exact: (proj1 (orprod_osr h)). Qed.
(** A product of total orders is total *)
Lemma orprod_total r g:
orprod_ax r g ->
(allf g total_order) ->
total_order (order_prod r g).
Proof.
move=> la alt.
have [ol sl] := (orprod_osr la).
have [[or wor] sr ao] := la.
split=>//; rewrite sl; move=> x y xsr ysr.
have fgf:fgraph (fam_of_substrates g) by rewrite/fam_of_substrates; fprops.
set s:=(Zo (substrate r) (fun i => Vg x i <> Vg y i)).
case: (emptyset_dichot s) => nse.
suff xy: x = y by left; rewrite xy; order_tac; rewrite sl.
apply: (setXb_exten xsr ysr).
move=> i idg; ex_middle u;empty_tac1 i.
by rewrite/s; apply: Zo_i; move: idg; rewrite/fam_of_substrates; bw; ue.
have ssr: sub s (substrate r) by rewrite/s; apply: Zo_S.
have [j jle] := (wor _ ssr nse).
move: (jle)=> [];rewrite iorder_sr // => js jp.
have jdg: inc j (domain g) by rewrite - sr; apply: ssr.
have [orj torj] := (alt _ jdg).
have px: (inc (Vg x j) (substrate (Vg g j))) by apply:prod_of_substrates_p.
have py: (inc (Vg y j) (substrate (Vg g j))) by apply:prod_of_substrates_p.
move:ysr; rewrite /prod_of_substrates/fam_of_substrates; aw.
have [ois sir] :=(iorder_osr or ssr).
move: js => /Zo_hi h h'.
case: (torj _ _ px py) => leaux.
left; apply /(orprod_gle1P la); rewrite - sr; split => // k kl.
rewrite - (unique_least ois jle kl); split =>//.
right; apply /(orprod_gle1P la); split => //.
have <-: s=(Zo (domain g) (fun i => Vg y i <> Vg x i)).
rewrite /s sr; set_extens t; move/Zo_P => [pa pb]; apply: Zo_i; fprops.
move => k kl.
by rewrite - (unique_least ois jle kl); split =>//; apply /nesym.
Qed.
(** Disjoint union of families of substrates *)
Definition sum_of_substrates g := disjointU (fam_of_substrates g).
Lemma du_index_pr1 g x: inc x (sum_of_substrates g) ->
[/\ inc (Q x) (domain g), inc (P x) (substrate (Vg g (Q x))) & pairp x].
Proof.
move=> xdu; move :(disjointU_hi xdu) => [].
by rewrite fos_d => h; bw => h1; split.
Qed.
Lemma disjoint_union_pi1 g x y:
inc y (domain g) -> inc x (substrate (Vg g y)) ->
inc (J x y) (sum_of_substrates g).
Proof. move=> ydg xsv; apply: disjointU_pi; bw. Qed.
Lemma canonical2_substrate r r':
fam_of_substrates (variantLc r r') = variantLc (substrate r) (substrate r').
Proof.
rewrite /fam_of_substrates /variantLc.
apply: fgraph_exten; fprops; bw.
move=> x xtp; try_lvariant xtp; fprops.
Qed.
(** ordinal sum of a family of orders g indexed by the substrate of r *)
Definition orsum_ax r g:=
[/\ order r, substrate r = domain g & order_fam g].
Definition order_sum_r r g x x' :=
(glt r (Q x) (Q x') \/ (Q x = Q x' /\ gle (Vg g (Q x)) (P x) (P x'))).
Definition order_sum r g :=
graph_on (order_sum_r r g) (sum_of_substrates g).
Section OrderSumBasic.
Variables r g: Set.
Hypothesis osa: orsum_ax r g.
Lemma orsum_gleP x x': gle (order_sum r g) x x' <->
[/\ inc x (sum_of_substrates g), inc x' (sum_of_substrates g) &
order_sum_r r g x x'].
Proof. apply: graph_on_P1. Qed.
Lemma orsum_gle1 x x':
gle (order_sum r g) x x' ->
(glt r (Q x) (Q x') \/ (Q x = Q x' /\ gle (Vg g (Q x)) (P x) (P x'))).
Proof. by move /orsum_gleP => [_ _]. Qed.
Lemma orsum_gle2 a b a' b':
gle (order_sum r g) (J a b)(J a' b') ->
(glt r b b' \/ (b = b' /\ gle (Vg g b) a a')).
Proof. move => h2; move:(orsum_gle1 h2); aw. Qed.
Lemma orsum_gle_id x x':
gle (order_sum r g) x x' -> gle r (Q x) (Q x').
Proof.
move /orsum_gleP => [xs _ ] [] [] => // <- _.
move: (du_index_pr1 xs)=> [qd _ _].
move: osa => [or srdg _]; order_tac; ue.
Qed.
Lemma orsum_or: order (order_sum r g).
Proof.
move: osa=> [or sr alo].
rewrite /order_sum; set s := _ r g; set x:= _ g.
have ->: (graph_on s x = graph_on (fun a b => [/\ inc a x, inc b x & s a b]) x).
by apply : Zo_exten1 => t /setX_P [_ pa pb]; split => //;move => [_ _].
apply: order_from_rel; split => //; rewrite /s/order_sum_r.
- move=> u v w [ux vx suv] [_ xw suw];split => //.
case: suv; case: suw.
+ by left; order_tac.
+ by move=> [sq leq]; rewrite sq; left.
+ by move=> h [sq leq]; rewrite sq;left.
+ move=> [sq1 le1][sq2 le2]; right; split; first by ue.
move: (du_index_pr1 ux) => [qdg _ _].
by rewrite - sq2 in le1; move: (alo _ qdg)=> ov; order_tac.
- move=> u v [ux vx suv] [_ _ svu].
have [qudg puv pu] := (du_index_pr1 ux).
have [qvdg pvv pv] := (du_index_pr1 vx).
case: suv; case: svu.
+ move=> lt1 lt2; order_tac.
+ by move => [eq _] [_ lt1]; case: lt1.
+ by move => [_ lt1] [eq _]; case: lt1.
+ move=> [eq le1][_ le2]; rewrite eq in le1; move: (alo _ qudg) => ou.
apply: pair_exten =>//;order_tac.
- move=> u v [ux vx suv].
have [qudg puv pu] := (du_index_pr1 ux).
have [qvdg pvv pv] := (du_index_pr1 vx).
by split; split => //;right; split => //;
[move: (alo _ qudg) | move: (alo _ qvdg) ] => ou; order_tac.
Qed.
Lemma orsum_sr: substrate (order_sum r g) = sum_of_substrates g.
Proof.
rewrite /order_sum graph_on_sr // => a asg.
have [qudg puv pu] := (du_index_pr1 asg).
by right; split => //;move: osa =>[_ _ alo];move: (alo _ qudg) => ou; order_tac.
Qed.
Lemma orsum_osr: order_on (order_sum r g) (sum_of_substrates g).
Proof. by split; [apply: orsum_or | rewrite orsum_sr]. Qed.
End OrderSumBasic.
Hint Resolve orsum_or orprod_or: fprops.
Hint Rewrite orsum_sr orprod_sr : bw.
Definition order_prod2 r r' :=
order_prod canonical_doubleton_order (variantLc r' r).
Definition order_sum2 r r' :=
order_sum canonical_doubleton_order (variantLc r r').
Lemma order_sp_axioms r r':
order r -> order r' -> order_fam (variantLc r r').
Proof.
move => or or';hnf; bw;move=> i itp; try_lvariant itp.
Qed.
Hint Resolve order_sp_axioms: fprops.
Section OrderSum2Basic.
Variables r r': Set.
Hypotheses (or: order r) (or': order r').
Lemma orsum2_osr:
order_on (order_sum2 r r') (canonical_du2 (substrate r) (substrate r')).
Proof.
move: cdo_wor => [[ord _ ] sr].
have aw: orsum_ax canonical_doubleton_order (variantLc r r').
by split => //; bw; fprops.
split; first by apply: orsum_or.
rewrite orsum_sr // /canonical_du2 /order_sum2 /sum_of_substrates.
rewrite canonical2_substrate //.
Qed.
Lemma orprod2_osr:
order_on (order_prod2 r r')(product2 (substrate r') (substrate r)).
Proof.
have [wor sr] := cdo_wor.
have aux: orprod_ax canonical_doubleton_order (variantLc r' r).
by split => //; bw; fprops.
split; first by apply: orprod_or.
rewrite /order_prod2 orprod_sr // /prod_of_substrates canonical2_substrate //.
Qed.
Lemma orsum2_or: order (order_sum2 r r').
Proof. exact: (proj1 orsum2_osr). Qed.
Lemma orsum2_sr:
substrate (order_sum2 r r') = canonical_du2 (substrate r) (substrate r').
Proof. exact: (proj2 orsum2_osr). Qed.
Lemma orprod2_or: order (order_prod2 r r').
Proof. exact: (proj1 orprod2_osr). Qed.
Lemma orprod2_sr:
substrate(order_prod2 r r') = product2 (substrate r') (substrate r).
Proof. exact: (proj2 orprod2_osr). Qed.
Lemma orsum2_gleP x x':
gle (order_sum2 r r') x x' <->
[/\ inc x (canonical_du2 (substrate r) (substrate r')),
inc x' (canonical_du2 (substrate r) (substrate r')) &
[\/ [/\ Q x = C0, Q x' = C0 & gle r (P x) (P x')],
[/\ Q x <> C0, Q x' <> C0 & gle r' (P x) (P x')] |
(Q x = C0 /\ Q x' <> C0)]].
Proof.
have Ha: C1 <> C0 by fprops.
set S1:= (canonical_du2 (substrate r) (substrate r')).
have S1p: S1 = (sum_of_substrates (variantLc r r')).
by rewrite /sum_of_substrates canonical2_substrate.
split.
move /orsum_gleP; rewrite - S1p.
move=> [xs xns' osr]; split => //; move: osr => [] [].
move /cdo_gleP => aux nsQ;case: aux.
by move=> [e1 e2]; rewrite e1 e2 in nsQ;case: nsQ.
case; first by move=> e1 e2; rewrite e1 e2 in nsQ; case: nsQ.
move=> [e1 e2]; constructor 3; rewrite e2; split => //.
move=> <-.
case: (candu2_pr2 xs) => ->; bw; [constructor 1| constructor 2]; split => //.
move=> [xs1 x's1 etc]; apply/orsum_gleP; split => //; try ue.
case: etc.
move=> [qxa qx'a lrxx']; right; rewrite qxa qx'a; bw;split => //.
move=> [qxa qx'a lrxx']; right.
have ->: (Q x' = C1) by case: (candu2_pr2 x's1) => //.
have ->: (Q x = C1) by case: (candu2_pr2 xs1) => //.
bw; split => //.
move=> [qxa qx'a]; left; rewrite qxa.
have ->: Q x' = C1 by case: (candu2_pr2 x's1) => //.
apply: cdo_glt1.
Qed.
Lemma orsum2_gle_spec x x':
inc x (substrate r) -> inc x' (substrate r') ->
glt (order_sum2 r r') (J x C0) (J x' C1).
Proof.
move=> xsr xsr'; split; last by move => h; move: (pr2_def h); fprops.
apply /orsum2_gleP; split; first by apply: candu2_pra.
by apply: candu2_prb.
constructor 3; aw; split; fprops.
Qed.
Lemma orprod2_gleP a b:
gle (order_prod2 r r') a b <->
[/\ inc a (product2 (substrate r') (substrate r)),
inc b (product2 (substrate r') (substrate r))&
( (Vg a C0 = Vg b C0 /\ gle r (Vg a C1) (Vg b C1))
\/ (glt r' (Vg a C0)(Vg b C0)))].
Proof.
have [wor sr] := cdo_wor.
have la: orprod_ax canonical_doubleton_order (variantLc r' r).
by split => //; bw; fprops.
apply: (iff_trans (orprod_gleP la a b)).
have ->: prod_of_substrates (variantLc r' r) =
(product2 (substrate r') (substrate r)).
rewrite - orprod2_sr // /order_prod2; bw.
rewrite (proj2 cdo_wor).
split; move => [ap2 bp2 h];split => //.
case: h.
move => <-; left;split => //; order_tac.
by move: ap2 => / setX2_P [_ _ _].
move=> [j [ /C2_P [] ->]]; bw;first by move => h _; right.
move=> p1 p2.
by move: (p2 _ cdo_glt1) => p4; move: p1 => [p1 _]; left.
case: h.
move=> [p1 p2]; case: (equal_or_not (Vg a C1) (Vg b C1)).
move:ap2 bp2 => /setX2_P [fga da Vaa VBa].
move => /setX2_P [fgb db Vab VBb].
move=> VV; left; apply: fgraph_exten =>//; first by ue.
rewrite da; move=> ix xda;try_lvariant xda.
move => nVV; right; exists C1; split => //; fprops; bw; first by split.
move=> i [] /cdo_gleP p3 p4; case: p3; [ | by case | by move=> [-> _]].
by move=> [r1 r2]; rewrite -r2 in r1.
move => pa; right; exists C0;bw;split => //; fprops.
move=> i [] /cdo_gleP []; case => // -> -> //.
Qed.
End OrderSum2Basic.
Hint Resolve orsum2_or orprod2_or: fprops.
Hint Rewrite orsum2_sr orprod2_sr : bw.
Lemma orprod2_totalorder r r':
total_order r -> total_order r' -> total_order (order_prod2 r r').
Proof.
move: cdo_wor => [ha hb].
move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orprod_total.
split => //; [ bw | hnf; bw => x xi; try_lvariant xi].
hnf;bw => x xi; try_lvariant xi.
Qed.
Lemma order_prod_pr r r': order r -> order r' ->
(order_prod2 r r') \Is (order_sum r' (cst_graph (substrate r') r)).
Proof.
move => or or'.
have oa: (orsum_ax r' (cst_graph (substrate r') r)).
hnf; split => //; bw; hnf; bw;move=> i isr; bw.
set fo:=order_sum r' (cst_graph (substrate r') r).
have odf: order fo by rewrite /fo; fprops.
move: (orsum_sr oa) => s1.
move: (orprod2_or or odf).
move: (orprod2_sr or or').
set io := order_prod2 r r'; move => s2 o2.
pose f x := J (Vg x C1) (Vg x C0).
have ta: (lf_axiom f (substrate io) (substrate fo)).
move=> t; rewrite /fo s1 s2; move /setX2_P => [fgt dt va vb].
apply: disjointU_pi; bw.
have bf: bijection (Lf f (substrate io) (substrate fo)).
apply: lf_bijective =>//.
move=> u v;rewrite s2 /f; move=> ud vd eq.
move: (pr2_def eq)(pr1_def eq) => p1 p2.
apply: (setXf_exten ud vd); move=> i itp; try_lvariant itp.
rewrite s1 /fam_of_substrates /cst_graph.
move=> y ys; move:(du_index_pr1 ys); rewrite Lg_domain.
move=> [Qsr]; bw; move=> Psr py.
exists (variantLc (Q y) (P y)).
rewrite s2; apply /setX2_P;split => //; bw; fprops.
symmetry;rewrite /f; bw; aw.
exists (Lf f (substrate io) (substrate fo));hnf; split; aw.
rewrite /io; fprops.
hnf; split; aw.
hnf; aw; move=> x y xs ys; aw.
move : (ta _ xs) (ta _ ys) => qa qb.
have p1: inc (Vg x C0) (substrate r').
by move: xs; rewrite s2; move /setX2_P => [_ _ ].
apply (iff_trans (orprod2_gleP or or' _ _)); rewrite - s2.
symmetry; apply (iff_trans (orsum_gleP _ _ _ _)).
have ->: sum_of_substrates (cst_graph (substrate r') r) = substrate fo by aw.
split; move => [_ _ xx]; split => //; move: xx;
rewrite /f /order_sum_r !pr1_pair !pr2_pair; bw; case; fprops.
Qed.
Lemma orsum_total r g:
orsum_ax r g -> total_order r ->
(forall i, inc i (domain g) -> total_order (Vg g i)) ->
total_order (order_sum r g).
Proof.
move=> oa [_ tor] alt; rewrite /total_order.
move: (oa) => [or sr alo]; bw.
rewrite sr in tor.
split =>//; first by fprops.
move=> x y xsr ysr; move: (du_index_pr1 xsr) (du_index_pr1 ysr).
move=> [Qx Px px][Qy Py py].
case: (equal_or_not (Q x) (Q y)).
move =>h; move: (alt _ Qx) => [lor ltor]; rewrite -h in Py.
case: (ltor _ _ Px Py) => h1;aw ; [left | right];
apply /orsum_gleP;split => //; right; split => //; ue.
move=> nQ; case: (tor _ _ Qx Qy) => h; [left | right];
apply /orsum_gleP;split => //; left;split; fprops.
Qed.
Lemma orsum2_totalorder r r':
total_order r -> total_order r' -> total_order (order_sum2 r r').
Proof.
have [ha hb] := cdo_wor.
have hc:= (worder_total ha).
have hd := proj1 ha.
move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orsum_total => //.
hnf; split => //; [ bw | hnf; bw => x xi; try_lvariant xi].
hnf;bw => x xi; try_lvariant xi.
Qed.
Lemma orsum_wor r g:
worder_on r (domain g) -> worder_fam g ->
worder (order_sum r g).
Proof.
move=> [wor sr] alw; move: (proj1 wor) => or.
have oa: orsum_ax r g by split => // i ie; exact (proj1 (alw _ ie)).
apply:(worder_prop_rev (orsum_or oa)); bw => x xs [x0 x0x].
set A := fun_image x Q.
have Asr: (sub A (substrate r)).
move=> t /funI_P [z zx ->].
rewrite sr;exact (proj31 (du_index_pr1 (xs _ zx))).
have neA: nonempty A by exists (Q x0); apply /funI_P; ex_tac.
move: (worder_prop wor Asr neA)=> [a aA ale].
set B:= Zo x (fun z => Q z = a).
set C := fun_image B P.
move: (Asr _ aA); rewrite sr => adg.
have Cs: (sub C (substrate (Vg g a))).
move=> t /funI_P [z zB ->].
move: zB => /Zo_P [zx] <-; exact (proj32 (du_index_pr1 (xs _ zx))).
have neC: nonempty C.
move: aA => /funI_P [z zx qz].
by exists (P z); apply /funI_P;exists z => //; apply: Zo_i.
move: (worder_prop (alw _ adg) Cs neC)=> [b bC leB].
have Jx: inc (J b a) x.
move: bC => /funI_P [z /Zo_P [zx <-] ->].
by rewrite (proj33 (du_index_pr1 (xs _ zx))).
have ors: order (order_sum r g) by fprops.
ex_tac => c cx.
move: (du_index_pr1 (xs _ cx))=> [Qc Pc pc].
apply /orsum_gleP;split; fprops.
hnf; rewrite pr1_pair pr2_pair.
have QcA: (inc (Q c) A) by apply /funI_P; ex_tac.
move: (ale _ QcA) => leac.
case: (equal_or_not a (Q c)).
move=> aQc; right;split => //.
have Pcb: (inc (P c) C) by apply/funI_P; exists c => //; apply: Zo_i.
exact: (leB _ Pcb).
by move => nac; left.
Qed.
End Worder.
Export Worder.