Library sset6
Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset5.
Set Implicit Arguments.
Import Correspondence.
Import Bfunction.
Import Border.
Module Worder.
Well ordering
Definition worder r :=
order r & forall x, sub x (substrate r) -> nonempty x ->
exists y, least_element (induced_order r x) y.
Definition worder_r r :=
order_r r & forall x, (forall a, inc a x -> r a a) -> nonempty x ->
exists y, least_element (graph_on r x) y.
Lemma worder_is_order: forall r, worder r -> order r.
Proof. move=> r [or _]; exact or. Qed.
Hint Resolve worder_is_order: fprops.
Lemma wordering_pr: forall r x, worder_r r ->
(forall a, inc a x -> r a a) ->
(substrate (graph_on r x) = x & worder (graph_on r x)).
Proof.
move=> r x [or wo] ar.
have sg: (substrate (graph_on r x) = x) by rewrite substrate_graph_on //.
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 ais;move: (sx _ ais); apply ar.
have sgs: substrate (graph_on r s) = s by rewrite substrate_graph_on //.
move: (wo _ rs nes)=> [a [ais lea]].
rewrite sgs in ais lea.
exists a.
split; first by aw; ue.
move=> y ys; awi ys =>//; try ue.
aw; move: (lea _ ys); rewrite /gle 2! graph_on_rw1; ee.
Qed.
We sometimes need an ordered set with two elements
Definition canonical_doubleton_order :=
union2 (doubleton (J TPa TPa) (J TPb TPb)) (singleton (J TPa TPb)).
Lemma canonical_doubleton_order_pr: forall x y,
related canonical_doubleton_order x y =
( (x= TPa & y = TPa) \/ (x= TPb & y = TPb) \/ (x= TPa & y = TPb)).
Proof.
move=> x y; rewrite /gle/related/canonical_doubleton_order.
apply iff_eq.
move=> h; case (union2_or h)=> h'.
case (doubleton_or h') => h''; move:(pr1_def h'')(pr2_def h'') => p1 p2; auto.
awi h'; move:(pr1_def h')(pr2_def h') => p1 p2; auto.
case; [| case]; move=> [r1 r2]; rewrite r1 r2;
try solve [apply union2_first; fprops].
apply union2_second; fprops.
Qed.
Lemma substrate_canonical_doubleton_order:
substrate canonical_doubleton_order = two_points.
Proof.
have gc:is_graph canonical_doubleton_order.
rewrite /canonical_doubleton_order=> t tu.
case (union2_or tu);last by aw=>->; fprops.
move=> h;case (doubleton_or h) => ->; fprops.
set_extens x.
rewrite (inc_substrate_rw x gc); move=> h; case h;move=> [y].
move: (canonical_doubleton_order_pr x y).
rewrite /related; move=> ->; intuition; ue.
move: (canonical_doubleton_order_pr y x).
rewrite /related; move=> ->; intuition; ue.
rewrite two_points_rw.
case => h; have aux: (related canonical_doubleton_order x x)
by rewrite canonical_doubleton_order_pr; auto.
substr_tac.
substr_tac.
Qed.
Lemma worder_canonical_doubleton_order: worder canonical_doubleton_order.
Proof.
have gc:is_graph canonical_doubleton_order.
rewrite /canonical_doubleton_order=> t tu.
case (union2_or tu);last by aw=>->; fprops.
move=> h;case (doubleton_or h) => ->; fprops.
move: (substrate_canonical_doubleton_order) => subs.
have oc: (order canonical_doubleton_order).
hnf; ee; split=>//.
move=> y; rewrite subs canonical_doubleton_order_pr two_points_rw.
intuition.
move=> x y z; rewrite 3! canonical_doubleton_order_pr; intuition.
elim two_points_distinct; ue.
move=> x y; rewrite 2! canonical_doubleton_order_pr.
move => h1.
case; first by move=> []->->.
case; first by move=> []->->.
move=> [p1 p2]; move: h1.
case; first by move=> []->->.
case; first by move=> []->->.
by rewrite p1 p2; move=> []->->.
split=>//.
move=> x xt nex.
case (inc_or_not TPa x)=> hyp.
exists TPa; red; aw; split=>//.
move=> y yx; aw; rewrite /gle canonical_doubleton_order_pr.
move: (xt _ yx); rewrite subs two_points_rw; intuition.
move: nex=> [y yx]; exists y; split; aw =>//.
have p: forall t, inc t x -> t = TPb.
move=> t tx; move: (xt _ tx); rewrite subs two_points_rw.
by case =>// ta; rewrite ta in tx; elim hyp.
move => t tx; aw; rewrite /gle canonical_doubleton_order_pr.
by rewrite (p _ yx)(p _ tx); intuition.
Qed.
A well ordering is total; bounded sets have a supremum
Lemma worder_total: forall r, worder r -> total_order r.
Proof.
move=> r [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_doubleton.
have si: substrate (induced_order r u) = u by aw.
have neu: nonempty u by ex_tac.
move: (wo _ ur neu)=> [z [zu zle]].
rewrite si in zu zle.
move: (zle _ xu)(zle _ yu); aw=> p1 p2.
case (doubleton_or zu) =><-; auto.
Qed.
Lemma worder_hassup: forall r A, worder r -> sub A (substrate r) ->
bounded_above r A -> has_supremum r A.
Proof.
move=> r A [or wo] As [t tA].
red; rewrite /least_upper_bound.
set X:= (Zo _ _).
have Xs: sub X (substrate r) by rewrite /W; apply Z_sub.
have nX: (nonempty X).
by exists t; rewrite /X; apply Z_inc =>//; move: tA=> [tA _].
move: (wo _ Xs nX)=> [x leX].
by exists x.
Qed.
Lemma induced_trans: forall r x y,
order r -> sub x y-> sub y (substrate r) ->
induced_order r x = induced_order (induced_order r y) x.
Proof.
rewrite /induced_order=> r x y or xy yr.
have aux: sub (coarse x)(coarse y) by rewrite /coarse; apply product_monotone.
set_extens t;aw; intuition.
Qed.
Lemma worder_restriction: forall r A, worder r -> sub A (substrate r) ->
worder (induced_order r A).
Proof.
move=> r A [or wo] As; split; fprops.
move => x sx nex; awi sx=>//.
rewrite -(induced_trans or sx As).
by apply wo=>//; apply sub_trans with A.
Qed.
Lemma worder_least: forall r, worder r -> nonempty (substrate r) ->
exists y, least_element r y.
Proof.
move=> r [or wo] ne.
move: (wo _ (@sub_refl (substrate r)) ne)=> [x lex].
rewrite induced_order_substrate // in lex.
by exists x.
Qed.
A set remains well-ordered after adjoining a greatest element
Lemma worder_adjoin_greatest: forall r a, worder r-> ~ (inc a (substrate r))
-> worder (order_with_greatest r a).
Proof.
move=> r a [or wo] nas.
move: (order_with_greatest_pr or nas) => [on [sn [rd gna]]].
split=>// x xs nex.
set (y := intersection2 x (substrate r)).
case (emptyset_dichot y) => ye.
have xa: x = singleton a.
apply singleton_pr1=>//.
move=> z zx; move: (xs _ zx); rewrite sn; aw.
by case=>// => zr; empty_tac1 z; rewrite /y;apply intersection2_inc.
exists a; red; aw; rewrite xa; split; fprops.
move=> t ta; awi ta; rewrite ta; aw; order_tac; rewrite sn; fprops.
have sys:sub y (substrate r) by rewrite /y; apply intersection2sub_second.
move: (wo _ sys ye)=> [z []]; aw=> zy lez.
move: (intersection2_first zy) => zx.
exists z; split; aw.
move=> t tx; aw.
move: (xs _ tx); rewrite sn; aw; case=> p.
have ty: inc t y by rewrite /y; apply intersection2_inc.
move: (lez _ ty); aw; rewrite /gle/related {1} rd; aw; intuition.
rewrite p.
move: gna=> [_]; apply; ue.
Qed.
Lemma inc_lt1_substrate: forall r x y, glt r x y -> inc x (substrate r).
Proof. move=> *;order_tac. Qed.
Lemma inc_lt2_substrate: forall r x y, glt r x y -> inc y (substrate r).
Proof. move=> *; order_tac. Qed.
Lemma not_lt_self: forall r x, glt r x x -> False.
Proof. by move=> r x [_ xx]; elim xx. Qed.
Lemma Zermelo_bis: forall E, exists r, worder r & substrate r = E.
Proof.
move=> E.
pose p a := complement a (singleton (rep a)).
pose chain 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).
pose om := intersection (Zo (powerset (powerset E)) chain).
pose m a := forall x, inc x om -> sub x a \/ sub a x.
pose d p := intersection (Zo om (fun x => sub p x)).
pose R x := d (singleton x).
have pe: p emptyset = emptyset.
by empty_tac x xe; move: xe; rewrite /p; srw; case; case; case.
have sp: forall a, sub (p a) a by move=> t; rewrite /p; apply sub_complement.
have cp:chain (powerset E).
split; fprops; split; first by apply powerset_inc; fprops.
split; first by move=> A; aw; move=> AE; apply sub_trans with A.
move=> A AP [x xA]; move: (AP _ xA); aw.
move=> xE t tA; exact (xE _ (intersection_forall tA xA)).
have co :chain om.
have aux: (nonempty (Zo (powerset (powerset E)) chain)).
by exists (powerset E); apply Z_inc; aw; fprops.
rewrite /om; red; ee.
by rewrite /om; apply intersection_sub; apply Z_inc; aw; fprops.
apply intersection_inc=>//; move=>y; rewrite Z_rw/chain; aw; intuition.
move=> A Ai; apply intersection_inc=>//.
move=> y yi; move: (yi); rewrite Z_rw; move=> [_ [_[_ [q _]]]]; apply q.
apply (intersection_forall Ai yi).
move=> A sAi neA; apply intersection_inc=> //.
move=> y yi; move: (yi); rewrite Z_rw; move=> [_ [_[_ [_ q]]]]; apply q=>//.
move=>t tA; move: (sAi _ tA) => ti.
by apply (intersection_forall ti yi).
move: (co)=> [sop [Eo [po io]]].
have cio: forall x, chain x -> sub om x.
move=> x xc; rewrite / om; apply intersection_sub; apply Z_inc =>//.
by aw; move:xc; rewrite /chain; intuition.
have am: om = Zo om m.
apply extensionality; last by apply Z_sub.
apply cio; red; ee.
apply sub_trans with om; [by apply Z_sub| apply sop].
by apply Z_inc=>//; move=> x xom; left;move: (sop _ xom); aw.
move=> A; rewrite Z_rw; move=> [Aom mA].
apply Z_inc; first by apply (po _ Aom).
have aux: (sub om (Zo om (fun x=> sub x (p A) \/ sub A x))).
apply cio; red; ee.
by apply sub_trans with om; first by apply Z_sub.
by apply Z_inc=>//; right; move: (sop _ Aom); aw.
move => B; rewrite Z_rw; move => [Bom ors].
apply Z_inc; first by apply (po _ Bom).
case ors => orsi.
left; apply sub_trans with B =>//; apply sp.
case (mA _ (po _ Bom)) => aux; last by auto.
case (inc_or_not (rep B) A)=> aux2.
have BA: (sub B A).
rewrite /p in aux2; move=> t tB.
case (equal_or_not t (rep B)).
by move=> ->.
by move=> trB; apply aux; rewrite /p; srw; aw.
have: (B = A) by apply extensionality.
by move=> ->; intuition.
right; move=> t tA; rewrite /p; srw; aw.
split; [ by apply orsi| dneg trB; ue].
move=> B sB neB; apply Z_inc.
apply io =>//; apply: sub_trans; [eexact sB| apply Z_sub].
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 (intersection_forall ti xB).
right; move=> t tA; apply intersection_inc=>//.
move=> y yB; move: (sB _ yB); rewrite Z_rw; move=> [yom ors].
case ors; last by apply.
by move => sy; elim aux; ex_tac.
move=> x xom; case (mA _ xom) => hyp.
move: (aux _ xom); rewrite Z_rw; move=> [_ xpA].
case xpA=>xpB; first by auto.
have Ax: (A = x) by apply extensionality.
rewrite Ax; right; apply sp.
by right; apply sub_trans with A=>//; apply sp.
move=> A sAZ neA; apply Z_inc.
apply io =>//; apply sub_trans with (Zo om m) =>//; apply Z_sub.
move=> x xom.
case (p_or_not_p (exists y, inc y A & sub y x)) => hyp.
move: hyp=> [y [yA yx]]; right; move => t ti.
apply yx; apply (intersection_forall ti yA).
left; move=> t tx; apply intersection_inc=>//.
move=> y yA; move: (sAZ _ yA); rewrite Z_rw; move=> [yom my].
case (my _ xom);[ by apply | move=> yx; elim hyp; ex_tac; apply Z_sub].
have st: forall a b, inc a om -> inc b om -> sub a b \/ sub b a.
move=> a b; rewrite {2} am Z_rw; move=> aom [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 Z_sub| exists E;apply Z_inc].
have pdp: forall q, sub q E -> sub q (d q).
rewrite /d=> q qE t tq; apply intersection_inc.
by exists E; apply Z_inc.
by move => y; rewrite Z_rw; move=>[_]; apply.
have dpq: forall q r, inc r om -> sub q r -> sub q E-> sub (d q) r.
by rewrite /d=> q r rom qr qE; apply intersection_sub; apply Z_inc.
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))).
by rewrite /p=> t tq; srw; aw; split; [ apply (pdp _ qE)| dneg tr; 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]; elim (emptyset_pr (x:= t)); apply aux.
move=> ned; move: (nonempty_rep ned) => rd dc; move: (dc _ rd); srw.
aw; intuition.
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 with r=>//; apply powerset_sub; apply sop.
move: (dpq _ _ rom qr spE) => sdqr.
case (st _ _ (dpo _ spE) (po _ rom)) => ch.
move: (pdp _ spE) => qdp.
have:(inc (rep r) (p r)) by apply ch; apply qdp.
rewrite /p; srw; aw; intuition.
apply extensionality =>// t tr.
case (equal_or_not t (rep r)). by move=> ->; apply (pdp _ spE).
by move=> tnr; apply ch; rewrite /p; srw; aw; auto.
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 sub_singleton.
move: (pdp _ p1) => p2; ee.
have nesi: (nonempty (singleton x)) by fprops.
by move: (rdq _ p1 nesi); aw.
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 =>//.
by move=> t; aw; move=> ->; apply nonempty_rep.
fprops.
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.
have p1:(sub (doubleton x y) (R y)).
by move=> t td; case (doubleton_or td)=>->.
have p2: (sub (doubleton x y) (R x)) by apply sub_trans with (R y).
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.
set (r := graph_on (fun x y => (sub (R y) (R x))) E).
have or:order r.
rewrite /r; apply order_from_rel1.
by move=> x y z /= xy yz; apply sub_trans with (R y).
by move=> u v uE vE vu uv; apply Ri=>//; apply extensionality.
move => u ue; fprops.
have sr: substrate r = E.
rewrite /r substrate_graph_on //; move => u ue; fprops.
exists r.
split=>//;split=>//.
move=> x xsr nex.
rewrite sr in xsr.
move: (rdq _ xsr nex) => rdx.
exists (rep (d x)); split.
by aw;rewrite sr.
aw; move=> a ax; aw; last by ue.
rewrite /r /gle graph_on_rw1;ee.
apply sRR; try apply xsr=>//.
move: ((pdp _ xsr) _ ax)=> adx.
have ne: (nonempty (d x)) by exists a.
rewrite Rrq //.
by apply dpo.
Qed.
Two stricly increasing functions with the same range are equal if the source is well-ordered
Lemma strict_increasing_extens: forall 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=> f g r r' sif sig wo.
have to: total_order r by apply worder_total.
have sm: (strict_monotone_fun f r r') by red; auto.
have smg: (strict_monotone_fun g r r') by red; auto.
move: (total_order_monotone_injective to sm)=> injf.
move: (total_order_monotone_injective to smg)=> injg {sm smg}.
move:sif sig=> [ff [or [or' [sr [sr' si]]]]] [fg [_ [_ [srg[sr'g sig]]]]] rr.
set (A:=Zo (source f)(fun x=> W x f <> W x g)).
case (emptyset_dichot A) => eA.
apply function_exten=>//; try ue.
by move=> x xsf; ex_middle sg; empty_tac1 x;rewrite /A; apply Z_inc.
have Asf: (sub A (substrate r)) by rewrite sr /A;apply Z_sub.
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 (W x f) (range (graph g)) by rewrite -rr; apply inc_W_range_graph.
rewrite range_inc_rw; aw; move=> [y [ysg WW]].
move:(ysg); rewrite -srg sr=> ysf.
have : inc (W x g) (range (graph f)) by rewrite rr; apply inc_W_range_graph.
rewrite range_inc_rw; aw; move=> [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' (W x g) (W x f).
have a0: x <> y by move=> h; move: xA WW; rewrite -h /A Z_rw; intuition.
rewrite WW; case (total_order_pr1 to xsr ysr); first by apply sig.
case => h; last by contradiction.
rewrite ggt_invb in h; move: (sig _ _ h) => [le ne].
suff: inc y A by move=> h'; move:(xl _ h'); aw; move=> h''; order_tac.
rewrite /A; apply Z_inc=>//.
by rewrite -WW; clear ne; dneg xx; symmetry; move: injf=> [_ p]; apply p.
have p2: glt r' (W x f) (W x g).
have a0: x <> z by move=> h; move: xA WWw; rewrite -h /A Z_rw; intuition.
rewrite WWw; case (total_order_pr1 to xsr zsr); first by apply si.
case => h; last by contradiction.
rewrite ggt_invb in h; move: (si _ _ h) => [le ne].
suff: inc z A by move=> h'; move:(xl _ h'); aw; move=> h''; order_tac.
rewrite /A; apply Z_inc=>//.
by rewrite -WWw; clear ne; dneg xx; move: injg=> [_ p]; apply p.
order_tac.
Qed.
strict_increasing_fun f r r'-> strict_increasing_fun g r r' -> worder r ->
range (graph f) = range (graph g) -> f = g.
Proof.
move=> f g r r' sif sig wo.
have to: total_order r by apply worder_total.
have sm: (strict_monotone_fun f r r') by red; auto.
have smg: (strict_monotone_fun g r r') by red; auto.
move: (total_order_monotone_injective to sm)=> injf.
move: (total_order_monotone_injective to smg)=> injg {sm smg}.
move:sif sig=> [ff [or [or' [sr [sr' si]]]]] [fg [_ [_ [srg[sr'g sig]]]]] rr.
set (A:=Zo (source f)(fun x=> W x f <> W x g)).
case (emptyset_dichot A) => eA.
apply function_exten=>//; try ue.
by move=> x xsf; ex_middle sg; empty_tac1 x;rewrite /A; apply Z_inc.
have Asf: (sub A (substrate r)) by rewrite sr /A;apply Z_sub.
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 (W x f) (range (graph g)) by rewrite -rr; apply inc_W_range_graph.
rewrite range_inc_rw; aw; move=> [y [ysg WW]].
move:(ysg); rewrite -srg sr=> ysf.
have : inc (W x g) (range (graph f)) by rewrite rr; apply inc_W_range_graph.
rewrite range_inc_rw; aw; move=> [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' (W x g) (W x f).
have a0: x <> y by move=> h; move: xA WW; rewrite -h /A Z_rw; intuition.
rewrite WW; case (total_order_pr1 to xsr ysr); first by apply sig.
case => h; last by contradiction.
rewrite ggt_invb in h; move: (sig _ _ h) => [le ne].
suff: inc y A by move=> h'; move:(xl _ h'); aw; move=> h''; order_tac.
rewrite /A; apply Z_inc=>//.
by rewrite -WW; clear ne; dneg xx; symmetry; move: injf=> [_ p]; apply p.
have p2: glt r' (W x f) (W x g).
have a0: x <> z by move=> h; move: xA WWw; rewrite -h /A Z_rw; intuition.
rewrite WWw; case (total_order_pr1 to xsr zsr); first by apply si.
case => h; last by contradiction.
rewrite ggt_invb in h; move: (si _ _ h) => [le ne].
suff: inc z A by move=> h'; move:(xl _ h'); aw; move=> h''; order_tac.
rewrite /A; apply Z_inc=>//.
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 is_segment 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 segment_c r s := interval_uc r s.
Lemma lt_in_segment: forall r s x y,
is_segment r s -> inc x s -> glt r y x -> inc y s.
Proof.
move=>r s x y [ss sp] xs [le ne]; apply (sp _ _ xs le).
Qed.
Lemma inc_segment: forall r x y,
inc y (segment r x) -> glt r y x.
Proof. move=> r x y;rewrite /segment/interval_uo Z_rw; intuition.
Qed.
Lemma not_in_segment : forall r x, inc x (segment r x) -> False.
Proof. move=> r x h; move: (inc_segment h) =>h'. elim (not_lt_self h'). Qed.
Lemma sub_segment: forall r x, sub (segment r x) (substrate r).
Proof. by move=> r x t ; rewrite /segment/interval_uo Z_rw; case.
Qed.
Lemma sub_segment1: forall r s, is_segment r s -> sub s (substrate r).
Proof. by move=> r rs [ss sp] t ts; apply ss.
Qed.
Lemma sub_segment2: forall r x y,
sub (segment (induced_order r x) y) x.
Proof.
move=> r x y t; rewrite /segment/interval_uo Z_rw.
move=> [_[ h _]]; move: h;rewrite /induced_order => h.
by move: (intersection2_second h); rewrite / coarse; aw; intuition.
Qed.
Lemma segment_inc: forall r x y,
glt r y x -> inc y (segment r x).
Proof. move=> r x y xy; rewrite /segment/interval_uo Z_rw.
split=>//. move: xy=> [];rewrite /gle=> xy nxy; substr_tac.
Qed.
Lemma segment_rw: forall r x y,
inc y (segment r x) = glt r y x.
Proof.
by move=> r x y; apply iff_eq; [ apply inc_segment | apply segment_inc].
Qed.
Lemma segmentc_rw: forall r x y,
inc y (segment_c r x) = gle r y x.
Proof.
move=> r x y; apply iff_eq; rewrite /segment_c/interval_uc Z_rw; intuition.
order_tac.
Qed.
Lemma inc_bound_segmentc: forall r x, order r -> inc x (substrate r) ->
inc x (segment_c r x).
Proof. move=> r x or xsr; rewrite segmentc_rw //; order_tac.
Qed.
Lemma sub_segmentc: forall r x, sub (segment_c r x) (substrate r).
Proof. move=> r x t; rewrite /segment_c/interval_uc Z_rw; intuition.
Qed.
Hint Resolve inc_bound_segmentc: fprops.
Lemma segment_c_pr: forall r x, order r -> inc x (substrate r) ->
tack_on (segment r x) x = segment_c r x.
Proof.
move=> r x or xsr; rewrite /segment_c/interval_uc; set_extens y.
aw; rewrite Z_rw; case=> h.
split;first by apply (sub_segment h).
move: (inc_segment h)=>h'; order_tac.
rewrite h; split=>//; order_tac.
rewrite Z_rw; move=> [ysr yx].
case (equal_or_not y x)=> h; first by rewrite h; fprops.
aw; left; apply segment_inc=>//.
Qed.
Examples of segments. Empty set, whole substrate, union, intersection, subsegments
Lemma empty_is_segment: forall r, is_segment r emptyset.
Proof.
move=> r; split; first by apply emptyset_sub_any.
move=> x y h; elim (emptyset_pr h).
Qed.
Lemma substrate_is_segment: forall r, order r -> is_segment r (substrate r).
Proof.
move=> r or; red; ee.
move=> x y xst xy; order_tac.
Qed.
Lemma subsegment_is_segment: forall r s s', order r ->
is_segment r s -> is_segment (induced_order r s) s' -> is_segment r s'.
Proof.
move=> r s s' or srs sis.
move: (sub_segment1 srs)=>ssr.
red. move: sis; rewrite /is_segment; aw.
move=> [s's hyp]; split.
by apply (sub_trans (a:=s')(b:=s)).
move=> x y xs' yx; move: (s's _ xs')=> xs; move: srs=> [_ h].
apply (hyp _ _ xs'); aw; apply (h _ _ xs yx).
Qed.
Lemma intersection_is_segment: forall r s , order r -> nonempty s ->
(forall x, inc x s -> is_segment r x) -> is_segment r (intersection s).
Proof.
move=> r s or nes als; split.
move :nes => [y ys] x xs; move: (als _ ys) => [yss _].
exact (yss _ (intersection_forall xs ys)).
move=> x y xi yx; apply intersection_inc=>//.
move=> z zs. move: (als _ zs) => [_ p].
apply (p _ _ (intersection_forall xi zs) yx).
Qed.
Lemma unionf_is_segment: forall r j s, order r ->
(forall x, inc x j -> is_segment r (s x)) -> is_segment r (unionf j s).
Proof.
move=> r j s or als; split.
move=> t tu;move: (unionf_exists tu)=> [y [yj ts]].
by move:(als _ yj) => [ss _]; apply ss.
move=> x y xu xy;move: (unionf_exists xu)=> [z [zj ts]].
move:(als _ zj) => [_ ss]; move: (ss _ _ ts xy) =>h.
union_tac.
Qed.
Lemma union_is_segment: forall r s , order r ->
(forall x, inc x s -> is_segment r x) -> is_segment r (union s).
Proof.
move=>r s or als. rewrite -unionb_identity /unionb.
apply unionf_is_segment =>//.
by rewrite identity_domain;move=> x xs; rewrite identity_ev //; apply als.
Qed.
Lemma segment_is_segment: forall r x, order r ->
inc x (substrate r) -> is_segment r (segment r x).
Proof.
move=> r x or xs; rewrite /segment/interval_uo.
split; first by apply Z_sub.
move=> a b; rewrite ? Z_rw; move=> [asr ax] ba.
split; order_tac.
Qed.
Theorem well_ordered_segment: forall r s, worder r -> is_segment r s ->
s = substrate r \/ (exists x, inc x (substrate r) & s = segment r x).
Proof.
move=> r s wor sr.
case (equal_or_not s (substrate r)); first by auto.
move=> snr; right.
set (y:= complement (substrate r) s).
have ney: nonempty y.
by move: sr=> [sr _] ; apply strict_sub_nonempty_complement; split.
move: (worder_total wor) => tor.
have sys: (sub y (substrate r)). by apply sub_complement.
move:wor=> [or wo]; move: (wo _ sys ney)=> [x []]; aw.
move=> xy xle.
have xis: inc x (substrate r) by apply sys.
exists x; split=>//.
set_extens z => zs.
have zsr: inc z (substrate r) by apply (sub_segment1 sr).
rewrite segment_rw //.
case (total_order_pr2 tor zsr xis) => //.
move: sr=> [_ h] xz; move: (h _ _ zs xz ) xy; rewrite /y; srw; intuition.
ex_middle zis.
have zy: (inc z y) by rewrite /y; srw; ee; apply (sub_segment zs).
move: (iorder_gle1 (xle _ zy)) (inc_segment zs)=> p1 p2.
order_tac.
Qed.
Lemma segment_alt: forall r x a, order r -> least_element r a ->
segment r x = interval_co r a x.
Proof.
rewrite /segment/interval_co/interval_uo=> r x a or [ais lea].
set_extens t;rewrite ? Z_rw; intuition.
Qed.
Lemma segment_alt1: forall r s, worder r -> is_segment r s ->
s = substrate r \/ (exists x, exists a, s = interval_co r a x).
Proof.
move => r s wo iss.
case (emptyset_dichot (substrate r)) => sre.
left; move: iss=> [p _].
apply extensionality=>//;rewrite sre; apply emptyset_sub_any.
case (well_ordered_segment wo iss); first by intuition.
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: forall r x y, order r -> gle r x y ->
sub (segment r x) (segment r y).
Proof.
move=> r x y or xy t ts; move: (inc_segment ts) => h.
apply segment_inc; order_tac.
Qed.
Lemma segment_dichot_sub: forall r x y,
worder r -> is_segment r x -> is_segment r y ->
(sub x y \/ sub y x).
Proof.
move=> r x y 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: forall 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=> r x y z or xsr ysr zy; apply segment_inc=>//.
move: (inc_segment ysr)=> aux; order_tac.
Qed.
Lemma coarse_segment_monotone: forall r x y, order r -> gle r x y ->
sub (coarse (segment r x)) (coarse (segment r y)).
Proof. move=> r x y or xy;move: (segment_monotone or xy) =>sm.
by rewrite /coarse; apply product_monotone.
Qed.
Lemma segment_induced_a: forall r s x,
order r -> is_segment r s -> inc x s ->
segment (induced_order r s) x = segment r x.
Proof.
move=> r s x 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; rewrite /glt; aw.
move: srs=> [h1 h2];apply (h2 _ _ xs); order_tac.
Qed.
Lemma tack_on_segment: forall r x,
order r -> inc x (substrate r) ->
is_segment r (segment_c r x).
Proof.
move=> r x or xs; rewrite /segment_c /interval_uc; split; first by apply Z_sub.
move=> a b; rewrite ? Z_rw; move => [asr ax] ba.
split; order_tac.
Qed.
Lemma segment_induced: forall r x x0, order r -> glt r x0 x ->
segment (induced_order r (segment r x)) x0 = segment r x0.
Proof.
move=> r a b or ab.
move: (inc_lt2_substrate ab)=> h.
rewrite segment_induced_a //.
apply segment_is_segment=>//.
rewrite segment_rw //.
Qed.
Lemma segment_induced1: forall r x x0, order r -> glt r x0 x ->
segment (induced_order r (segment_c r x)) x0 = segment r x0.
Proof.
move=> r a b or ab.
move:(inc_lt2_substrate ab)=> h.
rewrite segment_induced_a =>//.
apply tack_on_segment=>//.
rewrite - segment_c_pr //.
aw; left; rewrite segment_rw //.
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
Lemma union_segments: forall r, total_order r ->
let E := substrate r in
let A := union (fun_image E (fun x => (segment r x))) in
( (forall x, ~ (greatest_element r x)) -> A = E)
& (forall x, greatest_element r x -> A = complement E (singleton x)).
Proof.
move=> r tor E A.
have Ap: forall x, inc x A = exists y, glt r x y.
move=> x; apply iff_eq; rewrite union_rw.
by move=> [y [xy]]; aw; move=> [z [zE sy]]; exists z; apply inc_segment;ue.
move=> [y xy].
exists (segment r y); aw; split; first by apply segment_inc=>//; order_tac.
have yE:(inc y E) by rewrite /E; order_tac.
ex_tac.
have AE: sub A E by move=> t; rewrite Ap /E;move=> [y xy]; order_tac.
split.
move=> p; apply extensionality=>// t tE.
rewrite Ap; apply exists_proof.
move: (p t)=>px; dneg aux; split =>//.
move=> y ysr; case: (total_order_pr2 tor tE ysr)=>//.
by move=> ty; elim (aux y).
move=> x [xs gr]; set_extens y => ys.
srw;split; first by apply AE.
aw; move=> xy. move: ys; rewrite Ap; move=> [z yz].
move: (gr _ (inc_lt2_substrate yz)) => aux.
rewrite xy in yz; move:tor=> [or _];order_tac.
move: ys; srw; aw; rewrite Ap; move => [yE yx].
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 set_of_segments_strict r:=
fun_image (substrate r) (fun x => (segment r x)).
Definition set_of_segments r:=
tack_on (set_of_segments_strict r) (substrate r).
Definition set_of_segments_iso r:=
BL (segment r) (substrate r) (set_of_segments_strict r).
Lemma inc_set_of_segments: forall r x, worder r ->
is_segment r x = inc x (set_of_segments r).
Proof.
rewrite /set_of_segments/set_of_segments_strict=> r x wor.
apply iff_eq => hyp.
move: (well_ordered_segment wor hyp).
case ; first by move=> ->; fprops.
move=> [y [ysr]] ->; aw; left; ex_tac.
move:wor=> [or wor].
move: hyp; aw; case.
by move=> [z [zr]] <-; apply segment_is_segment=>//.
by move=> ->; apply substrate_is_segment.
Qed.
Lemma segment_insetof: forall r x, worder r -> inc x (substrate r) ->
inc (segment r x) (set_of_segments r).
Proof.
move=> r x wo xsr. rewrite -inc_set_of_segments //.
apply segment_is_segment;fprops.
Qed.
Lemma segmentc_insetof: forall r x, worder r -> inc x (substrate r) ->
inc (segment_c r x) (set_of_segments r).
Proof.
move=> r x wo xsr. rewrite -inc_set_of_segments //.
apply tack_on_segment; fprops.
Qed.
Lemma sub_set_of_segments: forall r x, worder r ->
inc x (set_of_segments r) -> sub x (substrate r).
Proof. move=> r x wor; rewrite -inc_set_of_segments//.
apply sub_segment1.
Qed.
Lemma set_of_segments_axiom: forall r, worder r ->
transf_axioms (segment r) (substrate r) (set_of_segments_strict r).
Proof. rewrite /set_of_segments_strict=> r wor t ts; aw; ex_tac. Qed.
Lemma segment_monotone1: forall 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=> r x y tor xsr ysr sxy.
case (total_order_pr2 tor ysr xsr)=>//.
rewrite - segment_rw //.
move=> yis; move: (sxy _ yis); rewrite segment_rw; aw.
rewrite /glt; intuition.
Qed.
Lemma segment_injective: forall r x y, total_order r ->
inc x (substrate r) -> inc y (substrate r) -> segment r x = segment r y ->
x = y.
Proof.
move=> r x y 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.
Lemma segment_injective1: forall r x y, worder r ->
inc x (substrate r) -> inc y (substrate r) -> segment r x = segment r y ->
x = y.
Proof. move=> r x y wor; apply (segment_injective (worder_total wor)). Qed.
Lemma set_of_segments_iso_bijective:forall r, worder r ->
bijection (set_of_segments_iso r).
Proof.
move=> r wor; rewrite /set_of_segments_iso; apply bl_bijective.
apply set_of_segments_axiom=> //.
move=> u v; apply (segment_injective1 wor).
move=> y; rewrite /set_of_segments_strict; aw.
Qed.
Theorem set_of_segments_iso_isomorphism:forall r, worder r ->
order_isomorphism (set_of_segments_iso r) r
(inclusion_suborder (set_of_segments_strict r)).
Proof.
move=> r wor;move: (wor)=> [or worp].
move: (set_of_segments_axiom wor)=> ta.
red; rewrite /set_of_segments_iso;aw;ee.
apply (set_of_segments_iso_bijective wor).
move=> x y xsr ysr;aw; apply iff_eq.
by move=> hyp; ee; apply segment_monotone.
move=> [_ [_ ss]].
by apply segment_monotone1=>//; apply worder_total.
Qed.
Theorem set_of_segments_worder:forall r, worder r ->
worder (inclusion_suborder (set_of_segments r)).
Proof.
move=>r wor; move: (wor)=> [or worp];move: (worder_total wor)=> tor.
have oi: order (inclusion_suborder (set_of_segments r)) by fprops.
split=>//.
aw; move => x xsr nex.
set (y := intersection2 x (set_of_segments_strict r)).
case (emptyset_dichot y) => hy.
have xs: x = singleton (substrate r).
apply singleton_pr1=>//.
move=> z zx.
move: (xsr _ zx); rewrite /set_of_segments tack_on_rw; case=>//.
by move=> aux; empty_tac1 z; rewrite /y; apply intersection2_inc.
exists (substrate r); red; aw; rewrite xs; ee.
move=> z; rewrite singleton_rw /set_of_segments=> ->; aw; ee.
have ysr: (sub y (set_of_segments_strict r)).
by move => t ty;rewrite /y;apply (intersection2sub_second ty).
have segp: (forall a, inc a y -> exists u,
inc u (substrate r) & segment r u = a).
move=> a ay; move: (ysr _ ay); rewrite /set_of_segments_strict; aw.
pose cf a := choose (fun u => inc u (substrate r) & segment r u = a).
have cfp: forall a, inc a y ->
(inc (cf a) (substrate r) & segment r (cf a) = a).
by move=> a ay; rewrite /cf; apply choose_pr; apply segp.
set (z:= fun_image y cf).
have nez: nonempty z by move:hy=> [w wy]; rewrite /z;exists (cf w); aw; ex_tac.
have zsr: sub z (substrate r).
by rewrite /z=> t; aw; move=> [u [uy]] <-; move: (cfp _ uy)=> [res _].
move: (worp _ zsr nez)=> [a []]; aw=> asr lea.
have sax: (inc (segment r a) x).
move: asr; rewrite /z; aw; move=> [u [uy]] <-.
move: (cfp _ uy)=> [h res]; rewrite res; apply (intersection2_first uy).
exists (segment r a); red; aw; split=>//.
move=> b bx; aw.
split; first by apply xsr.
split; first by apply xsr.
move: (xsr _ bx); rewrite /set_of_segments; aw.
case; last by move=>->; apply sub_segment.
move=> h.
have biy: (inc b y) by rewrite /y;apply intersection2_inc.
have cbz: (inc (cf b) z) by rewrite/z; aw; ex_tac.
move: (lea _ cbz); aw.
move: (cfp _ biy)=> [p1 p2]; rewrite - {2} p2.
apply segment_monotone=>//.
Qed.
We consider a property A(g) that says that g is a family of orders indexed
by I, such that if the substrate of g(i) is a subset of the substrate of g(j)
then both ordering coincides on g(i). Moreover, for every i, j there is k such
that the substrate of g(k) is a subset of the substrates of g(i) and g(j).
We consider B(g,h), that says that h is an ordering on the union of the
substrates, compatible with g. There is a unique h, the union of g.
Definition common_extension_order g h:=
order h & substrate h = unionf (domain g) (fun a => (substrate (V a g))) &
(forall a, inc a (domain g) -> V a g = induced_order h (substrate (V a g))).
Definition common_extension_order_axiom g :=
fgraph g &
(forall x, inc x (domain g) -> order (V x g)) &
(forall a b, inc a (domain g) -> inc b (domain g )-> exists c,
inc c (domain g) & sub (substrate (V a g)) (substrate (V c g))
& sub (substrate (V b g)) (substrate (V c g))) &
(forall a b, inc a (domain g) -> inc b (domain g) ->
sub (substrate (V a g)) (substrate (V b g)) ->
V a g = induced_order (V b g) (substrate (V a g))).
Lemma order_merge1: forall g,
common_extension_order_axiom g -> common_extension_order g (unionb g).
Proof.
move=> g [fg [alo [eVV pVV]]].
have gu:(is_graph (unionb g)).
move=> t tu; move: (unionb_exists tu)=> [x [xdg xp]].
by move: (alo _ xdg); fprops=> h; apply (order_is_graph h).
set (E:=unionf (domain g) (fun a : Set => substrate (V a g))).
have ur: forall y,inc y E -> related (unionb g) y y.
rewrite /E=> y yE; move: (unionf_exists yE)=> [x [xdg xp]].
move: (alo _ xdg); fprops=> h; red; apply unionb_inc with x=>//; order_tac.
have su: substrate (unionb g)= E.
set_extens x; last by move=> xE; move: (ur _ xE)=> h; substr_tac.
rewrite inc_substrate_rw /E//; case; move=> [y Ju];
move: (unionf_exists Ju)=> [z [zdg zp]]; union_tac;
move: (alo _ zdg)=> h; substr_tac.
have cov: (forall x y, inc x (unionb g) -> inc y (unionb g) ->
exists u, inc u (domain g) & inc x (V u g) & inc y (V u g)).
move=> x y xu yu.
move: (unionf_exists xu) (unionf_exists yu)=> [a [adg ap]][b [bdg bp]].
move: (eVV _ _ adg bdg)=> [c [cdg [sac sbc]]].
exists c; split=>//.
move:(pVV _ _ adg cdg sac)(pVV _ _ bdg cdg sbc)=> Vag Vbg.
move: ap bp; rewrite Vag Vbg /induced_order; aw; intuition.
split.
red; ee; split=>//.
by rewrite su.
rewrite /related; move=> x y z p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg [p1c p2c]]].
move: (alo _ cdg)=> or; 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=>//.
move=> a adg; rewrite /induced_order; set_extens x => xs; aw.
split; first by union_tac.
move: (alo _ adg)=> [[ga _] _].
by move:(sub_graph_coarse_substrate ga); apply.
move: (unionb_exists (intersection2_first xs))=> [z [zdg zpr]].
move: (eVV _ _ adg zdg)=> [t [tdg [sa sz]]].
rewrite (pVV _ _ adg tdg sa). rewrite /induced_order.
apply intersection2_inc; last by apply (intersection2_second xs).
move: zpr; rewrite(pVV _ _ zdg tdg sz); rewrite /induced_order.
apply (intersection2_first).
Qed.
Lemma order_merge2: forall g h1 h2, common_extension_order_axiom g ->
common_extension_order g h1 ->
common_extension_order g h2 -> (h1 = h2).
Proof.
move=> g h1 h2 [gg [alo [eVV pVV]]] 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: is_pair 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: (unionf_exists pxs) (unionf_exists pys)=> [u [udg psu]][v [vdg qsv]].
move:(eVV _ _ udg vdg)=> [w [wdg [wu wv]]].
move: (vr _ wdg)(vr' _ wdg).
rewrite /induced_order=> V1 V2.
have: (inc x (V w g)) by rewrite V1/coarse; aw; ee.
by rewrite V2; aw; intuition.
Qed.
order h & substrate h = unionf (domain g) (fun a => (substrate (V a g))) &
(forall a, inc a (domain g) -> V a g = induced_order h (substrate (V a g))).
Definition common_extension_order_axiom g :=
fgraph g &
(forall x, inc x (domain g) -> order (V x g)) &
(forall a b, inc a (domain g) -> inc b (domain g )-> exists c,
inc c (domain g) & sub (substrate (V a g)) (substrate (V c g))
& sub (substrate (V b g)) (substrate (V c g))) &
(forall a b, inc a (domain g) -> inc b (domain g) ->
sub (substrate (V a g)) (substrate (V b g)) ->
V a g = induced_order (V b g) (substrate (V a g))).
Lemma order_merge1: forall g,
common_extension_order_axiom g -> common_extension_order g (unionb g).
Proof.
move=> g [fg [alo [eVV pVV]]].
have gu:(is_graph (unionb g)).
move=> t tu; move: (unionb_exists tu)=> [x [xdg xp]].
by move: (alo _ xdg); fprops=> h; apply (order_is_graph h).
set (E:=unionf (domain g) (fun a : Set => substrate (V a g))).
have ur: forall y,inc y E -> related (unionb g) y y.
rewrite /E=> y yE; move: (unionf_exists yE)=> [x [xdg xp]].
move: (alo _ xdg); fprops=> h; red; apply unionb_inc with x=>//; order_tac.
have su: substrate (unionb g)= E.
set_extens x; last by move=> xE; move: (ur _ xE)=> h; substr_tac.
rewrite inc_substrate_rw /E//; case; move=> [y Ju];
move: (unionf_exists Ju)=> [z [zdg zp]]; union_tac;
move: (alo _ zdg)=> h; substr_tac.
have cov: (forall x y, inc x (unionb g) -> inc y (unionb g) ->
exists u, inc u (domain g) & inc x (V u g) & inc y (V u g)).
move=> x y xu yu.
move: (unionf_exists xu) (unionf_exists yu)=> [a [adg ap]][b [bdg bp]].
move: (eVV _ _ adg bdg)=> [c [cdg [sac sbc]]].
exists c; split=>//.
move:(pVV _ _ adg cdg sac)(pVV _ _ bdg cdg sbc)=> Vag Vbg.
move: ap bp; rewrite Vag Vbg /induced_order; aw; intuition.
split.
red; ee; split=>//.
by rewrite su.
rewrite /related; move=> x y z p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg [p1c p2c]]].
move: (alo _ cdg)=> or; 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=>//.
move=> a adg; rewrite /induced_order; set_extens x => xs; aw.
split; first by union_tac.
move: (alo _ adg)=> [[ga _] _].
by move:(sub_graph_coarse_substrate ga); apply.
move: (unionb_exists (intersection2_first xs))=> [z [zdg zpr]].
move: (eVV _ _ adg zdg)=> [t [tdg [sa sz]]].
rewrite (pVV _ _ adg tdg sa). rewrite /induced_order.
apply intersection2_inc; last by apply (intersection2_second xs).
move: zpr; rewrite(pVV _ _ zdg tdg sz); rewrite /induced_order.
apply (intersection2_first).
Qed.
Lemma order_merge2: forall g h1 h2, common_extension_order_axiom g ->
common_extension_order g h1 ->
common_extension_order g h2 -> (h1 = h2).
Proof.
move=> g h1 h2 [gg [alo [eVV pVV]]] 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: is_pair 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: (unionf_exists pxs) (unionf_exists pys)=> [u [udg psu]][v [vdg qsv]].
move:(eVV _ _ udg vdg)=> [w [wdg [wu wv]]].
move: (vr _ wdg)(vr' _ wdg).
rewrite /induced_order=> V1 V2.
have: (inc x (V w g)) by rewrite V1/coarse; aw; ee.
by rewrite V2; aw; intuition.
Qed.
A variant of the previous definition. We assume that the substrates s(i)
and s(j) of g(i) or g(j) are segments one of the other; moreover g(i) is
well-ordered. There exists a unique h, as above, with additional properties.
Definition common_worder_axiom g:=
fgraph g &
(forall x, inc x (domain g) -> worder (V x g)) &
(forall a b, inc a (domain g) -> inc b (domain g) ->
is_segment (V a g) (substrate (V b g))
\/ is_segment (V b g) (substrate (V a g))) &
(forall a b, inc a (domain g) -> inc b (domain g) ->
sub (substrate (V a g)) (substrate (V b g)) ->
V a g = induced_order (V b g) (substrate (V a g))).
Lemma order_merge3: forall g,
common_worder_axiom g -> common_extension_order_axiom g.
Proof.
move=> g [fg [alwo [eVV pVV]]].
red; ee.
move=> a b adg bdg;case (eVV _ _ adg bdg); rewrite /is_segment;move => [ss _].
exists a; ee.
exists b; ee.
Qed.
Lemma order_merge4: forall g,
common_worder_axiom g -> common_extension_order g (unionb g).
Proof. by move=> g ga; apply order_merge1; apply order_merge3. Qed.
Lemma order_merge5: forall g h1 h2, common_worder_axiom g ->
common_extension_order g h1 ->
common_extension_order g h2 -> (h1 = h2).
Proof.
move=> g h1 h2 ca a1 a2.
apply (order_merge2 (order_merge3 ca) a1 a2).
Qed.
Theorem worder_merge: forall g, common_worder_axiom g ->
( (common_extension_order g (unionb g)) &
worder (unionb g) &
(forall a x, inc a (domain g) -> is_segment (V a g) x
-> is_segment (unionb g) x ) &
(forall a x, inc a (domain g) -> inc x (substrate (V a g)) ->
segment (V a g) x = segment (unionb g) x) &
(forall x, is_segment (unionb g) x ->
x = substrate (unionb g) \/
exists a, inc a (domain g) & is_segment (V a g) x)).
Proof.
move=> g co.
move: (order_merge4 co)=>coe;split=>//.
move: coe=> [oh [sh Vag]].
have p1: (forall a, inc a (domain g) ->
sub (substrate (V a g)) (substrate (unionb g))).
by move=> a adg; rewrite sh; move=> t ts; apply unionf_inc with a.
have p2: (forall a, inc a (domain g) ->
is_segment (unionb g) (substrate(V a g))).
move=> a adg;split; first by apply p1.
move=> x y xs yx.
have ys: (inc y (substrate (unionb g))) by order_tac.
case (unionf_exists yx); move=> u [udg Jv].
move:co => [_ [_ [h _]]]; case:(h _ _ adg udg); move=> [p p'].
apply p; substr_tac.
apply (p' _ _ xs Jv).
have p3:(forall a x, inc a (domain g) -> inc x (substrate (V a g))
-> segment (V a g) x = segment (unionb g) x).
move=> a x adg xs; set_extens y => ys; move: (inc_segment ys) => [yx nyx].
rewrite segment_rw.
by split=>//; apply unionb_inc with a.
rewrite segment_rw //;split=>//.
move: (unionf_exists yx)=> [b [bdg Jv]]; rewrite (Vag _ adg); aw.
move: co=> [_ [_ [h _]]]; case:(h _ _ adg bdg); move=> [p p'].
apply p; substr_tac.
apply (p' _ _ xs Jv).
have p4: (forall a x, inc a (domain g) -> is_segment (V a g) x ->
is_segment (unionb g) x).
move=> a x adg sa; move:co=> [_ [wo _]]; move: (wo _ adg)=> woa.
case (well_ordered_segment woa sa).
by move=> ->; apply p2.
move=> [y [ysV]] ->; rewrite (p3 _ _ adg ysV); apply segment_is_segment=>//.
by apply (p1 _ adg).
have p5: worder (unionb g).
split=>//; move=> x xsr [y yx].
move: (xsr _ yx)=> ysr; rewrite sh in ysr.
move: (unionf_exists ysr) => [a [adg ysVa]].
set (x1:= intersection2 x (substrate (V a g))).
have sx1s: (sub x1 (substrate (V a g))) by apply intersection2sub_second.
have nx1: nonempty x1 by exists y; apply intersection2_inc.
move: co => [_ [wo' [sos _]]]; move: (wo' _ adg)=>[oa wo].
move: (wo _ sx1s nx1)=> [z[]]; aw=>zs zle.
have zx: inc z x by apply (intersection2_first zs).
have zVa: inc z (substrate (V a g)) by apply (intersection2_second zs).
exists z; red; aw; split=> //.
move=> t tx; aw.
move: (xsr _ tx); rewrite sh => tu; move: (unionf_exists tu)=> [b [bdg bV]].
have aux: inc t (substrate (V a g)) -> gle (unionb g) z t.
move=> hyp.
have tx1: inc t x1 by apply intersection2_inc.
by move: (zle _ tx1); aw; rewrite Vag //; aw.
case: (sos _ _ adg bdg); move => [p p'].
apply (aux (p _ bV)).
move: (p _ zVa)=> zVb.
case: (total_order_pr2 (worder_total (wo' _ bdg)) bV zVb).
move=> [tz ntz]; apply (aux (p' _ _ zVa tz)).
by rewrite Vag//; aw.
ee.
move=> x seg.
case (well_ordered_segment p5 seg); first by auto.
move=>[y [ysr]] ->; right.
rewrite sh in ysr; move: (unionf_exists ysr)=> [a [adg ap]]; exists a.
split=>//.
rewrite -(p3 _ _ adg ap); apply segment_is_segment => //.
move: co => [_ [wo' _]]; intuition.
Qed.
Let O(x) and C(x) be the set of all elements less than (resp. less or
equal than) x. These are segments, and C(x) is the union of O(x) and the
singleton x. In a well-ordered set every segment S is of the form C(x) or
the union of all segments of S, distinct from S. Consequence: a set of segments,
stable by union, and stable by the mapping O->C contains all segments.
Lemma transfinite_principle1: forall r s,
worder r -> (forall x, inc x s -> is_segment r x) ->
(forall s', sub s' s -> inc (union s') s) ->
(forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segment_c r x) s) ->
(forall x, is_segment r x -> inc x s).
Proof.
move=> r s wo als su sc x sx.
have or: order r by move: wo=> [].
move: (set_of_segments_worder wo) => woi.
set (cs:= complement (set_of_segments r) s).
case (emptyset_dichot cs) => necs.
rewrite inc_set_of_segments // in sx.
have nc: (~ inc x cs) by rewrite necs; case; case.
apply (use_complement sx nc).
have scs: sub cs (set_of_segments r) by rewrite /cs; apply sub_complement.
move: woi=> []; aw => oi woi; move: (woi _ scs necs).
move=> [y []]; aw; move=> ycs hyp; clear woi.
move: (scs _ ycs)=> yssr.
have nys: ~ (inc y s).
by move: ycs; rewrite /cs; srw; move=> [_]; apply.
have ysr:(sub y (substrate r)) by apply sub_set_of_segments=>//.
have woi: worder (induced_order r y) by apply worder_restriction.
case (p_or_not_p (exists a, greatest_element (induced_order r y) a)).
move=> [a []]; aw => [ay pa].
move: (ysr _ ay)=> asr.
have ysc: (y = segment_c r a).
set_extens t => ts.
by move: (pa _ ts); aw;rewrite segmentc_rw //.
move: ts; rewrite segmentc_rw // => ta.
move: yssr;rewrite -inc_set_of_segments//; move => [_ aux].
apply (aux _ _ ay ta).
case (p_or_not_p (inc (segment r a) cs))=> h.
move: (hyp _ h); aw; move=> [_[_ ysa]].
elim (not_in_segment (ysa _ ay)).
have p1: (inc (segment r a) (set_of_segments r)) by apply segment_insetof.
by elim nys; rewrite ysc; apply sc =>//; apply (use_complement p1 h).
move=> nge.
have aux: (forall x : Set, ~ greatest_element (induced_order r y) x).
by move=> b ngeb; elim nge; exists b.
move: (union_segments (worder_total woi))=> [unm _].
move: (unm aux)=> us; clear aux unm; awi us => //.
elim nys; rewrite -us; apply su.
move => z; aw; move => [u [uy zv]].
case (inc_or_not z cs) => zcs.
move: (hyp _ zcs); aw; move=> [_ [_ yz]]; move: (yz _ uy).
rewrite -zv=> aux; elim (not_in_segment aux).
rewrite -inc_set_of_segments // in yssr.
have siu: (is_segment (induced_order r y) z).
rewrite - zv; apply segment_is_segment; fprops; aw.
have zsr: (inc z (set_of_segments r)).
rewrite - inc_set_of_segments //.
apply (subsegment_is_segment or yssr siu).
by apply (use_complement zsr zcs).
Qed.
Lemma transfinite_principle2: forall r s,
worder r -> (forall x, inc x s -> is_segment r x) ->
(forall s', sub s' s -> inc (union s') s) ->
(forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segment_c r x) s) ->
inc (substrate r) s.
Proof.
move=> r s p1 p2 p3 p4.
move: (transfinite_principle1 p1 p2 p3 p4) => p5.
move: p1 => [or _].
move: (substrate_is_segment or).
apply p5.
Qed.
Two proofs of the transfinite principle; either by application of the
previous lemma or direct proof
Theorem transfinite_principle: forall r (p:Set -> Prop),
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 => r p wor hyp x xsr.
have or: order r by move: wor=> [or _].
set (s:= Zo (set_of_segments r)(fun z => forall y, inc y z -> p y)).
have alseg: forall x, inc x s -> is_segment r x.
by move=> t;rewrite /s Z_rw - inc_set_of_segments //; intuition.
have su:forall s', sub s' s -> inc (union s') s.
move=> s' s's ;rewrite /s Z_rw - inc_set_of_segments //.
split.
apply union_is_segment =>//.
by move=> t ts'; apply alseg; apply s's.
move=> y yu; move: (union_exists yu)=> [v [yv vs]].
by move: (s's _ vs); rewrite /s Z_rw; move=> [_]; apply.
have seg: forall x, inc x (substrate r) -> inc (segment r x) s ->
inc (segment_c r x) s.
move=> y ysr yxs; rewrite /s; apply Z_inc.
rewrite - inc_set_of_segments //; apply tack_on_segment =>//.
move: yxs; rewrite /s Z_rw;move=> [p1 p2].
move=> z; rewrite - segment_c_pr // tack_on_rw.
case; first by apply p2.
move=> ->; apply hyp =>//. move=> t tsr ty; apply p2. fprops.
by apply segment_inc.
move: (transfinite_principle2 wor alseg su seg).
by rewrite Z_rw;move => [_]; apply.
Qed.
Theorem transfinite_principle_bis: forall r (p:Set-> Prop),
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 => r p [or wor] hyp x xsr.
case (p_or_not_p (p x)) =>//npx.
set (X:=Zo (substrate r) (fun x => ~ p x)).
have neX: (nonempty X) by exists x; rewrite /X; apply Z_inc.
have Xsr: sub X (substrate r) by rewrite/X; apply Z_sub.
move:(wor _ Xsr neX)=> [y []]; aw => yX yle.
move: (yX); rewrite /X Z_rw; move=> [ysr npy].
elim npy; apply hyp =>//.
move=> t tsr ty; case (p_or_not_p (p t))=>// npt.
have tX: inc t X by rewrite /X; apply Z_inc.
move: (yle _ tX); aw =>//; move=> nty; order_tac.
Qed.
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 => r p wor hyp x xsr.
have or: order r by move: wor=> [or _].
set (s:= Zo (set_of_segments r)(fun z => forall y, inc y z -> p y)).
have alseg: forall x, inc x s -> is_segment r x.
by move=> t;rewrite /s Z_rw - inc_set_of_segments //; intuition.
have su:forall s', sub s' s -> inc (union s') s.
move=> s' s's ;rewrite /s Z_rw - inc_set_of_segments //.
split.
apply union_is_segment =>//.
by move=> t ts'; apply alseg; apply s's.
move=> y yu; move: (union_exists yu)=> [v [yv vs]].
by move: (s's _ vs); rewrite /s Z_rw; move=> [_]; apply.
have seg: forall x, inc x (substrate r) -> inc (segment r x) s ->
inc (segment_c r x) s.
move=> y ysr yxs; rewrite /s; apply Z_inc.
rewrite - inc_set_of_segments //; apply tack_on_segment =>//.
move: yxs; rewrite /s Z_rw;move=> [p1 p2].
move=> z; rewrite - segment_c_pr // tack_on_rw.
case; first by apply p2.
move=> ->; apply hyp =>//. move=> t tsr ty; apply p2. fprops.
by apply segment_inc.
move: (transfinite_principle2 wor alseg su seg).
by rewrite Z_rw;move => [_]; apply.
Qed.
Theorem transfinite_principle_bis: forall r (p:Set-> Prop),
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 => r p [or wor] hyp x xsr.
case (p_or_not_p (p x)) =>//npx.
set (X:=Zo (substrate r) (fun x => ~ p x)).
have neX: (nonempty X) by exists x; rewrite /X; apply Z_inc.
have Xsr: sub X (substrate r) by rewrite/X; apply Z_sub.
move:(wor _ Xsr neX)=> [y []]; aw => yX yle.
move: (yX); rewrite /X Z_rw; move=> [ysr npy].
elim npy; apply hyp =>//.
move=> t tsr ty; case (p_or_not_p (p t))=>// npt.
have tX: inc t X by rewrite /X; apply Z_inc.
move: (yle _ tX); aw =>//; move=> nty; order_tac.
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).
Definition restriction_to_segment_axiom r x g :=
worder r & inc x (substrate r) & is_function g & sub (segment r x) (source g).
Lemma rts_function: forall r x g, restriction_to_segment_axiom r x g ->
is_function (restriction_to_segment r x g).
Proof.
move=> r x g [p1 [p2 [p3 p4]]].
by rewrite /restriction_to_segment; apply restriction1_function.
Qed.
Lemma rts_W: forall r x g a, restriction_to_segment_axiom r x g ->
glt r a x -> W a (restriction_to_segment r x g) = W a g.
Proof.
move=> r x g a [p1 [p2 [p3 p4]]] ax.
rewrite /restriction_to_segment; apply restriction1_W =>//.
rewrite /segment/interval_uo; apply Z_inc=>//; order_tac.
Qed.
Lemma rts_surjective: forall r x g, restriction_to_segment_axiom r x g ->
surjection (restriction_to_segment r x g).
Proof.
move=> r x g [p1 [p2 [p3 p4]]] .
rewrite /restriction_to_segment.
by apply restriction1_surjective.
Qed.
Lemma rts_extensionality: forall r s x f g,
worder r -> inc x (substrate r) -> worder s -> inc x (substrate s) ->
segment r x = segment s x ->
is_function f -> sub (segment r x) (source f) ->
is_function g -> sub (segment s x) (source g) ->
(forall a , inc a (segment r x) -> W a f = W a g) ->
restriction_to_segment r x f = restriction_to_segment s x g.
Proof.
move=> r s x f g wor xsr wos xss srsx ff srf fg ssg sv.
have rf: (restriction_to_segment_axiom r x f) by red; ee.
have rg: (restriction_to_segment_axiom s x g) by red; ee.
apply function_exten =>//; try apply rts_function;
try solve [rewrite /restriction_to_segment/restriction1; aw].
rewrite /restriction_to_segment/restriction1; aw.
set_extens t;aw; move=> [u [us Wu]]; exists u.
by rewrite - srsx -sv //; split.
by rewrite srsx sv; [ split=>// | ue].
move=> u. rewrite /restriction_to_segment/restriction1; aw.
move=> us.
have p1: glt r u x by apply (inc_segment us).
have p2: glt s u x by rewrite srsx in us;apply (inc_segment us); ue.
rewrite rts_W // rts_W // sv //.
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.
Definition transfinite_def r p f :=
surjection f & source f = substrate r &
forall x, inc x (substrate r) -> W x f = p (restriction_to_segment r x f).
Definition transfinite_defined r p:= choose (fun f => transfinite_def r p f).
Lemma transfinite_unique1: forall r p f f' z, worder r ->
inc z (substrate r) ->
transfinite_def r p f -> transfinite_def r p f' ->
(forall x : Set, inc x (segment r z) -> W x f = W x f') ->
restriction_to_segment r z f = restriction_to_segment r z f'.
Proof.
move=> r p f f' z wo zsr [[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: forall r p f f', worder r ->
transfinite_def r p f -> transfinite_def r p f' -> f = f'.
Proof.
move=> r p f f' wo tf tf'.
set (s:=Zo(set_of_segments r) (fun z => forall x, inc x z -> W x f = W x f')).
move: (wo)=> [or _].
have alse:forall x, inc x s -> is_segment r x.
move=> x;rewrite /s Z_rw inc_set_of_segments//; intuition.
have su: forall s', sub s' s -> inc (union s') s.
move=> s' s's; rewrite /s Z_rw -inc_set_of_segments//.
split.
apply union_is_segment =>//; move=> x xs'; move: (s's _ xs'); apply alse.
move=> x xu; move: (union_exists xu)=> [y [xy ys']].
by move: (s's _ ys'); rewrite /s Z_rw; move =>[_];apply.
have sc: forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segment_c r x) s.
move=> x xsr; rewrite /s 2! Z_rw -inc_set_of_segments//.
move=> [s1 sW]; split; first by apply segmentc_insetof=>//.
move=> y; rewrite -segment_c_pr; aw.
case; first by apply sW.
move=> ->.
move: (transfinite_unique1 wo xsr tf tf' sW) => sWx.
by move: tf tf'=> [_[_ pf]] [_[_ pf']]; rewrite pf // pf' // sWx.
move: (transfinite_principle2 wo alse su sc).
rewrite /s Z_rw; move=> [_ asW].
move:tf tf'=> [suf [sf _]][suf' [sf' _ ]].
apply function_exten; try fct_tac; try ue.
set_extens y => yt.
move: (surjective_pr2 suf yt)=> [z [zs ]] <-.
rewrite sf in zs; rewrite asW //; rewrite -sf' in zs.
apply inc_W_target=>//; fct_tac.
move: (surjective_pr2 suf' yt)=> [z [zs ]] <-.
rewrite sf' in zs; rewrite -asW //; rewrite -sf in zs.
apply inc_W_target=>//; fct_tac.
Qed.
Lemma transfinite_pr: forall r x p, worder r -> transfinite_def r p x ->
transfinite_defined r p = x.
Proof.
move=> r x p 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.
Lemma transfinite_aux1: forall r p s' s'' f' f'',
worder r -> is_segment r s' -> is_segment 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=> r p s' s'' f' f'' wo ss' ss'' is'' tf' tf''.
set (f:=restriction1 f'' s').
have or:order r by fprops.
have s''s: sub s'' (substrate r) by move: ss''=>[q _]; exact q.
have ff'':is_function f'' by move: tf''=> [sf _]; fct_tac.
have s's: sub s' (substrate r) by move: ss'=>[q _]; exact q.
have woi: worder (induced_order r s') by apply worder_restriction.
have s'sf'': sub s' (source f'') by move: tf''=> [_ [sf'' _]]; rewrite sf''; aw.
have sf: source f = s' by rewrite /f/restriction1; aw.
have suf: surjection f by rewrite /f; apply restriction1_surjective=>//.
have ff: is_function f by fct_tac.
suff: transfinite_def (induced_order r s') p f.
by apply (transfinite_unique woi tf').
red; ee; 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 move:tf''=>[_ [sf'' _]]; rewrite sf''; apply sub_segment.
have p3: (forall a, inc a s' -> W a f = W a f'').
move=> a as''; rewrite /f restriction1_W //.
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.
apply worder_restriction =>//.
do 2 rewrite segment_induced_a //.
by move=> a asi; apply p3; rewrite -sf; apply p1.
by move: tf''=>[_ [_ h]]; rewrite - (h _ xsi); apply p3.
Qed.
Lemma transfinite_aux2: forall r p s tdf, worder r ->
(forall z, inc z s -> is_segment r z) ->
(forall z, inc z s -> transfinite_def (induced_order r z) p (tdf z)) ->
exists f,
(transfinite_def (induced_order r (union s)) p f &
target f = unionf s (fun z => target (tdf z))).
Proof.
move=> r p s tdf wo alseg altd.
have or: order r by fprops.
have alfun:forall i, inc i s -> is_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 _]]; awi so =>//.
by move: (alseg _ ins)=> [q _].
set (t:=unionf s (fun z => target (tdf z))).
set (tde:= fun z => corresp (source (tdf z)) t (graph (tdf z))).
have fpe:forall i, inc i s -> function_prop (tde i) i t.
move=>i ins; move: (alfun _ ins)=> fd; rewrite /tde; red; aw; ee.
apply is_function_pr; fprops.
apply sub_trans with (target (tdf i)); first by apply f_range_graph.
rewrite /t=> x xt; union_tac.
rewrite - f_domain_graph //.
have Wfe:forall i a, inc i s-> inc a i -> W a (tdf i) = W a (tde i).
move=> i a ins ai.
set (x:= W a (tde i)).
have : (inc (J a x) (graph (tde i))).
rewrite /x; move: (fpe _ ins)=> [fu [st tg]]; apply W_pr3 =>//; ue.
by rewrite /tde; aw; apply W_pr; apply alfun.
have agr: (forall i j, inc i s -> inc j s -> sub i j ->
agrees_on (intersection2 i j) (tde i) (tde j)).
move=> i j ins jns ij.
have ->: (intersection2 i j = i) by rewrite -intersection2_sub.
move: (fpe _ ins)(fpe _ jns)=> [ffi [sfi tfi]][ffj [sfj tfj]].
red; rewrite sfi sfj; ee.
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_W =>//; [ by apply alfun | by rewrite slso].
have agr':forall i j, inc i s -> inc j s ->
agrees_on (intersection2 i j) (tde i) (tde j).
move=> i j ins jns.
case (segment_dichot_sub wo (alseg _ ins) (alseg _ jns)).
by apply agr.
rewrite intersection2C.
move=> ji; move: (agr _ _ jns ins ji); rewrite /agrees_on.
by move => [s1 [s2 sv]]; ee; move => a ai; symmetry; apply sv.
have su:sub (union s) (substrate r).
move=> v vu; move: (union_exists vu)=> [i [vi ins]].
by move: (alseg _ ins)=> [q _]; apply q.
move: (extension_covering fpe agr') => [ [f [[sf [tf gf]]] agf] _].
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).
exists f; split=>//.
split.
apply surjective_pr6=>//.
rewrite gf=> y; rewrite /t=> yt; move: (unionf_exists yt)=> [i [ins ti]] .
move: (altd _ ins)=> [sfi [sofi vfi]].
move:(surjective_pr2 sfi ti)=> [z [zs Wz]].
rewrite (slso _ ins) in zs.
move: (agf _ ins)=> [sis [_ prop]].
have zf: inc z (source f) by apply sis.
by ex_tac; rewrite -Wz Wfe//; apply prop.
aw; rewrite -union_prop in tf.
split=>//.
move=> x xu; move: (union_exists xu)=> [i [xi ins]].
have ap:forall a, inc a i -> W a f = W a (tdf i).
by move=> a ai; move: (agf _ ins)=> [sis [_ prop]]; rewrite Wfe // prop //.
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 union_is_segment =>//.
have p4: sub (segment r x) i.
move: (alseg _ ins) => [_ si] y; rewrite segment_rw.
move=> [xle _]; apply (si _ _ xi xle).
apply rts_extensionality =>//; rewrite ? p2 ? p3;
try apply worder_restriction=>//; aw.
rewrite tf; move=> u us; move: (p4 _ us)=> ui; union_tac.
by apply alfun.
by rewrite slso.
move=> a asr; apply (ap _ (p4 _ asr)).
move: (altd _ ins)=> [_ [_]]; rewrite ap=>//;apply; aw.
Qed.
Lemma transfinite_aux3: forall 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 (segment_c r x)) p
(tack_on_f g x (p (restriction_to_segment r x g))).
Proof.
move=> r p x g 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:= segment_c 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: (tack_on_surjective (p h) sug nxsg) => sto.
have tos:tack_on (segment r x) x = tsx by rewrite /tsx segment_c_pr//.
red;rewrite sioc; ee.
rewrite /tack_on_f; aw; ue.
move=> y ytsx.
have syx: (sub (segment r y) (segment r x)).
move: ytsx; rewrite segmentc_rw=>//; apply segment_monotone =>//.
have fto: is_function (tack_on_f g x (p h)) by fct_tac.
have soto: source (tack_on_f g x (p h)) = tsx.
by rewrite/tack_on_f; aw; rewrite sog //.
have fg: is_function g by fct_tac.
have p2: segment (induced_order r tsx) y = segment r y.
apply segment_induced_a =>//.
rewrite /tsx; apply tack_on_segment=>//.
case (equal_or_not y x) => yx.
rewrite yx tack_on_W_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.
by apply worder_restriction.
rewrite soto p2; fprops.
move=> a asr; rewrite tack_on_W_in //; ue.
have ysx: inc y (segment r x) by move: ytsx; rewrite -tos; aw;case; intuition.
have p1: (forall u, inc u (segment r x) -> W u g = W u (tack_on_f g x (p h))).
move=> u usx; rewrite tack_on_W_in //; ue.
have p3: segment (induced_order r (segment r x)) y = segment r y.
by apply segment_induced_a =>//; apply segment_is_segment =>//.
rewrite -p1 // Wg //.
apply f_equal.
apply rts_extensionality =>//; rewrite ? p2 ? p3 ? soto ? sog;
try apply worder_restriction=>//;aw.
apply sub_trans with (segment r x) => //.
rewrite -tos; fprops.
move=> a asr; apply (p1 _ (syx _ asr)).
Qed.
Theorem transfinite_definition: forall r p,
worder r -> exists_unique (transfinite_def r p).
Proof.
move=> r p wo.
set (s:=Zo(set_of_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 -> is_segment r x.
move=> x;rewrite /s Z_rw -inc_set_of_segments; intuition.
have srs: inc (substrate r) s.
apply transfinite_principle2=>//.
move=> s' s's.
have als': (forall x : Set, inc x s' -> is_segment r x).
by move=> x xs'; apply (als _ (s's _ xs')).
rewrite /s; apply Z_inc.
rewrite -inc_set_of_segments => //; apply union_is_segment =>//.
set(tdf:= fun 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'); rewrite /s Z_rw;move=> [p1 p2].
apply (choose_pr p2).
move: (transfinite_aux2 wo als' atdf) => [f [fp1 fp2]].
by exists f.
move=> x xst; rewrite /s 2! Z_rw; move=> [_ [f tdf]].
split; first by apply segmentc_insetof => //.
exists (tack_on_f f x (p (restriction_to_segment r x f))).
apply (transfinite_aux3 wo xst tdf).
move: srs; rewrite /s Z_rw; rewrite induced_order_substrate //; move=> [_ ef].
split=> //.
move=> x y;apply (transfinite_unique wo).
Qed.
Theorem transfinite_definition_stable: forall r p F,
worder r ->
(forall f, is_function f -> is_segment r (source f) -> sub (target f) F ->
inc (p f) F) ->
sub (target (transfinite_defined r p)) F.
Proof.
move=> r p F wo hyp.
set (s:=Zo(set_of_segments r) (fun z =>
exists 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 -> is_segment r x.
move=> x;rewrite /s Z_rw -inc_set_of_segments; intuition.
have: inc (substrate r) s.
apply transfinite_principle2=>//.
move=> s' s's.
have als': (forall x : Set, inc x s' -> is_segment r x).
by move=> x xs'; apply (als _ (s's _ xs')).
rewrite /s; apply Z_inc.
rewrite -inc_set_of_segments => //; apply union_is_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'); rewrite /s Z_rw;move=> [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) => [f [fp1 fp2]].
exists f ; split =>//.
rewrite fp2.
move => u uu; move: (unionf_exists uu)=> [v [vs' uv]].
move: (s's _ vs'); rewrite /s Z_rw; move=> [vs [g [tdg tg]]].
move: (atdf _ vs') => tdf1.
have wa: (worder (induced_order r v)).
apply worder_restriction =>//; apply sub_segment1; apply (als' _ vs').
rewrite (transfinite_unique wa tdg tdf1) in tg.
by apply tg.
move=> x xst; rewrite /s 2! Z_rw; move=> [_ [f [tdf tfF]]].
split; first by apply segmentc_insetof => //.
exists (tack_on_f f x (p (restriction_to_segment r x f))).
split; first by apply (transfinite_aux3 wo xst tdf).
have srx: (sub (segment r x) (substrate r)) by apply sub_segment.
rewrite /tack_on_f; move=> t; aw.
case; first by apply tfF.
move: (tdf)=> [sf [sof Wf]].
have ff: is_function f by fct_tac.
have ssf: sub (segment r x) (source f) by rewrite sof; aw; fprops.
move => ->; apply hyp.
apply rts_function; red; ee.
rewrite /restriction_to_segment/restriction1; aw.
apply segment_is_segment=>//.
rewrite /restriction_to_segment/restriction1; aw.
move=> v; aw =>//; move => [u [us ]] <-; apply tfF.
by apply inc_W_target =>//; apply ssf.
rewrite /s Z_rw; move => [p1 [f [tdf tfF]]].
have aux: (induced_order r (substrate r) =r).
by apply induced_order_substrate.
rewrite aux in tdf.
have ->: (transfinite_defined r p = f) by apply (transfinite_pr wo tdf).
done.
Qed.
Lemma transfinite_defined_pr: forall r p, worder r ->
transfinite_def r p (transfinite_defined r p).
Proof.
move=> r p wo; rewrite /transfinite_defined.
move: (transfinite_definition p wo) => [res _].
by apply choose_pr.
Qed.
Given an ordering, let Sx be the segment with endpoint x,
considered as an ordered set. Given two orderings, we consider the set of
all x with Sx=Sx'.
This is a segment, ordered by any of the two induced orders.
Definition common_ordering_set r r' :=
Zo (intersection2 (substrate r) (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: forall r r',
common_ordering_set r r' = common_ordering_set r' r.
Proof.
move=> r r'; rewrite /common_ordering_set intersection2C.
set_extens t; rewrite 2! Z_rw; intuition.
Qed.
Lemma Zermelo_aux1: forall r r', worder r -> worder r' ->
is_segment r (common_ordering_set r r').
Proof.
rewrite /common_ordering_set=>r r' wor wor'.
split; first by move=> t; rewrite Z_rw; aw; intuition.
move=> x y; rewrite 2! Z_rw; aw; move=> [[xr xr'] [srr' iorr']] yx.
case (equal_or_not y x); first by move=> ->; intuition.
move=> hyp.
have ltyx:glt r y x by split.
have sry: inc y (segment r x) by rewrite segment_rw.
have sry': inc y (segment r' x) by rewrite -srr'.
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 -srr' in iorr'.
have or: order r by fprops.
have or': order r' by fprops.
split; first by split.
have sryy': (segment r y = segment r' y).
set_extens t; rewrite segment_rw//;move=> [ty nty];
apply segment_inc =>//; split=>//;
suff: (inc (J t y) (intersection2 r (coarse (segment r x)))).
rewrite iorr'; aw; intuition.
apply intersection2_inc=>//; apply product_pair_inc=>//.
apply (le_in_segment or xr sry ty).
aw; intuition.
rewrite iorr';apply intersection2_inc=>//; apply product_pair_inc=>//.
rewrite srr';apply (le_in_segment or' xr' sry' ty).
split=>//.
rewrite /induced_order -sryy'.
move: (coarse_segment_monotone or yx)=> p1.
set_extens z; aw;move=> [zr zc]; split=>//;
suff: (inc z (intersection2 r (coarse (segment r x)))).
by rewrite iorr'; aw; intuition.
by apply intersection2_inc=>//; apply p1.
aw; intuition.
by rewrite iorr'; apply intersection2_inc=>//; apply p1.
Qed.
Lemma Zermelo_aux2: forall 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=> r r' v wor wor' vd.
have or: order r' by fprops.
move=> t; aw; move=> [tr [pt [Pt Qt]]]; ee.
have pv: J (P t) (Q t) = t by aw.
move: Qt; rewrite vd Z_rw; aw; move=> [[Qtr Qtr'] [ss io]].
case (equal_or_not (P t) (Q t)).
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.
Zo (intersection2 (substrate r) (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: forall r r',
common_ordering_set r r' = common_ordering_set r' r.
Proof.
move=> r r'; rewrite /common_ordering_set intersection2C.
set_extens t; rewrite 2! Z_rw; intuition.
Qed.
Lemma Zermelo_aux1: forall r r', worder r -> worder r' ->
is_segment r (common_ordering_set r r').
Proof.
rewrite /common_ordering_set=>r r' wor wor'.
split; first by move=> t; rewrite Z_rw; aw; intuition.
move=> x y; rewrite 2! Z_rw; aw; move=> [[xr xr'] [srr' iorr']] yx.
case (equal_or_not y x); first by move=> ->; intuition.
move=> hyp.
have ltyx:glt r y x by split.
have sry: inc y (segment r x) by rewrite segment_rw.
have sry': inc y (segment r' x) by rewrite -srr'.
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 -srr' in iorr'.
have or: order r by fprops.
have or': order r' by fprops.
split; first by split.
have sryy': (segment r y = segment r' y).
set_extens t; rewrite segment_rw//;move=> [ty nty];
apply segment_inc =>//; split=>//;
suff: (inc (J t y) (intersection2 r (coarse (segment r x)))).
rewrite iorr'; aw; intuition.
apply intersection2_inc=>//; apply product_pair_inc=>//.
apply (le_in_segment or xr sry ty).
aw; intuition.
rewrite iorr';apply intersection2_inc=>//; apply product_pair_inc=>//.
rewrite srr';apply (le_in_segment or' xr' sry' ty).
split=>//.
rewrite /induced_order -sryy'.
move: (coarse_segment_monotone or yx)=> p1.
set_extens z; aw;move=> [zr zc]; split=>//;
suff: (inc z (intersection2 r (coarse (segment r x)))).
by rewrite iorr'; aw; intuition.
by apply intersection2_inc=>//; apply p1.
aw; intuition.
by rewrite iorr'; apply intersection2_inc=>//; apply p1.
Qed.
Lemma Zermelo_aux2: forall 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=> r r' v wor wor' vd.
have or: order r' by fprops.
move=> t; aw; move=> [tr [pt [Pt Qt]]]; ee.
have pv: J (P t) (Q t) = t by aw.
move: Qt; rewrite vd Z_rw; aw; move=> [[Qtr Qtr'] [ss io]].
case (equal_or_not (P t) (Q t)).
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: forall E s p r r',
let q := fun r r' => sub (substrate r) (substrate r')
& r = induced_order r' (substrate r) & is_segment r' (substrate r) in
Zermelo_axioms E p s r -> Zermelo_axioms E p s r' ->
q r r' \/ q r' r.
Proof.
move=> E s p r r' 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; ee.
rewrite -io evr;symmetry; apply induced_order_substrate; fprops.
case: (equal_or_not v (substrate r')) => evr'.
right; rewrite /q -evr'; ee.
rewrite io evr';symmetry; apply induced_order_substrate; fprops.
case (emptyset_dichot (complement (substrate r) v)) => co.
by elim evr; apply extensionality=>//; apply empty_complement.
case (emptyset_dichot (complement (substrate r') v)) => co'.
by elim evr'; apply extensionality=>//; apply empty_complement.
have sc: (sub (complement (substrate r) v) (substrate r)).
by apply sub_complement.
have sc': (sub (complement (substrate r') v) (substrate r')).
by apply sub_complement.
move:(worder_total wor) (worder_total wor')=> tor tor'.
move:wor=> [or wo]; move: (wo _ sc co)=> [x []]; aw;srw ;move=> [xs xc] px.
move:wor'=> [or' wo']; move: (wo' _ sc' co')=> [y []]; aw;srw;move=>[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 (complement (substrate r) v) by srw; split=>//; order_tac.
move: (px _ zc) => h.
move: (iorder_gle1 h)=> xz; order_tac.
rewrite segment_rw //.
case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz.
elim 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 (complement (substrate r') v) by srw; split=>//; order_tac.
move: (py _ zc) => h.
move: (iorder_gle1 h)=> yz; order_tac.
rewrite segment_rw //.
case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz.
elim yc; move: svr'=> [_ h]; apply: (h _ _ zs yz).
have xy: x = y by rewrite - (pr _ xs) -(pr' _ ys) p1 p2.
elim xc.
rewrite /v /common_ordering_set; apply Z_inc.
aw; split=>//; ue.
rewrite p1 xy p2; split=>//.
Qed.
Lemma Zermelo_aux4: forall r a, worder r ->
let owg := order_with_greatest r a in
~ (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=> r a wor owg nas.
move:(worder_adjoin_greatest wor nas) => woe.
split=>//.
move: (order_with_greatest_pr (worder_is_order wor) nas)=> [oe [se [rv ge]]].
move: ge=>[asr prop].
split.
set_extens x => xs.
move:(inc_segment xs)=> xa.
move: (inc_lt1_substrate xa); rewrite se; aw; case =>//.
move: xa=>[_ nxa] xa; contradiction.
have ax: x <> a by dneg ax; rewrite -ax.
rewrite segment_rw //; split=>//; apply prop; rewrite se; fprops.
move=> x; rewrite se; aw; case; auto.
move=> xsr; right.
have xsre: inc x (substrate owg) by rewrite se; aw; fprops.
set_extens y; do 2 rewrite segment_rw // /glt; move=> [yx nyx]; split=>//.
red; red; rewrite rv; apply intersection2_inc =>//.
rewrite/ coarse; apply product_pair_inc=> //.
move: (inc_arg1_substrate yx).
rewrite se; aw; case =>//.
move=> ya; elim nyx.
move: (prop _ xsre); fold owg; rewrite -ya => p1; order_tac.
move: yx; rewrite /gle/related rv; aw; intuition.
Qed.
Lemma Zermelo_aux: forall E s p, sub s (powerset E) ->
(forall x, inc x s -> (inc (p x) E & ~ (inc (p x) x))) ->
exists r, Zermelo_axioms E p s r & (~ (inc (substrate r) s)).
Proof.
move=> E s p 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) & is_segment r' (substrate r).
have qq:(forall r r', inc r m -> inc r' m -> q r r' \/ q r' r).
move=> r r'; rewrite /m 2! Z_rw; move=> [rp za][rp' za'].
apply (Zermelo_aux3 za za').
set (g:= L m id).
have cog: common_worder_axiom g.
rewrite /g; red; bw; ee.
by move=> x xm; bw; move: xm; rewrite /m Z_rw; move=> [_ [a _]].
move=> a b am bm; bw.
move: am bm; rewrite /m 2! Z_rw; move=> [ac za][bc zb].
move: (Zermelo_aux3 za zb); intuition.
move=> a b am bm; bw.
move: am bm; rewrite /m 2! Z_rw; move=> [ac za][bc zb].
case: (Zermelo_aux3 za zb); first by intuition.
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.
rewrite ssab induced_order_substrate // bi -ssab induced_order_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 -> V a g = 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; ee; rewrite som0=> t tu; move: (unionf_exists tu)=> [u [ud ts]];
move: (ud); rewrite /m Z_rw; move => [_ [_ [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; split=>//.
move=> 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)).
split=>//; rewrite su.
move: Za=> [p1 [p2 [p3 p4]]]; ee; move=> t; aw; 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 Z_inc =>//.
apply powerset_inc.
apply sub_trans with (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 product_monotone.
elim nps.
rewrite som0.
apply unionf_inc with (order_with_greatest m0 a) =>//.
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: forall E, exists r, worder r & substrate r = E.
Proof.
move => E.
set (s:=complement (powerset E) (singleton E)).
have p1: sub s (powerset E) by rewrite /s; apply sub_complement.
set (p:= fun x => rep (complement E x)).
have p2: forall x, inc x s -> inc (p x) (complement E x).
move=> x xs; rewrite /p. apply nonempty_rep.
apply strict_sub_nonempty_complement.
move: xs; rewrite /s; srw; aw; red; intuition.
have p3: forall x, inc x s -> (inc (p x) E & ~ (inc (p x) x)).
move => x xs; move: (p2 _ xs); srw.
move: (Zermelo_aux p1 p3) => [r [[xor [so [alse ps]]]] ns].
exists r; split=> //.
have : (inc (substrate r) (complement (powerset E) s)) by srw; aw; split.
rewrite /s double_complement //; aw.
move=> t; aw; move=> ->; fprops.
Qed.
Definition inductive_set 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: forall a b,
inductive_set (opposite_order (extension_order a b)).
Proof.
move => a b.
move: (extension_is_order a b)=> or.
have ooi: order (opposite_order (extension_order a b)) by fprops.
move=> X; aw; move=> Xs toX.
have sXs :sub X (substrate (extension_order a b))
by rewrite substrate_extension_order.
have Ha:forall i, inc i X -> is_function i.
move=> i iX; move: (Xs _ iX); bw; intuition.
have Hb:forall i, inc i X -> target i = b.
move=> i iX; move: (Xs _ iX); bw; intuition.
move: toX=> [orX]; aw.
move=> tor.
have Hd: forall i j, inc i X -> inc j X ->
agrees_on (intersection2 (source i) (source j)) i j.
move=> i j iX jX.
split; first by apply intersection2sub_first.
split; first by apply intersection2sub_second.
move=> t; aw; move=> [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 X -> function_prop i (source i) b.
move=> i iX; red; ee.
move: (extension_covering He Hd) => [[g [[fg [sg tg]] agg]] _].
have gs: (inc g (set_of_sub_functions a b)).
bw;ee; move => t tsg.
rewrite sg in tsg; move: (unionf_exists tsg)=> [v [vx tv]].
by move: (Xs _ vx); bw; move=> [_ [sv _]]; apply sv.
exists g; red; aw; split=>//.
move=> y yX; move: (Xs _ yX)=> ys; move: (agg _ yX)=> ag.
have fy: (is_function y) by move: ys; bw;intuition.
bw; rewrite -[related]/gle extension_order_pr1;ee.
rewrite sub_function //.
move: ag; rewrite /agrees_on. move=> [p1 [p2 p3]].
by ee; move=> u; symmetry; apply p3.
Qed.
inductive_set (opposite_order (extension_order a b)).
Proof.
move => a b.
move: (extension_is_order a b)=> or.
have ooi: order (opposite_order (extension_order a b)) by fprops.
move=> X; aw; move=> Xs toX.
have sXs :sub X (substrate (extension_order a b))
by rewrite substrate_extension_order.
have Ha:forall i, inc i X -> is_function i.
move=> i iX; move: (Xs _ iX); bw; intuition.
have Hb:forall i, inc i X -> target i = b.
move=> i iX; move: (Xs _ iX); bw; intuition.
move: toX=> [orX]; aw.
move=> tor.
have Hd: forall i j, inc i X -> inc j X ->
agrees_on (intersection2 (source i) (source j)) i j.
move=> i j iX jX.
split; first by apply intersection2sub_first.
split; first by apply intersection2sub_second.
move=> t; aw; move=> [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 X -> function_prop i (source i) b.
move=> i iX; red; ee.
move: (extension_covering He Hd) => [[g [[fg [sg tg]] agg]] _].
have gs: (inc g (set_of_sub_functions a b)).
bw;ee; move => t tsg.
rewrite sg in tsg; move: (unionf_exists tsg)=> [v [vx tv]].
by move: (Xs _ vx); bw; move=> [_ [sv _]]; apply sv.
exists g; red; aw; split=>//.
move=> y yX; move: (Xs _ yX)=> ys; move: (agg _ yX)=> ag.
have fy: (is_function y) by move: ys; bw;intuition.
bw; rewrite -[related]/gle extension_order_pr1;ee.
rewrite sub_function //.
move: ag; rewrite /agrees_on. move=> [p1 [p2 p3]].
by ee; move=> u; symmetry; apply p3.
Qed.
Full and short version of Zorn's lemma
Theorem Zorn_aux: forall r, order r ->
(forall s, sub s (substrate r) -> worder (induced_order r s) ->
(bounded_above r s)) ->
exists a, maximal_element r a.
Proof.
move=> r 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; rewrite /s Z_rw /p;move => [_ ev]; apply choose_pr.
have sp: sub s (powerset E) by rewrite /s; apply Z_sub.
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].
move: up; rewrite /upper_bound; intuition.
move: (Zermelo_aux sp zp)=> [r' [[xor [so [alse ps]]]] ns].
have oi: order (induced_order r (substrate r')) by fprops.
have ext: sub r' (induced_order r (substrate r')).
have gr: is_graph r' by fprops.
move=> x xr.
move: (gr _ xr) => xp; rewrite - xp in xr |- *.
move: (inc_arg2_substrate xr) => qs.
move: (inc_arg1_substrate 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 rewrite segment_rw //.
move: (alse _ qs)(ps _ qs) => p1 p2; move: (apx _ p1).
by rewrite p2; rewrite /px; move=> [[_ h]] _; 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: is_graph (induced_order r (substrate r')) by fprops.
move: (p2 _ tio) => pt.
rewrite -pt in tio |- *.
have Ps: inc (P t) (substrate r') by move: (inc_arg1_substrate tio); aw.
have Qs: inc (Q t) (substrate r') by move: (inc_arg2_substrate tio); aw.
case (total_order_pr2 (worder_total xor) Qs Ps) =>//.
move=> [lePQ nPQ]; move: (ext _ lePQ)=>tio'; elim 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.
elim ns; rewrite /s Z_rw; aw.
split=>//; 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: forall r, order r -> inductive_set r ->
exists a, maximal_element r a.
Proof.
move=> r or isr; apply Zorn_aux =>//.
move=> s ssr wo; red; apply isr =>//.
by apply worder_total.
Qed.
Consequences
Lemma inductive_max_greater: forall r a, order r -> inductive_set r ->
inc a (substrate r) -> exists m, maximal_element r m & gle r a m.
Proof.
move=> r a or isr asr.
set (F:= Zo (substrate r)(fun z => gle r a z)).
have Fs: sub F (substrate r) by rewrite /F; apply Z_sub.
have oi: order (induced_order r F) by fprops.
have aF: inc a F by rewrite /F; apply Z_inc=> //; order_tac.
have isF: inductive_set (induced_order r F).
move=> u; aw=> uF; rewrite -induced_trans // => toi.
have tos: (sub (tack_on u a) (substrate r)).
apply sub_trans with F=>//.
move=> t; aw; by case; [ apply uF| move=> ->].
have oit: (order (induced_order r (tack_on u a))) by fprops.
have toit: total_order (induced_order r (tack_on u a)).
split=>//; aw; rewrite /gge.
move=> x y xt yt; rewrite ? iorder_gle //.
move: xt yt; aw; case=> hx; case => hy.
move: toi => [_]; aw.
move=> h; move: (h _ _ hx hy); rewrite /gge; aw.
by apply sub_trans with F.
rewrite hy; move: (uF _ hx); rewrite /F Z_rw; intuition.
rewrite hx; move: (uF _ hy); rewrite /F Z_rw; intuition.
rewrite hx hy; left; order_tac.
move: (isr _ tos toit) => [b [bs bub]].
move: (bub _ (inc_tack_on_x a u)) => ab.
have bF: inc b F by rewrite /F; apply Z_inc.
exists b; split; aw=>//.
move=> y yu.
by move: (bub _ (inc_tack_on_y a yu)) => yb; aw; apply uF.
move:(Zorn_lemma oi isF)=> [b []]; aw => [bF bm].
move: (bF); rewrite /F Z_rw; move=> [bs ab].
exists b.
split =>//; split =>//.
move=> x h; apply bm; aw; rewrite /F; apply Z_inc; order_tac.
Qed.
Lemma inductive_powerset: forall 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_set (inclusion_suborder A).
Proof.
move=> A F sp Sp X XA [oX tX]; awi tX; fprops; awi XA.
exists (union X).
have p1: inc (union X) A.
apply Sp =>//;move=> x y xX yX.
move: (tX _ _ xX yX); rewrite /gge; aw;intuition.
split; first by aw.
move=> y yX; aw; ee.
by apply union_sub.
Qed.
Lemma maximal_in_powerset: forall 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_element (inclusion_suborder A) a.
Proof.
move=> A F Ap pA.
have oA: (order (inclusion_suborder A)) by fprops.
move: (inductive_powerset Ap pA).
by apply Zorn_lemma.
Qed.
Lemma minimal_in_powerset: forall A F, sub A (powerset F) -> nonempty A ->
(forall So, (forall x y, inc x So -> inc y So -> sub x y \/ sub y x) ->
sub So A -> inc (intersection So) A) ->
exists a, minimal_element (inclusion_suborder A) a.
Proof.
move=> A F Ap [x xA] pA.
have oA: order (inclusion_suborder A) by fprops.
have ooA:order ( opposite_order (inclusion_suborder A)) by fprops.
have ioA: inductive_set (opposite_order (inclusion_suborder A)).
move=> X XS [oX tX]. awi tX =>//.
case (emptyset_dichot X) => neX.
exists x; rewrite neX;split;[ aw| move=> y; case; case].
awi XS =>//.
have iXA:inc (intersection X) A.
apply pA =>//; move=> a b aX bX;
move: (tX _ _ aX bX); rewrite /gge; aw;intuition.
exists (intersection X); split; first by aw.
move=> y yX; aw; ee; by apply intersection_sub.
move: (Zorn_lemma ooA ioA)=> [a ]; rewrite maximal_opposite //.
by exists a.
Qed.
The next theorem essentially says that f is injective
Lemma order_morphism_pr1: forall f r r',
order r -> order r' -> is_function f -> substrate r = source f ->
substrate r' = target f ->
(forall x y, inc x (source f) -> inc y (source f) ->
gle r x y = gle r' (W x f) (W y f))
-> order_morphism f r r'.
Proof.
move=> f r r' or or' ff sr sr' p.
red; ee.
split=>// x y xsf ysf sW.
have le1: (gle r' (W x f) (W x f))
by order_tac; rewrite sr';apply inc_W_target =>//.
by apply (order_antisymmetry or); rewrite -[related]/gle p // -sW.
Qed.
Uniqueness of morphism between segments of well-ordered sets
Lemma increasing_function_segments: forall r r' f g,
worder r -> worder r' ->
increasing_fun f r r' -> strict_increasing_fun g r r'->
is_segment r' (range (graph f)) ->
forall x, inc x (source f) -> gle r' (W x f) (W x g).
Proof.
move=> r r' f g wor wor'
[ff [or [or' [sf [tf incf]]]]] [fg [_ [ _ [sg [tg sing]]]]] sr x xsf.
set (s :=Zo (source f) (fun x => (glt r' (W x g) (W x f)))).
have sfsg: source f = source g by ue.
move: (worder_total wor) => tor.
move: (worder_total wor') => tor'.
have Wfsr': inc (W x f) (substrate r') by rewrite tf; fprops.
have Wgsr': inc (W x g) (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 Z_inc.
have ssf: sub s (source f) by rewrite /s; apply Z_sub.
rewrite - sf in ssf; move: wor=> [_ pwor].
move:(pwor _ ssf nes)=> [y []]; aw => ys yle.
move: ys; rewrite /s Z_rw; move=> [ysf [leWy neWy]].
have Wrg: inc (W y f) (range (graph f)) by apply inc_W_range_graph.
move: sr => [ _ sr']; move: (sr' _ _ Wrg leWy).
dw; fprops ; move => [z Jg].
move: (W_pr ff Jg) (inc_pr1graph_source ff Jg) => sW zf.
have lt1: glt r' (W z f) (W y f) by rewrite sW; 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 (W z f) (substrate r') by rewrite tf; fprops.
have Wzg: inc (W z g) (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 Z_inc.
move: (yle _ zs)=> yz; move: (iorder_gle1 yz) => lt3.
order_tac.
move: (sing _ _ lt2); rewrite -sW => lt3; order_tac.
Qed.
Lemma isomorphism_worder_unique: forall r r' x y,
worder r -> worder r' -> is_segment r' (range (graph x)) ->
is_segment r' (range (graph y)) ->
order_morphism x r r' -> order_morphism y r r'
-> x = y.
Proof.
move=> r r' x y wor wor' srx sry mx my.
move:(order_morphism_increasing mx) => six.
move:(order_morphism_increasing my) => siy.
move: (increasing_fun_from_strict six)=> sx.
move: (increasing_fun_from_strict 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.
Lemma induced_order_trans: forall a b c, sub c b ->
induced_order (induced_order a b) c = induced_order a c.
Proof.
move=> a b c cb; rewrite /induced_order.
have scc: (sub (coarse c) (coarse b)).
by rewrite /coarse; apply product_monotone.
rewrite - intersection2A.
apply f_equal.
by rewrite intersection2C - intersection2_sub.
Qed.
Theorem isomorphism_worder: forall r r', worder r -> worder r' ->
let iso:= (fun u v f =>
is_segment v (range (graph f)) & order_morphism f u v) in
exists_unique (fun f => iso r r' f) \/ exists_unique (fun f => iso r' r f).
Proof.
move=> r r' wor wor' iso.
set (E:= substrate r).
set (E':= substrate r').
have or: order r by fprops.
have or': order r' by fprops.
have oe:order (extension_order E E') by fprops.
have ooe: order (opposite_order (extension_order E E')) by fprops.
have soe: set_of_sub_functions E E' =
substrate (opposite_order (extension_order E E')) by aw; fprops.
set (s:= (Zo (set_of_sub_functions E E') (fun z => exists u,
is_segment r u & iso (induced_order r u) r' z))).
have ssee: sub s (set_of_sub_functions E E') by rewrite /s; apply Z_sub.
have sse: sub s (substrate (extension_order E E')) by aw.
have ssoee: sub s (substrate (opposite_order (extension_order E E'))) by aw.
have ins:inductive_set (induced_order(opposite_order(extension_order E E')) s).
move=> X; aw=> Xs; rewrite induced_order_trans// => pX.
have Xse:sub X (set_of_sub_functions E E') by apply (sub_trans Xs ssee).
have Xsoe:sub X (substrate (opposite_order (extension_order E E'))) by aw.
have alseg: forall x, inc x s -> is_segment r (source x).
move=> x; rewrite /s Z_rw; move=> [_ [u [su [_ [_ [_ [_ [sx _ ]]]]]]]].
by rewrite -sx; aw; by apply sub_segment1.
have alsegr: forall x, inc x s -> is_segment r' (range (graph x)).
by move=> x; rewrite /s Z_rw; move=> [_ [u [_ [sv _]]]].
have Xso: sub X (substrate (extension_order E E')) by aw.
move: pX => [_ ]; aw => ppX.
have cov: forall u v x, inc u X -> inc v X -> inc x (source u) ->
inc x (source v) -> W x u = W x v.
move=> u v x uX vX xsu xsv.
move: (ppX _ _ uX vX); rewrite /gge;aw.
by case; move=> [_ [_ h]]; [ | symmetry];apply W_extends.
move:(sup_extension_order2 Xse cov)=> [x [lubx [sx [rgx gx]]]].
move: lubx; aw; move=> [[xsoe xb] lub]; rewrite -soe in xsoe.
have xs: inc x s.
rewrite /s; apply Z_inc=>//; exists (source x).
have ssx: is_segment r (source x).
rewrite sx; apply unionf_is_segment =>//.
by move=> a aX; apply alseg; apply Xs.
split =>//.
have srgx: is_segment r' (range (graph x)).
rewrite rgx; apply unionf_is_segment =>//.
by move=> a aX; apply alsegr; apply Xs.
split =>//.
have sxsr: sub (source x) (substrate r) by red in ssx; ee.
have srxs: sub (range (graph x)) (substrate r') by red in srgx; ee.
have xi: (forall a b,
inc a (source x) -> inc b (source x) ->
gle (induced_order r (source x)) a b =
gle r' (W a x) (W b x)).
move=> a b; rewrite sx => asX bsX; aw.
move: (unionf_exists asX)=> [u [uX au]].
move: (unionf_exists bsX)=> [v [vX av]].
have [w [wX [asw bsw]]] :exists z,
inc z X & inc a (source z) & inc b (source z).
move: (ppX _ _ uX vX). rewrite/ gge; aw.
case; move=> [_ [_ ext]]; move: (source_extends ext)=> sext;
[ exists v | exists u ]; ee.
rewrite - (extension_order_pr (xb _ wX) asw).
rewrite - (extension_order_pr (xb _ wX) bsw).
move:(Xs _ wX); rewrite /s Z_rw.
move=> [_ [z [[sz _] [_ [_ [_ [_ [dd [_ isz]]]]]]]]].
awi dd =>//; rewrite dd in isz.
rewrite - (isz _ _ asw bsw); aw.
move: xsoe; bw; move => [fx [srcx tx]].
apply order_morphism_pr1; fprops; aw.
exists x.
split; first by rewrite substrate_induced_order //.
move=> y yX; move: (Xs _ yX)=> ys.
by rewrite iorder_gle //; apply xb.
have oio: order (induced_order (opposite_order (extension_order E E')) s).
fprops.
move: (Zorn_lemma oio ins) => [f []]; aw =>fis fmax.
move: (fis); rewrite /s Z_rw;move => [fee [x [sx xiso]]].
case (equal_or_not x (substrate r)) => h.
move: xiso; rewrite h induced_order_substrate //; move=> xiso.
left; split; first by exists f.
move=> a b [s1 m1][s2 m2].
by apply (isomorphism_worder_unique (r:=r) (r':=r')).
right; 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'.
set (g:= corresp E' E (inverse_graph (graph f))).
move: xiso=> [_ [_ [_ [injf [sf [tf vf]]]]]].
have ff: is_function f by fct_tac.
have gf: is_graph (graph f) by fprops.
have sf': source f = x by awi sf =>//; apply sub_segment1.
have rgg: range (graph g) = x by rewrite /g; aw; rewrite range_inverse; aw.
have fg: is_function g.
rewrite /g; apply is_function_pr.
split;fprops; move=> a b.
rewrite ? inverse_graph_rw //; move => [pa J1g][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 domain_inverse =>//.
exists g.
red; rewrite rgg; split=>//.
apply order_morphism_pr1=>//; try solve [ rewrite /g; aw].
move=> a b asg bsg.
have fgp: (forall u, inc u (source g) ->
(inc (W u g) (source f) & W (W u g) f = u)).
move=> u usg; move: (W_pr3 fg usg); rewrite {2} /g; aw => Jg.
split; [ graph_tac | apply (W_pr ff Jg)].
move: (fgp _ asg)(fgp _ bsg)=> [W1s va][W2s vb].
rewrite -{1} va -{1} vb.
rewrite - (vf _ _ W1s W2s); aw; ue.
case (well_ordered_segment wor sx)=> aux; first by contradiction.
move: aux=> [a [asr xa]].
move: xiso=> [st [_ [_ [injf [sf [tf isf]]]]]].
case (well_ordered_segment wor' st)=> aux; first by contradiction.
move: aux=> [b [vsr tb]].
set (g:=tack_on_f f a b).
have ff: is_function f by fct_tac.
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:is_function g by rewrite /g; apply tack_on_function.
have tg: target g = E'.
rewrite/g /tack_on_f; aw; rewrite -tf /E'.
by apply tack_on_when_inc.
have sg: source g = segment_c r a.
by rewrite /g/tack_on_f; aw; rewrite sfx xa; apply segment_c_pr.
have sap: forall a, sub (segment_c r a) (substrate r).
move=> t; rewrite/segment_c/interval_uc; apply Z_sub.
have rgg: (range (graph g) = segment_c r' b).
rewrite/g/tack_on_f; aw; rewrite -segment_c_pr // range_tack_on; ue.
have gs: inc g s.
rewrite /s; apply Z_inc; bw.
by ee; rewrite sg; apply sap.
exists (segment_c r a).
split; first by apply tack_on_segment.
split; first by rewrite rgg; apply tack_on_segment.
apply order_morphism_pr1 =>//; fprops; try solve [symmetry; aw].
move=> u v; rewrite sg; rewrite -segment_c_pr //.
rewrite 2!tack_on_rw -xa -sfx => ut vt; aw.
have p1: forall w, inc w (source f) -> glt r' (W w f) b.
move=> w wsf.
have: inc (W w f) (range (graph f)) by apply inc_W_range_graph.
rewrite tb; rewrite segment_rw //.
have p2: forall w, inc w (source f) -> glt r w a.
move=> w; rewrite sfx xa; rewrite segment_rw //.
case ut => hu; [rewrite tack_on_W_in // | rewrite hu tack_on_W_out //].
case vt => hv; [rewrite tack_on_W_in // | rewrite hv tack_on_W_out //].
rewrite - isf //; aw; ue.
move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _]; by apply iff_eq.
case vt => hv; [rewrite tack_on_W_in // | rewrite hv tack_on_W_out //].
move: (p1 _ hv)(p2 _ hv)=> [e1 ne1][e2 ne2].
apply iff_eq => h'';[ elim ne2 | elim ne1];order_tac.
apply iff_eq=> _; order_tac.
have eqfg: g = f.
apply fmax;aw;rewrite/ extends; ee; rewrite /g/tack_on_f; aw; fprops.
elim asf; rewrite -eqfg sg.
by apply inc_bound_segmentc.
Qed.
Consequences
Lemma identity_isomorphism: forall r, order r ->
order_isomorphism (identity (substrate r)) r r.
Proof.
move=> r or; red; ee; aw.
apply identity_bijective.
move=> x t xsr ysr;rewrite ? identity_W //.
Qed.
Lemma identity_morphism: forall r, order r ->
order_morphism (identity (substrate r)) r r.
Proof.
move=> r or; move: (identity_isomorphism or).
have bi: forall f, bijection f -> injection f by move=> f [injf _].
rewrite /order_isomorphism /order_morphism; intuition.
Qed.
Lemma unique_isomorphism_onto_segment: forall r f, worder r ->
is_segment r (range (graph f)) -> order_morphism f r r ->
f = identity (substrate r).
Proof.
move=> r f wor seg mor.
have aux: is_segment r (range (graph (identity (substrate r)))) &
order_morphism (identity (substrate r)) r r.
split.
have [_ si]: (bijection (identity (substrate r))) by apply identity_bijective.
rewrite (surjective_pr3 si); aw; apply substrate_is_segment; fprops.
apply identity_morphism; fprops.
case (isomorphism_worder wor wor); move=> [_ un]; apply un; ee.
Qed.
Lemma compose_order_isomorphism: forall r r' r'' f f',
order_isomorphism f r r' -> order_isomorphism f' r' r''
-> order_isomorphism (f' \co f) r r''.
Proof.
rewrite /order_isomorphism => r r' r'' f f'.
move=>[or [or' [bf [sf [tf fp]]]]][_ [or'' [bf' [sf' [tf' fp']]]]].
have cff': f' \coP f by red; ee; try fct_tac; rewrite -sf'.
ee; try solve [aw].
by apply compose_bijective.
aw; move=> x y xsf ysf.
have ff: (is_function f) by fct_tac.
move: (inc_W_target ff xsf)(inc_W_target ff ysf) => xt yt.
rewrite -sf' tf in fp'.
aw; rewrite -fp' // - fp =>//.
Qed.
Lemma inverse_order_isomorphism: forall r r' f ,
order_isomorphism f r r' -> order_isomorphism (inverse_fun f) r' r.
Proof.
rewrite /order_isomorphism => r r' f.
move=>[or [or' [bf [sf [tf fp]]]]]; ee; aw.
by apply inverse_bij_is_bij.
move=> x y xt yt.
move Wx: (W x (inverse_fun f)) => x'.
move Wy: (W y (inverse_fun f)) => y'.
have aux: (source f = target (inverse_fun f)); aw.
rewrite aux in fp.
move: (inverse_bij_is_bij bf) => [[fi _] _].
rewrite (W_inverse bf xt (sym_equal Wx)).
rewrite (W_inverse bf yt (sym_equal Wy)).
symmetry; apply fp.
rewrite - Wx; apply inc_W_target =>//; aw.
rewrite - Wy; apply inc_W_target =>//; aw.
Qed.
Lemma compose_order_morphism: forall r r' r'' f f',
f' \coP f -> order_morphism f r r' -> order_morphism f' r' r''
-> order_morphism (f' \co f) r r''.
Proof.
rewrite /order_morphism => r r' r'' f f' cf'f.
move=>[or [or' [bf [sf [tf fp]]]]][_ [or'' [bf' [sf' [tf' fp']]]]].
ee; try solve [aw].
by apply compose_injective.
aw; move=> x y xsf ysf.
have ff: (is_function f) by fct_tac.
move: (inc_W_target ff xsf)(inc_W_target ff ysf) => xt yt.
rewrite -sf' tf in fp'.
aw; rewrite -fp' // - fp =>//.
Qed.
Lemma bij_pair_isomorphism_onto_segment: forall r r' f f',
worder r -> worder r' ->
is_segment r' (range (graph f)) -> order_morphism f r r' ->
is_segment 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=> r r' f f' wor wor' sr1 om sr2 om'.
move: (om)(om')=>[or [or' [bf [sf [tf fp]]]]] [_ [_ [bf' [sf' [tf' fp']]]]].
have ff :is_function f by fct_tac.
have ff' :is_function f' by fct_tac.
have gf: is_graph (graph f) by fprops.
have gf': is_graph (graph f') by fprops.
have cff': (f \coP f') by red; intuition; ue.
have cf'f: (f' \coP f) by red; intuition; ue.
move: (compose_order_morphism cff' om' om) => mor1.
move: (compose_order_morphism cf'f om om') => mor2.
have fc: is_function (f' \co f) by fct_tac.
have srg: is_segment r (range (graph (f'\co f))).
split.
have <-: target (f' \co f) = substrate r by aw.
by apply f_range_graph.
move=> x y xr yr.
move: xr; rewrite /compose; dw; fprops.
move=> [z]; aw; move => [_ [u [Jg1 Jg2]]].
have urg: (inc u (range (graph f))) by ex_tac.
have xrg: (inc x (range (graph f'))) by ex_tac.
move:sr2 => [_ sr2]; move: (sr2 _ _ xrg yr) => yrg.
move: yrg; dw; move=> [v Jg3].
rewrite -(W_pr ff' Jg2) -(W_pr ff' Jg3) in yr.
move :(inc_pr1graph_source ff' Jg2) (inc_pr1graph_source ff' Jg3)=> us vs.
rewrite -fp' // in yr .
move:sr1 => [_ sr1]; move: (sr1 _ _ urg yr).
dw;move=> [w Jg4].
exists w; aw; split; fprops; by exists v; split.
have srg': is_segment r' (range (graph (compose f f'))).
have fc': is_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 xr yr.
move: xr; rewrite /compose; dw; fprops.
move=> [z]; aw; move => [_ [u [Jg1 Jg2]]].
have urg: (inc u (range (graph f'))) by ex_tac.
have xrg: (inc x (range (graph f))) by ex_tac.
move:sr1 => [_ sr1]; move: (sr1 _ _ xrg yr) => yrg.
move: yrg; dw; move=> [v Jg3].
rewrite -(W_pr ff Jg2) -(W_pr ff Jg3) in yr.
move :(inc_pr1graph_source ff Jg2) (inc_pr1graph_source ff Jg3)=> us vs.
rewrite -fp // in yr .
move:sr2 => [_ sr2]; move: (sr2 _ _ urg yr).
dw;move=> [w Jg4].
exists w; aw; split; fprops; by exists v; split.
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.
ee.
Qed.
Lemma isomorphic_subset_segment: forall r a,
worder r -> sub a (substrate r) ->
exists w, exists f, is_segment r w &
order_isomorphism f (induced_order r a) (induced_order r w).
Proof.
move=> r a wo asr.
move: (worder_restriction wo asr) => woi.
move: (isomorphism_worder woi wo).
case; move=> [[f [sr [oir [or [[ff injf] [sf [tf fp]]]]]]] _].
awi sf=>//.
have ta: transf_axioms (fun z => W z f) (source f) (range (graph f)).
by move=> c csf /=; apply inc_W_range_graph=>//; fct_tac.
set (g := BL (fun z => W z f) (source f) (range (graph f))).
exists (range (graph f)); exists g.
have aux:sub (range (graph f)) (substrate r) by red in sr; ee.
have gf: is_graph (graph f) by fprops.
rewrite /order_isomorphism /g;ee; aw.
apply bl_bijective =>//.
move=> y; dw; fprops; move=> [x Jg]; exists x;split; graph_tac.
move=> x y xsf ysf; rewrite ? bl_W // fp//.
aw; dw; [ exists x; apply W_pr3 =>// | exists y; apply W_pr3 =>//].
case: (well_ordered_segment woi sr)=> hyp.
rewrite -hyp in tf.
have oi: order_isomorphism f r (induced_order r a).
red; ee; last by rewrite -hyp tf.
split=>//; apply surjective_pr4 =>//.
move: (inverse_order_isomorphism oi) => ioi.
exists (substrate r); exists (inverse_fun f).
split; first by apply substrate_is_segment.
rewrite induced_order_substrate //.
move: hyp=>[x [xsr rgf]].
awi xsr=>//.
have xsf: inc x (source f) by rewrite -sf; apply asr.
have Ws: inc (W x f) (segment (induced_order r a) x).
by rewrite -rgf; apply inc_W_range_graph=>//.
set (s :=Zo (source f) (fun a => (glt r (W a f) a))).
have nes: nonempty s.
exists x; rewrite /s; apply Z_inc =>//.
move: (inc_segment Ws); apply (iorder_gle2).
have ssf: sub s (substrate r) by rewrite sf /s;apply Z_sub.
move: wo=> [_ wor].
move: (wor _ ssf nes) => [y []]; aw => ys ley.
move: ys; rewrite /s Z_rw; move => [ysf [leW neW]].
have p1: inc (W y f) (source f) by rewrite -sf; order_tac.
elim neW.
have p2: inc (W y f) s.
rewrite/s; apply Z_inc =>//.
split; last by dneg h; apply injf.
rewrite (fp _ _ p1 ysf) in leW; apply(iorder_gle1 leW).
move: (iorder_gle1 (ley _ p2)) => geW.
order_tac.
Qed.
Definition lexicographic_order_r (r g:Set): Set -> Set -> Prop :=
fun x x' =>
forall j, least_element (induced_order r (Zo (domain g)
(fun i => V i x <> V i x'))) j -> glt (V j g) (V j x)(V j x').
Definition lexicographic_order_axioms r g:=
worder r & substrate r = domain g & fgraph g &
(forall i, inc i (domain g) -> order (V i g)).
Definition lexicographic_order r g :=
graph_on (lexicographic_order_r r g)(prod_of_substrates g).
Lemma lexorder_substrate_aux: forall r g x,
lexicographic_order_axioms r g ->
lexicographic_order_r r g x x.
Proof.
move=> r g x [wor [sr [fgx ao]]].
move=> j [js _]; move: js; aw; fprops; last by rewrite sr; apply Z_sub.
rewrite Z_rw.
by move=> [_ h]; elim h.
Qed.
Lemma lexorder_substrate: forall r g,
lexicographic_order_axioms r g ->
substrate(lexicographic_order r g) = prod_of_substrates g.
Proof.
move=> r g la; rewrite /lexicographic_order substrate_graph_on //.
by move=> a ap; apply lexorder_substrate_aux.
Qed.
Hint Rewrite lexorder_substrate : bw.
Lemma lexorder_order: forall r g,
lexicographic_order_axioms r g -> order (lexicographic_order r g).
Proof.
move=> r g lea; move: (lea)=> [wor [sr [fgx ao]]].
have tor: total_order r by apply worder_total.
move:wor=> [or wor].
rewrite/lexicographic_order.
apply order_from_rel1; last by move=> u up; apply lexorder_substrate_aux.
rewrite /lexicographic_order_r -sr => x y z xy yz j [].
aw; try apply Z_sub.
rewrite Z_rw; move => [jd jxy] jp.
set (s:= Zo (substrate r) (fun i => (V i x <> V i y) \/ (V i y <> V i z)
\/ V i x <> V i z)).
have sst: sub s (substrate r) by rewrite /s; apply Z_sub.
have js: inc j s by rewrite /s ; apply Z_inc; auto.
have nes: nonempty s by ex_tac.
move: (wor _ sst nes) => [k []]; aw => ks kp.
move: ks; rewrite /s Z_rw; move => [ksr kp1].
case (equal_or_not (V k x) (V k y))=> kxy.
have kyz: (V k y <> V k z).
case kp1; first( by contradiction); case;[ done| ue].
have kj: k = j.
move: (iorder_gle1 (kp _ js))=> kj.
have ks: (inc k (Zo (substrate r) (fun i => V i x <> V i z))).
by apply Z_inc=>//; ue.
move: (iorder_gle1 (jp _ ks))=> jk; order_tac.
have jp':(least_element (induced_order r (Zo (substrate r)
(fun i => V i y <> V i z))) j).
red; aw;last (by apply Z_sub); split.
by rewrite -kj; apply Z_inc.
move=> l; rewrite Z_rw; move=> [ls lyz].
have ils: inc l s by rewrite /s; apply Z_inc=>//; auto.
move: (iorder_gle1 (kp _ ils)) => kl.
aw; first (by ue); [apply Z_inc=>//; ue | apply Z_inc=>//].
by move: (yz _ jp'); rewrite -kj kxy.
case: (equal_or_not (V k y) (V k z)) => Vyz.
have kj: (k = j).
move:(iorder_gle1 (kp _ js)) => kj.
have ks: (inc k (Zo (substrate r) (fun i => V i x <> V i z))).
apply Z_inc=>//; ue.
move: (iorder_gle1 (jp _ ks)) => jk; order_tac.
have jp': (least_element (induced_order r (Zo (substrate r)
(fun i => V i x <> V i y))) j).
red; aw; last (by apply Z_sub); split.
apply Z_inc=>//; ue.
move=> l; rewrite Z_rw; move=> [ls lxy].
have ils: inc l s by rewrite /s; apply Z_inc=>//; auto.
move: (iorder_gle1 (kp _ ils)) => kl.
aw; first (by ue); [apply Z_inc=>//; ue | apply Z_inc=>//].
by move: (xy _ jp'); rewrite -kj Vyz.
have pk1: least_element (induced_order r (Zo (substrate r)
(fun i => V i x <> V i y))) k.
red; aw; last (by apply Z_sub); split; first by apply Z_inc =>//.
move => l; rewrite Z_rw; move=> [lr lxy].
have ils: inc l s by rewrite /s; apply Z_inc=>//; auto.
move: (iorder_gle1 (kp _ ils)) => kl.
aw;apply Z_inc=>//.
have pk2: least_element (induced_order r (Zo (substrate r)
(fun i => V i y <> V i z))) k.
red; aw; last (by apply Z_sub); split; first by apply Z_inc =>//.
move => l; rewrite Z_rw; move=> [lr lxy].
have ils: inc l s by rewrite /s; apply Z_inc=>//; auto.
move: (iorder_gle1 (kp _ ils)) => kl.
aw;apply Z_inc=>//.
move: (xy _ pk1)(yz _ pk2) => Vkxy Vkyz.
have Vkxz: glt (V k g) (V k x) (V k z).
by 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 => V i x <> V i z))).
by apply Z_inc =>//; 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 => V i u <> V i v))).
case (emptyset_dichot s) => es.
have fg:fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; gprops.
apply (productb_exten fg up vp).
rewrite /fam_of_substrates=> i; bw=> idg.
by ex_middle uv; empty_tac1 i; rewrite /s; apply Z_inc.
have ssym: s=(Zo (domain g) (fun i : Set => V i v <> V i u)).
rewrite /s; set_extens t; rewrite ? Z_rw; intuition.
have ssr: (sub s (substrate r)) by rewrite /s sr; apply Z_sub.
move: (wor _ ssr es)=> [j jp].
have js: (inc j s) by move: jp=> [jd _]; awi jd; fprops.
move: (le1 _ jp) => p1.
rewrite ssym in jp; move: (le2 _ jp) => p2.
rewrite -sr in ao; move: (ao _ (ssr _ js))=> oj.
order_tac.
Qed.
Lemma lexorder_gle: forall r g x x',
lexicographic_order_axioms r g ->
related (lexicographic_order r g) x x' =
(inc x (prod_of_substrates g)& inc x' (prod_of_substrates g) &
forall j, least_element (induced_order r (Zo (domain g)
(fun i => V i x <> V i x'))) j -> glt (V j g) (V j x)(V j x')).
Proof.
move=> r g x x' ax;rewrite /lexicographic_order graph_on_rw1 //.
Qed.
Hint Resolve lexorder_order: fprops.
Hint Rewrite lexorder_gle : aw.
Lemma lexorder_total: forall r g,
lexicographic_order_axioms r g ->
(forall i, inc i (domain g) -> total_order (V i g)) ->
total_order (lexicographic_order r g).
Proof.
move=> r g la alt.
have ol: order (lexicographic_order r g) by fprops.
move: (la)=> [[or wor] [sr [fgx ao]]].
split=>//.
bw; move=> x y xsr ysr.
have fgf:fgraph (fam_of_substrates g) by rewrite/fam_of_substrates; gprops.
set s:=(Zo (substrate r) (fun i : Set => V i x <> V i y)).
case (emptyset_dichot s) => nse.
have xy: x = y.
apply (productb_exten fgf xsr ysr).
move=> i idg; ex_middle u;empty_tac1 i.
by rewrite/s; apply Z_inc; move: idg; rewrite/fam_of_substrates; bw; ue.
left; rewrite xy; order_tac; bw.
have ssr: sub s (substrate r) by rewrite/s; apply Z_sub.
move: (wor _ ssr nse)=> [j jle].
move: (jle)=> [];rewrite substrate_induced_order // => js jp.
have jdg: inc j (domain g) by rewrite -sr; apply ssr.
move: (alt _ jdg)=>[orj torj].
have px: (inc (V j x) (substrate (V j g))).
move:xsr; rewrite /prod_of_substrates/fam_of_substrates; aw.
bw; move=>[_ [dx px]]; rewrite dx in px; move: (px _ jdg); bw.
have py: (inc (V j y) (substrate (V j g))).
move:ysr; rewrite /prod_of_substrates/fam_of_substrates; aw.
bw; move=>[_ [dy py]]; rewrite dy in py; move: (py _ jdg); bw.
have ois: order (induced_order r s) by fprops.
case: (torj _ _ px py) => leaux.
left; rewrite /gle lexorder_gle //; ee.
rewrite -sr; fold s; move=> k kl.
rewrite - (unique_least ois jle kl); split =>//.
move: js; rewrite /s Z_rw; intuition.
right; rewrite /gge/gle lexorder_gle //; ee.
have ssym: s=(Zo (domain g) (fun i : Set => V i y <> V i x)).
rewrite /s; set_extens t; rewrite ? Z_rw; intuition; ue.
rewrite -ssym; move=> k kl.
rewrite - (unique_least ois jle kl); split =>//.
move: js; rewrite /s Z_rw; intuition.
Qed.
Lemma disjoint_union2_rw: forall a b x y, y <> x ->
disjoint_union (variantL x y a b) =
union2 (product a (singleton x)) (product b (singleton y)).
Proof.
move=> a b x y yx.
rewrite/ disjoint_union /disjoint_union_fam.
have dv: domain (variantL x y a b) = doubleton x y. rewrite/ variantL; bw.
set_extens z; rewrite dv unionb_rw union2_rw; bw.
move=> [u [ud]]; bw.
by case (doubleton_or ud)=> h;
[rewrite h variant_V_a | rewrite h variant_V_b]; auto.
move=> h.
have Qz: (inc (Q z) (doubleton x y)).
by case h; aw; move=> [pz [Pz Qz]]; rewrite Qz; fprops.
exists (Q z); bw; ee.
aw.
case h; aw; move=> [pz [Pz qz]]; rewrite qz; ee; fprops.
by rewrite variant_V_a.
by rewrite variant_V_b.
Qed.
Lemma disjoint_union2_rw1: forall a b,
disjoint_union (variantLc a b) =
union2 (product a (singleton TPa)) (product b (singleton TPb)).
Proof.
move=> a b; rewrite/ variantLc disjoint_union2_rw //.
fprops.
Qed.
End Worder.
Export Worder.