Library sset6
Theory of Sets EIII-2 Well ordered sets
Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm).Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset5.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Worder.
Definition worder r :=
order r /\ forall x, sub x (substrate r) -> nonempty x ->
exists y, least (induced_order r x) y.
Definition worder_r (r: relation) :=
order_r r /\ forall x, (forall a, inc a x -> r a a) -> nonempty x ->
exists y, least (graph_on r x) y.
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 -> (forall a, inc a x -> r a a) ->
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; move=> s sx nes.
have rs: (forall a, inc a s -> r a a) 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.
move=> y;rewrite (iorder_sr gor ss) => ys; aw.
move: (lea _ ys) => /graph_on_P1 [pa pb pc]; apply/iorder_gleP => //.
by apply/graph_on_P1;split => //; apply: sx.
Qed.
The empty set is well-ordered
Lemma set0_or: order emptyset.
Proof. rewrite - setI_0; apply: setIrel_or => t;case; case. 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.
move => aux; apply /domain_set0_P; apply /set0_P => y h.
by empty_tac1 y; apply /setU2_P; left.
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: (G = diagonal (singleton x)).
set_extens t; first by move /set1_P => ->; apply/diagonal_pi_P;fprops.
move/diagonal_i_P => [pa] /set1_P pb pc; apply/set1_P.
by rewrite - pa -pc pb.
move:(diagonal_osr (singleton x)) => [pa pb].
have oE: (order G) by rewrite Ei.
have sE: (substrate G = singleton x) by rewrite Ei pb.
split =>//; split =>//.
move=> y yE [z zy]; exists z; red; aw;split => //.
move=> t ty; apply/iorder_gleP => //.
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.
move: (set1_wor x) => [[o1 _] s1].
move: (set1_wor y) => [[o2 _] s2].
have ta: lf_axiom (fun _ : Set => y) (singleton x) (singleton y).
by move=> t;fprops.
exists (Lf (fun _ => y) (singleton x) (singleton y)).
red; split => //.
rewrite s1 s2; split; aw => //.
apply lf_bijective => //.
by move=> u v /set1_P -> /set1_P ->.
move=> t /set1_P ->; exists x;fprops.
move=> a b; rewrite lf_source => 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_is1 r:
order r -> singletonp (substrate r) ->
exists x, r = singleton (J x x).
Proof.
move=> or [u sxsu]; exists u; set_extens v; aw.
move=> vx; move: ((order_sgraph or) _ vx) => p.
rewrite - p in vx |- *.
move: (arg1_sr vx) (arg2_sr vx);rewrite sxsu.
by move /set1_P => -> /set1_P ->; apply/set1_P.
move/set1_P => ->; order_tac;rewrite sxsu; fprops.
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].
suff: r = singleton (J e e) by move => ->; exact (proj1(set1_wor e)).
apply: set1_pr; first by order_tac; rewrite sr; fprops.
move=> t tr; rewrite - (order_sgraph or tr).
move: (pr1_sr tr) (pr2_sr tr); rewrite sr.
by move => /set1_P -> /set1_P ->.
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.
case/set3_P; move => h;rewrite(pr1_def h)(pr2_def h); in_TP4.
case; move=> [-> ->]; apply /set3_P; in_TP4.
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: substr_i; apply /cdo_gleP; in_TP4.
have oc: (order canonical_doubleton_order).
red; 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; [split =>// x xt nex | exact].
rewrite /least (proj2 (iorder_osr oc xt)).
case: (inc_or_not C0 x)=> hyp.
ex_tac => y yx; apply iorder_gleP => //; apply /cdo_gleP.
move: (xt _ yx); rewrite subs; case /C2_P => ye; in_TP4.
move: nex=> [y yx]; ex_tac.
have p: forall t, inc t x -> t = C1.
move=> t tx; move: (xt _ tx); rewrite subs; case/C2_P => //.
by move => ta;rewrite ta in tx; case: hyp.
move => t tx; apply iorder_gleP => //; apply /cdo_gleP.
by 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=> [or wo]; split=>//.
move=> x y xs ys.
set (u:=doubleton x y).
have xu: (inc x u) by rewrite /u; fprops.
have yu: (inc y u) by rewrite /u; fprops.
have ur: sub u (substrate r) by rewrite /u; apply: sub_set2.
have si: substrate (induced_order r u) = u by aw.
have neu: nonempty u by ex_tac.
move: (wo _ ur neu)=> [z []]; rewrite si => zu zle.
have aux: forall t, inc t u -> gle r z t.
by move => t tu; move:(iorder_gle1 (zle _ tu)).
move: (aux _ xu)(aux _ 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.
set (u:=doubleton x y).
have xu: (inc x u) by rewrite /u; fprops.
have yu: (inc y u) by rewrite /u; fprops.
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=> [or wo] As [t tA].
red; rewrite /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 =>//; move: tA=> [tA _].
by move: (wo _ 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) ->
exists y, least r y.
Proof.
move=> [or wo] ne.
move: (wo _ (@sub_refl (substrate r)) ne)=> [x lex].
rewrite iorder_substrate // in lex.
by 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=> [or wo] nas.
move: (order_with_greatest_pr or nas) => [[on sn] rd gna].
split=>// 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; move /setU1_P.
case=>// => zr; empty_tac1 z; apply:setI2_i => //.
have ax: inc a x by rewrite xa; fprops.
exists a; red; aw;split => //.
rewrite xa => t /set1_P ->; apply /iorder_gleP; fprops.
by order_tac; apply: xs.
have sys:sub y (substrate r) by apply: subsetI2r.
move: (wo _ sys ye)=> [z []]; aw=> zy lez.
move: (setI2_1 zy) => zx.
exists z; split; aw => t tx; apply/iorder_gleP => //.
move: (xs _ tx); rewrite sn; case /setU1_P => p.
have ty: inc t y by rewrite /y; apply: setI2_i.
by move: (iorder_gle1 (lez _ ty)) => pa; apply:setU2_1.
rewrite p; move: gna=> [_]; apply; ue.
Qed.
Every set can be well-ordered;
We assume here inc (rep a) a for any non-empty subset of E
Definition worder_of E :=
let p:= fun a => a -s1 (rep a) in
let chain:= fun F => [/\ 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)] in
let om := intersection (Zo (powerset (powerset E)) chain) in
let d:= fun p => intersection (Zo om (fun x => sub p x)) in
let R := fun x => d (singleton x) in
graph_on (fun x y => (sub (R y) (R x))) E.
Lemma Zermelo_ter E: worder (worder_of E) /\ substrate (worder_of E) = E.
Proof.
rewrite /worder_of.
set p:= fun a => a -s1 (rep a).
set chain:= fun F => [/\ _,_, _ & _ ].
set om := intersection (Zo (powerset (powerset E)) chain).
set d:= fun p => intersection (Zo om (fun x => sub p x)).
set R := fun x => d (singleton x).
set res:= graph_on (fun x y => (sub (R y) (R x))) E.
have pe: p emptyset = emptyset by apply /set0_P => x /setC_P [/in_set0 xe _].
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;apply: sub_trans AE; apply: sp.
move=> A AP [x xA]; move: (AP _ xA) => /setP_P xE; apply/setP_P.
move=> t ti; apply: xE; apply: (setI_hi ti xA).
have omv: om = intersection (Zo (powerset (powerset E)) chain) by done.
have co :chain om.
rewrite omv.
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: (yi)=> /Zo_hi [_ _ q _];apply: q;apply: (setI_hi Ai yi).
move=> A sAi neA; apply: (setI_i aux) => y yi.
move: (yi) => /Zo_hi [_ _ _]; apply => //.
by move=>t /sAi /setI_hi; apply.
move: (co)=> [sop Eo po io].
have cio: forall x, chain x -> sub om x.
move=> x xc; apply: setI_s1; apply: Zo_i =>//;apply /setP_P.
by move: xc => [].
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; red; 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))) => aux.
move: aux=> [x [xB xp]]; left; move=> t ti; apply: xp.
apply: (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: aux; 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)) => hyp.
move: hyp=> [y yA yx]; right; move => t ti.
apply: yx; apply: (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: hyp ;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 q, sub q E -> inc (d q) om.
by move=> q qE; rewrite /d; apply: io;[ apply:Zo_S| exists E;apply: Zo_i].
have pdp: forall q, sub q E -> sub q (d q).
rewrite /d=> q qE t tq; apply: setI_i; first by exists E; apply: Zo_i.
by move => y /Zo_hi; apply.
have dpq: forall q r, inc r om -> sub q r -> sub q E-> sub (d q) r.
by rewrite /d=> q r0 rom qr qE; apply: setI_s1; apply: Zo_i.
have rdq: forall q, sub q E -> nonempty q -> inc (rep (d q)) q.
move=> q qE neq; case: (inc_or_not (rep (d q)) q)=>// ni.
have aux: (sub q (p (d q))).
move=> t tq;apply /setC1_P; split; [ by apply: (pdp _ qE)|].
move => h;case: ni; ue.
move: (dpq _ _ (po _ (dpo _ qE)) aux qE).
rewrite /p; case: (emptyset_dichot (d q)).
move=> dqe; rewrite dqe pe in aux.
by move: neq=> [t tq]; case: (@in_set0 t); apply: aux.
move=> ned; move: (rep_i ned) => rd dc; move: (dc _ rd).
by move /setC1_P => [_].
have qdp: forall q r, inc r om -> sub q r -> inc (rep r) q -> r = d q.
move => q r rom qr rq.
have spE: sub q E by apply: (sub_trans qr); apply /setP_P; apply: sop.
move: (dpq _ _ rom qr spE) => sdqr.
case: (st _ _ (dpo _ spE) (po _ rom)) => ch.
by case /setC1_P: (ch _ ( (pdp _ spE) _ rq)) => _.
apply: extensionality =>// t tr.
case: (equal_or_not t (rep r)); first by move=> ->; apply: (pdp _ spE).
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].
rewrite /R=> x xE.
have p1: sub (singleton x) E by apply: set1_sub.
have nesi: (nonempty (singleton x)) by fprops.
move: (rdq _ p1 nesi) => /set1_P => p3.
split; [ by apply: dpo | apply:(pdp _ p1); fprops | done].
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 q, inc q om -> nonempty q -> R (rep q) = q.
move=> a qom neq; rewrite /R; 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.
move: (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4).
move=> -> ->; fprops.
have -> : res = graph_on (fun x y => sub (R y) (R x)) E by done.
have or:order res.
rewrite /res; 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.
move => u ue; fprops.
have sr: substrate res = E.
rewrite /res graph_on_sr //; move => u ue; fprops.
split=>//;split=>//.
move=> x xsr nex; exists (rep (d x));red; rewrite -/res iorder_sr //.
rewrite sr in xsr.
move: (rdq _ xsr nex) => rdx; split => //.
move => a ax; apply/iorder_gleP => //; 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).
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.
move: (total_order_monotone_injective to sm)=> injf.
move: (total_order_monotone_injective to smg)=> injg {sm smg}.
move:sif sig=> [or or' [ff sr sr'] si] [_ _ [fg srg sr'g] sig] rr.
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:wo=> [_ wo]; move: (wo _ Asf eA)=> [x []]; aw => 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=> h'; move:(iorder_gle1 (xl _ h'))=> h''; 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 ne].
suff: inc z A by move=> h'; move:(iorder_gle1 (xl _ h'))=> h''; order_tac.
apply: Zo_i=>//.
by rewrite -WWw; clear ne; dneg xx; move: injg=> [_ p]; apply: p.
order_tac.
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) -> False.
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_P; case. 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.
move=> t /Zo_hi [ h _]; move: h;rewrite /induced_order => h.
by move: (setI2_2 h) => /setXp_P [].
Qed.
Lemma segment_inc r x y:
glt r y x -> inc y (segment r x).
Proof. move=> xy;apply /Zo_P; split=>//;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_P []. 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.
red; move: sis; rewrite /segmentp; aw.
move=> [s's hyp]; split.
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).
move=> 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.
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; split.
move: (worder_total wor) => tor.
have sys: (sub y (substrate r)) by apply: sub_setC.
move:wor=> [or wo]; move: (wo _ sys ney)=> [x []]; aw.
move=> 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) => //.
case /setC_P: xy => [_ bad].
by move: sr=> [_ h] xz; move: (h _ _ zs xz ).
ex_middle zis.
have zy: (inc z y) by apply/setC_P; split => // ;apply: (sub_segment zs).
move: (iorder_gle1 (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=> [x xsr p].
move: (worder_least wo sre)=> [a lea].
right; exists x; exists 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.
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.
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: total_order r ->
let E := substrate r in
let A := union (segmentss r) in
( (forall x, ~ (greatest r x)) -> A = E)
/\ (forall x, greatest r x -> A = E -s1 x).
Proof.
move=> tor E A.
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; rewrite Ap; move=> [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.
apply/Ap; exists x; split=>//; by 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 x y: total_order r ->
inc x (substrate r) -> inc y (substrate r) -> segment r x = segment r y ->
x = y.
Proof.
move=> tor 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.
move: (segment_monotone1 tor xsr ysr p1)=> p3.
move: (segment_monotone1 tor ysr xsr p2)=> p4.
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].
red; 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.
red; aw; move=> x y xsr ysr; aw; split.
move=> hyp; apply/sub_gleP;split => //; fprops.
by apply: segment_monotone.
move /sub_gleP=> [_ _ ss].
by apply: segment_monotone1=>//; apply: worder_total.
Qed.
Theorem segments_worder r: worder r ->
worder (sub_order (segments r)).
Proof.
move=> wor; move: (wor)=> [or worp];move: (worder_total wor)=> tor.
move: (sub_osr (segments r)) => [oi sr].
split=>//.
rewrite sr; move => x xsr nex.
set y := x \cap (segmentss r).
move: (xsr); rewrite -{1} sr => h.
rewrite /least (proj2 (iorder_osr oi h)); clear h.
case: (emptyset_dichot y) => hy.
have xs: x = singleton (substrate r).
apply: set1_pr1=>// z zx.
move: (xsr _ zx); case /setU1_P => //.
by move=> aux; empty_tac1 z; apply: setI2_i.
exists (substrate r); rewrite xs; split; fprops.
move=> z => /set1_P ->;apply /iorder_gleP; fprops; order_tac.
rewrite sr; apply: xsr; rewrite xs; fprops.
have ysr: (sub y (segmentss r)) by move => t ty; apply (setI2_2 ty).
have segp: (forall a, inc a y -> exists2 u,
inc u (substrate r) & a = segment r u).
by move=> a ay; move: (ysr _ ay) => /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].
suff : u = cf a by move => <-; split => //.
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: (worp _ zsr nez)=> [a []]; aw=> 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 /iorder_gleP; (try apply: xsr) => //.
move: (xsr _ bx) => pa.
apply /sub_gleP;split; fprops.
case /setU1_P: pa; last by move=>->; apply: sub_segment.
move=> h.
have biy: (inc b y) by apply: setI2_i.
have cbz: (inc (cf b) z) by apply /funI_P; ex_tac.
move: (iorder_gle1 (lea _ cbz)).
move: (cfp _ biy)=> [p1 p2]; rewrite {2} p2.
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 : Set => 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 red; rewrite su.
rewrite /related; move=> x y z p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
move: (alo _ cdg) => or; rewrite /G; red; union_tac; order_tac.
rewrite /related; move=> 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 move:(sub_graph_coarse_substrate ga); apply.
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: pairp x by move: or=>[gr _ _ _]; apply: gr.
have px: J (P x) (Q x) = x by aw.
have pxs: (inc (P x) (substrate r)) by substr_tac.
have pys: (inc (Q x) (substrate r)) by substr_tac.
rewrite sr in 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 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.
have ys: (inc y (substrate G)) by order_tac.
move: (setUf_hi yx) => [ u udg Jv].
case: (pc _ _ adg udg); move=> [p p']; first by apply: p; substr_tac.
apply: (p' _ _ xs Jv).
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 => //.
move: (setUf_hi yx)=> [b bdg Jv]; rewrite (Vag _ adg).
apply/iorder_gleP => //.
case:(pc _ _ adg bdg); move=> [p p']; first by apply: p; substr_tac.
apply: (p' _ _ xs Jv).
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.
split=>//; move=> 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: (pb _ adg)=>[oa wo].
move: (wo _ sx1s nx1)=> [z []]; aw => 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; red; aw; split=> //.
move=> t tx; apply/iorder_gleP => //.
move: (xsr _ tx); rewrite sh => tu; move: (setUf_hi tu)=> [b bdg bV].
have aux: inc t (substrate (Vg g a)) -> gle (unionb g) z t.
move=> hyp.
have tx1: inc t x1 by apply: setI2_i.
move:(iorder_gle1 (zle _ tx1)); rewrite Vag // => h.
by move:(iorder_gle1 h).
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
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 move: 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: woi=> []; rewrite sr1 => oi woi.
move: (woi _ scs necs).
move: (scs); rewrite - {1} sr1 => src1.
move=> [y []]; rewrite (proj2 (iorder_osr oi src1));move=> ycs hyp; clear woi.
move: (scs _ ycs)=> yssr.
have nys: ~ (inc y s).
move: ycs => / setC_P [_]; apply.
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: (iorder_gle1 (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 : Set, ~ 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:(iorder_gle1 (hyp _ zcs)) => /sub_gleP [_ _ yz].
move: uy; aw => uy; move: (yz _ uy).
rewrite zv=> aux; case: (not_in_segment aux).
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 move: wor=> [or _].
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.
rewrite /restriction_to_segment/restriction1; aw.
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.
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 _].
simpl.
set si := Lg s id.
set t:= unionf _ _.
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.
red;aw;split => //.
apply: function_pr; fprops.
apply: (@sub_trans (target (tdf i))); first by apply: f_range_graph.
rewrite /t => x xt; union_tac.
rewrite - f_domain_graph //.
by apply: slso.
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))).
rewrite /x; 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].
red; 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].
split=>//.
split.
split => //.
rewrite gf=> y; rewrite /t=> 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.
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; red; apply: not_in_segment.
set (h:= (restriction_to_segment r x g)).
move: (extension_fs (p h) (proj1 sug) nxsg sug) => sto.
have tos:(segment r x) +s1 x = tsx by rewrite /tsx segmentc_pr//.
red;rewrite sioc; split => //.
rewrite /extension; aw; ue.
move=> y ytsx.
have syx: (sub (segment r y) (segment r x)).
move: ytsx => /segmentcP; apply: segment_monotone =>//.
have fto: function (extension g x (p h)) by fct_tac.
have soto: source (extension g x (p h)) = tsx.
by rewrite/extension; aw; rewrite sog //.
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.
apply: f_equal.
apply: rts_extensionality =>//; aw; try ue.
rewrite soto p2; fprops.
red; 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 rewrite /transfinite_defined; apply choose_pr; exists x.
apply: (transfinite_unique wo tdt td).
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=> 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: forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(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.
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 [red _].
by apply:choose_pr.
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 = image_by_fun 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 = image_by_fun 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:
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.
have srr: sub (substrate r) (substrate r) by fprops.
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.
move => x xX.
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
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.
apply: Zo_i; first 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;apply:setI2_i => //;rewrite pb;apply:setXp_i;apply/segmentP =>//.
order_tac.
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].
have pv: J (P t) (Q t) = t by aw.
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 -pv eq; order_tac.
move=> neq; rewrite -pv in tr.
have: (inc (P t) (segment r (Q t))) by apply: segment_inc=>//; split.
rewrite ss -{3} pv => aux.
move: (inc_segment aux)=> [h _]; exact h.
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: (px _ zc) => h.
move: (iorder_gle1 h)=> xz; order_tac.
apply /segmentP.
case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz.
case: xc; move: svr=> [_ h]; apply: (h _ _ 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: (py _ zc) => h.
move: (iorder_gle1 h)=> yz; order_tac.
apply /segmentP.
case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz.
case: yc; move: svr'=> [_ h]; apply: (h _ _ zs yz).
have xy: x = y by rewrite - (pr _ xs) -(pr' _ ys) p1 p2.
case: xc.
rewrite /v /common_ordering_set; apply: Zo_i.
apply /setI2_i => //; ue.
rewrite p1 xy p2; split=>//.
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.
have: inc x (substrate owg) by order_tac.
rewrite se => /setU1_P;case =>//.
move: xa=>[_ nxa] xa; contradiction.
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: setI2_i => //;apply /setXp_i => //.
move: (arg1_sr yx); rewrite se => /setU1_P; case => //.
move=> ya; case: nyx.
move: (prop _ xsre); fold owg; rewrite -ya => p1; 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 red; 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 ].
red; 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.
red;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 Vg: forall a, inc a m -> Vg g a = a by move=> a am; rewrite /g; bw.
move: coex => [om0 som0 pom0].
rewrite dg in alsu ssu ssup som0 pom0.
set (m0:= unionb g) in *.
have Za: (Zermelo_axioms E p s m0).
red; split => //; rewrite som0=> t tu; move: (setUf_hi tu)=> [u ud ts];
move: (ud) => /Zo_P [_ [_ p1 p2 p3]];
move: (ts); rewrite Vg // => tb.
by apply: p1.
by rewrite -(ssu _ _ ud ts); rewrite Vg //; apply: p2.
by rewrite -(ssu _ _ ud ts); rewrite Vg //; apply: p3.
exists m0 => // sm0s.
move:(pp _ sm0s)=> [pE nps].
set (a:= p (substrate m0)) in *.
move: (Zermelo_aux4 wou nps) => [woe seu asu].
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].
split=>//; rewrite su => t /setU1_P; case.
- apply: p2.
- by move=> ->.
- move=> ts.
have p5: inc t (substrate (order_with_greatest m0 a)) by rewrite su; fprops.
move: (asu _ p5); case.
move=> hyp; rewrite hyp in ts; contradiction.
by move=> ->; apply: p3.
- by move => ->; rewrite seu.
- move=> ts.
have p5: inc t (substrate (order_with_greatest m0 a)) by rewrite su; fprops.
move: (asu _ p5); case.
move=> hyp; rewrite hyp in ts; contradiction.
by move=> ->; apply: p4.
- by move=> ->; rewrite seu.
have um:inc (order_with_greatest m0 a) m.
rewrite /m; apply: Zo_i =>//.
apply /setP_P.
apply: (@sub_trans (coarse (substrate (order_with_greatest m0 a)))).
apply: sub_graph_coarse_substrate; fprops.
have aux: (sub (substrate (order_with_greatest m0 a)) E).
move: Zae=> [_ res _ _]; apply: res.
by apply: setX_Slr.
case: nps.
rewrite som0.
apply: (setUf_i um); rewrite Vg //; rewrite 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; split.
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; apply/setC_P; split.
by apply /setP_P.
by move/set1_P.
Qed.
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) => /sfun_set_P [].
have Hb:forall i, inc i X -> target i = b.
by move=> i iX; move: (Xs _ iX) => /sfun_set_P [_ ].
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; first 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; red; 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 /sfun_set_P;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) => /sfun_set_P [_ 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 => //.
rewrite sub_function //.
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)).
move=> x xs; move: (apx _ xs); rewrite /px; move=> [up h].
by move: up => [].
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')).
have gr: sgraph r' by fprops.
move=> x xr.
move: (gr _ xr) => xp; rewrite - xp in xr |- *.
move: (arg2_sr xr) => qs.
move: (arg1_sr xr) => Ps.
case: (equal_or_not (P x) (Q x)) => aux.
rewrite aux; order_tac; aw.
have ltPQ: glt r' (P x) (Q x) by split.
change (gle (induced_order r (substrate r')) (P x) (Q x)); aw.
have Pse: (inc (P x) (segment r' (Q x))) by apply/ segmentP.
move: (alse _ qs)(ps _ qs) => p1 p2; move: (apx _ p1).
rewrite p2; rewrite /px; move=> [[_ h]] _; apply /iorder_gleP => //.
by apply: h.
have r'v: r' = induced_order r (substrate r').
apply: extensionality => //.
move=> 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.
rewrite -pt in tio |- *.
have Ps: inc (P t) (substrate r') by move: (arg1_sr tio); aw.
have Qs: inc (Q t) (substrate r') by move: (arg2_sr tio); aw.
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 =>//; move=> x ux.
case: (equal_or_not u x) => h; first by [].
have xu: (glt r u x) by split.
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; red; 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)(fun z => gle r a z)).
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.
have isF: inductive (induced_order r F).
move=> u; aw=> uF; rewrite iorder_trans // => toi.
have tos: (sub (u +s1 a) (substrate r)).
apply: sub_trans Fs.
by move=> 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 a u)) => ab.
idtac.
have bF: inc b F by rewrite /F; apply: Zo_i.
exists b; split; aw=>//.
move=> y yu.
by move: (bub _ (setU1_r a yu)) => yb; apply/iorder_gleP => //; apply: uF.
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.
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.
exists (union X).
have p1: inc (union X) A.
apply: Sp =>//;move=> x y xX yX.
move: (tX _ _ xX yX); case.
by move /(iorder_gleP _ xX yX) => /sub_gleP [_ _ h]; left.
by move /(iorder_gleP _ yX xX) => /sub_gleP [_ _ h]; right.
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 =>//; move=> 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).
by exists a.
Qed.
EIII-2-5 Isomorphisms 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 (source f) by rewrite /s; apply: Zo_S.
rewrite sf in ssf; move: wor=> [_ pwor].
move:(pwor _ ssf nes)=> [y []]; aw => ys yle.
move: ys => /Zo_P [ysf [leWy neWy]].
have Wrg: inc (Vf f y) (range (graph f)) by Wtac.
move: sr => [ _ sr']; move: (sr' _ _ Wrg leWy).
move/(range_fP ff) => [z zf vv].
have lt1: glt r' (Vf f z) (Vf f y) by rewrite - vv; split =>//.
have lt2: glt r z y.
have lt3: (glt r z y \/ gle r y z).
rewrite sf in ysf zf; apply: (total_order_pr2 tor zf ysf).
case: lt3=>// 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 rewrite /s; apply: Zo_i.
move: (yle _ zs)=> yz; move: (iorder_gle1 yz) => lt3.
order_tac.
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 =>//.
red;by 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 red;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 => /sfun_set_P [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]].
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')).
right; apply /unique_existence;split; last first.
move=> a b [s1 m1][s2 m2].
by apply: (isomorphism_worder_unique (r:=r') (r':=r)) =>//.
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.
red; rewrite rgg; rewrite /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.
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 rewrite /g; apply: extension_f.
have tg: target g = E'.
rewrite/g /extension; aw; rewrite tf /E'; by apply: setU1_eq.
have sg: source g = segmentc r a.
by rewrite /g/extension; aw; rewrite sfx xa; apply: segmentc_pr.
have sap: forall a, sub (segmentc r a) (substrate r).
move=> t; rewrite/segmentc/interval_uc; 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/sfun_set_P;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.
red;split => //; move=> u v; rewrite sg; rewrite - 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 //].
rewrite - isf //.
rewrite - sfx; symmetry;apply /(iorder_gleP r hu hv).
move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _]; by split.
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.
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.
apply /extension_orderP;split => //.
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 red; split => //; ue.
have cf'f: (f' \coP f) by red; split => //; ue.
move: (compose_order_morphism om' om) => mor1.
move: (compose_order_morphism om om') => mor2.
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].
have xrg: (inc x (range (graph f'))) by ex_tac.
have usr: inc u (source f') by Wtac.
move => yx; move:sr2 => [_ sr2]; move: (sr2 _ _ xrg yx).
move /(range_fP ff') => [v vsf' vp].
move: yx; rewrite (Vf_pr ff' p2) vp -fp'// => yr.
move:sr1 => [_ sr1]; move: (sr1 _ _ urg yr) => va.
apply /dirim_P; ex_tac; Wtac.
have srg': segmentp r' (range (graph (compose f 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].
have xrg: (inc x (range (graph f))) by ex_tac.
have usr: inc u (source f) by Wtac.
move => yx; move:sr1 => [_ sr1]; move: (sr1 _ _ xrg yx).
move /(range_fP ff) => [v vsf' vp].
move: yx; rewrite (Vf_pr ff p2) vp -fp// => yr.
move:sr2 => [_ sr2]; move: (sr2 _ _ urg yr) => va.
apply /dirim_P; ex_tac; Wtac.
move: (unique_isomorphism_onto_segment wor srg mor2) => p1.
move: (unique_isomorphism_onto_segment wor' srg' mor1) => p2.
rewrite - sf in p1; rewrite - sf' in p2.
move: (bijective_from_compose cff' cf'f p2 p1) => [p3 p4 p5].
rewrite /order_isomorphism.
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.
move: (induced_wor wo asr) => woi.
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 move: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.
red; 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).
red; split => //; split => //;last by rewrite -hyp tf.
split=>//; apply: surjective_pr4 =>//.
move: (inverse_order_is oi) => ioi.
exists (substrate r); exists (inverse_fun f).
split; first by apply: substrate_segment.
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 => //.
move: (inc_segment Ws); apply: (iorder_gle2).
have ssf: sub s (substrate r) by rewrite - sf /s;apply: Zo_S.
move: wo=> [_ wor].
move: (wor _ ssf nes) => [y []]; aw => 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: (iorder_gle1 (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 oi.
move: oi => [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=> tif; move: ((proj2 sjf) _ tif) => [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; red; 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).
red; split => //; rewrite /g; aw.
split; aw.
red; aw; move=> x y xB yB /=; aw.
move:(iorder_gleP r (ta _ xB) (ta _ yB)) => xx.
red 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.
move => f1a f2a.
apply: (iff_trans (iorder_gleP r f1a f2a)).
by symmetry.
move: (induced_wor woa Bs) => wob.
move: (unique_isomorphism_onto_segment wob sr om) => gi.
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; red; 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 => //.
red; rewrite qb /restriction1; aw; split => //.
by apply: restriction1_fb.
by rewrite -rgx - image_by_fun_source.
red; 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; red; 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)); red; split => //.
rewrite qb /restriction1; split; aw; first by apply: restriction1_fb => //.
by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
red; 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.
EIII-2-6 Lexicographic Products
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).
Lemma orprod_osr r g:
orprod_ax r g -> order_on (order_prod r g) (prod_of_substrates g).
Proof.
move=> [wor sr ao].
have aux: forall x, order_prod_r r g x x.
move=> x j [js _]; move: js; aw; fprops; last by rewrite sr; apply: Zo_S.
by move /Zo_hi; case.
have osr: substrate (order_prod r g) = prod_of_substrates g.
rewrite /order_prod graph_on_sr //.
split => //.
have tor: total_order r by apply: worder_total.
move:wor=> [or wor].
rewrite/order_prod.
apply: order_from_rel1; last by move=> u up; apply: aux.
rewrite /order_prod_r - sr => y x z xy yz j [].
aw; try apply: Zo_S.
move /Zo_P => [jd jxy] jp.
set (s:= Zo (substrate r) (fun i => [\/ Vg x i <> Vg y i, Vg y i <> Vg z i
| Vg x i <> Vg z i] )).
have sst: sub s (substrate r) by rewrite /s; apply: Zo_S.
have js: inc j s by rewrite /s ; apply: Zo_i => //; constructor 3.
have nes: nonempty s by ex_tac.
move: (wor _ sst nes) => [k []]; aw => ks kp.
move: ks => /Zo_P [ksr kp1].
case: (equal_or_not (Vg x k) (Vg y k))=> kxy.
have kyz: (Vg y k <> Vg z k) by case: kp1 => //; ue.
have kj: k = j.
move: (iorder_gle1 (kp _ js))=> kj.
have ks: (inc k (Zo (substrate r) (fun i => Vg x i <> Vg z i))).
by apply: Zo_i=>//; ue.
move: (iorder_gle1 (jp _ ks))=> jk; order_tac.
have jp':(least (induced_order r (Zo (substrate r)
(fun i => Vg y i <> Vg z i))) j).
red; aw;last (by apply: Zo_S); split.
by rewrite -kj; apply: Zo_i.
move=> l /Zo_P [ls lyz].
have ils: inc l s by apply: Zo_i => //; constructor 2.
move: (iorder_gle1 (kp _ ils)) => kl.
apply/iorder_gleP; try apply /Zo_i => //; ue.
by move: (yz _ jp'); rewrite -kj kxy.
case: (equal_or_not (Vg y k) (Vg z k)) => Vyz.
have kj: (k = j).
move:(iorder_gle1 (kp _ js)) => kj.
have ks: (inc k (Zo (substrate r) (fun i => Vg x i <> Vg z i))).
apply: Zo_i=>//; ue.
move: (iorder_gle1 (jp _ ks)) => jk; order_tac.
have jp': (least (induced_order r (Zo (substrate r)
(fun i => Vg x i <> Vg y i))) j).
red; aw; last (by apply: Zo_S); split.
apply: Zo_i=> //; ue.
move=> l /Zo_P [ls lxy].
have ils: inc l s by rewrite /s; apply: Zo_i=>//; constructor 1.
move: (iorder_gle1 (kp _ ils)) => kl.
apply/iorder_gleP; try apply /Zo_i => //; ue.
by move: (xy _ jp'); rewrite -kj Vyz.
have pk1: least (induced_order r (Zo (substrate r)
(fun i => Vg x i <> Vg y i))) k.
red;aw; last (by apply: Zo_S); split; first by apply: Zo_i =>//.
move => l /Zo_P [lr lxy].
have ils: inc l s by apply: Zo_i=>//; constructor 1.
move: (iorder_gle1 (kp _ ils)) => kl.
by apply/iorder_gleP => //; apply /Zo_i.
have pk2: least (induced_order r (Zo (substrate r)
(fun i => Vg y i <> Vg z i))) k.
red; aw; last (by apply: Zo_S); split; first by apply: Zo_i =>//.
move => l /Zo_P [lr lxy].
have ils: inc l s by rewrite /s; apply: Zo_i=>//; constructor 2.
move: (iorder_gle1 (kp _ ils)) => kl.
by apply/iorder_gleP => //; apply /Zo_i.
move: (xy _ pk1)(yz _ pk2) => Vkxy Vkyz.
have Vkxz: glt (Vg g k) (Vg x k) (Vg z k).
by hnf in ao;rewrite - sr in ao; move: (ao _ ksr)=> ok; order_tac.
suff: (k = j) by move => <-.
move: (iorder_gle1 (kp _ js)) => r1.
have ks:(inc k(Zo (substrate r) (fun i => Vg x i <> Vg z i))).
by apply: Zo_i =>//; move: Vkxz=> [_ prop].
move: (iorder_gle1 (jp _ ks))=> r2.
by order_tac.
move=> u v; rewrite /prod_of_substrates; move=> up vp le1 le2.
set (s:=(Zo (domain g) (fun i : Set => Vg u i <> Vg v i))).
case: (emptyset_dichot s) => es.
have fg:fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops.
apply: (setXb_exten up vp).
rewrite /fam_of_substrates=> i; bw=> idg.
by ex_middle uv; empty_tac1 i; rewrite /s; apply: Zo_i.
have ssym: s=(Zo (domain g) (fun i : Set => Vg v i <> Vg u i)).
rewrite /s; set_extens t; move/Zo_P => [pa pb]; apply: Zo_i; fprops.
have ssr: (sub s (substrate r)) by rewrite /s sr; apply: Zo_S.
move: (wor _ ssr es)=> [j jp].
have js: (inc j s) by move: jp=> []; aw; fprops.
move: (le1 _ jp) => p1.
rewrite ssym in jp; move: (le2 _ jp) => p2.
hnf in ao; rewrite - sr in ao; move: (ao _ (ssr _ js))=> oj.
order_tac.
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.
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.
Alternate formulation without least_element
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 : Set => 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.
move: (proj2 wor _ ssr nse)=> [j jle].
move: (aux _ jle) => jp.
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: js => /Zo_P [jdg Vj].
case: aux => haux.
rewrite haux in Vj;move: Vj => h;split => //.
move: haux => [i [isr lti aeq]].
have iis: inc i s by move:lti => [_ ok];apply: Zo_i =>//; ue.
move: (iorder_gle1 (jmin _ iis)) => ij.
case: (equal_or_not j i) => ji; first by ue.
have ltji: glt r j i by split.
by case: Vj; apply: aeq.
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.
move: (orprod_osr la) => [ol sl].
move: (la)=> [[or wor] sr ao].
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 : Set => Vg x i <> Vg y i)).
case: (emptyset_dichot s) => nse.
have xy: x = y.
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.
by left; rewrite xy; order_tac; rewrite sl.
have ssr: sub s (substrate r) by rewrite/s; apply: Zo_S.
move: (wor _ ssr nse)=> [j jle].
move: (jle)=> [];rewrite iorder_sr // => js jp.
have jdg: inc j (domain g) by rewrite - sr; apply: ssr.
move: (alt _ jdg)=>[orj torj].
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.
move: (iorder_osr or ssr) => [ois sir].
case: (torj _ _ px py) => leaux.
left; apply /(orprod_gle1P la); split => //.
rewrite - sr; fold s; move=> k kl.
rewrite - (unique_least ois jle kl); split =>//.
by move: js => /Zo_P [].
right; apply /(orprod_gle1P la); split => //.
have ssym: s=(Zo (domain g) (fun i : Set => Vg y i <> Vg x i)).
rewrite /s sr; set_extens t; move/Zo_P => [pa pb]; apply: Zo_i; fprops.
rewrite - ssym; move=> k kl.
rewrite - (unique_least ois jle kl); split =>//.
by move: js => /Zo_hi h h'; case: h.
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) => h.
by move : h => [];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;red; 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].
move: (du_index_pr1 ux) => [qudg puv pu].
move: (du_index_pr1 vx) => [qvdg pvv pv].
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].
move: (du_index_pr1 ux) => [qudg puv pu].
move: (du_index_pr1 vx) => [qvdg pvv pv].
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 // .
move => a asg;rewrite /order_sum_r.
move: (du_index_pr1 asg) => [qudg puv pu].
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.
Lemma cdo_glt1: glt canonical_doubleton_order C0 C1.
Proof. split; [ apply /cdo_gleP; in_TP4 | fprops]. Qed.
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.
move: cdo_wor => [wor sr];
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.
apply /orsum2_gleP.
split; first by apply: candu2_pra.
by apply: candu2_prb.
constructor 3; aw; split; fprops.
by move => h; move: (pr2_def h); apply: TP_ne.
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.
move: cdo_wor => [wor sr];
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 move=> [r1 r2]; rewrite -r2 in r1; contradiction.
case; first by move=> r1 _; contradiction.
by move=> [ia _]; rewrite ia.
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 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)).
red; 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));red; split; aw.
rewrite /io; fprops.
red; split; aw.
red; 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 orsum2_totalorder r r':
total_order r -> total_order r' -> total_order (order_sum2 r r').
Proof.
move=> [or tor][or' tor'].
split; first by fprops.
rewrite orsum2_sr//.
move=> x y xc yc;red.
move: (xc)(yc) => /candu2P [px p1] /candu2P [py p2].
have ba: C1 <> C0 by fprops.
case: p1; case: p2; move=> [Py Qy][Px Qx].
by case: (tor _ _ Px Py); [ left | right]; apply /orsum2_gleP;
split => //; constructor 1.
by left; apply /orsum2_gleP; split => //; constructor 3; split => //; ue.
by right; apply /orsum2_gleP; split => //; constructor 3; split => //; ue.
by case: (tor' _ _ Px Py); [ left | right];
apply /orsum2_gleP; split => //; constructor 2; split => //; ue.
Qed.
Lemma orsum_wor r g:
worder r -> substrate r = domain g ->
worder_fam g ->
worder (order_sum r g).
Proof.
move=> [or wor] sr alw.
have oa: orsum_ax r g. red;split => // i ie; exact (proj1 (alw _ ie)).
split; first by fprops.
move=> x; bw => 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: (wor _ Asr neA)=> [a []]; aw; move=> 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: (alw _ adg)=> [or' wor']; move: (wor' _ Cs neC) => [b []].
rewrite (iorder_sr or' Cs).
move=> bC leB.
have Jx: inc (J b a) x.
move: bC => /funI_P [z zB ->].
move /Zo_P: zB => [zx <-].
by rewrite (proj33 (du_index_pr1 (xs _ zx))).
have ors: order (order_sum r g) by fprops.
have xso: sub x (substrate (order_sum r g)) by bw.
exists (J b a); red; rewrite (iorder_sr ors xso).
split; first (by exact); move=> c cx.
move: (du_index_pr1 (xs _ cx))=> [Qc Pc pc].
apply /(iorder_gleP _ Jx cx); apply /orsum_gleP;split; fprops.
red; rewrite pr1_pair pr2_pair.
have QcA: (inc (Q c) A) by apply /funI_P; ex_tac.
move: (iorder_gle1 (ale _ QcA)) => leac.
case: (equal_or_not a (Q c)).
move=> aQc; right;split => //.
have Pcb: (inc (P c) C).
apply/funI_P; exists c => //; apply: Zo_i => //xs.
exact (iorder_gle1 (leB _ Pcb)).
by move => nac; left.
Qed.
End Worder.
Export Worder.