Library ssete6
Require Import ssreflect ssrbool eqtype ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset15.
Module Exercise6.
Definition csup_s A := \csup (fun_image A succ_c).
Lemma csup_s1 A (x := csup_s A): cardinal_set A ->
(forall y, inc y A -> y <c x).
Proof.
move => csa y yA.
rewrite /x/csup_s; set B := fun_image _ _.
apply /(succ_c_pr5P (csa _ yA)) ; apply:card_sup_ub.
move => t /funI_P [z za ->]; first by exact: (CS_succ_c (csa _ za)).
by apply /funI_P; ex_tac.
Qed.
Lemma csup_s2 A z: cardinal_set A -> cardinalp z ->
(forall y, inc y A -> y <c z) -> csup_s A <=c z.
Proof.
move => csa cz h2; apply: card_ub_sup => //.
move => t /funI_P [u za ->]; exact (CS_succ_c (csa _ za)).
move => i /funI_P [t /h2 tA ->]; apply /succ_c_pr5P => //; co_tac.
Qed.
Definition disjointness_degree F :=
csup_s (fun_image (coarse F -s diagonal F)
(fun z => cardinal ((P z) \cap (Q z)))).
Lemma dd_pr1 F x y: inc x F -> inc y F -> x <> y ->
cardinal (x \cap y) <c (disjointness_degree F).
Proof.
move => xF yF xy; apply: csup_s1.
move=> t /funI_P [z _ ->]; fprops.
apply /funI_P; exists (J x y); aw => //.
apply /setC_P;split => //; first by apply :setXp_i.
by case /diagonal_pi_P.
Qed.
Lemma dd_pr2 F z: cardinalp z ->
(forall x y, inc x F -> inc y F -> x <> y ->
cardinal (x \cap y) <c z)
-> (disjointness_degree F) <=c z.
Proof.
move => cz h; apply:csup_s2 => //.
move=> t /funI_P [u _ ->]; fprops.
move => y /funI_P [t /setC_P [/setX_P [pt Pt Qt] pb ->]]; apply: h => //.
by move => xy; case: pb; apply /diagonal_i_P.
Qed.
Lemma dd_pr3 F : (disjointness_degree F = \0c) <-> small_set F.
Proof.
split => h.
move => x y fx fy; ex_middle xy.
by move: (dd_pr1 fx fy xy); rewrite h => /card_lt0.
by apply: card_le0; apply: (dd_pr2 CS0) => x y xf yf; move: (h _ _ xf yf).
Qed.
Lemma dd_pr4 F : (disjointness_degree F = \1c) <->
(~ small_set F /\ forall x y, inc x F -> inc y F -> disjointVeq x y).
Proof.
split => h.
split; first by move /dd_pr3; rewrite h; fprops.
move => x y xf yf; case: (equal_or_not x y); first by left.
move => xny; move: (dd_pr1 xf yf xny); rewrite h.
by move /card_lt1 /cardinal_nonemptyset; right.
move: h => [/dd_pr3 dn0 h1]; ex_middle aux.
have aux2: disjointness_degree F <=c \1c.
apply: (dd_pr2 CS1) => x y xF yF; case: (h1 _ _ xF yF) => // -> _.
rewrite cardinal_set0 ; exact: card_lt_01.
by case: dn0; move/card_lt1: (conj aux2 aux).
Qed.
Exercise 5.7
Definition Noetherian r :=
(forall X, sub X (substrate r) -> nonempty X ->
exists a, maximal (induced_order r X) a).
Definition Noetherian_set r x:=
sub x (substrate r) /\ Noetherian (induced_order r x).
Lemma Noetherian_set_pr r x: order r -> sub x (substrate r) ->
(Noetherian_set r x <->
(forall X, sub X x -> nonempty X ->
exists2 a, inc a X & (forall x, inc x X -> gle r a x -> x = a))).
Proof.
move => or xsr; rewrite /Noetherian_set /Noetherian.
rewrite (iorder_sr or xsr); split.
move => [_ h] X Xx xne; move: (h _ Xx xne);rewrite (iorder_trans _ Xx).
move=> [a []]; rewrite (iorder_sr or (sub_trans Xx xsr)) => ax ap.
by ex_tac; move => t tX lat; apply: ap; apply /iorder_gleP.
move => h; split; first by exact.
move => X Xx ne; rewrite (iorder_trans _ Xx); move: (h _ Xx ne) => [a ax ap].
exists a; split; first by rewrite (iorder_sr or (sub_trans Xx xsr)).
by move => b => /iorder_gle5P; move=> [_ bx ab]; apply: ap.
Qed.
Lemma Exercise6_29a r: order r ->
Noetherian r -> Noetherian_set r (substrate r).
Proof.
move => or nr; split; [fprops | by rewrite (iorder_substrate or) ].
Qed.
Lemma Exercise6_29b r: Noetherian_set r emptyset.
Proof.
split; fprops.
move => X xns [w wx]; move: (xns _ wx).
have ->: (induced_order r emptyset) = emptyset.
by apply /set0_P => y /setI2_P [_]/setX_P [_ /in_set0].
by rewrite /substrate domain_set0 range_set0 setU2_id => /in_set0.
Qed.
Lemma Exercise6_29c r a b: order r ->
Noetherian_set r a -> Noetherian_set r b -> Noetherian_set r (a \cup b).
Proof.
move => or pa pb.
move: (proj1 pa) (proj1 pb) => asr bsr.
move: pa; rewrite (Noetherian_set_pr or asr) => pa.
move: pb; rewrite (Noetherian_set_pr or bsr) => pb.
have usr: sub (a \cup b) (substrate r)
by move=> t; case /setU2_P; [apply asr | apply: bsr].
rewrite (Noetherian_set_pr or usr).
move => X Xu neX.
set Xa:= intersection2 X a.
case: (emptyset_dichot Xa) => Xane.
have sb: sub X b.
move => t tX; move: (Xu _ tX); case /setU2_P => // ta.
empty_tac1 t; apply /setI2_P;split => //.
by apply: pb.
have sxa: sub Xa a by apply: subsetI2r.
move: (pa _ sxa Xane) => [ea sea eap].
set Xb:= Zo X (fun t => glt r ea t).
case: (emptyset_dichot Xb) => Xbne.
have eax: inc ea X by move: sea;move /setI2_P=> [].
exists ea => //; move => x xE le1; ex_middle ne.
by empty_tac1 x; apply: Zo_i => //;split => //; apply:nesym.
have sxb: sub Xb b.
move => t /Zo_P [tx [le1 ne1]].
move: (Xu _ tx);case /setU2_P=> // ta.
have txa: inc t Xa by rewrite /Xa; fprops.
by move: (eap _ txa le1) =>eq1; case: ne1.
move: (pb _ sxb Xbne) => [eb seb ebp].
have ebx: inc eb X by move: seb => /Zo_P [].
exists eb => //; move => x xE le1.
apply: ebp => //; apply: Zo_i => //.
move: seb => /Zo_P [_ lt1]; order_tac.
Qed.
Lemma Exercise6_29d r X: order r ->
finite_set X ->
(forall x, inc x X -> Noetherian_set r x) ->
Noetherian_set r (union X).
Proof.
move => or; move: X.
apply: (finite_set_induction).
move => _; rewrite setU_0; apply: Exercise6_29b.
move => a n Hrec aux.
have ->: union (a +s1 n) = (union a) \cup n.
set_extens t.
move => /setU_P [y ty] /setU1_P;
case => h; apply /setU2_P; [ left;union_tac | right; ue].
case /setU2_P.
move /setU_P=> [y ty ya]; union_tac.
by move => tn; apply /setU_P;exists n;fprops.
apply: (Exercise6_29c or); last by apply: aux; fprops.
apply: Hrec=> x xa; apply: aux; fprops.
Qed.
Lemma Exercise6_29e r X: order r -> Noetherian r ->
sub X (substrate r) -> Noetherian_set r X.
Proof.
move => or Nr xsr.
rewrite (Noetherian_set_pr or xsr) => Y YX neY.
move: (sub_trans YX xsr) => Ysr.
move: (Nr _ Ysr neY) => [a []]. rewrite (iorder_sr or Ysr) => pa pb.
by ex_tac; move => x xY ax; apply: pb; apply /iorder_gleP.
Qed.
Lemma Exercise6_29f r: order r ->
(Noetherian r <->
(forall i, inc i (substrate r) -> Noetherian_set r (interval_ou r i))).
Proof.
move => or; split => h.
by move => i isr; apply: (Exercise6_29e or h); apply: Zo_S.
move => X Xsr neX.
move: (neX) => [a aX].
case: (p_or_not_p (maximal (induced_order r X) a)) => ma.
by exists a.
set Y := Zo X (fun z => glt r a z).
case: (emptyset_dichot Y) => neY.
case: ma; split; first by rewrite (iorder_sr or Xsr).
move => x /iorder_gle5P [_ pa pb].
by ex_middle exa; empty_tac1 x; apply: Zo_i=> //; split => //; apply: nesym.
have sY: sub Y (interval_ou r a).
move => y /Zo_P [yX ay]; apply /Zo_P; split => //; order_tac. fprops.
move: (h _ (Xsr _ aX)).
have Isr: sub (interval_ou r a) (substrate r) by apply: Zo_S.
rewrite (Noetherian_set_pr or Isr) => aux.
move: (aux _ sY neY) => [b ibY etc].
move: ibY => /Zo_P [bX ab].
exists b; split; first by rewrite (iorder_sr or Xsr).
move=> x /iorder_gle5P [_ xX bx].
apply: etc => //;apply /Zo_P; split => //; order_tac.
Qed.
Definition restriction_to_segmentA r x g :=
[/\ order r, inc x (substrate r), function g& sub (segment r x) (source g)].
Lemma rts_function1 r x g: restriction_to_segmentA r x g ->
function (restriction_to_segment r x g).
Proof.
move=> [p1 p2 p3 p4].
rewrite /restriction_to_segment; apply: (proj31 (restriction1_prop p3 p4)).
Qed.
Lemma rts_W1 r x g a: restriction_to_segmentA r x g ->
glt r a x -> Vf (restriction_to_segment r x g) a = Vf g a.
Proof.
move=> [p1 p2 p3 p4] ax.
rewrite /restriction_to_segment; apply: restriction1_V =>//.
rewrite /segment/interval_uo; apply: Zo_i=>//; order_tac.
Qed.
Lemma rts_surjective1 r x g: restriction_to_segmentA r x g ->
surjection (restriction_to_segment r x g).
Proof.
move=> [p1 p2 p3 p4].
rewrite /restriction_to_segment.
by apply: restriction1_fs.
Qed.
Lemma rts_extensionality1 r s x f g:
order r -> inc x (substrate r) -> order s -> inc x (substrate s) ->
segment r x = segment s x ->
function f -> sub (segment r x) (source f) ->
function g -> sub (segment s x) (source g) ->
(forall a , inc a (segment r x) -> Vf f a = Vf g a) ->
restriction_to_segment r x f = restriction_to_segment s x g.
Proof.
move=> wor xsr wos xss srsx ff srf fg ssg sv.
have rf: (restriction_to_segmentA r x f) by done.
have rg: (restriction_to_segmentA s x g) by done.
apply: function_exten =>//; try apply: rts_function1;
try solve [rewrite /restriction_to_segment/restriction1; aw].
rewrite /restriction_to_segment/restriction1; aw.
set_extens t.
move/(Vf_image_P ff srf)=> [u us Wu]; apply /(Vf_image_P fg ssg).
by rewrite - srsx; ex_tac; rewrite - sv.
move/(Vf_image_P fg ssg)=> [u us Wu]; apply /(Vf_image_P ff srf).
by rewrite - srsx in us; ex_tac; rewrite sv.
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_W1 // rts_W1 // sv //.
Qed.
Lemma transfinite_unique11 r p f f' z: order r ->
inc z (substrate r) ->
transfinite_def r p f -> transfinite_def r p f' ->
(forall x : Set, inc x (segment r z) -> Vf f x = Vf f' x) ->
restriction_to_segment r z f = restriction_to_segment r z f'.
Proof.
move=> wo zsr [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW.
have ss: sub (segment r z) (substrate r) by apply: sub_segment.
apply: rts_extensionality1=> //; ue.
Qed.
Lemma inc_set_of_segments1 r x: order r ->
inc x (segments r) -> segmentp r x.
Proof.
rewrite /segments/segmentss=> or.
case /setU1_P.
by move /funI_P => [z zr ->]; apply: segment_segment=>//.
by move=> ->; apply: substrate_segment.
Qed.
Lemma Exercise_6_20b a:
\2c <c a ->
(forall m, \0c <c m -> m <c a -> a ^c m = a) -> regular_cardinal a.
Proof.
move => a2 h.
have ca: cardinalp a by co_tac.
case: (finite_dichot ca).
move /BnatP => aB.
move: (h _ card_lt_02 a2); rewrite cpowx2 => eq1.
have aa: a <=c a by fprops.
have anz: a <> \0c by move => eq2; rewrite eq2 in a2; case: (card_lt0 a2).
move: (cprod_Mlelt aB aB aa a2 anz); rewrite eq1 => le1.
move: (cprod_M1le ca card2_nz) => le2; co_tac.
move => ica; apply /regular_cardinalP; split; first by exact.
ex_middle ne1.
have sa: singular_cardinal a by split.
have pa: (cpow_less_ec_prop a a \1c).
split; first by apply: finite_lt_infinite; fprops.
move => b; rewrite (cpowx1 ca); move /card_ge1P => b1 ba.
by rewrite (h _ b1 ba).
move: (cantor ca); rewrite - (infinite_power1_b ica).
move: (cpow_less_ec_pr3 pa (proj1 a2) sa) => [-> <-].
by rewrite (cpowx1 ca); move => [].
Qed.
Lemma Exercise_6_20c1 a:
GenContHypothesis -> regular_cardinal a ->
(forall m, \0c <c m -> m <c a -> a ^c m = a).
Proof.
move => gch /regular_cardinalP [ia ra] m [_ m0] ma.
move: (infinite_power10 gch m ia); move=> [_ pa _ _].
by apply: pa; [ apply:nesym | ue].
Qed.
Lemma Exercise_6_20c2:
(forall a, regular_cardinal a ->
(forall m, \0c <c m -> m <c a -> a ^c m = a)) ->
GenContHypothesis.
Proof.
move => h.
move => t ict; move: (ict) => [ct _].
move: (ord_index_pr1 ict)=> [on tv].
move: (regular_initial_successor on).
rewrite - (succ_c_pr on) tv => rs.
move: (h _ rs _ (finite_lt_infinite finite_0 ict) (succ_c_pr2 ct)).
move => le1.
apply: card_leA; first by apply: (succ_c_pr3 ct).
have pa: \2c <=c succ_c t.
rewrite -tv (succ_c_pr on).
apply: (finite_le_infinite finite_2 (aleph_pr5c (OS_succ on))).
by rewrite -le1; apply: (cpow_Mleeq _ pa card2_nz).
Qed.
Lemma Exercise6_22c1 x:
card_dominant x ->
(x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
Proof.
move => [pa pb].
move: (ord_index_pr1 pa); set c := ord_index x; move => [pd pe].
case: (limit_ordinal_pr2 pd) => ln;last by right; exists c.
by left; rewrite -pe ln aleph_pr1.
move: ln => [m om mv].
set y:= \aleph m.
have yx: y <c x.
by rewrite /y -pe; apply: aleph_lt_ltc; rewrite mv; apply: ord_succ_lt.
move: (pb _ _ yx yx); rewrite (infinite_power1_b (aleph_pr5c om)) => le1.
move: (succ_c_pr3 (CS_aleph om));rewrite (succ_c_pr om) -mv pe => le2;co_tac.
Qed.
Lemma Exercise6_22c2 x
(p1 := forall z, \0c <c z -> z <c x -> x ^c z = x)
(p2:= forall z, \0c <c z -> x ^c z = x *c \2c ^c z):
[/\ (infinite_c x -> p1 -> p2),
(card_dominant x -> (p1 <-> p2)),
(card_dominant x -> p1 -> (x = omega0 \/ inaccessible x)) &
(x = omega0 \/ inaccessible x -> (card_dominant x /\ p1))].
Proof.
have r1:infinite_c x -> p1 -> p2.
move=> icx hp1 z zp.
move: (infinite_ge_two icx) => x2.
move: (infinite_nz icx) => xnz.
have cz: cardinalp z by co_tac.
case: (card_le_to_ee (proj1 icx) (CS_pow \2c z)).
move => le1.
move: (ge_infinite_infinite icx le1) => icp.
case: (finite_dichot cz) => icz.
have f1: finite_c (\2c ^c z).
by apply /BnatP; apply BS_pow; fprops; rewrite inc_Bnat.
case: (infinite_dichot1 f1 icp).
rewrite (infinite_power1 x2 le1 icz).
by rewrite cprodC product2_infinite.
have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
move => le1.
rewrite (hp1 _ zp (card_lt_leT (cantor cz) le1)).
rewrite product2_infinite //.
have r2: card_dominant x -> (p1 <-> p2).
move=> [icx cdx]; split; first by apply: r1.
move => hp2 z z0 zx.
have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
move: (cdx _ _ (finite_lt_infinite finite_2 icx) zx) => [l1 _].
rewrite (hp2 _ z0) product2_infinite //.
have r3: card_dominant x -> p1 -> x = omega0 \/ inaccessible x.
move => pa pc; case: (Exercise6_22c1 pa); first by left.
move => h; right.
move: pa => [pa pb].
split; last first.
by move => t tx; apply: pb => //; apply: (finite_lt_infinite finite_2 pa).
split; last by exact.
move: (cofinality_c_small (infinite_ge_two pa)) => h1.
split => //; ex_middle eq1.
have pd: \0c <c cofinality_c x.
apply: (finite_lt_infinite finite_0 (cofinality_infinite pa)).
move: (power_cofinality (infinite_ge_two pa)).
by rewrite (pc _ pd (conj h1 eq1)); move => [_].
split => //.
case => ix.
rewrite ix; split; first by apply: card_dominant_pr2.
move => z z0 zf.
have pa: infinite_c x by rewrite ix; apply: omega_infinitec.
have pb: inc z Bnat.
by rewrite ix in zf; move:(ordinal_cardinal_lt zf) => /ord_ltP0 [_ _].
have pc: z <> \0c by move: z0 => [_ /nesym].
by rewrite power_of_infinite.
split; first by apply: inaccessible_dominant.
by move => z [_ zc] zx;apply: inaccessible_pr7 => //; apply:nesym.
Qed.
Exercise 6 33
Section Exercise6_33.
Variables a b E F: Set.
Hypothesis ha: \2c <=c a.
Hypothesis hb: \1c <=c b.
Hypothesis iab: infinite_c a \/ infinite_c b.
Hypothesis HF0: sub F (powerset E).
Hypothesis HF1: a ^c b <c cardinal F.
Hypothesis HF2: forall x, inc x F -> cardinal x <=c b.
Definition Ex6_33_conc:=
exists G q, [/\ sub G F , a ^c b <c cardinal G &
forall a b, inc a G -> inc b G -> a <> b -> intersection2 a b = q].
Lemma Exercise6_33a: infinite_c (a ^c b).
Proof.
have ca: cardinalp a by move: ha => [_ ca _].
have bnz : b <> \0c.
move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
move: (cpow_Mleeq b ha card2_nz) => h1.
case iab => iiab; first by apply: infinite_pow => //.
exact: (ge_infinite_infinite (infinite_powerset iiab) h1).
Qed.
Definition E6_33_c := succ_c (a ^c b).
Definition E6_33_X :=
choose (fun f => injection_prop f E6_33_c F).
Definition E6_33_M := unionb (Lg (source E6_33_X) (Vf E6_33_X)).
Lemma Exercise6_33b (d := (a ^c b)):
[/\ d <c E6_33_c,
(forall z, d <c z -> E6_33_c <=c z) &
(forall z, z <c E6_33_c -> z <=c d)].
Proof.
move: (succ_c_pr1 (proj1 (Exercise6_33a))).
move => [pa pb pc]; split => // z; apply: succ_c_pr4; fprops.
Qed.
Lemma Exercise6_33c: infinite_c E6_33_c.
Proof.
move: Exercise6_33a Exercise6_33b => pb [[pa _] _ _].
by move: (ge_infinite_infinite pb pa).
Qed.
Lemma Exercise6_33d (f := E6_33_X):
injection_prop f E6_33_c F.
Proof.
rewrite /f/ E6_33_X; apply choose_pr; apply eq_subset_ex_injP.
apply /eq_subset_cardP1.
move: ( Exercise6_33b)=> [[[_ cc _] _] pa _].
by rewrite (card_card cc);apply: pa.
Qed.
Lemma Exercise6_33e n: inc n E6_33_c -> sub (Vf E6_33_X n) E6_33_M.
Proof.
move => nc.
move: Exercise6_33d => [[fx ix] sx tx].
rewrite /E6_33_M => t tw; apply /setUb_P; bw; rewrite sx; ex_tac; bw.
Qed.
Lemma Exercise6_33f: cardinal E6_33_M = E6_33_c.
Proof.
have le: cardinal E6_33_M <=c E6_33_c.
set f := (Lg (source E6_33_X) (fun z => Vf E6_33_X z)).
have fx: fgraph f by rewrite /f; fprops.
move: (csum_pr1 f); rewrite -/ E6_33_M; bw.
set f1 := (Lg (domain f) (fun a0 : Set => cardinal (Vg f a0))).
set g := cst_graph (source E6_33_X) b.
have f1x: fgraph f1 by rewrite /f1/cst_graph; fprops.
have gx: fgraph g by rewrite /g/cst_graph; fprops.
have sd: domain f1 = domain g by rewrite /f1 /g /f /cst_graph; bw.
move: Exercise6_33d => [[ff ijf] sf tf].
have le1: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg g x).
rewrite /f1/f/g/cst_graph; bw => x xd; bw; apply: HF2.
by rewrite -tf; Wtac.
move: (csum_increasing sd le1).
rewrite /g csum_of_same sf.
have pd: b <=c E6_33_c.
move: Exercise6_33b => [qa qb qc].
apply: (card_leT (proj1 (cantor (proj32 hb)))).
apply: card_leT (proj1 qa); apply: cpow_Mleeq => //; apply card2_nz.
have bnz : b <> \0c.
move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
move: Exercise6_33c => pc.
rewrite cprodC product2_infinite //.
by move => le2 le3; co_tac.
ex_middle ne.
move: Exercise6_33b => [sa sb sc]; move: (sc _ (conj le ne)) => le1.
move: le => [_ cc _].
set T := (fun_image (functions b E6_33_M) image_of_fun) +s1 emptyset.
move: (Exercise6_33d) => [[fx ix] sx tx].
have pa: forall i, inc i E6_33_c -> inc (Vf E6_33_X i) T.
move => i ic.
rewrite - sx in ic.
move: ((Vf_target fx) _ ic); rewrite tx => wf.
move: (HF2 wf) => cl.
case: (emptyset_dichot (Vf E6_33_X i)) => wne; first by rewrite wne /T; fprops.
apply /setU1_P; left; aw.
move: cl; rewrite - {1} (card_card (proj32 hb)) => le2.
have [c cb ecb]: equipotent_to_subset (Vf E6_33_X i) b.
apply /(eq_subset_cardP); exact: (cardinal_le_aux1 le2).
have [f [bf sf tf]]: c \Eq Vf E6_33_X i by eqsym.
pose g z := Yo (inc z c) (Vf f z) (rep (Vf E6_33_X i)).
have pa: forall z, inc (g z) (Vf E6_33_X i).
move => z; rewrite /g; Ytac zc; last by apply: rep_i.
rewrite -tf; Wtac; fct_tac.
have pb: forall z, inc z (Vf E6_33_X i) -> exists2 i, inc i b & g i = z.
rewrite -tf; move=> z ztf; move: ((proj2 (proj2 bf)) _ ztf)=> [y ysf <-].
rewrite sf in ysf; exists y; [by apply: cb | by rewrite /g; Ytac0].
have pc: lf_axiom g b E6_33_M.
move => z zb; move: (pa z) => i1; apply /setUb_P; bw; ex_tac; bw.
set G := Lf g b E6_33_M.
have fg: function G by apply: lf_function.
have pd: inc G (functions b E6_33_M).
by rewrite /G;apply /fun_set_P;split => //; aw.
apply /funI_P;ex_tac; symmetry;set_extens t.
move /(Vf_image_P1 fg) => [u usg ->].
rewrite /G; aw; move: usg; rewrite /G;aw.
move => tw; move: (pb _ tw) => [z zi <-]; apply /(Vf_image_P1 fg).
exists z; rewrite /G; aw;split => //.
have : equipotent_to_subset E6_33_c T.
rewrite eq_subset_ex_injP.
exists (Lf (fun z => (Vf E6_33_X z)) E6_33_c T); split; aw.
apply: lf_injective; first by apply: pa.
rewrite - sx; apply: ix.
move /eq_subset_cardP1; rewrite (card_card cc) => eq1.
set T1:= fun_image (functions b E6_33_M) image_of_fun.
set aa:= (functions b E6_33_M); set ff:= image_of_fun.
have sj: (surjection (Lf ff aa (fun_image aa ff))).
apply: lf_surjective.
by move=> t ta; apply /funI_P;exists t.
by move=> y /funI_P.
move: (image_smaller_cardinal (proj1 sj)).
move: (surjective_pr0 sj); aw; move => ->; rewrite /aa /ff -/T1.
rewrite cpow_pr1 (card_card (proj32 hb)).
have ->: cardinal T1 = cardinal T.
case: (inc_or_not emptyset T1) => eT.
by rewrite /T (setU1_eq eT).
move: Exercise6_33c => i1.
move: (ge_infinite_infinite Exercise6_33c eq1) => it.
have pb: cardinal T = succ (cardinal T1) by rewrite /T -/T1 (card_succ_pr eT).
case: (finite_dichot (CS_cardinal T1)).
move/ (finite_succP (CS_cardinal T1)); rewrite - pb => nit.
case: (infinite_dichot1 nit it).
by move /infinite_cP; rewrite - pb; move => [_].
move => l2; move: (card_leT eq1 l2).
have bnz : b <> \0c.
move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
case: (equal_or_not (cardinal E6_33_M) \0c) => mz.
by rewrite mz (cpow0x bnz) => h; symmetry; apply: card_le0.
move: (cpow_Mleeq b le1 mz); rewrite - cpow_pow.
suff ->: a ^c (b *c b) = a ^c b.
by move => l1 l3; move: (card_leT l3 l1) => l4; co_tac.
case: (finite_dichot (proj32 hb)) => fb.
move: fb => /BnatP => fb.
move: (BS_prod fb fb) => fb2.
case: iab => fa.
rewrite (power_of_infinite fa fb2 (cprod2_nz bnz bnz)).
by rewrite (power_of_infinite fa fb bnz).
by rewrite square_of_infinite.
by rewrite square_of_infinite.
Qed.
Definition E6_33_x:= choose (fun z => bijection_prop z E6_33_c E6_33_M).
Definition E6_33_r :=
image_by_fun (ext_to_prod E6_33_x E6_33_x) (ordinal_o E6_33_c).
Definition E6_33_rho n := ordinal (induced_order E6_33_r (Vf E6_33_X n)).
Lemma Exercise6_33g : bijection_prop E6_33_x E6_33_c E6_33_M.
Proof.
move: Exercise6_33f.
rewrite -{1} (card_card (proj1 Exercise6_33c)) => h.
by rewrite /E6_33_x; apply choose_pr; eqsym; apply /card_eqP.
Qed.
Lemma Exercise6_33h (x := E6_33_x) (r:= E6_33_r) (c := E6_33_c):
[/\ worder_on r E6_33_M,
order_isomorphism x (ordinal_o E6_33_c) r &
(forall a b, inc a c -> inc b c ->
(a <=o b <-> gle r (Vf x a) (Vf x b)))].
Proof.
move: (proj1 (proj1 Exercise6_33c)) => oc.
move: (ordinal_o_wor oc) => wo1; move: (wo1) => [o1 _].
move: (ordinal_o_sr E6_33_c) => sr1.
move: Exercise6_33g; rewrite -/x; move => [bx sx tx].
rewrite -{2} sx in sr1.
move: (order_transportation bx o1 sr1); rewrite /x -/ E6_33_r -/r => oi1.
move: (oi1) => [_ or [_ _ sr2] xinc].
red in xinc; rewrite tx in sr2; rewrite sx in xinc.
have wo: worder r by apply: worder_invariance wo1; exists E6_33_x.
split => //.
move => u v ux vx; rewrite - (xinc _ _ ux vx); split.
move => [_ _ h]; apply /ordo_leP;split => //.
move /ordo_leP => [_ _ h]; split => //; ord_tac0.
Qed.
Lemma Exercise6_33i n: inc n E6_33_c ->
[/\ worder (induced_order E6_33_r (Vf E6_33_X n)),
ordinalp (E6_33_rho n) & cardinal (E6_33_rho n) <=c b].
Proof.
move => ni; rewrite /E6_33_rho.
set r := induced_order _ _.
move: Exercise6_33h => [[wo1 sr] oi oie].
move: Exercise6_33d => [[fx ix] sx tx].
have wr: inc (Vf E6_33_X n) F by rewrite -tx; Wtac.
move: (Exercise6_33e ni); rewrite - sr => pa.
have wor: worder r by move: (induced_wor wo1 pa).
split; first (by exact);first by apply: OS_ordinal.
rewrite (cardinal_of_ordinal wor) (iorder_sr (proj1 wo1) pa).
by apply: HF2.
Qed.
Definition E6_33_y n := the_ordinal_iso (induced_order E6_33_r (Vf E6_33_X n)).
Definition E6_33_Mi m := Zo E6_33_M
(fun z => exists n, [/\ inc n E6_33_c, inc m (source (E6_33_y n)) &
z = Vf (E6_33_y n) m]).
Definition E6_33_al :=
intersection (Zo (a ^c b) (fun m => (cardinal (E6_33_Mi m) = E6_33_c))).
Lemma Exercise6_33j n
(yn := E6_33_y n) (r := induced_order E6_33_r (Vf E6_33_X n)):
inc n E6_33_c ->
[/\ order_isomorphism yn (ordinal_o (E6_33_rho n)) r,
source yn = E6_33_rho n & target yn = (Vf E6_33_X n)].
Proof.
move=> nc.
have pa: order_isomorphism yn (ordinal_o (E6_33_rho n)) r.
by apply: the_ordinal_iso1; move: (Exercise6_33i nc) => [].
move: (pa) => [_ _ [_ sf tf] _].
move: (Exercise6_33i nc) => [pd pb pc].
rewrite sf tf.
move: (Exercise6_33h) => [[pe pf] _ _].
have pg: sub (Vf E6_33_X n) (substrate E6_33_r).
by rewrite pf; apply: Exercise6_33e.
by rewrite ordinal_o_sr /r (iorder_sr (proj1 pe)).
Qed.
Lemma Exercise6_33k n: inc n E6_33_c ->
((forall t, inc t (E6_33_rho n) -> t <o a ^c b)
/\ sub (E6_33_rho n) E6_33_c).
Proof.
move=> ns.
move: Exercise6_33b => [sa sb sc].
have le1: b <c a ^c b.
apply: card_lt_leT (cpow_Mleeq b ha card2_nz).
exact (cantor (proj32 hb)).
move: (Exercise6_33i ns) => [_ qa qb].
move: (card_le_ltT qb le1).
move/(ordinal_cardinal_le2P (CS_pow a b) qa) => h.
split.
move => t /(ord_ltP qa) [pa _]; ord_tac.
have o3: ordinalp E6_33_c by exact (proj1 (proj1 Exercise6_33c)).
move: h sa => [[_ _ s1] _] [[_ _ s2] _].
apply: (sub_trans s1 s2).
Qed.
Lemma Exercise6_33l: E6_33_M = unionb (Lg (a ^c b) E6_33_Mi).
Proof.
set_extens x.
move: Exercise6_33d => [[fc ix] sx tx].
move => xM; move: (xM) => /setUb_P; bw; move => [y ys]; bw => xW.
rewrite sx in ys.
move: (Exercise6_33j ys) => [[o1 o2 [bf sf tf] _] sy ty].
rewrite - ty in xW.
move: (proj2 (proj2 bf) _ xW) => [n ns xv].
move: ( Exercise6_33k ys) => [s1 s2].
rewrite - sy in s1; move: (s1 _ ns) => ns1.
move: (s1 _ ns) => /(ord_ltP (proj32_1 ns1)) np.
apply /setUb_P; exists n=> //; bw; apply: Zo_i; first by exact.
exists y; split => //.
by move /setUb_P; bw;move => [y yp]; bw => /Zo_P [].
Qed.
Lemma Exercise6_33m x (c:= cardinal (E6_33_Mi x)):
inc x (a ^c b) -> c <=c (a ^c b) \/ c = E6_33_c.
Proof.
move: Exercise6_33l => eq1 xs.
have s1: sub (E6_33_Mi x) E6_33_M.
move =>t ti; rewrite eq1; apply /setUb_P; bw; ex_tac; bw.
move: (sub_smaller s1); rewrite Exercise6_33f => le1.
move:(Exercise6_33b) => [pa pb pc].
by case: (equal_or_not c E6_33_c) => cc; [ right | left; apply: pc; split].
Qed.
Lemma Exercise6_33n: exists2 m,
m <o (a ^c b) & (cardinal (E6_33_Mi m)) = E6_33_c.
Proof.
ex_middle pa.
have le1: forall x, inc x (a ^c b) -> cardinal (E6_33_Mi x) <=c (a ^c b).
move=> x xab; case: (Exercise6_33m xab) => // e1; case: pa; exists x => //.
have oab: ordinalp (a ^c b) by move: (CS_pow a b) => [].
by move: xab => /(ord_ltP oab).
set f := (Lg (a ^c b) E6_33_Mi).
move: (csum_pr1 f); rewrite /f -/E6_33_M - Exercise6_33l Exercise6_33f.
rewrite /card_sumb;bw.
set f1 := Lg _ _.
set f2 := cst_graph (a ^c b) (a ^c b).
have fgf1: fgraph f1 by rewrite /f1; fprops.
have fgf2: fgraph f2 by rewrite /f2/cst_graph; fprops.
have sd: domain f1 = domain f2 by rewrite /f1/f2/cst_graph; bw.
have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x).
by rewrite /f1/f2/cst_graph;bw => x xa; bw; apply: le1.
move: (csum_increasing sd pb).
rewrite /f2 csum_of_same (square_of_infinite Exercise6_33a).
move => l1 l2; move: (card_leT l2 l1) => l3.
move: (Exercise6_33b) => [l4 _ _]; co_tac.
Qed.
Lemma Exercise6_33o (al:= E6_33_al):
[/\ al <o (a ^c b), (cardinal (E6_33_Mi al) = E6_33_c) &
(forall m, m <o al -> cardinal (E6_33_Mi m) <=c (a ^c b))].
Proof.
rewrite /al /E6_33_al; set Z := Zo _ _.
have oab: ordinalp (a ^c b) by move: (CS_pow a b) => [].
have nez: nonempty Z.
move: Exercise6_33n => [m [m1 m2]]; exists m; apply: Zo_i=> //.
by apply/(ord_ltP oab).
have oz: ordinal_set Z by move=> t => /Zo_P [tab _]; ord_tac0.
move: (ordinal_setI nez oz); set c := intersection Z => cz.
move: (cz) => /Zo_P [pa pb].
have lt: c <o a ^c b by apply /(ord_ltP oab).
split => //.
move => m mc; move: (ord_lt_leT mc (proj1 lt)).
move/(ord_ltP oab) => mab.
case: (Exercise6_33m mab) => // eq1.
move: mc => /(ord_ltP (oz _ cz)) mc.
have mz: inc m Z by apply: Zo_i.
case: (ordinal_irreflexive (oz _ mz) (setI_hi mc mz)).
Qed.
Lemma Exercise6_33p:
cardinal (unionb (Lg E6_33_al E6_33_Mi)) <=c a ^c b.
Proof.
set f := Lg _ _.
move: (csum_pr1 f); rewrite /card_sumb.
set f1 := Lg _ _.
set f2 := cst_graph E6_33_al (a ^c b).
have fgf1: fgraph f1 by rewrite /f1; fprops.
have fgf2: fgraph f2 by rewrite /f2/cst_graph; fprops.
have sd: domain f1 = domain f2 by rewrite /f1/f/f2/cst_graph; bw.
have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x).
rewrite /f1/f/f2/cst_graph; bw => x xa; bw.
move: Exercise6_33o=> [[[oa _] _] _ _]; apply.
by apply /(ord_ltP oa).
move: (csum_increasing sd pb).
move => l1 l2; move: (card_leT l2 l1).
move: Exercise6_33o=> [[pa _] _ _].
rewrite /f2 csum_of_same => l3; apply: (card_leT l3).
move: (ordinal_cardinal_le1 pa); rewrite (card_card (CS_pow a b)) => le3.
rewrite - cprod2_pr2b; apply: (product2_infinite1 le3 Exercise6_33a).
Qed.
Definition E6_33_N0 := fun_image (E6_33_Mi E6_33_al)
(fun t => rep (Zo E6_33_c
(fun n => inc E6_33_al (source (E6_33_y n))
/\ Vf (E6_33_y n) E6_33_al = t))).
Lemma Exercise6_33q (N0 := E6_33_N0) (al := E6_33_al)
(Ma := E6_33_Mi E6_33_al):
[/\ forall t, inc t N0 ->
[/\ inc t E6_33_c, inc al (source (E6_33_y t))& inc (Vf (E6_33_y t) al) Ma],
(forall t1 t2, inc t1 N0 -> inc t2 N0 ->
(Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2),
(forall s, inc s Ma -> exists2 t, inc t N0 & s = (Vf (E6_33_y t) al)),
sub N0 E6_33_c &
cardinal N0 = E6_33_c].
Proof.
pose Z z := Zo E6_33_c
(fun n : Set =>
inc E6_33_al (source (E6_33_y n)) /\ Vf (E6_33_y n) E6_33_al = z).
have znz: forall z, inc z (E6_33_Mi E6_33_al) -> nonempty (Z z).
move => z => /Zo_P [zM [n [nc als zv]]].
by exists n; apply: Zo_i.
have pa: forall t, inc t N0 ->
[/\ inc t E6_33_c, inc al (source (E6_33_y t)) & inc (Vf (E6_33_y t) al) Ma].
move => t /funI_P [z z1 rz].
move: (rep_i (znz _ z1)); rewrite rz; move /Zo_P => [pa [pb pc]].
split => //; rewrite pc //.
have pb: (forall t1 t2, inc t1 N0 -> inc t2 N0 ->
(Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2).
move => t1 t2 t1n t2n sv.
move: t1n => /funI_P [z z1 rz].
move: (rep_i (znz _ z1)); rewrite rz; move => /Zo_hi [_ pc].
move: t2n => /funI_P [z' z1' rz'].
move: (rep_i (znz _ z1')); rewrite rz'; move /Zo_hi => [_ pc'].
by move: pc pc' sv; rewrite - {1}rz - {1} rz' -/al => -> -> ->.
have pc: (forall s, inc s Ma -> exists2 t, inc t N0 & s = Vf (E6_33_y t) al).
move => s sm.
set u := rep (Z s).
have un: inc u N0 by apply /funI_P; rewrite -/Ma; exists s => //.
exists u => //.
by move: (rep_i (znz _ sm)) => /Zo_P [_ [_ ->]].
split => //.
by move => t tn; move: (pa _ tn) => [ok _].
set f:= Lf (fun t => Vf (E6_33_y t) al) N0 Ma.
have bf: bijection f.
by apply: lf_bijective => // t ta; move: (pa _ ta) => [_ _ ok].
have: (source f \Eq target f) by exists f; split => //.
rewrite /f; aw; move /card_eqP.
by move: Exercise6_33o => [_ -> _].
Qed.
End Exercise6_33.
End Exercise6.
A numeration is a functional graph f such that f(x)
is the set of all f(y)
where y<x for r. A set is numerable if well-ordered and there is a
numeration.
Definition numeration r f:=
[/\ fgraph f, domain f = substrate r &
forall x, inc x (domain f) -> Vg f x = direct_image f (segment r x)].
Definition numerable r :=
worder r /\ exists f, numeration r f.
Each set has at most one numeration
Lemma direct_image_exten f f' a:
fgraph f -> fgraph f' -> (forall x, inc x a -> Vg f x = Vg f' x) ->
sub a (domain f) -> sub a (domain f') ->
direct_image f a = direct_image f' a.
Proof.
move=> fgf fgf' sVVg adf adf'.
set_extens x; move /dirim_P => [u us Jg]; apply /dirim_P; ex_tac.
move: (pr2_V fgf Jg); aw; move=> ->; rewrite (sVVg _ us).
by apply: fdomain_pr1 =>//; apply: adf'.
move: (pr2_V fgf' Jg); aw; move=> ->; rewrite -(sVVg _ us).
by apply: fdomain_pr1 =>//; apply: adf.
Qed.
Lemma numeration_unique r f f':
worder r -> numeration r f -> numeration r f' -> f = f'.
Proof.
move=> [or wor] [fgf df Vf][fgf' df' Vf'].
set A :=Zo (substrate r)(fun x=> Vg f x <> Vg f' x).
case: (emptyset_dichot A)=> neA.
apply: fgraph_exten=>//; try ue.
rewrite df=> a xdf.
by ex_middle nVV; empty_tac1 a; rewrite /A; apply: Zo_i.
have sAs: sub A (substrate r) by apply: Zo_S.
move: (wor _ sAs neA)=> [y []]; aw => yA leyA.
move: (sAs _ yA)=> ysr.
have srp: forall z, inc z (segment r y) -> Vg f z = Vg f' z.
move=> z /segmentP zy.
ex_middle nVV.
have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac.
move: (iorder_gle1 (leyA _ zA)) => yz; order_tac.
have nyA: Vg f y = Vg f' y.
rewrite df in Vf; rewrite df' in Vf'.
rewrite Vf // Vf' //.
apply: direct_image_exten =>//.
rewrite df; apply: sub_segment.
rewrite df'; apply: sub_segment.
move: yA => /Zo_P [_ cnyA]; contradiction.
Qed.
fgraph f -> fgraph f' -> (forall x, inc x a -> Vg f x = Vg f' x) ->
sub a (domain f) -> sub a (domain f') ->
direct_image f a = direct_image f' a.
Proof.
move=> fgf fgf' sVVg adf adf'.
set_extens x; move /dirim_P => [u us Jg]; apply /dirim_P; ex_tac.
move: (pr2_V fgf Jg); aw; move=> ->; rewrite (sVVg _ us).
by apply: fdomain_pr1 =>//; apply: adf'.
move: (pr2_V fgf' Jg); aw; move=> ->; rewrite -(sVVg _ us).
by apply: fdomain_pr1 =>//; apply: adf.
Qed.
Lemma numeration_unique r f f':
worder r -> numeration r f -> numeration r f' -> f = f'.
Proof.
move=> [or wor] [fgf df Vf][fgf' df' Vf'].
set A :=Zo (substrate r)(fun x=> Vg f x <> Vg f' x).
case: (emptyset_dichot A)=> neA.
apply: fgraph_exten=>//; try ue.
rewrite df=> a xdf.
by ex_middle nVV; empty_tac1 a; rewrite /A; apply: Zo_i.
have sAs: sub A (substrate r) by apply: Zo_S.
move: (wor _ sAs neA)=> [y []]; aw => yA leyA.
move: (sAs _ yA)=> ysr.
have srp: forall z, inc z (segment r y) -> Vg f z = Vg f' z.
move=> z /segmentP zy.
ex_middle nVV.
have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac.
move: (iorder_gle1 (leyA _ zA)) => yz; order_tac.
have nyA: Vg f y = Vg f' y.
rewrite df in Vf; rewrite df' in Vf'.
rewrite Vf // Vf' //.
apply: direct_image_exten =>//.
rewrite df; apply: sub_segment.
rewrite df'; apply: sub_segment.
move: yA => /Zo_P [_ cnyA]; contradiction.
Qed.
A numeration of a segment is obtained by restriction
Lemma sub_numeration r f x:
let r' := induced_order r (segment r x) in
worder r -> numeration r f -> inc x (substrate r) ->
numeration r' (restr f (segment r x)).
Proof.
move=> r' wor num xsr.
move: (@sub_segment r x)=> sss.
move: (induced_wor wor sss)=> wor'.
move: num=> [fgf df pf].
have sr':substrate r' = (segment r x) by rewrite /r'; aw; fprops.
have dr:domain (restr f (segment r x)) = substrate r' by bw.
have ssd: sub (segment r x) (domain f) by ue.
split;fprops.
rewrite dr sr'; move=> a asr.
have sra: (segment r' a = (segment r a)).
rewrite /r'; apply: segment_induced_a =>//; fprops.
apply: segment_segment; fprops.
rewrite sra restr_ev // pf; try ue.
have ssad: sub (segment r a) (domain f).
move => w /segmentP; rewrite df => wlt; order_tac.
have sax: sub (segment r a) (segment r x).
move=> t; move: asr => /segmentP p1 /segmentP p2.
have or: order r by fprops.
apply /segmentP;order_tac.
apply: direct_image_exten; try rewrite dr sr'//; fprops.
move=> z zs; rewrite restr_ev => //.
by apply: sax.
Qed.
If all segments are numerable so is the whole set
Lemma segments_numerables r:
let r' := fun x => induced_order r (segment r x) in
worder r -> (forall x, inc x (substrate r)-> numerable (r' x)) ->
numerable r.
Proof.
move=> r' wor aln.
set f:= (fun x => choose (fun y=> numeration (r' x) y)).
have fp: forall x, inc x (substrate r) -> numeration (r' x) (f x).
by move=> x xsr; move: (aln _ xsr)=> [_ c];rewrite /f;apply: choose_pr.
set g:= fun x => range (f x).
have or: order r by fprops.
have restrp: forall x y, glt r y x ->
f y = restr (f x) (substrate (r' y)).
move=> x y ryx.
have sss: sub (segment r x) (substrate r) by apply: sub_segment.
have ssy: sub (segment r y) (substrate r) by apply: sub_segment.
have p6: worder (r' y) by rewrite /r'; apply: induced_wor =>//.
apply: (numeration_unique p6); first by apply: fp; order_tac.
have <-: (segment (r' x) y) = (substrate (r' y)).
rewrite /r'; aw; try apply: sub_segment; rewrite segment_induced //.
have p1: worder (r' x) by rewrite /r'; apply: induced_wor =>//.
have p2: numeration (r' x) (f x) by apply: fp; order_tac.
have p3: inc y (substrate (r' x)) by rewrite /r'; aw; apply /segmentP.
move: (sub_numeration p1 p2 p3) => p5.
have di: induced_order (r' x) (segment (r' x) y) = r' y.
rewrite /r' segment_induced // iorder_trans //.
apply: segment_monotone =>//; order_tac.
by rewrite di in p5.
have gp: forall x y, inc x (substrate r) -> glt r y x -> g y = Vg (f x) y.
move=> x y xsr yx; rewrite/g.
have ysr: (inc y (substrate r)) by order_tac.
move: (fp _ xsr) => [fg df vf].
move: df; rewrite /r' ; aw => df; last by apply: sub_segment.
have ysrx: (inc y (segment r x)) by apply /segmentP.
rewrite df in vf; rewrite (vf _ ysrx). rewrite (restrp _ _ yx).
have p0: (segment (r' x) y) = (substrate (r' y)).
rewrite /r'; aw; try apply: sub_segment; rewrite segment_induced //.
rewrite p0.
have gr: sgraph (restr (f x) (substrate (r' y))) by fprops.
have fgr: fgraph (restr (f x) (substrate (r' y))) by fprops.
have hh: sub (substrate (r' y)) (domain (f x)).
rewrite df; rewrite /r' (iorder_sr or (@sub_segment r y)).
apply:(segment_monotone or (proj1 yx)).
set_extens u.
move /(range_gP fgr); bw; move => [z pa pb]; apply /dirim_P; exists z => //.
by move: pb; bw => ->; apply:(fdomain_pr1 fg); apply: hh.
move /dirim_P => [z za zb];apply /(range_gP fgr); exists z; bw.
move: (pr2_V fg zb); aw.
split =>//; exists (Lg (substrate r) g).
red; bw; split;fprops.
move=> x xsr; bw; rewrite {1} /g.
move: (fp _ xsr) => [ff df vf].
move: df; rewrite /r' ; aw => df; last by apply: sub_segment.
have gf: sgraph (f x) by fprops.
have p0: sub (segment r x) (substrate r) by apply: sub_segment.
have fgL: fgraph (Lg (substrate r) g) by fprops.
set_extens t.
move=> /(range_gP ff) [z pa pb]; apply /dirim_P; exists z; first ue.
move: pa; rewrite df => /segmentP h; rewrite pb - (gp _ _ xsr h); apply: Lg_i.
order_tac.
move /dirim_P => [z xs JL]; move: (p0 _ xs) => zs.
move /segmentP: (xs) => lt1.
move: (pr2_V fgL JL); aw; bw => ->; rewrite (gp _ _ xsr lt1).
by apply /(range_gP ff); exists z => //; ue.
Qed.
Any well-ordered is numerable
Lemma worder_numerable r:
worder r -> numerable r.
Proof.
move=> wor; apply: segments_numerables =>//.
move=> x xsr.
set r' := fun x => induced_order r (segment r x).
set (A:= Zo (substrate r)(fun z=> ~numerable (r' z))).
case: (p_or_not_p (numerable (induced_order r (segment r x)))) =>//.
move => h.
have sA: (sub A (substrate r)) by rewrite /A; apply: Zo_S.
have neA: nonempty A by exists x; apply/Zo_P.
move: (wor)=> [or aux]; move: (aux _ sA neA)=> [y []]; aw=> ys yp.
have rec: forall z, glt r z y -> numerable (r' z).
move=>z zy; case: (p_or_not_p (numerable (r' z))) =>// nnz.
have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac.
move: (iorder_gle1 (yp _ zA)) => yz; order_tac.
move: ys => /Zo_P [ys ny]; case: ny.
have sss: sub (segment r y) (substrate r) by apply: sub_segment.
apply: segments_numerables.
rewrite /r'; apply: induced_wor =>//.
rewrite /r'; aw; move=> z zy.
have rzy: glt r z y by apply /segmentP.
rewrite segment_induced // iorder_trans //.
by apply: rec.
apply: segment_monotone =>//; order_tac.
Qed.
The previous result is obvious by transfinite_defined
Definition the_numeration r := transfinite_defined r target.
Lemma worder_numerable_bis r:
worder r -> numeration r (graph (the_numeration r)).
Proof.
move=> wor.
move: (transfinite_defined_pr target wor) => [suf sf vf].
set f := (transfinite_defined r target).
have ff: function f by fct_tac.
have dg: (domain (graph f) = substrate r) by rewrite f_domain_graph.
split;fprops.
rewrite dg.
move=> x xsr; move: (vf _ xsr); rewrite /Vf; move=> ->.
rewrite /restriction_to_segment/ restriction1; aw.
Qed.
End VonNeumann.
Lemma worder_numerable_bis r:
worder r -> numeration r (graph (the_numeration r)).
Proof.
move=> wor.
move: (transfinite_defined_pr target wor) => [suf sf vf].
set f := (transfinite_defined r target).
have ff: function f by fct_tac.
have dg: (domain (graph f) = substrate r) by rewrite f_domain_graph.
split;fprops.
rewrite dg.
move=> x xsr; move: (vf _ xsr); rewrite /Vf; move=> ->.
rewrite /restriction_to_segment/ restriction1; aw.
Qed.
End VonNeumann.
Require Import ssete2 sset10b.
Lemma BZdvd_latticeD: distributive_lattice1 BZdvdordering.
Proof.
suff: forall a b g z, inc a BZps -> inc b BZps -> inc g BZps -> inc z BZps ->
BZ_Bezout a b -> BZgcd z ((a *z b) *z g) %|z BZlcm (g *z a) (BZgcd (g *z b) z).
move => h.
apply:(proj32 (Exercise1_16b BZdvd_lattice)).
apply /(Exercise1_16cP BZdvd_lattice).
move => x y z; rewrite BZdvdordering_sr => xs ys zs.
rewrite (BZdvd_inf ys zs) (BZdvd_sup xs ys).
move: (BZpsS_gcd ys zs) (BZpsS_lcm xs ys) (BZpsS_gcd xs ys)=> gs ls g1s.
rewrite (BZdvd_inf zs ls) (BZdvd_sup xs gs).
apply /BZdvdordering_gle; split; first by apply: (BZpsS_gcd zs ls).
by apply: (BZpsS_lcm xs gs).
move /BZps_iP: (xs)=> [xp xnz]; move: (sub_BZp_BZ xp) => xz.
move /BZps_iP: (ys)=> [yp ynz]; move: (sub_BZp_BZ yp) => yz.
move /BZps_iP: (g1s)=> [g1p g1nz]; move: (sub_BZp_BZ g1p) => g1z.
move: (BZ_exists_Bezout3 xz yz (or_introl (y <> \0z) xnz)).
move: (BZpS_quo xp g1p) (BZpS_quo yp g1p).
rewrite (proj33 (BZlcm_prop1 xz yz)).
move: (BZgcd_div xz yz) => [].
set a := (x %/z BZgcd x y); set b := (y %/z BZgcd x y); set g := BZgcd x y.
move => e1 e2 az bz; rewrite e1 e2.
have ap: inc a BZps.
by apply/BZps_iP; split => // aez; case: xnz; rewrite e1 aez; qw.
have bp: inc b BZps.
by apply/BZps_iP; split => // aez; case: ynz; rewrite e2 aez; qw.
by apply: h.
move => a b g z azp bzp gzp zzp bzt.
set t := BZgcd g z.
move: (BZpsS_gcd gzp zzp); rewrite -/t => /BZps_iP [tp tnz].
move: (sub_BZps_BZ gzp) (sub_BZp_BZ tp) => gz tz.
move: (sub_BZps_BZ azp)(sub_BZps_BZ bzp)(sub_BZps_BZ zzp) => az bz zz.
move /BZps_iP: gzp => [gp gnz]; move /BZps_iP: azp => [ap anz].
move /BZps_iP: bzp => [_ bnz]; move: (BZSp az bz) => abz.
move: (BZSp gz az) (BZS_gcd (BZSp gz bz) zz) => pa pb.
move: (BZgcd_div gz zz).
move: (BZ_exists_Bezout3 gz zz (or_introl (z <> \0z) gnz)).
set g' := (g %/z t); set z' := (z %/z t); move => bz1 [eq1 eq2].
move: (BZS_quo gz tz) (BZS_quo zz tz); rewrite -/g' -/z'; move => g'z z'z.
move: (BZSp abz g'z) => abgz.
move: (BZS_gcd z'z bz) => gs1.
have ->: BZgcd z ((a *z b) *z g) = t *z BZgcd z' ((a *z b) *z g').
rewrite eq1 {1} eq2 -/t (BZprodC _ g').
rewrite (BZprodA abz g'z tz) (BZprodC _ t).
rewrite (BZgcd_prodD z'z abgz tp); reflexivity.
have cp1:BZ_coprime z' g'
by rewrite /BZ_coprime BZgcd_C;apply: (BZ_exists_Bezout2 g'z z'z bz1).
have ->: BZgcd z' ((a *z b) *z g') = BZgcd z' ((a *z b)).
rewrite BZprodC; apply: (BZgcd_simp z'z g'z abz cp1).
move: (BZlcm_prop1 pa pb) => [_ _ ->].
have ->: BZgcd (g *z a) (BZgcd (g *z b) z) = t.
rewrite /t (BZgcd_A (BZSp gz az)(BZSp gz bz) zz).
rewrite (BZgcd_prodD az bz gp).
move: (BZ_exists_Bezout2 az bz bzt); rewrite /BZ_coprime => ->.
by rewrite (BZprod_1r gz).
have ->: ((g *z a) %/z t) = g' *z a.
rewrite eq1 -/t.
rewrite - (BZprodA tz (BZS_quo gz tz) az).
by rewrite (BZdvds_pr5 tz (BZSp g'z az) tnz).
have ->: (BZgcd (g *z b) z %/z t) = BZgcd z' b.
move: (BZSp g'z bz) => h.
rewrite eq2 {1} eq1 -/t - (BZprodA tz g'z bz) (BZgcd_prodD h z'z tp) BZgcd_C.
by rewrite (BZgcd_simp z'z g'z bz cp1) (BZdvds_pr5 tz gs1 tnz).
suff: BZgcd z' (a *z b) %|z ((g' *z a) *z BZgcd z' b).
rewrite (BZprodC t).
move: (BZS_gcd z'z abz) (BZSp (BZSp g'z az) (BZS_gcd z'z bz)) => r1 r2.
by move/ (BZdvds_prod r1 r2 tz tnz).
rewrite - (BZprodA g'z az gs1).
apply: (@BZdvds_trans (a *z BZgcd z' b)).
apply: (BZdvds_pr1 g'z (BZSp az gs1)); apply:BZprod_nz => //.
by move => h1; move: (BZgcd_nz z'z bz h1) => [aa bb]; case: bnz.
rewrite - (BZgcd_prodD z'z bz ap).
have h1:(z' <> \0z \/ a *z b <> \0z) by right; apply:BZprod_nz.
have h2:((a *z z') <> \0z \/ a *z b <> \0z) by right; apply:BZprod_nz.
move: (BZgcd_prop3 z'z abz h1)=> [[p1 p2 _ ] _].
move: (BZgcd_prop3 (BZSp az z'z) abz h2)=> [[_ _ p3] _ ].
apply: p3; last by apply: p2.
apply: (@BZdvds_trans z'); last by exact.
apply: (BZdvds_pr1 az z'z).
by move => h; move /BZps_iP:zzp => [_]; rewrite eq2 h; qw.
Qed.
Module OrderType.
Lemma oprod0r' x: ordinalp x -> x *o \0o = \0o.
Proof.
by move => ox; rewrite (oprod_rec_def ox OS0) setX_0r funI_set0.
Qed.
Lemma oprod0l' x: ordinalp x -> \0o *o x = \0o.
Proof.
by move => ox; rewrite (oprod_rec_def OS0 ox) setX_0l funI_set0.
Qed.
Lemma osum_assoc2 a b c:
order a -> order b -> order c ->
(order_sum2 a (order_sum2 b c)) \Is (order_sum2 (order_sum2 a b) c).
Proof.
move=> oa ob oc.
have oab: order (order_sum2 a b) by fprops.
have obc: order (order_sum2 b c) by fprops.
set E:= substrate (order_sum2 a (order_sum2 b c)).
set F:= substrate (order_sum2 (order_sum2 a b) c).
set A:= substrate a; set B := substrate b; set C := substrate c.
have Ev: E = canonical_du2 A (canonical_du2 B C).
by rewrite /E ! orsum2_sr.
have Fv: F = canonical_du2 (canonical_du2 A B) C.
by rewrite /F ! orsum2_sr.
move: TP_ne1 => nT.
move: TP_ne => nT1.
set f := fun z => Yo (Q z = C0) (J (J (P z) C0) C0)
(Yo (Q (P z) = C0) (J (J (P (P z)) C1) C0) (J (P (P z)) C1)).
have p1: forall x, inc x E -> inc (f x) F.
move => x; rewrite Ev Fv; move /candu2P => [px]; case.
by move=> [PA Qa]; rewrite /f; Ytac0; apply: candu2_pra; apply: candu2_pra.
move => [] /candu2P [pPx alt] Qb.
have nQa: Q x <> C0 by rewrite Qb.
rewrite /f; Ytac0.
case: alt;move => [Ppx Qpx].
by Ytac0; apply: candu2_pra; apply: candu2_prb.
rewrite (Y_false); [ apply: candu2_prb => // | rewrite Qpx; fprops].
have p2: forall y, inc y F -> exists2 x, inc x E & y = f x.
move => y; rewrite Ev Fv; move /candu2P => [px]; case.
move=> [] /candu2P [pPy aux] Qpy; case: aux.
move=> [PPa QP]; exists (J (P (P y)) C0).
by apply: candu2_pra.
rewrite /f pr2_pair; Ytac0; aw.
apply: pair_exten =>//; fprops; aw; try ue.
move=> [PPy QPy]; exists (J (J (P (P y)) C0) C1).
by apply: candu2_prb; apply: candu2_pra.
rewrite /f !(pr1_pair, pr2_pair); Ytac0; Ytac0.
apply: pair_exten =>//; fprops; aw; try ue.
move=> [Py Qy]; exists (J (J (P y) C1) C1).
by apply: candu2_prb; apply: candu2_prb.
rewrite /f !(pr2_pair, pr1_pair); Ytac0; Ytac0.
apply: pair_exten =>//;fprops; aw;ue.
have p3: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
move => x y; rewrite Ev; move /candu2P => [px hx] /candu2P [py hy].
rewrite /f;case: hx.
move => [PxA Qxa]; Ytac0.
case: hy.
move => [PyA Qya]; Ytac0 => sf; move:(pr1_def sf).
by rewrite - {1} Qxa - Qya px py.
move=> [_ ] Qy; rewrite Qy; Ytac0; Ytac h1.
move => h2;case: nT1; exact: (pr2_def(pr1_def h2)).
move => h2;case: nT1; exact: (pr2_def h2).
move => [] /candu2P [pPx auxx] Qx; rewrite Qx; Ytac0.
case: hy.
move=> [_ Qy]; Ytac0; Ytac h.
move => h2;case: nT; exact: (pr2_def(pr1_def h2)).
move => h2;case: nT; exact: (pr2_def h2).
move=> [] /candu2P [pPy auxy] Qy; rewrite Qy; Ytac0.
case: auxx; move=> [PPx Qpx].
Ytac0.
case: auxy; move=> [PPy Qpy].
Ytac0 => sf; move: (pr1_def (pr1_def sf)) => sf1.
apply: pair_exten =>//; try ue.
apply: pair_exten =>//; try ue.
rewrite Qpy;Ytac0=> sf; case: nT1; exact: (pr2_def sf).
case: auxy; move=> [_ Qpy].
rewrite Qpx Qpy; Ytac0; Ytac0 => sf; case: nT; exact: (pr2_def sf).
rewrite Qpx Qpy; Ytac0; Ytac0.
move=> sf; move: (pr1_def sf) => sf1.
apply: pair_exten =>//; try ue.
apply: pair_exten =>//; try ue.
exists (Lf f E F); split;fprops;aw.
split; aw;apply: lf_bijective => //.
red; rewrite lf_source;move=> x y xE yE; aw.
move: (xE); rewrite Ev ; move=> /candu2P [px hx].
move: (yE); rewrite Ev ; move=> /candu2P [py hy].
split.
move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP; rewrite orsum2_sr //.
split => //; first by move: (p1 _ xE); rewrite Fv.
by move: (p1 _ yE); rewrite Fv.
case: h.
move=> [Qx Qy le]; constructor 1; rewrite /f (Y_true Qx) (Y_true Qy).
rewrite ! pr1_pair ! pr2_pair; split => //.
apply /orsum2_gleP;split => //; last by aw; constructor 1.
apply candu2_pra; order_tac.
apply candu2_pra; order_tac.
move => [hxa hxb] /orsum2_gleP [_ _].
case: hx; move => [pxa qxa]; first by case: hxa.
case: hy; move => [pya qya]; first by case: hxb.
case; last first.
by move => [sa sb]; constructor 3; rewrite /f; do 4 Ytac0; aw.
by move => [sa sb sc];constructor 2; rewrite /f; do 4 Ytac0; aw.
move => [sa sb sc]; constructor 1; rewrite /f; do 4 Ytac0; aw.
case /candu2P: pxa => _ [] [ta tb]; last by case: nT; rewrite - sa - tb.
case /candu2P: pya => _ [] [ta' tb']; last by case: nT; rewrite - sb - tb'.
split => //; apply/orsum2_gleP; split => //.
by apply: candu2_prb.
by apply: candu2_prb.
aw; by constructor 2.
move=> [Qxa Qyb].
case: hy; move => [pya qya]; first by case: Qyb.
case: hx; move => [pxa qxa]; last by case: nT; ue.
move /candu2P: pya =>[_]; case; move => [sa sb].
constructor 1; rewrite /f; Ytac0; Ytac0; Ytac0; aw; split => //.
apply /orsum2_gleP; split => //.
- by apply candu2_pra.
- by apply candu2_prb.
- by constructor 3; aw.
by constructor 3; rewrite /f sb; Ytac0; Ytac0; aw; Ytac0;aw.
move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP.
rewrite orsum2_sr // -/A -/B -/C - Ev;split => //.
case: hx; move => [Px Qx].
have fx: f x = (J (J (P x) C0) C0) by rewrite /f Y_true.
case: hy; move => [Py Qy].
have fy: f y = (J (J (P y) C0) C0) by rewrite /f Y_true.
constructor 1; split => //.
move: h; rewrite fx fy ! pr1_pair ! pr2_pair; case.
- move=> [_ _] /orsum2_gleP [_ _]; case; aw; first by move => [_ _ s].
+ by move=> [_ bad _].
+ by move=> [_ bad].
- by move=> [_ bad _].
- by move=> [_ bad].
constructor 3; rewrite Qx Qy; split; exact.
case: hy; move => [Py Qy].
case: (nT); case: h.
move=> [Qfx Qfy] /orsum2_gleP [Pfx Pfy].
have -> : Q (P (f y)) = C0 by rewrite /f; Ytac0; aw.
case; [ | move => [_ pa _] | move => [_ pa]]; try by case: pa.
move=> [h1 _]; move: h1 Qfx; rewrite /f Qx (Y_false) //;Ytac ww; aw.
by move => [_ pa _]; move: pa; rewrite /f; Ytac0; aw.
by move => [ _ ]; rewrite /f; Ytac0; aw.
rewrite Qx Qy; constructor 2; split => //.
apply /orsum2_gleP; split => //.
move: Px Py => /candu2P [pPx hpx] /candu2P [pPy hpy].
case: hpx; move => [pa pb].
case: hpy; move => [pc pd]; last by constructor 3; rewrite pd;split => //.
constructor 1; split => //; move: h; rewrite /f Qx Qy; do 4 Ytac0.
case; [move => [_ _ ba] | move => [ba _] | move=> [_ ba]]; move: ba; aw => //.
move /orsum2_gleP => [_ _];rewrite !pr1_pair !pr2_pair.
by case; [ move => [sa _] | move => [_ _] | move => [sa _]].
constructor 2; rewrite pb; move: h; rewrite /f Qx Qy pb.
Ytac0; Ytac0; Ytac0; case; first by move => [sa _]; move: sa; aw.
Ytac ww; first by move => [_ qa _]; move: qa; aw.
by move => [_ _]; aw.
by move => [sa _]; move: sa; aw.
Qed.
Lemma oprod_assoc2 a b c:
order a -> order b -> order c ->
(order_prod2 a (order_prod2 b c))
\Is (order_prod2 (order_prod2 a b) c).
Proof.
move=> oa ob oc.
have oab: order (order_prod2 a b) by fprops.
have obc: order (order_prod2 b c) by fprops.
set E:= substrate (order_prod2 a (order_prod2 b c)).
set F:= substrate (order_prod2 (order_prod2 a b) c).
set A:= substrate a; set B := substrate b; set C := substrate c.
have Ev: E = product2 (product2 C B) A.
by rewrite /E ! orprod2_sr.
have Fv: F = product2 C (product2 B A).
by rewrite /F ! orprod2_sr.
have CB_pr: forall z, inc z (product2 C B) <->
[/\ fgraph z, domain z = C2, inc (Vg z C0) C & inc (Vg z C1) B].
by move=> z; apply /setX2_P.
have BA_pr: forall z, inc z (product2 B A) <->
[/\ fgraph z, domain z = C2, inc (Vg z C0) B & inc (Vg z C1) A].
by move=> z; apply /setX2_P.
set f := fun z => variantLc (Vg (Vg z C0) C0)
(variantLc (Vg (Vg z C0) C1) (Vg z C1)).
have p01: forall x, inc x E -> inc (f x) F.
move=> x; rewrite Ev Fv; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
rewrite /f; bw; apply /setX2_P; split => //; fprops; bw.
apply /setX2_P; split => //; fprops; bw.
have p02: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
move=> x y; rewrite Ev; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
rewrite /f; move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'] sf.
move: (f_equal (Vg ^~ C0) sf) (f_equal (Vg ^~C1) sf); bw => sf1 sf2.
move: (f_equal (Vg ^~C0) sf2) (f_equal (Vg ^~C1) sf2); bw => sf3 sf4.
apply: fgraph_exten =>//; try ue.
rewrite p2; move=> z zdx;try_lvariant zdx.
apply: fgraph_exten =>//; try ue.
rewrite p5; move=> zz zdx; try_lvariant zdx.
have p03: forall y, inc y F -> exists2 x, inc x E & y = f x.
move=> y; rewrite Fv; move /setX2_P => [p1 p2 p3 /setX2_P [p4 p5 p6 p7]].
exists (variantLc (variantLc (Vg y C0) (Vg (Vg y C1) C0))
(Vg (Vg y C1) C1)).
rewrite Ev;apply /setX2_P; split;fprops; bw.
apply /setX2_P; split;fprops; bw.
rewrite /f; symmetry;apply: fgraph_exten => //; bw; fprops.
move=> x xtp; try_lvariant xtp.
apply: fgraph_exten => //; bw ; [fprops | by symmetry | ].
move=> z xtp; try_lvariant xtp.
exists (Lf f E F); split => //; fprops;aw.
split; aw;apply: lf_bijective => //.
red; aw; move=> x y xE yE; aw.
move: (xE); rewrite Ev;move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
move: (yE);rewrite Ev;move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'].
split.
move: (p01 _ xE)(p01 _ yE) => xF yF.
move: xF; rewrite Fv; case /setX2_P=>[q1 q2 q3 /setX2_P [q4 q5 q6 q7]].
move: yF; rewrite Fv; case /setX2_P=>[r1 r2 r3 /setX2_P [r4 r5 r6 r7]].
have x1: inc (Vg (f x) C1) (product2 B A) by rewrite BA_pr.
have y1: inc (Vg (f y) C1) (product2 B A) by rewrite BA_pr.
set hi1:= inc (Vg (f x) C1) (product2 B A).
set hi2:= inc (Vg (f y) C1) (product2 B A).
move => tmp; apply /(orprod2_gleP oab oc).
rewrite orprod2_sr // -/A -/B -/C -Fv;split => //; try apply: p01 => //.
move: tmp => /(orprod2_gleP oa obc) [_ _]; case.
move => [pa pb];left; split; first by rewrite /f; bw;ue.
apply /(orprod2_gleP oa ob);split => //;left.
by rewrite /f; bw;split => //; rewrite pa.
move => [] /(orprod2_gleP ob oc) [_ _ aux'] nse.
case: aux'; last by move=> aux2; right; rewrite /f; bw.
move=> [Vaa Vba]; left; split; first by rewrite /f; bw.
apply /(orprod2_gleP oa ob);split => //; right.
rewrite /f; bw; split => //; dneg aux3.
apply: fgraph_exten =>//; try ue.
rewrite p5; move=> z zd; try_lvariant zd.
move /(orprod2_gleP oab oc) => [_ _ tmp].
apply/(orprod2_gleP oa obc); rewrite orprod2_sr // -/A -/B -/C -Ev;split => //.
have x1: inc (Vg x C0) (product2 C B) by rewrite CB_pr.
have y1: inc (Vg y C0) (product2 C B) by rewrite CB_pr.
case: tmp; last first.
rewrite /f; bw; move=> [h1 h2]; right; split.
apply /(orprod2_gleP ob oc);split => //; by right.
by dneg eql; rewrite eql.
rewrite /f; bw; move => [xaa] /(orprod2_gleP oa ob) [fxb fxa]; bw.
case.
move=> [sVab le]; left; split =>//.
apply: fgraph_exten => //; first by ue.
rewrite p5; move=> z zd; try_lvariant zd.
move=> [lt2 neq]; right;split; last by dneg aux; rewrite aux.
by apply /(orprod2_gleP ob oc);split => //; left.
Qed.
Lemma osum_distributive a b c:
order a -> order b -> order c ->
(order_prod2 c (order_sum2 a b))
\Is (order_sum2 (order_prod2 c a) (order_prod2 c b)).
Proof.
move=> oa ob oc.
move: (orsum2_or oa ob) => oab.
move: (orprod2_or oc oa) => oca.
move: (orprod2_or oc ob) => ocb.
move: (orprod2_or oc oab) => ocab.
move:(orsum2_or oca ocb) => ocacb.
set (f := fun z => J (variantLc (P (Vg z C0)) (Vg z C1)) (Q (Vg z C0))).
set A := substrate a; set B := substrate b; set C := substrate c.
set E:= substrate (order_prod2 c (order_sum2 a b)).
set F:= substrate(order_sum2 (order_prod2 c a)(order_prod2 c b)).
have Ep: E = product2 (canonical_du2 A B) C.
rewrite /E orprod2_sr // orsum2_sr //.
have Fp: F = canonical_du2 (product2 A C)(product2 B C).
rewrite /F orsum2_sr // !orprod2_sr //.
have Ev: forall x, inc x E <-> [/\ fgraph x, domain x = C2,
pairp (Vg x C0),
((inc (P (Vg x C0)) A /\ Q (Vg x C0) = C0) \/
(inc (P (Vg x C0)) B /\ Q (Vg x C0) = C1))
&inc (Vg x C1) C].
move=> x; rewrite Ep; split.
move /setX2_P => [pa pb pc pd]; move/candu2P: pc => [pe] [] [pf pg];
split => //; [left | right ]; split => //.
by move => [pa pb pc pd pe]; apply /setX2_P;split => //; apply/candu2P.
have Fv: forall x, inc x F <-> [/\ pairp x, fgraph (P x),
domain (P x) = C2, inc (Vg (P x) C1) C &
((inc (Vg (P x) C0) A /\ Q x = C0) \/
(inc (Vg (P x) C0) B /\ Q x = C1))].
move=> x; rewrite Fp; split.
move /candu2P => [pa []] [] /setX2_P [pb pc pd pe] pf; split;fprops.
move => [pa pb pc pd];case; move =>[pe pf];
apply /candu2P;split => //; [left | right];
split => //;apply /setX2_P; split; fprops.
have p1: forall x, inc x E -> inc (f x) F.
move=> x /Ev [pa pb pc pd pe]; rewrite /f; apply/Fv.
rewrite !pr1_pair !pr2_pair; bw; split;fprops.
have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
move=> x y /Ev [fgx dx px hx qx] /Ev [fgy dy py hy qy].
rewrite /f => sf; move: (pr1_def sf)(pr2_def sf) => r1 r2.
move: (f_equal (Vg ^~C0) r1)(f_equal (Vg ^~C1) r1); bw; move => r3 r4.
apply: fgraph_exten =>//; [ ue | rewrite dx; move=> z zd; try_lvariant zd].
apply: pair_exten =>//.
have p3: forall y, inc y F -> exists2 x, inc x E & y = f x.
move=> y /Fv [py fPy dPy Vby Vay].
exists (variantLc (J (Vg (P y) C0) (Q y)) (Vg (P y) C1)).
apply /Ev; bw; rewrite !pr1_pair !pr2_pair; split;fprops.
rewrite /f; bw;aw; apply: pair_exten =>//; [ fprops | aw | aw].
apply: fgraph_exten; [ exact| fprops | bw | bw].
rewrite dPy; move=> x xtp; try_lvariant xtp.
exists (Lf f E F); split => //; aw; first by split; aw;apply: lf_bijective.
red; aw;move=> x y xE yE; rewrite lf_V // lf_V //.
have r1: Q (f x) = Q (Vg x C0) by rewrite /f pr2_pair.
have r2: Q (f y) = Q (Vg y C0) by rewrite /f pr2_pair.
have r3: Vg (P (f x)) C0 = P (Vg x C0) by rewrite /f; aw; bw.
have r4: Vg (P (f y)) C0 = P (Vg y C0) by rewrite /f; aw; bw.
have r5: Vg (P (f x)) C1 = Vg x C1 by rewrite /f; aw; bw.
have r6: Vg (P (f y)) C1 = Vg y C1 by rewrite /f; aw; bw.
have pa: pairp (Vg x C0) by move /Ev: xE => [_ _ px _].
have pb: pairp (Vg y C0) by move /Ev:yE => [_ _ px _].
move: (xE) => /Ev [fgx dx px hx qx].
move: (yE) => /Ev [fgy dy py hy qy].
move: TP_ne => nab.
split.
move /(orprod2_gleP oc oab) => [_ _ h]; apply /(orsum2_gleP).
split; first by move: (p1 _ xE); rewrite /F orsum2_sr.
by move: (p1 _ yE); rewrite /F orsum2_sr.
rewrite r1 r2; case: h.
move=> [q1 q2]; rewrite -q1.
case: (equal_or_not (Q (Vg x C0)) C0)=> q3.
case: hx; move=> [q4 q5]; last by case: nab ; rewrite - q3 - q5.
constructor 1; rewrite q3; split => //.
apply /(orprod2_gleP oc oa).
split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue.
left; rewrite r3 r4 r5 r6 q1; split =>//.
constructor 2; split => //.
case: hx; move=> [q4 q5]; first by case: q3.
apply /(orprod2_gleP oc ob).
split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue.
left; rewrite r3 r4 r5 r6 -q1; split =>//.
move => [] /(orsum2_gleP) [_ _ h1] h2; case: h1.
move=> [q1 q2 q3]; constructor 1.
split; [exact | exact | ].
case: hx; move=> [q4 q5]; last by case: nab; rewrite -q1 -q5.
case: hy; move=> [q4' q5']; last by case: nab; rewrite -q2 -q5'.
apply /(orprod2_gleP oc oa).
split; first by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops.
by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops.
right; rewrite r3 r4;split => //;dneg aux.
apply: pair_exten => //; ue.
move => [q1 q2 q3]; constructor 2.
case: hx; move=> [q4 q5]; first by case: q1.
case: hy; move=> [q4' q5']; first by case: q2.
split; [exact | exact | ].
apply /(orprod2_gleP oc ob).
split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
right; rewrite r3 r4; split => // sP; case: h2.
by apply: pair_exten => //; rewrite q5 q5'.
move=> res; constructor 3; exact.
move/(orsum2_gleP) => [_ _ h]; apply /(orprod2_gleP oc oab).
split; first by move: xE; rewrite /E orprod2_sr //.
by move: yE; rewrite /E orprod2_sr //.
have pc: inc (Vg x C0) (canonical_du2 (substrate a) (substrate b)).
by move: xE => /Ev [_ _ px' etc _]; apply/candu2P.
have pd: inc (Vg y C0) (canonical_du2 (substrate a) (substrate b)).
by move: yE => /Ev [_ _ px' etc _]; apply/candu2P.
case: h.
move=> [q1 q2] /(orprod2_gleP oc oa) [q3 q4].
rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ].
by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 q1 q2.
split =>//; last by dneg neq; rewrite neq.
by apply /orsum2_gleP;split => //; constructor 1;rewrite -r1 -r2 q1 q2.
move=> [q1 q2] /(orprod2_gleP oc ob) [q3 q4].
case: hx; rewrite -r1; move => [_ sb]; first by case: q1.
case: hy; rewrite -r2; move => [_ sb']; first by case: q2.
rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ].
by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 sb sb'.
split =>//; last by dneg neq; rewrite neq.
apply /orsum2_gleP;split => //; constructor 2; rewrite - r1 -r2;split => //.
move=> [q5 q6]; right; split.
apply /orsum2_gleP;split => //; constructor 3; rewrite - r1 -r2;split => //.
by dneg neq; rewrite r2 -neq -r1.
Qed.
Lemma osum_increasing1 r f g:
orsum_ax r f -> orsum_ax r g ->
(forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) ->
order_le (order_sum r f) (order_sum r g).
Proof.
move => oa oa1 ale.
have o1: order (order_sum r f) by fprops.
have o2: order (order_sum r g) by fprops.
split => //; apply: (proj33 (order_le_alt o1 o2 _)).
set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)).
have sip: forall j, inc j (domain f) ->
order_morphism (si j) (Vg f j) (Vg g j).
move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [ fx1 fx2]]]].
move: (order_le_alt2 p1 p2 fx1 fx2) => [res _].
rewrite /si; apply choose_pr.
by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))).
have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue.
set E := (substrate (order_sum r g)).
set F := (disjointU_fam (fam_of_substrates f)).
have p1: partition_w_fam F (substrate (order_sum r f)).
bw;rewrite /F /sum_of_substrates; rewrite /disjointU.
apply: partition_disjointU; rewrite /fam_of_substrates; fprops.
have p3: (domain F = domain f).
rewrite /F/disjointU_fam /fam_of_substrates; bw.
set di:= fun i => ((substrate (Vg f i)) *s1 i).
set sj:= fun i => Lf (fun z => J (Vf (si i) (P z)) i) (di i) E.
have p0: forall i, inc i (domain f) ->
lf_axiom (fun z => J (Vf (si i) (P z)) i) (di i) E.
move=> i idf z zV.
move: (sip _ idf) => [_ _ [ff sf tf] _].
have aux: inc (Vf (si i) (P z) ) (substrate (Vg g i)).
Wtac;move: zV => /indexed_P [_ Ps _]; ue.
rewrite /E;bw; apply: disjoint_union_pi1 => //; ue.
have FP: forall i, inc i (domain f) -> Vg F i = di i.
move=> i idf; rewrite /F /disjointU_fam/fam_of_substrates ; bw.
have p2: forall i, inc i (domain F) ->
function_prop (sj i) (Vg F i) E.
rewrite p3;move=> i idf; rewrite /sj FP => //; aw.
by split;aw;apply: lf_function; apply: p0.
move: (extension_partition1 p1 p2).
set G := common_ext _ _ _; move=> [[fG sG tG] alg].
rewrite p3 in alg.
have aux: forall x, inc x (source G) ->
[/\ inc (Q x) (domain f), inc x (di (Q x)), pairp x,
inc (P x)(substrate (Vg f (Q x))) & Vf G x = J (Vf(si (Q x)) (P x)) (Q x)].
rewrite sG; bw; move => x xs; move: (du_index_pr1 xs)=> [Qxd Pxd px].
have xdi: inc x (di (Q x)) by apply /indexed_P;split => //.
split => //.
move: (alg _ Qxd); rewrite /agrees_on; move=> [q1 q2 q3].
move: (xdi); rewrite -FP // => q4.
move: (q3 _ q4); rewrite /sj; rewrite lf_V; aw;apply: p0 => //.
exists G; split => //.
move=> x y xs ys.
move: (aux _ xs) (aux _ ys) => [Qx xdi px Px Wx][Qy ydi py Py Wy].
have qa: (sum_of_substrates f = source G) by rewrite sG; bw.
have qb: (sum_of_substrates g = target G) by rewrite tG /E; bw.
split; move /orsum_gleP =>[q1 q2 q3]; apply /orsum_gleP.
rewrite qb;split=> //; try Wtac; rewrite Wx Wy;red;aw; case: q3; first by left.
move=> [Qxx le1]; right; split => //.
rewrite -Qxx; move: (sip _ Qx) => [_ _ [_ sf tf] orf].
rewrite - orf //; rewrite sf //; ue.
move: q3; rewrite /order_sum_r Wx Wy !pr2_pair !pr1_pair.
move => q3; rewrite qa;split => //; case: q3; first by left.
move=> [Qxx]; rewrite - {1} Qxx => le1; right; split => //.
move: (sip _ Qx) => [_ _ [_ sf tf] orf].
apply /orf; rewrite ? sf //; ue.
Qed.
Lemma osum_increasing2 r f g: worder r ->
substrate r = domain f -> substrate r = domain g ->
(forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) ->
(ord_sum r f) <=o (ord_sum r g).
Proof.
move=> wor sf sg alo.
apply /ordinal_le_P0; apply /order_le_compatible1.
apply: orsum_wor => //; bw.
hnf; bw;move=> i idf; bw; fprops; move: (alo _ idf) => [aa bb _]; fprops.
apply: orsum_wor => //;bw.
hnf; bw;rewrite - sg sf; move=> i idf; bw.
move: (alo _ idf) => [aa bb _]; fprops.
apply osum_increasing1.
- split => //;bw; fprops; hnf; bw.
move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
- rewrite - sg sf;split;fprops;hnf; bw.
move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
- rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le].
bw; apply/order_le_compatible1; fprops.
by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ordinal_le_P0.
Qed.
Lemma osum_increasing3 r f j:
orsum_ax r f ->
sub j (domain f) ->
order_le (order_sum (induced_order r j) (restr f j)) (order_sum r f).
Proof.
move=> oa jd.
move: (oa) => [or sr alo].
set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) emptyset)).
have dfdg: domain f = domain g by rewrite /g; bw.
have oa': orsum_ax r g.
split => //; first by ue.
hnf;bw;rewrite - dfdg /g;move=> i idg; bw; Ytac ij;first by apply: alo.
apply: set0_or.
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i ((domain g) -s j) -> Vg g i = \0o).
by move=> i /setC_P; rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
move: (osum_unit1 oa' sjd' cz).
have ->: (restr f j = restr g j).
apply: Lg_exten => s sj;bw; rewrite /g; bw; [ by Ytac0 | by apply:jd ].
move=> oi1.
have oi2: order_isomorphic (order_sum r f) (order_sum r f).
by apply: orderIR; apply: orsum_or.
apply /(order_le_compatible oi1 oi2).
apply: osum_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac xj; first by apply: order_leR=>//; apply: alo.
move: set0_or => eo.
split; fprops;exists (identity emptyset); exists emptyset.
have auw: sub emptyset (substrate (Vg f x)) by fprops.
split => //; split;fprops; aw.
- apply: (proj1 (iorder_osr _ auw)); fprops.
split; aw; first by apply: identity_fb.
by rewrite (proj2 set0_wor).
- apply: (alo _ xdg).
- by move=> u v; rewrite identity_s => /in_set0.
Qed.
Lemma osum_increasing4 r f j:
worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f ->
(ord_sum (induced_order r j) (restr f j)) <=o (ord_sum r f).
Proof.
move => [wor sr] sjf alo.
have sjr: sub j (substrate r) by ue.
have or: order r by move: wor => [or _].
have dr: (domain (restr f j)) = j by bw.
rewrite /ord_sum; apply /ordinal_le_P0; apply /order_le_compatible1.
apply: orsum_wor.
by apply: induced_wor => //; ue.
by bw; aw;rewrite dr.
by hnf; rewrite dr; bw; move=> i ij; bw; fprops.
apply: orsum_wor => //; bw; hnf; bw; move=> i idf; bw; fprops.
set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))).
have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z)))
= restr g j.
bw;apply: Lg_exten.
by rewrite /g;red; bw;move => x xj; bw; apply: sjf.
apply: osum_increasing3 => //.
rewrite /g;red; bw;split => //; hnf;bw; move=> i idf; bw; fprops.
rewrite /g; bw.
Qed.
Lemma oprod_increasing1 r f g:
orprod_ax r f -> orprod_ax r g ->
(forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) ->
order_le (order_prod r f) (order_prod r g).
Proof.
move => oa oa1 ale.
have o1: order (order_prod r f) by fprops.
have o2: order (order_prod r g) by fprops.
split => //; apply: (proj33 (order_le_alt o1 o2 _)).
set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)).
have sip: forall j, inc j (domain f) ->
order_morphism (si j) (Vg f j) (Vg g j).
move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [fx1 fx2]]]].
move: (order_le_alt2 p1 p2 fx1 fx2) => [res _].
rewrite /si; apply choose_pr.
by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))).
have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue.
set E:= substrate (order_prod r f).
set F := substrate(order_prod r g).
have Ep: E = (prod_of_substrates f) by apply: orprod_sr => //.
have Fp: F = (prod_of_substrates g) by apply: orprod_sr => //.
set h:= fun z => Lg (domain f) (fun i => Vf (si i) (Vg z i)).
have ta: lf_axiom h E F.
rewrite Ep Fp ; move => t /prod_of_substratesP [fgt dt als].
apply /prod_of_substratesP.
rewrite - dfdg /h; bw;split;fprops;move=> i idf; bw.
move: (sip _ idf) => [_ _ [fsi ssi tsi] _].
by Wtac; rewrite ssi;apply: als.
have hi: forall u v, inc u E -> inc v E -> h u = h v -> u = v.
rewrite Ep; move=> u v / prod_of_substratesP [fgu du alu]
/prod_of_substratesP [fgv dv alv] sh.
apply: fgraph_exten =>//; first by ue.
rewrite du; move=> x xdf; move: (f_equal (Vg ^~x) sh); rewrite /h;bw => sW.
move: (order_morphism_fi (sip _ xdf)) => [_ insi].
move: (sip _ xdf) => [_ _ [fsi ssi tsi] _].
apply: insi =>//; rewrite ssi; [ apply: alu => // |apply: alv => //].
exists (Lf h E F); red; aw; split => //.
split; aw;by apply: lf_function.
red; aw; move=> x y xE yE; rewrite /h; aw.
have srdf: substrate r = domain f by move: oa => [_ sr _].
move: (xE); rewrite Ep; move /prod_of_substratesP => [fgx dx alx].
move: (yE); rewrite Ep; move /prod_of_substratesP => [fgy dy aly].
split.
move /(orprod_gleP oa) => [_ _ aux]; apply /(orprod_gleP oa1).
rewrite -Fp;split; [by apply: ta | by apply: ta |].
case: aux; first by move=>->; left.
move=> [j [jsr jlt jle]]; right; ex_tac.
rewrite srdf in jsr;move: jlt; bw.
move: (order_morphism_fi (sip _ jsr)) => [_ insi].
move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp].
have vsx: inc (Vg x j) (source (si j)) by rewrite ssi; apply: alx => //.
have vsy: inc (Vg y j) (source (si j)) by rewrite ssi; apply: aly => //.
rewrite /glt -jsrp //;move=> [p1 p2]; split =>//; dneg sV; apply: insi =>//.
move=> i ij.
have idf: inc i (domain f) by rewrite - srdf; order_tac.
by move: (jle _ ij); bw; move=> ->.
move /(orprod_gleP oa1) => [h1 h2 aux]; apply /(orprod_gleP oa).
rewrite -Ep; split=> //; case: aux.
move => sh; left; apply: hi =>//.
move=> [j [jsr jlt jle]]; right; ex_tac.
rewrite srdf in jsr;move: jlt; bw.
move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp].
rewrite /glt jsrp; first by move=> [p1 p2]; split =>//; dneg sV; ue.
rewrite ssi; apply: alx => //.
rewrite ssi; apply: aly => //.
move=> i ij.
have idf: inc i (domain f) by rewrite - srdf; order_tac.
move: (jle _ ij); bw.
move: (order_morphism_fi (sip _ idf)) =>[_ insi].
move: (sip _ idf) => [_ _ [fsi ssi tsi] jsrp].
apply: insi; rewrite ssi;[ apply: alx => // | apply: aly => //].
Qed.
Lemma oprod_increasing2 r f g: worder r ->
substrate r = domain f -> substrate r = domain g ->
(forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) ->
finite_set (substrate r) ->
(ord_prod r f) <=o (ord_prod r g).
Proof.
move=> wor sf sg alo fse.
apply/ordinal_le_P0; apply /order_le_compatible1.
apply: orprod_wor => //; [ split;bw | hnf; bw ].
move=> i idf; bw; move: (alo _ idf) => [aa bb _]; fprops.
apply: orprod_wor => //; [split; bw | hnf;bw ].
rewrite - sg sf; move=> i idf; bw.
by move: (alo _ idf) => [aa bb _]; fprops.
apply: oprod_increasing1.
split => //;bw; hnf; bw => i idf; bw;move: (alo _ idf) =>[aa bb _];fprops.
split => //; bw; hnf; bw; rewrite - sg sf.
move => i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le].
bw; apply /order_le_compatible1; fprops.
by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ordinal_le_P0.
Qed.
Lemma oprod_increasing3 r f j:
orprod_ax r f ->
sub j (domain f) ->
(forall x, inc x ((domain f) -s j) ->
substrate (Vg f x) <> emptyset) ->
order_le (order_prod (induced_order r j) (restr f j)) (order_prod r f).
Proof.
move=> oa jd anot.
move: (oa) => [or sr alo].
set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) (ordinal_o \1o))).
have dfdg: domain f = domain g by rewrite /g; bw.
have oa': orprod_ax r g.
hnf; rewrite /order_fam /allf - dfdg;split => //.
move=> i idg; rewrite /g; bw; Ytac ij; first by apply: alo.
by apply: (ordinal_o_or).
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i ((domain g) -s j) ->
singletonp (substrate (Vg g i))).
move=> i /setC_P;rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
by rewrite (ordinal_o_sr); exists emptyset.
move: (oprod_unit1 oa' sjd' cz).
have ->: (restr f j = restr g j).
apply: Lg_exten; bw; move=> x xj; move: (jd _ xj) => xdf.
by bw; rewrite /g; bw; Ytac0.
move=> oi1.
have oi2: order_isomorphic (order_prod r f) (order_prod r f).
by apply: orderIR; apply: orprod_or.
apply /(order_le_compatible oi1 oi2).
apply: oprod_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac nij; first by apply: order_leR=>//; apply: alo.
have p2: order (Vg f x) by move: oa => [q1 q2 q4]; apply: q4.
have [y yd]: nonempty (substrate (Vg f x)).
case: (emptyset_dichot (substrate (Vg f x))) => // p1.
have xcz: inc x ((domain f) -s j) by apply /setC_P.
move: (anot _ xcz) => p4; contradiction.
have s1: sub (singleton y) (substrate (Vg f x)) by apply: set1_sub.
set h:= Lf (fun z => y) (singleton emptyset) (singleton y).
have ta: lf_axiom (fun _ : Set => y) (singleton emptyset) (singleton y).
move=> t _ /=; fprops.
split => //; [fprops | exists h; exists (singleton y); split => //].
rewrite /h;split;fprops;bw; aw.
apply (proj1 (iorder_osr p2 s1)).
split; rewrite ? ordinal_o_sr;aw; apply: lf_bijective => //.
by move=> u v /set1_P -> /set1_P ->.
move=> u /set1_P ->; exists emptyset; [fprops | done].
move => u v;rewrite lf_source => aa bb; aw.
move: aa bb => /set1_P -> /set1_P ->.
split; move => _.
by apply /iorder_gleP; fprops; order_tac.
rewrite / \1o/ \1c;apply /ordo_leP;split;fprops.
Qed.
Lemma oprod_increasing4 r f j:
worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f ->
finite_set (substrate r) ->
(forall x, inc x ((domain f) -s j) -> Vg f x <> \0o) ->
(ord_prod (induced_order r j) (restr f j)) <=o (ord_prod r f).
Proof.
move => [wor sr] sjf alo fsr alnz.
have sjr: sub j (substrate r) by ue.
have or: order r by move: wor => [or _].
apply /ordinal_le_P0; apply /order_le_compatible1.
apply: orprod_wor.
split; bw;aw; apply: induced_wor => //; ue.
hnf; bw; move=> i ij; bw; fprops.
rewrite iorder_sr //; apply: (sub_finite_set sjr fsr).
apply: orprod_wor => //; [ split;bw | hnf;bw ].
move=> i idf; bw; fprops.
set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))).
have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z)))
= restr g j.
bw;apply: Lg_exten; rewrite /g; bw.
by move => x xj /=; bw;apply: sjf.
apply: oprod_increasing3 => //.
rewrite /g;split=> //;hnf; bw; move=> i idf; bw; fprops.
rewrite /g; bw.
move => x; rewrite {1} /g; bw => xd; move: (alnz _ xd).
move: xd => /setC_P [xdf _]; move: (alo _ xdf) => ov.
by rewrite /g; bw; rewrite ordinal_o_sr.
Qed.
Parameter order_type: Set -> Set.
Axiom order_type_exists:
forall x, order x -> order_isomorphic x (order_type x).
Axiom order_type_unique:
forall x y, order_isomorphic x y -> (order_type x = order_type y).
Definition is_order_type x := exists2 y, order y & x = order_type y.
Definition order_type_le x y:=
[/\ is_order_type x, is_order_type y &
exists f z,
sub z (substrate y) /\ order_isomorphism f x (induced_order y z)].
Notation "x <=t y" := (order_type_le x y) (at level 60).
Notation "x <=O y" := (order_le x y) (at level 60).
Lemma OT_ordinal_compat x: worder x ->
order_type x = order_type (ordinal_o (ordinal x)).
Proof.
by move=> wor; apply: order_type_unique;move:(ordinal_o_is wor).
Qed.
Lemma OT_prop0 x: order x -> (order_type x) \Is x.
Proof. by move=> ox; apply: orderIS; apply: order_type_exists. Qed.
Lemma OT_prop1 x: order x -> is_order_type (order_type x).
Proof. by move=> ox; exists x. Qed.
Lemma OT_prop2 x: is_order_type x -> order x.
Proof.
move=> [y pa pb].
by move: (order_type_exists pa); rewrite -pb; move=> [f [oy ox _]].
Qed.
Lemma OT_prop3 x: order x -> order (order_type x).
Proof. by move => ox; apply: OT_prop2; apply: OT_prop1. Qed.
Lemma OT_prop4 x: order x ->
order_type (order_type x) = order_type x.
Proof.
move => ox.
by apply: order_type_unique; apply: orderIS; apply: order_type_exists.
Qed.
Lemma order_le_alt4 r r': r <=O r' ->
(exists f, order_morphism f r r').
Proof.
move=> [o1 o2 [f [z [sr [oa ob [[ [ff injf] sjf] sf tf] etc]]]]].
move: tf; aw => tf.
have ta: lf_axiom (Vf f) (substrate r) (substrate r').
rewrite - sf; move=> t tsf; apply: sr; Wtac.
exists (Lf (Vf f) (substrate r) (substrate r')).
split => //;first split;aw.
by apply: lf_function.
red; aw;move=> x y xsr ysr; aw; rewrite - sf in xsr ysr.
split => h; first by move/(etc _ _ xsr ysr): h => t; exact (iorder_gle1 t).
apply /(etc _ _ xsr ysr); apply /iorder_gleP => //; Wtac.
Qed.
Lemma order_le_alt3P r r':
r <=O r' <-> (exists f, order_morphism f r r').
Proof.
split.
apply: order_le_alt4.
move => h; move: (h) => [_ [or or' _ _]].
by apply: order_le_alt.
Qed.
Lemma order_le_transitive x y z:
x <=O y -> y <=O z -> x <=O z.
Proof.
move=> [ox oy [f [y1 [pa pb]]]] [_ oz [g [z1 [pc pd]]]].
split => //.
move: pb => [orx oix [[[ff injf] sjf] sf tf] etcf].
move: pd => [ory oiy [[[fg injg] sjg] sg tg] etcg].
move: tf tg; aw => tf tg.
set z2:= image_by_fun g y1.
have y1sg: sub y1 (source g) by ue.
have sz2z1: sub z2 z1 by rewrite - tg /z2; apply: fun_image_Starget1.
have sz2: sub z2 (substrate z) by apply: (sub_trans sz2z1).
set h:= Lf (fun t => (Vf g (Vf f t))) (substrate x) z2.
have ta: lf_axiom (fun t => Vf g(Vf f t)) (substrate x) z2.
rewrite - sf;move=> t rx; apply /(Vf_image_P fg y1sg).
exists (Vf f t) => //; Wtac.
move: (iorder_osr oz sz2) => [pa1 pb1].
exists h; exists z2; split => //; rewrite /h; split;fprops;aw.
split; aw;apply: lf_bijective => //.
rewrite - sf => u v ux vx sw; apply: injf => //.
apply: injg =>//; rewrite sg; apply: pa; rewrite - tf;Wtac.
move=> u /(Vf_image_P fg y1sg) [a ay1] ->.
move: ay1; rewrite - tf => af; move: ((proj2 sjf) _ af).
move=> [b bsf <-]; exists b => //; ue.
red; aw;move => a b asf bsf.
move: (ta _ asf) (ta _ bsf) => ta1 ta2; aw.
rewrite - sf in asf bsf.
have wa: inc (Vf f a) y1 by rewrite - tf; Wtac.
have wb: inc (Vf f b) y1 by rewrite - tf; Wtac.
have wa1: inc (Vf f a) (source g) by ue.
have wb1: inc (Vf f b) (source g) by ue.
set H1 := (etcf _ _ asf bsf); set Hb := (etcg _ _ wa1 wb1).
split.
move /H1 => p1; apply /iorder_gleP => //.
move: (iorder_gle1 p1); move /Hb => p2; exact :(iorder_gle1 p2).
move => p2; apply /H1;apply /iorder_gleP => //; apply /Hb.
move: (iorder_gle1 p2) => p1.
by apply /iorder_gleP => //; apply: sz2z1.
Qed.
Lemma OTorder_le_altP r r':
r <=t r' <-> [/\ is_order_type r, is_order_type r' &
exists f, order_morphism f r r'].
Proof.
split;move=> [o1 o2 etc]; split => //.
apply /order_le_alt3P.
by split => //; by apply: OT_prop2.
by move: (order_le_alt (OT_prop2 o1)(OT_prop2 o2) etc) => [_ _].
Qed.
Lemma OTorder_le_compat1 r: order r ->
r <=O (order_type r).
Proof.
move=> or; apply /order_le_alt3P.
move: (order_type_exists or) => [f oi]; exists f => //.
by apply: order_isomorphism_w.
Qed.
Lemma OTorder_le_compat2 r: order r ->
(order_type r) <=O r.
Proof.
move=> or; apply /order_le_alt3P.
move: (OT_prop0 or) => [f oi]; exists f => //.
by apply: order_isomorphism_w.
Qed.
Lemma OTorder_le_compatP r r': order r -> order r' ->
(r <=O r' <-> (order_type r) <=O (order_type r')).
Proof.
move=> or or'.
split => h.
apply: (@order_le_transitive _ r).
apply: OTorder_le_compat2 => //.
apply: (@order_le_transitive _ r') => //.
apply: OTorder_le_compat1 => //.
apply: (@order_le_transitive _ (order_type r)).
apply: OTorder_le_compat1 => //.
apply: (@order_le_transitive _ (order_type r')) => //.
apply: OTorder_le_compat2 => //.
Qed.
Lemma OT_order_le_reflexive x: is_order_type x -> x <=t x.
Proof.
move=> ox; split => //; exists (identity (substrate x)); exists (substrate x).
split; first by fprops.
move: (OT_prop2 ox) => orx.
rewrite (iorder_substrate orx); exact: (identity_is orx).
Qed.
Lemma OTorder_le_alt2P r r':
r <=t r' <-> [/\ is_order_type r, is_order_type r' & r <=O r'].
Proof.
split; first by move /OTorder_le_altP => [pa pb /order_le_alt3P pc].
by move => [pa pb /order_le_alt3P pc]; apply /OTorder_le_altP.
Qed.
Lemma OT_order_le_transitive x y z:
x <=t y -> y <=t z -> x <=t z.
Proof.
move /OTorder_le_alt2P => [pa pb pc] /OTorder_le_alt2P [pd pe pf].
apply /OTorder_le_alt2P.
split => //; apply: (order_le_transitive pc pf).
Qed.
Definition OT_sum r g :=
order_type (order_sum r (Lg (domain g) (fun z => (order_type (Vg g z))))).
Definition OT_prod r g :=
order_type (order_prod r (Lg (domain g) (fun z => (order_type (Vg g z))))).
Definition OT_sum2 a b :=
order_type (order_sum2 (order_type a) (order_type b)).
Definition OT_prod2 a b :=
order_type (order_prod2 (order_type a) (order_type b)).
Notation "x +t y" := (OT_sum2 x y) (at level 50).
Notation "x *t y" := (OT_prod2 x y) (at level 40).
Lemma OT_sum2_pr a b:
a +t b = OT_sum canonical_doubleton_order (variantLc a b).
Proof.
rewrite /OT_sum2 /OT_sum /order_sum2.
by rewrite variantLc_comp.
Qed.
Lemma OT_prod2_pr a b:
a *t b = OT_prod canonical_doubleton_order (variantLc b a).
Proof.
rewrite /OT_prod2 /OT_prod /order_prod2.
by rewrite variantLc_comp.
Qed.
Lemma OT_sum_ordertype r g:
order r -> substrate r = domain g -> order_fam g ->
is_order_type (OT_sum r g).
Proof.
move=> or sr alo; apply: OT_prop1.
apply: orsum_or; bw; split => //; bw.
by hnf; bw; move=> i idg; bw; apply: OT_prop3; apply: alo.
Qed.
Lemma OT_prod_ordertype r g:
worder r -> substrate r = domain g -> order_fam g
-> is_order_type (OT_prod r g).
Proof.
move=> or sr alo; apply: OT_prop1.
apply: orprod_or; split => //; hnf;bw.
by move=> i idg; bw;apply: OT_prop3; apply: alo.
Qed.
Lemma OT_sum2_ordertype a b: is_order_type a -> is_order_type b ->
is_order_type (a +t b).
Proof.
move=> wo1 wo2;rewrite /OT_sum2; apply: OT_prop1.
by apply: orsum2_or;apply: OT_prop3; apply: OT_prop2.
Qed.
Lemma OT_prod2_ordertype a b: is_order_type a -> is_order_type b ->
is_order_type (a *t b).
Proof.
move=> wo1 wo2;rewrite /OT_prod2; apply: OT_prop1.
by apply: orprod2_or; apply: OT_prop3; apply: OT_prop2.
Qed.
Lemma OT_sum_invariant3 r g:
order r -> substrate r = domain g -> order_fam g ->
order_type (order_sum r g) =
OT_sum r (Lg (substrate r) (fun i => order_type (Vg g i))).
Proof.
move => or sr alo.
rewrite /OT_sum;apply: order_type_unique.
apply: orsum_invariant2; fprops;bw.
rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.
Lemma OT_prod_invariant3 r g:
worder r -> substrate r = domain g -> order_fam g ->
order_type (order_prod r g) =
OT_prod r (Lg (substrate r) (fun i => order_type (Vg g i))).
Proof.
move => or sr alo.
rewrite /OT_prod;apply: order_type_unique.
apply: orprod_invariant2;fprops;bw.
rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.
Lemma OT_sum_invariant5 a b c: order a -> order b -> order c ->
(order_sum2 a b) \Is c ->
(order_type a) +t (order_type b) = order_type c.
Proof.
move=> oa ob oc => h.
rewrite /ord_sum2; apply: order_type_unique.
rewrite OT_prop4 // OT_prop4 //.
by apply: (@orderIT (order_sum2 a b)) => //;
apply: orsum_invariant4;apply: OT_prop0.
Qed.
Lemma OT_prod_invariant5 a b c: order a -> order b -> order c ->
(order_prod2 a b) \Is c ->
(order_type a) *t (order_type b) = order_type c.
Proof.
move=> oa ob oc => h.
rewrite /ord_sum2; apply: order_type_unique.
rewrite OT_prop4 // OT_prop4 //.
by apply: (@orderIT (order_prod2 a b)) => //;
apply: orprod_invariant4;apply: OT_prop0.
Qed.
Definition order_type_fam g := (allf g is_order_type).
Lemma OT_sum_assoc1 r g r' g':
order r -> substrate r = domain g -> order_type_fam g ->
order r' -> substrate r' = domain g' -> order_fam g' ->
r = order_sum r' g' ->
let order_sum_assoc_aux :=
fun l =>
OT_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
OT_sum r g = OT_sum r' (Lg (domain g') (order_sum_assoc_aux)).
Proof.
move=> wor sr alB wor' sr' alw oal osa.
rewrite /OT_sum.
have oa': orsum_ax r' g' by [].
apply: order_type_unique.
set g'' := (Lg (domain g) (fun z => order_type (Vg g z))).
have oa: orsum_ax r g''.
rewrite /g'';red; bw; split => //;hnf;bw; move=> i idg; bw.
by move: (OT_prop3 (OT_prop2 (alB _ idg))).
move: (orsum_assoc_iso oa oa' oal) => /=.
set aux' := fun l =>
order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))).
set f:= Lf _ _ _.
move => oi1; move: (oi1) => [o1 o2 _ _].
apply: (@orderIT (order_sum r' (Lg (domain g') aux'))); first by exists f.
apply: orsum_invariant2 =>//; bw; fprops.
rewrite sr';move=> i isr; bw; rewrite /osa /OT_sum; bw.
set s := order_sum _ _.
have os: order s.
rewrite /s; apply: orsum_or; split => //; bw; first by apply: alw.
hnf; bw;move=> j js; bw.
have jdg: inc (J j i) (domain g).
by rewrite - sr oal (orsum_sr oa'); apply: disjoint_union_pi1.
apply: (OT_prop3 (OT_prop2 (alB _ jdg))).
have -> : (aux' i = s).
rewrite /aux' /s; apply: f_equal.
apply: Lg_exten => //;move=> j js.
have pd: inc (J j i) (domain g).
by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
rewrite /g''; bw.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.
Lemma OT_prod_assoc1 r g r' g':
worder r -> substrate r = domain g -> order_type_fam g ->
worder r' -> substrate r' = domain g' -> worder_fam g' ->
r = order_sum r' g' ->
(forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) ->
let order_prod_assoc_aux :=
fun l =>
OT_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
OT_prod r g = OT_prod r' (Lg (domain g') order_prod_assoc_aux).
Proof.
move=> wor sr alB wor' sr' alw oal alfs osa.
rewrite /OT_prod.
have oa': orsum_ax r' g'.
by split;fprops; move => t ta; move: (proj1 (alw _ ta)).
apply: order_type_unique.
set g'' := (Lg (domain g) (fun z => order_type (Vg g z))).
have oa: orprod_ax r g''.
rewrite /g'';red; bw;split => //; hnf;bw; move=> i idg; bw.
apply: (OT_prop3 (OT_prop2 (alB _ idg))).
move: (orprod_assoc_iso oa oa' oal wor' alw) => /=.
set aux' := fun l =>
order_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))).
set f:= Lf _ _ _.
move => oi1; move: (oi1) => [o1 o2 _ _].
apply: (@orderIT (order_prod r' (Lg (domain g') aux')));
first by exists f.
apply: orprod_invariant2 =>//; bw; fprops.
rewrite sr';move=> i isr; bw; rewrite /osa /OT_prod; bw.
set s:= order_prod _ _.
have -> : (aux' i = s).
rewrite /aux' /s; apply: f_equal.
apply: Lg_exten => //;move=> j js.
have pd: inc (J j i) (domain g).
by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
rewrite /g''; bw.
have os: order s.
rewrite /s; apply: orprod_or; split;bw; first fprops.
hnf; bw;move=> j js; bw.
have jdg: inc (J j i) (domain g).
rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
apply: (OT_prop3 (OT_prop2 (alB _ jdg))).
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.
Lemma OT_sum_assoc3 a b c:
is_order_type a -> is_order_type b -> is_order_type c ->
a +t (b +t c) = (a +t b) +t c.
Proof.
move => oa ob oc.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
rewrite/OT_sum2; apply: order_type_unique.
have pa: order (order_sum2 (order_type b) (order_type c)).
by apply: orsum2_or.
have pb: order (order_sum2 (order_type a) (order_type b)).
by apply: orsum2_or.
rewrite OT_prop4 // OT_prop4 //.
apply: (@orderIT
(order_sum2 (order_type a) (order_sum2 (order_type b) (order_type c)))).
apply: orsum_invariant4; [by apply: orderIR | by apply: OT_prop0 ].
apply: (@orderIT
(order_sum2 (order_sum2 (order_type a) (order_type b))(order_type c))).
apply: osum_assoc2; fprops.
apply: orsum_invariant4; [ by apply: order_type_exists | by apply: orderIR].
Qed.
Lemma OT_prod_assoc3 a b c:
is_order_type a -> is_order_type b -> is_order_type c ->
a *t (b *t c) = (a *t b) *t c.
Proof.
move => oa ob oc.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
rewrite/OT_prod2; apply: order_type_unique.
have pa: order (order_prod2 (order_type b) (order_type c)).
by apply: orprod2_or.
have pb: order (order_prod2 (order_type a) (order_type b)).
by apply: orprod2_or.
rewrite OT_prop4 // OT_prop4 //.
apply: (@orderIT
(order_prod2 (order_type a) (order_prod2 (order_type b) (order_type c)))).
apply: orprod_invariant4; [ by apply: orderIR |by apply: OT_prop0 ].
apply: (@orderIT
(order_prod2 (order_prod2 (order_type a) (order_type b))(order_type c))).
apply: oprod_assoc2; fprops.
apply: orprod_invariant4; [ by apply: order_type_exists | by apply: orderIR].
Qed.
Lemma OT_sum_distributive3 a b c:
is_order_type a -> is_order_type b -> is_order_type c ->
c *t (a +t b) = (c *t a) +t (c *t b).
Proof.
move => oa ob oc.
rewrite /OT_sum2 /OT_prod2; apply: order_type_unique.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
have pa: order (order_prod2 (order_type c) (order_type a)).
by apply: orprod2_or.
have pb: order (order_prod2 (order_type c) (order_type b)).
by apply: orprod2_or.
have pc: order (order_sum2 (order_type a) (order_type b)).
by apply: orsum2_or.
rewrite OT_prop4 // OT_prop4 // OT_prop4 //.
apply: (@orderIT
(order_prod2 (order_type c) (order_sum2 (order_type a) (order_type b)))).
apply: orprod_invariant4; [ by apply: orderIR | by apply: OT_prop0].
apply: (@orderIT
(order_sum2
(order_prod2 (order_type c) (order_type a))
(order_prod2 (order_type c) (order_type b)))).
apply: osum_distributive => //.
by apply: orsum_invariant4;apply: order_type_exists.
Qed.
Lemma OT_sum_increasing2 r f g: order r ->
substrate r = domain f -> substrate r = domain g ->
(forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) ->
(OT_sum r f) <=t (OT_sum r g).
Proof.
move=> wor sf sg alo.
have Xa: orsum_ax r (Lg (domain f) (fun z : Set => order_type (Vg f z))).
split => //;hnf; bw; move=> i isf; bw.
move: (alo _ isf) => [pa pb _].
by apply: OT_prop3; apply: OT_prop2.
have Xb: orsum_ax r (Lg (domain g) (fun z : Set => order_type (Vg g z))).
split => //; hnf;bw; rewrite - sg sf.
move=> i isf; bw;move: (alo _ isf) => [pa pb _].
by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_sum r (Lg (domain f) (fun z => order_type (Vg f z)))).
by apply: orsum_or.
have pb:order (order_sum r (Lg (domain g) (fun z => order_type (Vg g z)))).
by apply: orsum_or.
have pc: is_order_type (OT_sum r f) by apply: OT_prop1.
have pd: is_order_type (OT_sum r g) by apply: OT_prop1.
apply / OTorder_le_altP;split =>// ; apply: order_le_alt4.
apply /(OTorder_le_compatP pa pb); apply:osum_increasing1 => //.
bw; move=> x xdf; bw; last by rewrite - sg sf.
move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2].
by move /(OTorder_le_compatP (OT_prop2 ot1) (OT_prop2 ot2)).
Qed.
Lemma OT_prod_increasing2 r f g: worder r ->
substrate r = domain f -> substrate r = domain g ->
(forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) ->
(OT_prod r f) <=t (OT_prod r g).
Proof.
move=> wor sf sg alo.
have Xa: orprod_ax r (Lg (domain f) (fun z : Set => order_type (Vg f z))).
split => //;hnf ;bw; move=> i isf; bw.
move: (alo _ isf) => [pa pb _].
by apply: OT_prop3; apply: OT_prop2.
have Xb: orprod_ax r (Lg (domain g) (fun z : Set => order_type (Vg g z))).
split => //; hnf;bw; rewrite - sg sf.
move=> i isf; bw;move: (alo _ isf) => [pa pb _].
by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_prod r (Lg (domain f) (fun z => order_type (Vg f z)))).
by apply: orprod_or.
have pb:order (order_prod r (Lg (domain g) (fun z => order_type (Vg g z)))).
by apply: orprod_or.
have pc: is_order_type (OT_prod r f) by apply: OT_prop1.
have pd: is_order_type (OT_prod r g) by apply: OT_prop1.
apply /OTorder_le_altP;split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pa pb).
apply: oprod_increasing1 => //.
bw; move=> x xdf; bw; last by rewrite - sg sf.
move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2].
by move /(OTorder_le_compatP (OT_prop2 ot1)(OT_prop2 ot2)).
Qed.
Lemma OT_sum_increasing4 r f j: order r ->
substrate r = domain f ->
sub j (domain f) -> order_type_fam f ->
(OT_sum (induced_order r j) (restr f j)) <=t (OT_sum r f).
Proof.
move => or sr sjf alo.
have sjr: sub j (substrate r) by ue.
have dr: (domain (restr f j)) = j by rewrite restr_d //.
have Xa: orsum_ax r (Lg (domain f) (fun z => order_type (Vg f z))).
split => //; hnf; bw;move=> i isf; bw;move: (alo _ isf) => iot.
by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_sum r (Lg (domain f) (fun z => order_type (Vg f z)))).
by apply: orsum_or.
have pc: is_order_type (OT_sum r f) by apply: OT_prop1.
have dj: j = domain (restr f j) by rewrite restr_d.
move: (iorder_osr or sjr) => [pa' pb'].
have p2: orsum_ax (induced_order r j)
(Lg (domain (restr f j)) (fun z : Set => order_type (Vg (restr f j) z))).
split;fprops;bw;aw; hnf; bw; move=> i idf; bw.
move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot.
by apply: OT_prop3; apply: OT_prop2.
have pb: order (order_sum (induced_order r j)
(Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))).
by apply: orsum_or.
have pd: is_order_type (OT_sum (induced_order r j) (restr f j)).
by apply: OT_prop1.
apply /OTorder_le_altP; split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pb pa).
set g:= (Lg (domain f) (fun z : Set => order_type (Vg f z))).
have fgg: fgraph g by rewrite /g; fprops.
have sjdg: sub j (domain g) by rewrite /g; bw; ue.
have ->: (Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))
= restr g j.
by apply: fgraph_exten;fprops; bw;rewrite /g; move => k kj /= ;bw; apply: sjf.
apply: osum_increasing3 => //.
Qed.
Lemma OT_prod_increasing4 r f j: worder r ->
substrate r = domain f ->
sub j (domain f) -> order_type_fam f ->
(forall x, inc x ((domain f) -s j) ->
substrate (Vg f x) <> emptyset) ->
(OT_prod (induced_order r j) (restr f j)) <=t (OT_prod r f).
Proof.
move => or sr sjf alo alne .
have sjr: sub j (substrate r) by ue.
have dr: (domain (restr f j)) = j by rewrite restr_d //.
have Xa: orprod_ax r (Lg (domain f) (fun z => order_type (Vg f z))).
split => //; hnf;bw; move=> i isf; bw;move: (alo _ isf) => iot.
by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_prod r (Lg (domain f) (fun z => order_type (Vg f z)))).
by apply: orprod_or.
have pc: is_order_type (OT_prod r f) by apply: OT_prop1.
have dj: j = domain (restr f j) by rewrite restr_d.
have odr: order r by move: or => [ok _].
have p2: orprod_ax (induced_order r j)
(Lg (domain (restr f j)) (fun z : Set => order_type (Vg (restr f j) z))).
have woi: worder (induced_order r j) by apply:induced_wor.
split => //; bw; aw; hnf; bw=> i idf; bw.
move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot.
by apply: OT_prop3; apply: OT_prop2.
have pb: order (order_prod (induced_order r j)
(Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))).
by apply: orprod_or.
have pd: is_order_type (OT_prod (induced_order r j) (restr f j)).
by apply: OT_prop1.
apply/OTorder_le_altP; split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pb pa).
set g:= (Lg (domain f) (fun z : Set => order_type (Vg f z))).
have fgg: fgraph g by rewrite /g; fprops.
have sjdg: sub j (domain g) by rewrite /g; bw; ue.
have ->: (Lg (domain (restr f j)) (fun z=> order_type (Vg (restr f j) z)))
= restr g j.
by apply: fgraph_exten; fprops; bw;rewrite /g; move => k kj /= ;bw;apply: sjf.
apply: oprod_increasing3 => //.
move=> x; rewrite /g Lg_domain => xg.
have xdf: inc x (domain f) by move: xg => /setC_P [].
bw; move: (alne _ xg) => t; dneg bad.
move: (order_type_exists (OT_prop2 (alo _ xdf)))
=> [h [_ _ [[[fh _] _] sh tgh] _]].
apply /set0_P => t' ts.
empty_tac1 (Vf h t'); rewrite - tgh; Wtac.
Qed.
Lemma OT_prod_pr1 a b c:
is_order_type a -> is_order_type b -> worder c -> b \Is c ->
a *t b = OT_sum c (cst_graph (substrate c) a).
Proof.
move=> ota otb woc ibc.
rewrite /OT_prod2 /OT_sum.
have ora: order a by apply: OT_prop2.
have orb: order b by apply: OT_prop2.
move: (proj1 woc) => oc.
apply: order_type_unique.
have ->: domain (cst_graph (substrate c) a) = substrate c.
rewrite /cst_graph; bw.
apply: (@orderIT (order_prod2 a b)).
by apply: orprod_invariant4; apply: OT_prop0.
move: (order_prod_pr ora orb);set aux := order_sum _ _ ; move=> h.
apply: (@orderIT aux) => //.
move: ibc => [f isf].
rewrite /aux /cst_graph; apply: (orsum_invariant1(f:=f)); bw => //.
move: isf => [_ _ [[[ff _] _] sf tf] _].
rewrite - sf; move=> i id.
move: (Vf_target ff id); rewrite -tf=> vt.
by bw ; apply: order_type_exists.
Qed.
Definition OT_opposite x := order_type (opp_order x).
Lemma OT_opposite1 a b: a \Is b ->
(opp_order a) \Is (opp_order b).
Proof.
move=> [f [o1 o2 bp isf]].
move: (opp_osr o1)(opp_osr o2) => [pa pb][pc pd].
exists f;split => //;fprops; rewrite ? pb ? pd //.
move=> x y asf bsf.
by split; move /opp_gleP /(isf _ _ bsf asf) /opp_gleP.
Qed.
Lemma OT_opposite2 x: order x -> opp_order (opp_order x) = x.
Proof. move =>[pa _ _ _]; apply :(igraph_involutive pa). Qed.
Lemma OT_double_opposite x: is_order_type x ->
OT_opposite (OT_opposite x) = x.
Proof.
move=> otx; rewrite /OT_opposite.
have ox : order x by apply: OT_prop2.
have xp1: x= order_type x by move: otx => [y yo yp]; rewrite yp OT_prop4 //.
rewrite {2} xp1; apply: order_type_unique.
rewrite -{2} (OT_opposite2 ox);apply: OT_opposite1.
apply: OT_prop0; apply: (proj1 (opp_osr ox)).
Qed.
Lemma OT_opposite_sum r f: order r ->
substrate r = domain f -> order_type_fam f ->
OT_opposite (OT_sum r f) =
OT_sum (opp_order r) (Lg (substrate r) (fun z => OT_opposite (Vg f z))).
Proof.
move=> or sr alo.
rewrite /OT_opposite /OT_sum Lg_domain; apply: order_type_unique.
set s1 := order_sum _ _.
have alor : forall x , inc x (domain f) -> order (Vg f x).
move=> i idf; apply: (OT_prop2 (alo _ idf)).
set s2:= order_sum r (Lg (domain f) (fun z => (Vg f z))).
apply: (@orderIT (opp_order s2)).
apply: OT_opposite1;apply: (@orderIT s1).
apply: OT_prop0.
apply: orsum_or; bw;split => //; hnf; bw => i idf; bw.
apply: (OT_prop3 (alor _ idf)).
rewrite /s1 /s2.
apply: orsum_invariant2 ; bw; fprops.
rewrite sr;move=> i isr; bw; apply: (OT_prop0 (alor _ isr)).
set g := (Lg (domain f) (fun z => (opp_order (Vg f z)))).
move: (opp_osr or) => [pa pb].
have ta: orsum_ax (opp_order r) g.
rewrite /g;split => //;fprops;aw; bw;first by ue.
hnf; bw;move=> i idf; bw; exact: (proj1 (opp_osr (alor _ idf))).
have os2: order s2.
by apply: orsum_or; split => //; hnf; bw; move=> i idf; bw; apply: alor.
have tb:orsum_ax r (Lg (domain f) (fun z => Vg f z)).
split => //; bw;aw;hnf;bw.
move=> i idf; bw; move: (alor _ idf) => aux; fprops.
have osg: order (order_sum (opp_order r) g) by apply: orsum_or.
have ss:substrate (order_sum (opp_order r) g) = substrate s2.
rewrite /s2 orsum_sr // orsum_sr //.
rewrite /sum_of_substrates /fam_of_substrates /g; bw.
apply: f_equal; apply: Lg_exten => // x xdf; bw.
apply (proj2 (opp_osr (alor _ xdf))).
apply: (@orderIT (order_sum (opp_order r) g)).
move: ( identity_fb (substrate s2)) => hh.
move: (opp_osr os2) => [oo3 sr2].
exists (identity (substrate s2)).
split;fprops; first split;aw; fprops.
hnf;aw;move => x y xsr ysr; rewrite !identity_V //.
have qy:inc (Q y) (domain f).
move: ysr; rewrite /s2 orsum_sr // => h.
move: (du_index_pr1 h) => [h1 _]; move: h1; bw.
have qx:inc (Q x) (domain f).
move: xsr; rewrite /s2 orsum_sr // => h.
move: (du_index_pr1 h) => [h1 _]; move: h1; bw.
have sgs2: sum_of_substrates g = substrate s2.
by move: ss; rewrite /s2 orsum_sr // orsum_sr //.
have sgs3: (sum_of_substrates (Lg (domain f) (Vg f))) = substrate s2.
rewrite /s2 orsum_sr //.
split.
move /opp_gleP => ha; apply /orsum_gleP; rewrite sgs2;split => //.
move: ha => /orsum_gleP [pa' pb']; case => pc.
by left; apply /opp_gltP.
rewrite /order_sum_r;right; move: pc => []; bw; move => -> pc; split => //.
by rewrite /g; bw; apply /opp_gleP.
move /orsum_gleP => [_ _ h]; apply /opp_gleP; apply /orsum_gleP.
rewrite sgs3;split => //; case: h; first by move /opp_gltP => h;left.
move => [sq]; rewrite /g; bw;move /opp_gleP => h.
right; bw;split => //; ue.
apply: orsum_invariant2 => //; rewrite /g pb; bw.
rewrite sr;move=> i isr; bw.
move: (alor _ isr) => aux.
have aux2: order (opp_order (Vg f i)) by apply: (proj1 (opp_osr (alor _ isr))).
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.
End OrderType.