proposition: Lemma Exercise1_18b E: \3c <=c (cardinal E) -> ~ (distributive_lattice1 (coarser E)).
proof: Proof. move /cardinal_ge3 => [x [y [z [xE yE zE [xy xz yz]]]]]. set (o:= tripleton x y z); set (F:= E -s o). have oz: inc z o by apply /set3_P; in_TP4. have oy: inc y o by apply /set3_P; in_TP4. have ox: inc x o by apply /set3_P; in_TP4. have xnF: ~ (inc x F) by move /setC_P => [_]; case. have ynF: ~ (inc y F) by move /setC_P => [_]; case. have znF: ~ (inc z F) by move /setC_P => [_]; case. have Ha: forall x, singleton x <> emptyset by move => u se; empty_tac1 u. pose with_F u := (u +s1 F) -s1 emptyset. have wf1: (forall u, ~ (inc emptyset u) -> F = emptyset -> with_F u = u). by move=> u nsu Fe; rewrite /with_F Fe; apply: setU1_K. have wf2: (forall u, ~ (inc emptyset u) -> F <> emptyset -> with_F u = u +s1 F). move=> u une Fne; apply: setC1_eq => /setU1_P; case; fprops. have oe: (sub o E) by move=> t /set3_P;case => ->. have wfp: (forall u, partition_s u o -> partition_s (with_F u) E). move=> u [[p1 p3] p2]; split; last by move=> a /setC1_P [_] /nonemptyP. split. set_extens t. move /setU_P=> [a ta]; case/setC1_P; case /setU1_P => h _. apply: oe; rewrite -p1; union_tac. by move: ta; rewrite h => /setC_P []. move=> tE; case: (inc_or_not t o). rewrite -p1 => /setU_P [v tv vu]; apply /setU_P; exists v =>//. apply /setC1_P;split; first by apply /setU1_P; left. move=> ve;empty_tac1 t. move => to; have tF: inc t F by apply /setC_P. apply /setU_P; exists F => //; apply /setC1_P;split;fprops. move=> Fe;empty_tac1 t. move=> a b /setC1_P [] /setU1_P; case=> aa ane. move /setC1_P => [] /setU1_P; case=> bb bne; first by apply: p3. right; apply: disjoint_pr => v va vb. move: vb; rewrite bb => /setC_P [_]; case; rewrite -p1; union_tac. move /setC1_P => [] /setU1_P; case => bb bn; last by rewrite aa; left. right; apply: disjoint_pr => v vb va. move: vb; rewrite aa => /setC_P [_]; case; rewrite -p1; union_tac. pose pa3 a b c := doubleton (singleton a) (doubleton b c). have pa3p: (forall a b c, (singleton a) \cup (doubleton b c) = o -> partition_s (pa3 a b c) o). move => a b c H; split; last first. move=> u /set2_P; case=> ->; [apply: set1_ne | apply: set2_ne]. have H1: disjoint (singleton a) (doubleton b c). apply: disjoint_pr => u /set1_P eq1; move: H; rewrite eq1 => e1 e2. have: sub o (doubleton b c). by rewrite - e1 => t /setU2_P; case => // /set1_P ->. move/sub_smaller; rewrite (cardinal_tripleton xy xz yz) => ha. case: (cleNgt (cleT ha (cardinal_doubleton b c)) (cltS NS2)). split => // u v /set2_P [] -> /set2_P [] ->; try (by left); right => //. by apply: disjoint_S. set (Px:= with_F (pa3 x y z)). set (Py:= with_F (pa3 y x z)). set (Pz:= with_F (pa3 z x y)). have pox: partition_s (pa3 x y z) o. apply: pa3p;rewrite setU2_C. set_extens t;case/set3_P => ->; apply/set3_P; in_TP4. have poy: partition_s (pa3 y x z) o. apply: pa3p; rewrite setU2_C. set_extens t;case/set3_P => ->; apply/set3_P; in_TP4. have poz: partition_s (pa3 z x y) o by apply: pa3p; rewrite setU2_C. have ppx: partition_s Px E by apply: wfp; apply: pox. have ppy: partition_s Py E by apply: wfp; apply: poy. have ppz: partition_s Pz E by apply: wfp; apply: poz. move: (coarser_osr E) => [oce pb]. have auxP: forall u, inc u (substrate (coarser E)) <-> partition_s u E. by move=> u; rewrite pb; apply: partitionsP. have Pxr: inc Px (substrate (coarser E)) by apply/auxP. have Pyr: inc Py (substrate (coarser E)) by apply/auxP. have Pzr: inc Pz (substrate (coarser E)) by apply/auxP. set (alpha:= with_F(greatest_partition o)). set (omga:= with_F(least_partition o)). have ppa: (partition_s alpha E) by apply: wfp; apply: greatest_is_partition. have ppo: (partition_s omga E). by apply: wfp; apply: least_is_partition; exists z. have lr: lattice (coarser E). move: (Exercise1_18a E) => [cl1 cl2]. by split => // u v uE vE;apply:cl2; move=> t /set2_P [] ->. have or: order (coarser E) by move: lr => [ok _]. move=> bad; move: (bad Px Py Pz Pxr Pyr Pzr). have one: o <> emptyset by move => h; empty_tac1 z. have op1:forall u, partition_s u o -> gle (coarser E) omga (with_F u). move=> u pu; apply /coarser_gleP; split;fprops. move=> a /setC1_P [] /setU1_P; case => h ae. exists o => //. by apply /setC1_P; split => //; apply /setU1_P; left; apply/set1_P. by move: pu => [[pu1 pu3] pu2]; rewrite -pu1; apply: setU_s1. exists a;fprops; apply /setC1_P;split => //;rewrite h; fprops. have oPx: gle (coarser E) omga Px by apply: op1. have oPy: gle (coarser E) omga Py by apply: op1. have oPz: gle (coarser E) omga Pz by apply: op1. have Hb: forall u v, doubleton u v <> emptyset by move => u uv h; empty_tac1 u. have ->: (inf (coarser E) Py Pz = omga). move: (lattice_inf_pr lr Pyr Pzr) => [e1 e2 e3]. move: (arg1_sr e1) => /auxP infp. move: e1 => /coarser_gleP [_ _ cc]. have d1Py: inc (doubleton x z) Py. by apply /setC1_P;split; fprops;apply /setU1_P; left; apply /set2_P; right. move: e2 (cc _ d1Py)=> /coarser_gleP [_ _ cc2] [s1 p1 p2]. have d2Py: inc (doubleton x y) Pz. by apply /setC1_P;split;fprops; apply /setU1_P; left; apply /set2_P; right. move: (cc2 _ d2Py)=> [s2 p3 p4]. case: (proj2 (proj1 infp) _ _ p1 p3) => s1s2;last by empty_tac1 x. apply: (order_antisymmetry or); last by apply: e3. apply /coarser_gleP; split => // a. move /setC1_P => [] /setU1_P [] /set1_P p5 p6. rewrite p5;ex_tac => t;case/set3_P => ->; first by apply: p4; fprops. by apply p4; fprops. by rewrite - s1s2; apply p2; fprops. move: p6; move /set1_P: p5 => -> p6. have FPy: inc F Py by apply /setC1_P;split => //; apply /setU1_P; right. move: (cc _ FPy)=> [s3 p7 p8]; ex_tac. rewrite sup_C (sup_comparable1 or oPx). suff p3: forall a b, doubleton a b = doubleton y z -> (sup (coarser E) Px (with_F (pa3 a x b)) = alpha). rewrite /Py/Pz p3 // p3; last by apply: set2_C. rewrite (inf_comparable1 or); last (by order_tac; apply/auxP); move => pa. have: inc (singleton y) alpha. by apply/setC1_P; split;fprops; apply /setU1_P;left; apply /funI_P;exists y. rewrite -pa; move /setC1_P => [] /setU1_P; case. move /set2_P; case =>h; first by move: (set1_inj h) => h1; case: xy. have /set1_P /(nesym yz) //: inc z (singleton y) by rewrite h; fprops. by move=> yF; move: (set1_1 y); rewrite yF; move /setC_P => [_]; case. move=> a b da. have ax: a <> x. by move=> ax; move: (set2_1 a b); rewrite da ax;case /set2_P. have bx: b <> x. by move=> bx; move: (set2_2 a b); rewrite da bx; case/set2_P. have ab: a <> b. move=> ab; move: (set2_2 y z)(set2_1 y z). by rewrite -da ab => /set1_P <- /set1_P. have ao: inc a o by move: (set2_1 a b); rewrite da; case/set2_P =>->. have bo: inc b o by move: (set2_2 a b); rewrite da; case/set2_P =>->. set Pt:= with_F (pa3 a x b). have Ptsw: (Pt = Py \/ Pt = Pz). rewrite /Py /Pz /Pt. by case: (doubleton_inj da); move => [av bv]; rewrite av bv; [left | right]. rewrite intersection_is_sup2_b //; last by case: Ptsw => ->. have fg1: fgraph (Lg o singleton) by fprops. have in1: forall a b, (doubleton a b) \cap (singleton a) = singleton a. move=> A B; set_extens t; first by move /setI2_P => []. move => h; apply /setI2_P;split => //; move /set1_P: h => ->; fprops. have in2:(doubleton a b) \cap (doubleton x b) = singleton b. set_extens s. by move => /setI2_P []; case/set2_P => ->; fprops; case/set2_P. move /set1_P => ->; apply /setI2_P; split; fprops. set_extens t. move /Zo_P => [] /setI_covering2_P [u [v [u1 v1 i1]]] /set1_P net. apply /setC1_P; split => //. move/nonemptyP : net; rewrite -i1; move=> [w] /setI2_P [wu wv]. move: u1 v1 => /setC1_P [p1 p2] /setC1_P [p3 p4]. case /setU1_P: p1. - case /set2_P => p5; case /setU1_P: p3; first case /set2_P => p6. + by case: ax; move: wu wv; rewrite p5 p6 => /set1_P -> /set1_P ->. + by apply /setU1_P; left; apply /funI_P; exists x=> //; rewrite p5 p6 setI2_C in1. + by move => vF;case: xnF; move: wu wv; rewrite p5 vF; move => /set1_P ->. - case/set2_P => p6. + by rewrite p5 p6 -da in1; apply /setU1_P; left; apply /funI_P; exists a. + by rewrite p5 p6 -da in2; apply /setU1_P; left; apply /funI_P; exists b. + by move => vF; move: wu wv; rewrite vF p5; case/set2_P => -> h; [ by case: ynF | by case: znF ]. - move => uF; case/setU1_P: p3; first case/set2_P => h. + move:wv wu; rewrite h uF => /set1_P. move: (set2_1 a b); rewrite da; case/set2_P => -> -> h1; [ by case: ynF | by case: znF ]. + move: wv wu; rewrite h uF; case/set2_P; first by move => -> h2; case: xnF. move: (set2_2 a b); rewrite da; case/set2_P => -> -> h1; [ by case: ynF | by case: znF ]. + by move=> ->; apply /setU1_P;right; rewrite uF; rewrite setI2_id. move => /setC1_P [pa pb']; apply/setC1_P; split => //. apply /setI_covering2_P. case/setU1_P: pa; last first. move=> tf ; exists t, t; rewrite setI2_id;split => //; apply /setC1_P;split => //; apply /setU1_P; right; ue. move /funI_P => [c co] => tC. set C1 := (((pa3 x y z) +s1 F) -s1 emptyset). set C2 := (((pa3 a x b) +s1 F) -s1 emptyset). have xc1: inc (singleton x) C1. apply /setC1_P;split; first (apply /setU1_P; left; apply /set2_P);fprops. have ac2: inc (singleton a) C2. apply /setC1_P;split; first (apply /setU1_P; left; apply /set2_P);fprops. have bx2: inc (doubleton x b) C2. apply /setC1_P;split; first (apply /setU1_P; left; apply /set2_P);fprops. have ab2: inc (doubleton a b) C1. apply /setC1_P;split; first (apply /setU1_P; left; apply /set2_P);fprops. have cxab: (c = x \/ (c = a \/ c = b)). move: co =>/set3_P; case; first (by fprops); move => -> ;right. by move: (set2_1 y z); rewrite -da; move /set2_P. by move: (set2_2 y z); rewrite -da; move /set2_P. rewrite tC;case: cxab. move=> ->;exists (singleton x), (doubleton x b); split => //. by rewrite setI2_C in1. case=> ->. by exists (doubleton a b), (singleton a). by exists (doubleton a b), (doubleton x b). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)