(** * Theory of Sets EIII-4 Natural integers. Finite sets Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm). *) (* $Id: sset8.v,v 1.151 2016/07/01 16:28:45 grimm Exp $ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset7. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module CardinalOps. (** ** EIII-3-3 Operations on Cardinals *) Definition csum x := cardinal (disjointU x). Definition cprod x := cardinal (productb x). Definition csumb a f := csum (Lg a f). Definition cprodb a f := cprod (Lg a f). Lemma csum_gr f: csumb (domain f) (Vg f) = csum f. Proof. congr cardinal; rewrite /disjointU /disjointU_fam; bw. congr unionb; apply:Lg_exten => x xdf; bw. Qed. Lemma cprod_gr f: cprodb (domain f) (Vg f) = cprod f. Proof. congr cardinal;apply: @productb_gr. Qed. Lemma csumb_exten A f g : {inc A, f =1 g} -> csumb A f = csumb A g. Proof. by move => h; congr csum; apply: Lg_exten. Qed. Lemma cprodb_exten A f g : {inc A, f =1 g} -> cprodb A f = cprodb A g. Proof. by move => h; congr cprod; apply: Lg_exten. Qed. Lemma CS_csum f: cardinalp (csum f). Proof. rewrite /csum; fprops. Qed. Lemma CS_cprod f: cardinalp (cprod f). Proof. rewrite /cprod; fprops. Qed. Hint Resolve CS_csum CS_cprod: fprops. Theorem cprod_pr f: cardinal (productb f) = cprodb (domain f) (fun a => cardinal (Vg f a)). Proof. rewrite - /(cprod f) - cprod_gr; apply /card_eqP. apply: Eq_setXb; split; fprops; bw => i idx; bw; fprops. Qed. Theorem csum_pr f: cardinal (disjointU f) = csumb (domain f) (fun a => cardinal (Vg f a)). Proof. rewrite - /(csum f) - csum_gr; apply /card_eqP. apply: equipotent_disjointU1;split;fprops; bw => i idx;bw;fprops. Qed. Lemma csum_pr3 f g: domain f = domain g -> (forall i, inc i (domain f) -> cardinal (Vg f i) = cardinal (Vg g i)) -> csum f = csum g. Proof. by move=> dfg sc; rewrite /csum 2!csum_pr -dfg; apply:csumb_exten. Qed. Lemma csum_pr4 f: mutually_disjoint f -> cardinal (unionb f) = csumb (domain f) (fun a => cardinal (Vg f a)). Proof. move => pa; rewrite - csum_pr; apply /card_eqP. apply: equipotent_disjointU => //; last by exact (@disjointU_disjoint f). rewrite /disjointU_fam; split; fprops; bw => i idx; bw;exact:Eq_indexed. Qed. Lemma csum_pr4_bis X f: (forall i j, inc i X -> inc j X -> i = j \/ disjoint (f i) (f j)) -> cardinal (unionf X f) = csumb X (fun a => cardinal (f a)). Proof. set x := Lg X f => h. have h1: mutually_disjoint x. by rewrite /x;hnf; bw => i j iX jX; bw; apply:h. have ->: unionf X f = unionb x. rewrite/unionb/x; bw;apply:setUf_exten => t tX; bw. have ->: csumb X (fun a => cardinal (f a)) = csumb (domain x) (fun a => cardinal (Vg x a)). rewrite /x; bw; apply:csumb_exten => t tx; bw. apply:(csum_pr4 h1). Qed. Lemma csum_pr1 f: cardinal (unionb f) <=c csumb (domain f) (fun a => cardinal (Vg f a)). Proof. rewrite - (csum_pr f);apply: surjective_cle. move: (disjointU_pr f) => /=; set g := common_ext _ _ _. by move => [sf tg srfj _]; exists g. Qed. Lemma csum_pr1_bis X f: cardinal (unionf X f) <=c csumb X (fun a => cardinal (f a)). Proof. set x := Lg X f. have ->: unionf X f = unionb x. rewrite/unionb/x; bw; apply:setUf_exten => t tX; bw. have ->: csumb X (fun a => cardinal (f a)) = csumb (domain x) (fun a => cardinal (Vg x a)). rewrite /x; bw; apply:csumb_exten => t tx; bw. apply:(csum_pr1 x). Qed. Theorem csum_Cn X f: target f = domain X -> bijection f -> csum X = csum (X \cf (graph f)). Proof. move=> tf [[ff injf] sjf]. have sf:source f = domain (graph f) by aw. set X' := Lg (domain X) (Vg X). have <-: (Lg (source f) (fun z => Vg X (Vf f z))) = X \cf (graph f). rewrite /composef -(proj33 ff); apply: Lg_exten => i idf; rewrite /X';bw. have aux : (Lg (source f) (fun z => Vg X (Vf f z))) = X' \cf (graph f). rewrite /composef -(proj33 ff); apply: Lg_exten => i idf; rewrite /X';bw. rewrite -tf -/(Vf _ _); Wtac. have ->: csum X = csumb (domain X) (Vg X) by rewrite csum_gr. pose g:= Lg (source f) (fun i => (Vg (X' \cf (graph f)) i) *s1 (Vf f i)). apply /card_eqP; apply:(@EqT (unionb g)); last first. rewrite /g - aux ;apply: equipotent_disjointU; first(rewrite/disjointU_fam;hnf;bw;split=> // i isf; bw; apply:Eq_indexed3); apply: mutually_disjoint_prop2; bw => i j y isf jsf; bw; move /setX_P => [_ _ /set1_P e1] /setX_P [_ _ /set1_P e2]; rewrite e1 // in e2; apply: (injf _ _ isf jsf e2). rewrite/csum /disjointU/ disjointU_fam; aw. set h := Lg _ _. have ->: (g = h \cf (graph f)). rewrite /h/g; apply: fgraph_exten; fprops;bw;rewrite ? composef_domain //. by move=> x xsf /=; bw; try ue;rewrite /X' -tf -/ (Vf f x); bw; Wtac. rewrite - setUb_rewrite1 /h //; bw; fprops. rewrite (surjective_pr3 sjf) tf /X'; bw. Qed. Lemma csum_Cn' X f: bijection f -> csumb (target f) X = csumb (source f) (fun i => (X (Vf f i))). Proof. move => bf; rewrite /csumb. have ff: function f by fct_tac. have h: target f = domain (Lg (target f) X) by bw. rewrite (csum_Cn h bf) /composef; aw; apply: f_equal;apply: Lg_exten. by move => i isf /=; bw; rewrite -/(Vf f i); Wtac. Qed. Theorem cprod_Cn X f: target f = domain X -> bijection f -> cprod X = cprod (X \cf (graph f)). Proof. move=> tF bijf;apply /card_eqP. exists (product_compose X f); hnf; rewrite lf_source lf_target. split => //; first by apply: pc_fb. rewrite /composef; aw; fct_tac. Qed. Theorem csum_An f g: partition_w_fam g (domain f) -> csum f = csumb (domain g) (fun l => csumb (Vg g l) (Vg f)). Proof. move=> pfg. apply /card_eqP; set h := fun l:Set => _. rewrite/disjointU/disjointU_fam Lg_domain. set g0 := fun l:Set => _; set a:= unionb _. have ->: a = unionb (Lg (domain g) (fun l => unionf (Vg g l) g0)). rewrite /a /unionb; bw; transitivity (unionf (domain f) g0). by apply: setUf_exten; move => t tdf /=; bw. rewrite - (proj33 pfg) /unionb setUf_A. apply: setUf_exten; move=> i idg /=; bw. apply: equipotent_disjointU; fprops; bw; last first. apply: mutually_disjoint_prop2; move=> u v y _ _. by move /setX_P => [_ _ /set1_P <-] /setX_P [_ _ /set1_P]. apply: mutually_disjoint_prop2; rewrite /g0=> u v y udg vdg; aw. move /setUf_P => [u' u'Vg /setX_P [py Py /set1_P Qy]]. move /setUf_P => [v' v'Vg /setX_P [py' Py' /set1_P Qy']]. case :(proj32 pfg _ _ udg vdg) =>// di. rewrite -Qy' Qy in v'Vg; case: (nondisjoint u'Vg v'Vg di). split; fprops; bw => i idg; bw. set g1:= (fun i0 => (Vg f i0) *s1 i0). have ->: unionf (Vg g i) g1 = unionb (Lg (Vg g i) g1). rewrite /unionb; bw; apply: setUf_exten; move=> j jVg /=; bw. apply:EqT (Eq_indexed (h i) i). apply:EqT (cardinal_pr0 (disjointU (Lg (Vg g i) (Vg f)))). rewrite /disjointU/disjointU_fam; bw. apply: equipotent_disjointU => //. split; fprops;bw; move=> j jVg; bw; apply: Eq_setX;fprops. apply: mutually_disjoint_prop2; move=> u v y _ _; rewrite /g1. by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. apply: mutually_disjoint_prop2; move=> u v y _ _. by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. Qed. Theorem cprod_An f g: partition_w_fam g (domain f) -> cprod f = cprodb (domain g) (fun l => cprodb (Vg g l) (Vg f)). Proof. move=> pfa; apply /card_eqP. set h := (productb (Lg (domain g) (fun l => restriction_product f (Vg g l)))). apply:(@EqT h). exists (prod_assoc_map f g); split; first by apply: pam_fb. by rewrite/ prod_assoc_map; aw. by rewrite/ prod_assoc_map; aw. apply: Eq_setXb => //; split; fprops; bw. move=> i idg; bw; rewrite /cprodb /cprod /restriction_product;fprops. Qed. Theorem cprodDn f: cprodb (domain f) (fun l => csum (Vg f l)) = csumb (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (cprodb (domain f) (fun l => Vg (Vg f l) (Vg g l)))). Proof. apply /card_eqP. apply: (@EqT (productf (domain f) (fun l => (disjointU (Vg f l))))). apply: Eq_setXb;split; fprops; bw. move=> i idf; bw; rewrite /csum; fprops. set (g:= Lg (domain f) (fun l => disjointU_fam (Vg f l))). have dg: domain g = domain f by rewrite /g; bw. have ->: productf (domain f) (fun l => unionb (disjointU_fam (Vg f l))) = productf (domain g) (fun l => unionb (Vg g l)). rewrite -dg /productf;apply: f_equal; apply: Lg_exten. move=> x xdg; rewrite /g; bw; ue. rewrite distrib_prod_union //. set d0 := (productf (domain g) (fun l => domain (Vg g l))). set g0:= fun g0:Set => _. have ->: unionf d0 g0 = unionb (Lg d0 g0). rewrite /unionb; bw;apply: setUf_exten; move=> i ip /=; bw. rewrite /d0 dg. set ld:= productf _ _. have lde: ld = productf (domain f) (fun l => domain (Vg f l)). rewrite /ld/productf; apply: f_equal; apply: Lg_exten. move=> x xdg; rewrite /g; bw; rewrite / disjointU_fam; bw. rewrite - lde. apply: equipotent_disjointU;last by fprops. split => //; bw; first by rewrite/ disjointU_fam; bw. move=> i ip; bw. set h := (productb (Lg (domain f) (fun l => Vg (Vg f l) (Vg i l)))). apply:(@EqT (cardinal h)); last by rewrite /disjointU_fam;bw;apply:Eq_indexed. apply:EqT (cardinal_pr0 h); apply: Eq_setXb; split => //; bw; fprops. move=> k kdg; rewrite /g /disjointU_fam -dg; bw; first exact:Eq_indexed2. move: ip; rewrite lde; move/setXf_P => [_ dif hyp]. by apply: hyp; rewrite - dg. have myel: forall i j y, inc i ld -> inc y (productf (domain f) (fun l => Vg (Vg g l) (Vg i l))) -> inc j (domain f) -> Q (Vg y j) = Vg i j. rewrite /g/ disjointU_fam. move=>k j y; bw=> kp1 yp jdf. move: kp1;rewrite lde;move /setXf_P=> [fgk dk kp1]. move: (kp1 _ jdf)=> iVjk. move: yp => /setXf_P [fgy dy yp1]. by move: (yp1 _ jdf); bw; move /setX_P => [_ _ /set1_P]. apply: mutually_disjoint_prop; bw. move=>i j y ild jld; rewrite /g0 dg; bw=> xp yp. apply: (setXf_exten ild jld) => k kdf /=. by rewrite - (myel _ _ _ ild xp kdf) - (myel _ _ _ jld yp kdf). Qed. (** Product and sums of two cardinals *) Definition csum2 a b := csum (variantLc a b). Definition cprod2 a b := cprod (variantLc a b). Notation "x +c y" := (csum2 x y) (at level 50). Notation "x *c y" := (cprod2 x y) (at level 40). Lemma CS_sum2 a b: cardinalp (a +c b). Proof. rewrite/csum2/csum; fprops. Qed. Lemma CS_prod2 a b: cardinalp (a *c b). Proof. rewrite /cprod2/cprod; fprops. Qed. Hint Resolve CS_sum2 CS_prod2: fprops. Lemma csum2_pr a b f: doubleton_fam f a b -> a +c b = csum f. Proof. move=> /two_terms_bij [g [bg tg ->]]; apply: (csum_Cn tg bg). Qed. Lemma cprod2_pr a b f: doubleton_fam f a b -> a *c b = cprod f. Proof. move=> /two_terms_bij [g [bg tg ->]]; apply: (cprod_Cn tg bg). Qed. Fact card_commutative_aux a b: doubleton_fam (variantLc b a) a b. Proof. by exists C1, C0; bw;split; fprops; rewrite set2_C. Qed. Lemma csumC a b: a +c b = b +c a. Proof. apply: (csum2_pr (card_commutative_aux a b)). Qed. Lemma cprodC a b: a *c b = b *c a. Proof. by rewrite (cprod2_pr (card_commutative_aux a b)). Qed. Lemma disjointU2_pr3 a b x y: y <> x -> (a +c b) \Eq ((a *s1 x) \cup (b *s1 y)). Proof. move=> yx. rewrite -(disjointU2_rw _ _ yx) /csum2/csum. have aux: forall z t, t <> z -> doubleton_fam (variantL z t a b) a b. move=> z t zt; exists z; exists t; split => //; bw. - by apply: nesym. - fprops. - rewrite /variantL; bw. - rewrite variant_V_a //. - rewrite variant_V_b //. apply: (EqT (cardinal_pr(disjointU (variantL C0 C1 a b)))). by apply /card_eqP; move:(csum2_pr (aux _ _ yx)) (csum2_pr (aux _ _ C0_ne_C1)). Qed. Lemma csum2_pr5 a b: disjoint a b -> cardinal (a \cup b) = a +c b. Proof. move => h. rewrite - (card_card (CS_sum2 a b)). apply/card_eqP; apply: EqT (EqS (disjointU2_pr3 a b C1_ne_C0)). apply: (equipotent_disjointU2 h); fprops; apply:Eq_indexed. Qed. Lemma csum2_pr4 a b a' b': a \Eq a' -> b \Eq b' -> a +c b = a' +c b'. Proof. move=> /card_eqP eaa /card_eqP ebb. rewrite - (card_card (CS_sum2 a b)) - (card_card (CS_sum2 a' b')). move: (disjointU2_pr3 a b C1_ne_C0)(disjointU2_pr3 a' b' C1_ne_C0)=> eq1 eq2. apply /card_eqP/(EqT eq1)/(EqT _ (EqS eq2)). by apply:equipotent_disjointU2;fprops;apply/card_eqP; rewrite!cardinal_indexed. Qed. Lemma csum2_pr2 a b a' b': cardinal a = cardinal a' -> cardinal b = cardinal b' -> a +c b = a' +c b'. Proof. by move => /card_eqP p1 /card_eqP p2; apply: csum2_pr4. Qed. Lemma csum2cl x y: (cardinal x) +c y = x +c y. Proof. exact: (csum2_pr2 (double_cardinal x) (erefl (cardinal y))). Qed. Lemma csum2cr x y: x +c (cardinal y) = x +c y. Proof. exact: (csum2_pr2 (erefl (cardinal x)) (double_cardinal y)). Qed. Lemma cardinal_setC2 a b: sub a b -> cardinal b = a +c (b -s a). Proof. by rewrite - (csum2_pr5 (set_I2Cr b a)) setU2_C; move /setCU_K => ->. Qed. Lemma cardinal_setC3 a b: (a -s b) \Eq (b -s a) -> a \Eq b. Proof. move /card_eqP => h; apply /card_eqP. rewrite (cardinal_setC2 (@subsetI2l a b)) (cardinal_setC2 (@subsetI2r a b)). move: (set_CI2 a b a); rewrite setC_v set0_U2 => ->. move: (set_CI2 b a b); rewrite setC_v set0_U2 setI2_C => ->. by rewrite - csum2cr h csum2cr. Qed. Lemma cprod2_pr1 a b: a *c b = cardinal (a \times b). Proof. have h:= (product2_canon_fb a b). symmetry;apply/card_eqP. exists (product2_canon a b); split => //;rewrite/product2_canon; aw. Qed. Lemma cprod2_pr2 a b: cardinal (a \times cardinal b) = cardinal (a \times b). Proof. by move: (Eq_setX (EqR a) (cardinal_pr b)) => h; apply/card_eqP. Qed. Lemma cprod2cr x y: x *c (cardinal y) = x *c y. Proof. by rewrite !cprod2_pr1 cprod2_pr2. Qed. Lemma cprod2cl x y: (cardinal x) *c y = x *c y. Proof. by rewrite cprodC cprod2cr cprodC. Qed. Definition quasi_bij f I J := [/\ (forall x, inc x I -> inc (f x) J), (forall x y, inc x I -> inc y I -> f x = f y -> x = y) & (forall y, inc y J -> exists2 x, inc x I & y = f x)]. Lemma cardinal_commutativity_aux f I J g (F := (Lf f I J)) (G := Lg J g) : quasi_bij f I J -> [/\ target F = domain G, bijection F & G \cf (graph F) = Lg I (fun z => Vg G (f z))]. Proof. move=> [p1 p2 p3]. rewrite /F /G; aw; bw;split => //; first by apply: lf_bijective. rewrite /composef;aw; last by apply:lf_function. apply: fgraph_exten;bw; fprops. by move => t tI /=; bw; rewrite -/(Vf _ _); aw; apply: p1. Qed. Lemma csum_Cn2 J g I f : quasi_bij f I J -> csumb J g = csumb I (fun z => (g (f z))). Proof. move=> h; move:(cardinal_commutativity_aux g h) => [tF bF vF]. rewrite /csumb (csum_Cn tF bF) vF; apply:csumb_exten. by move => i iI /=; bw; apply: (proj31 h). Qed. Lemma cprod_Cn2 J g I f : quasi_bij f I J -> cprodb J g = cprodb I (fun z => (g (f z))). Proof. move=> h; move:(cardinal_commutativity_aux g h) => [tF bF vF]. rewrite /cprodb (cprod_Cn tF bF) vF; apply:cprodb_exten. by move => i iI /=; bw; apply: (proj31 h). Qed. Lemma sum_of_sums_aux I f g: (csumb I f) +c (csumb I g) = csumb I (fun i => (f i) +c (g i)) /\ (cprodb I f) *c (cprodb I g) = cprodb I (fun i => (f i) *c (g i)). Proof. set K := I \times C2. set K1 := I *s1 C0. set K2 := I *s1 C1. pose R i := indexedr i C2. set h := Lg I R. set k := fun p=> Yo (Q p = C0) (f (P p)) (g (P p)). set G:= variantLc K1 K2. have uK: K = K1 \cup K2 by rewrite /K/K1/K2 - distrib_union_prod2 setU2_11. have sk1: sub K1 K by move=> t; rewrite uK; fprops. have sk2: sub K2 K by move=> t; rewrite uK; fprops. have ue: K1 \cap K2 = emptyset. rewrite /K1 /K2 - distrib_inter_prod2. apply /set0_P => t /setX_P [_ _ /setI2_P [] /set1_P -> /set1_P]; fprops. have pfa: partition_w_fam G (domain (Lg K k)). by hnf;rewrite /G;split; fprops; [apply: disjointLv| bw; rewrite - union2Lv ]. have kp1: forall p, k (J p C0) = f p by move=> p; rewrite /k; aw; Ytac0. have kp2: forall p, k (J p C1) = g p by move=> p; rewrite /k; aw;Ytac0. have p1: forall x, inc x I -> sub (R x) K. move=> x xI t /setX_P [pt /set1_P pa pb]; apply: setX_i => //; ue. have pf1: partition_w_fam h (domain (Lg K k)). hnf; rewrite /h; split; fprops. apply: mutually_disjoint_prop2; move=> i j y _ _. by move /setX_P => [_ /set1_P <- _] /setX_P [_ /set1_P <- _]. bw; set_extens t. by move/setUf_P; bw; move => [y yI];bw; apply: p1. move => /setX_P [tp Pi Qt]; apply /setUb_P; bw; ex_tac; bw. apply /setX_i; fprops. have pa: (quasi_bij (fun p=> J p C0) I K1). rewrite /quasi_bij; bw;split => //. - move=> x xI; apply /setXp_i; fprops. - by move=> x y _ _ q; apply: (pr1_def q). - rewrite /K1; bw; move=> y /setX_P [py pI /set1_P <-]; ex_tac; aw. have pa': (quasi_bij (fun p=> J p C1) I K2). rewrite /quasi_bij; bw;split => //. - move=> x xI; apply /setXp_i; fprops. - by move=> x y _ _ q; apply: (pr1_def q). - rewrite /K2; bw; move=> y /setX_P [py pI /set1_P <-]; ex_tac; aw. rewrite /csumb/cprodb. have <-: Lg I (fun z => (Vg (Lg K k)) (J z C0)) = Lg I f. apply: Lg_exten => x xI; bw; apply: setXp_i; fprops. have <-: Lg I (fun z => (Vg (Lg K k)) (J z C1)) = Lg I g. apply: Lg_exten => x xI; bw; apply: setXp_i; fprops. rewrite -/(csumb _ _) - (csum_Cn2 (Vg (Lg K k)) pa). rewrite -/(csumb _ _) - (csum_Cn2 (Vg (Lg K k)) pa'). rewrite -/(cprodb _ _) - (cprod_Cn2 (Vg (Lg K k)) pa). rewrite -/(cprodb _ _) - (cprod_Cn2 (Vg (Lg K k)) pa'). move: (csum_An pfa) (cprod_An pfa); rewrite /csumb /cprodb. set f1 := Lg (domain _) _; set f2 := Lg (domain _) _. set X1 := (Lg K1 (Vg (Lg K k))). set X2 := (Lg K2 (Vg (Lg K k))). have ->: f1 = variantLc (csum X1) (csum X2). rewrite /f1 /variantLc /variantL /G; bw. symmetry;apply: Lg_exten => x /C2_P; case; move=> ->;bw. have ->: f2 = variantLc (cprod X1) (cprod X2). rewrite /f2 /variantLc /variantL /G; bw. symmetry;apply: Lg_exten => x /C2_P; case; move=> ->;bw. rewrite {1} /csum2; move => <-. rewrite {1} /cprod2; move => <-. clear pfa G f1 f2 X1 X2 pa pa'. have dh: domain h = I by rewrite /h; bw. rewrite (csum_An pf1) (cprod_An pf1) dh /csumb /cprodb. have dfI: forall x, inc x I -> doubleton_fam (Lg (R x) (Vg (Lg K k))) (f x) (g x). move => x xI. have p2: sub (R x) (domain (Lg K k)) by bw; apply: p1. have fK: inc (J x C0) K by apply: sk1; apply: setXp_i; fprops. have sK: inc (J x C1) K by apply: sk2; apply: setXp_i; fprops. have pa: inc (J x C0) (R x) by apply: setXp_i; fprops. have pb: inc (J x C1) (R x) by apply: setXp_i; fprops. exists (J x C0); exists (J x C1). have fgk: fgraph (Lg K k) by fprops. have xa: J x C0 <> J x C1 by move => H; move: (pr2_def H); fprops. have xb: domain (Lg (R x) (Vg (Lg K k))) = doubleton (J x C0) (J x C1). bw; set_extens t; last by case /set2_P => ->. move /setX_P => [qa /set1_P qb /C2_P]. case =>qc; rewrite -qa qb qc; fprops. split => //; fprops; bw; try apply: (p1 _ xI); rewrite kp1 kp2. split;apply: f_equal; apply: Lg_exten;move => x xI; rewrite /h; bw. by symmetry; apply: csum2_pr; apply: dfI. by symmetry; apply: cprod2_pr; apply: dfI. Qed. Lemma sum_of_sums f g I: (csumb I f) +c (csumb I g) = csumb I (fun i => (f i) +c (g i)). Proof. exact (proj1 (sum_of_sums_aux I f g)). Qed. Lemma prod_of_prods f g I: (cprodb I f) *c (cprodb I g) = cprodb I (fun i =>(f i) *c (g i)). Proof. exact (proj2 (sum_of_sums_aux I f g)). Qed. Lemma cprodA a b c: a *c (b *c c) = (a *c b) *c c. Proof. rewrite (cprodC (a*c b)) !cprod2_pr1 !cprod2_pr2. apply/card_eqP /(EqT (product2A a b c))/equipotent_product_sym. Qed. Lemma csumA a b c: a +c (b +c c) = (a +c b) +c c. Proof. move: a b c. have aux: (forall u v w a b c, v <> u-> u <> w -> w <> v -> a +c (b +c c) = cardinal ((a *s1 u) \cup ((b *s1 v) \cup (c *s1 w)))). move=> u v w a b c vu uw wv. rewrite - (card_card (CS_sum2 a (b +c c))); apply/card_eqP. apply: (EqT (disjointU2_pr3 a (b +c c) vu)). apply: equipotent_disjointU2; fprops. apply: disjoint_pr; move=> z; move/setX_P => [_ _ /set1_P pa] /setU2_P [] /setX_P [_ _ /set1_P]; rewrite pa => //; apply:nesym => //. exact:(EqT (EqS (Eq_indexed (b +c c) v)) (disjointU2_pr3 b c wv)). move: card1_nz => ne1 a b c. have ne2:=(nesym card_12). have ne3:=(nesym card2_nz). rewrite - (csumC c (a +c b)). rewrite(aux _ _ _ a b c ne1 ne3 ne2) (aux _ _ _ c a b ne3 ne2 ne1). by rewrite setU2_A setU2_C. Qed. Lemma csum_permute24: interchange csum2 csum2. Proof. move => s1 s2 r1 r2; rewrite (csumA _ s2 r2) (csumA _ r1 r2). by rewrite -(csumA s1) (csumC s2 r1) (csumA s1). Qed. Lemma cprodDl a b c: a *c (b +c c) = (a *c b) +c (a *c c). Proof. have aux: forall a b c, (a \times (b \times c)) \Eq ((a *c b) \times c). move=> a' b' c'. by apply/card_eqP; rewrite - 2!cprod2_pr1 - cprod2cr - cprod2_pr1 cprodA. rewrite cprod2_pr1. rewrite -(card_card(CS_sum2 (a *c b) (a *c c)));apply/card_eqP. apply: (@EqT (a \times ((b *s1 C0) \cup (c *s1 C1)))). apply: Eq_setX; fprops; apply: disjointU2_pr3 C1_ne_C0. rewrite distrib_union_prod2. apply: (@EqT (disjointU (variantLc (a *c b) (a *c c)))); last first. apply:EqS; rewrite disjointU2_rw1; apply: disjointU2_pr3 C1_ne_C0. rewrite disjointU2_rw1; apply: equipotent_disjointU2. - by apply: disjointU2_pr0; apply: disjointU2_pr; fprops. - by apply: disjointU2_pr; fprops. - by apply: aux. - by apply: aux. Qed. Lemma cprodDr a b c: (b +c c) *c a = (b *c a) +c (c *c a). Proof. rewrite cprodC (cprodC b a) (cprodC c a); apply: cprodDl. Qed. Lemma cprod2Dn a f: a *c (csum f) = csumb (domain f) (fun i => a *c (Vg f i)). Proof. rewrite cprod2_pr1 /csum cprod2_pr2; apply/card_eqP. rewrite/disjointU distrib_prod2_sum /disjointU_fam; bw. apply: equipotent_disjointU => //. - split => //; fprops; bw;move=> i idf; bw. by apply/card_eqP; rewrite - 2!cprod2_pr1 - cprod2cr - cprod2_pr1 cprodA. - apply: mutually_disjoint_prop2=> i j y idf jdf; bw. move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]]. by move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]]. - apply: mutually_disjoint_prop2=> i j y idf jdf; bw. by move => /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. Qed. (** ** EIII-3-4 Properties of the cardinals 0 and 1 *) Lemma csum_trivial f: domain f = emptyset -> csum f = \0c. Proof. move=> dge; rewrite/csum /disjointU /disjointU_fam dge /Lg funI_set0. by rewrite setUb_0 cardinal_set0. Qed. Lemma csum_trivial0 f: csumb emptyset f = \0c. Proof. apply:csum_trivial; bw. Qed. Lemma csum_trivial1 x f: domain f = singleton x -> csum f = cardinal (Vg f x). Proof. rewrite/csum /disjointU/disjointU_fam => ->. by rewrite /unionb Lg_domain setUf_1 (LVg_E _ (set1_1 x)) cardinal_indexed. Qed. Lemma csum_trivial2 x f: domain f = singleton x -> cardinalp (Vg f x) -> csum f = Vg f x. Proof. by move=> df cV; rewrite (csum_trivial1 df) (card_card cV). Qed. Lemma csum_trivial3 x f: csumb (singleton x) f = cardinal (f x). Proof. rewrite /csumb (csum_trivial1 (Lg_domain (singleton x) f)); bw; fprops. Qed. Lemma csum_trivial4 f a: csum (restr f (singleton a)) = cardinal (Vg f a). Proof. have <-: Vg (restr f (singleton a)) a = Vg f a by bw; fprops. apply: csum_trivial1; rewrite restr_d //. Qed. Lemma cprod_trivial f: domain f = emptyset -> cprod f = \1c. Proof. by move=> /domain_set0_P ->; rewrite/cprod setXb_0 cardinal_set1. Qed. Lemma cprod_trivial0 f: cprodb emptyset f = \1c. Proof. by apply:cprod_trivial; bw. Qed. Lemma cprod_trivial1 x f: domain f = singleton x -> cprod f = cardinal (Vg f x). Proof. move=> df; symmetry; apply /card_eqP. exists (product1_canon (Vg f x) x); split. - apply: setX1_canon_fb. - rewrite /product1_canon; aw. - by rewrite/ product1_canon; aw;apply: setX1_pr2. Qed. Lemma cprod_trivial2 x f: domain f = singleton x -> cardinalp (Vg f x) -> cprod f = Vg f x. Proof. by move=> df cV; rewrite (cprod_trivial1 df) (card_card cV). Qed. Lemma cprod_trivial3 x f: cprodb (singleton x) f = cardinal (f x). Proof. rewrite /cprodb (cprod_trivial1 (Lg_domain (singleton x) f)); bw; fprops. Qed. Lemma cprod_trivial4 f a: cprod (restr f (singleton a)) = cardinal (Vg f a). Proof. have <-: Vg (restr f (singleton a)) a = Vg f a by bw; fprops. apply: cprod_trivial1; rewrite restr_d //. Qed. Lemma csumA_setU2 A B f: disjoint A B -> csumb (A \cup B) f = csumb A f +c csumb B f. Proof. move => dab; rewrite /csumb. pose h := Lg (A \cup B) f. set g := variantLc A B. have pa: partition_w_fam g (domain h). rewrite /h /g; bw; hnf; rewrite union2Lv;split; fprops. move => i j; bw; case/C2_P => ->; case/C2_P => ->; bw; fprops. by right; apply: disjoint_S. have pb:= inc_C1_C2. have pc:=inc_C0_C2. rewrite (csum_An pa) /csumb; symmetry; apply: csum2_pr. rewrite /g;bw;exists C0, C1; bw; rewrite /h. split;fprops; apply: csumb_exten => t ts;bw; fprops. Qed. Lemma csumA_setU1 A b f: ~ (inc b A) -> csumb (A +s1 b) f = csumb A f +c (f b). Proof. move => pa. transitivity (csumb A f +c cardinal (f b)); last by apply:csum2_pr4; fprops. have pc: disjoint A (singleton b). by apply: disjoint_pr => t tA /set1_P tb; case:pa; rewrite - tb. by rewrite (csumA_setU2 _ pc) csum_trivial3. Qed. Lemma cprodA_setU2 A B f: disjoint A B -> cprodb (A \cup B) f = cprodb A f *c cprodb B f. Proof. move => dab; rewrite /cprodb. pose h := Lg (A \cup B) f. set g := variantLc A B. have pa: partition_w_fam g (domain h). rewrite /h /g; bw; hnf; rewrite union2Lv;split; fprops. move => i j; bw; case/C2_P => ->; case/C2_P => ->; bw; fprops. by right; apply: disjoint_S. have pb:= inc_C1_C2. have pc:=inc_C0_C2. rewrite (cprod_An pa)/cprodb; symmetry; apply: cprod2_pr. rewrite /g;bw;exists C0, C1; bw; rewrite /h. split;fprops; apply: cprodb_exten => t ts;bw; fprops. Qed. Lemma cprodA_setU1 A b f: ~ (inc b A) -> cprodb (A +s1 b) f = cprodb A f *c (f b). Proof. move => pa. have pc: disjoint A (singleton b). by apply: disjoint_pr => t tA /set1_P tb; case: pa; rewrite - tb. by rewrite - cprod2cr (cprodA_setU2 _ pc) - cprod_trivial3. Qed. Lemma card_partition_induced X f F: (forall x, inc x X -> inc (f x) F) -> cardinal X = csumb F (fun k => cardinal (Zo X (fun z => f z = k))). Proof. move => fim. pose g k := Zo X (fun z => f z = k). have pa:= (@disjointU_disjoint (Lg F g)). move: (csum_pr (Lg F g)). have <- : csumb (domain (Lg F g)) (fun a => cardinal (Vg (Lg F g) a)) = csumb F (fun k => cardinal (Zo X (fun z => f z = k))). bw; apply: csumb_exten => i ie; rewrite /g; bw. move <-;apply /card_eqP. rewrite /disjointU /disjointU_fam /g; bw. set S := unionb _. pose h x := J x (f x). exists (Lf h X S); hnf; aw;split => //; apply lf_bijective. move => x xX; move: (fim _ xX) => ok. by apply /setUb_P; bw; ex_tac; bw; apply: indexed_pi; apply /Zo_P. move => u v _ _ sv; exact: (pr1_def sv). move => y /setUb_P; bw; move => [z zf]; bw. move =>/indexed_P [px /Zo_P [pc pd] pe];ex_tac. by rewrite -{1} px /h pd pe. Qed. Lemma card_partition_induced1 X f F g: (forall x, inc x X -> inc (f x) F) -> csumb X g = csumb F (fun i => csumb (Zo X (fun z => f z = i)) g). Proof. move => fim. pose h i := (Zo X (fun z => f z = i)). have pa: (partition_w_fam (Lg F h) (domain (Lg X g))). bw; split; first by fprops. rewrite /h; hnf; bw => i j iF jF; bw; mdi_tac eq1 => u /Zo_hi fu. by move /Zo_hi => fv; case: eq1; rewrite -fu fv. rewrite /h;set_extens t. by move /setUb_P; bw; move => [y yf]; bw; move => /Zo_P []. move => tx; apply /setUb_P; bw; move: (fim _ tx) => ft; ex_tac; bw. by apply /Zo_P. rewrite {1} /csumb (csum_An pa); bw. apply:csumb_exten => i iF; rewrite /h; bw. apply:csumb_exten => z zi; bw; apply: Zo_S zi. Qed. Theorem csum_zero_unit f j: sub j (domain f) -> (forall i, inc i ((domain f) -s j) -> (Vg f i) = \0c) -> csum f = csumb j (Vg f). Proof. move=> jdf acz; congr cardinal. rewrite /disjointU/disjointU_fam; bw. set_extens x; move /setUb_P; bw; move => [y yd]; bw => h; apply/setUb_P; bw. case: (inc_or_not y j)=> yj; first by ex_tac; bw. have yc: (inc y ((domain f) -s j)) by apply /setC_P. move: h; rewrite (acz _ yc)=> /setX_P [_ /in_set0 [] _]. by exists y; bw; apply: jdf. Qed. Theorem cprod_one_unit f j: sub j (domain f) -> (forall i, inc i ((domain f) -s j) -> (Vg f i) = \1c) -> cprod f = cprodb j (Vg f). Proof. move=> jdf alo; apply /card_eqP; exists (pr_j f j); split. - by apply: prj_fb=>// i ici; rewrite (alo _ ici); exists emptyset. - by rewrite /pr_j; aw. - by rewrite /pr_j; aw. Qed. Lemma csum_zero_unit_bis f: (allf f (fun z => z = \0c)) -> csum f = \0c. Proof. move => ha. have hc:(forall i, inc i (domain f -s emptyset) -> Vg f i = \0c). by move => i /setC_P [/ha ]. by rewrite (csum_zero_unit (sub0_set _) hc) csum_trivial0. Qed. Lemma csum0l a: cardinalp a -> \0c +c a = a. Proof. by move=> ca; rewrite - (csum2_pr5 (set0_I2 a)) set0_U2 (card_card ca). Qed. Lemma csum0r a: cardinalp a -> a +c \0c = a. Proof. by move => ca;rewrite csumC csum0l. Qed. Lemma cprod1r a: cardinalp a -> a *c \1c = a. Proof. by move=> ca; rewrite cprod2_pr1 cardinal_indexed (card_card ca). Qed. Lemma cprod1l a: cardinalp a -> \1c *c a = a. Proof. by move=> ca; rewrite cprodC cprod1r. Qed. Hint Rewrite csum0r cprod1r csum0l cprod1l: aw. Lemma cprod0r a: a *c \0c = \0c. Proof. rewrite cprod2_pr1; bw; apply: cardinal_set0. Qed. Lemma cprod0l a: \0c *c a = \0c. Proof. by rewrite cprodC cprod0r. Qed. Lemma cprod_eq0 f: (exists2 i, inc i (domain f) & cardinal (Vg f i) = \0c) -> cprod f = \0c. Proof. move=> [i idf cVz]; rewrite /cprod. case: (emptyset_dichot (productb f)); first by move => ->; apply: cardinal_set0. by move /setXb_ne2 => h; move: (h i idf)=> /card_nonempty1. Qed. Lemma csum_of_ones b: csum (cst_graph b \1c) = cardinal b. Proof. rewrite/csum /disjointU/disjointU_fam; bw. set f:= Lg _ _. have fv: (f= Lg b (fun i=> \1c *s1 i)). rewrite /f/cst_graph; apply: Lg_exten => x xj /=; bw. suff: (unionb f = \1c \times b). by move ->; symmetry;apply/card_eqP/Eq_rindexed. rewrite fv;set_extens t. - move=> /setUb_P; bw ; move => [y yj]; bw. move => /setX_P [pa pb /set1_P pc]; apply /setX_P;split => //; ue. - move /setX_P => [pa pb pc]; apply/setUb_P; bw; ex_tac; bw. apply:setX_i;fprops. Qed. Lemma csum_of_ones1 b j: cardinalp b -> b \Eq j -> csum (cst_graph j \1c) = b. Proof. move=> cb bj; rewrite csum_of_ones - (card_card cb). by symmetry; apply/card_eqP. Qed. Lemma csum_of_same a b: csum (cst_graph b a) = a *c b. Proof. rewrite - cprod2cr - cprod2cl - (csum_of_ones b) cprod2Dn; bw. apply: csum_pr3; bw => i ib; bw; rewrite cprod1r ?double_cardinal //. fprops. Qed. Lemma csum_of_same1 a b j: cardinalp a -> cardinalp b -> b \Eq j -> csum (cst_graph j a) = a *c b. Proof. move=> ca cb /card_eqP h. by rewrite csum_of_same - cprod2cr - h cprod2cr. Qed. Lemma csucc_pr3 x: csucc (cardinal x) = x +c \1c. Proof. have p: disjoint (cardinal x) (singleton (cardinal x)). apply /set0_P => y /setI2_P [pa] /set1_P => pb. by case: (cardinal_irreflexive (CS_cardinal x)); rewrite -{1} pb. by rewrite /csucc (csum2_pr5 p) - csum2cr csum2cl cardinal_set1. Qed. Lemma csucc_pr4 x: cardinalp x -> csucc x = x +c \1c. Proof. by rewrite - csucc_pr3;move /card_card => ->. Qed. Lemma csucc_pr5 a: cardinal (csucc a) = csucc a. Proof. apply: (card_card (CS_succ a)). Qed. Lemma card_two_pr: \1c +c \1c = \2c. Proof. by rewrite - (csucc_pr4 CS1) succ_one. Qed. Lemma two_times_n n: \2c *c n = n +c n. Proof. rewrite - csum2cl - csum2cr - cprod2cr - card_two_pr cprodDr. by rewrite (cprod1l (CS_cardinal n)). Qed. Definition card_nz_fam f := allf f (fun z => z <> \0c). Theorem cprod_nzP f: card_nz_fam f <-> (cprod f <> \0c). Proof. split => h. have alne: (forall i, inc i (domain f) -> nonempty (Vg f i)). move=> i /h vz;case: (emptyset_dichot (Vg f i))=> // p. move: (setXb_ne alne); apply: card_nonempty1. move=> i idf /=; dneg vz; apply: cprod_eq0=>//; ex_tac. by rewrite vz; apply: cardinal_set0. Qed. Lemma cprod2_nz a b: a <> \0c -> b <> \0c -> a *c b <> \0c. Proof. move=> az bz; apply /cprod_nzP; hnf; bw => i itp;try_lvariant itp. Qed. Lemma cprod2_eq0 a b: a *c b = \0c -> a = \0c \/ b = \0c. Proof. move =>h. case: (equal_or_not a \0c) => az; first by left. case: (equal_or_not b \0c) => bz; first by right. by case: (cprod2_nz az bz). Qed. Theorem succ_injective a b: cardinalp a -> cardinalp b -> a +c \1c = b +c \1c -> a = b. Proof. move=> ca cb. rewrite - (csucc_pr4 ca)- (csucc_pr4 cb). by apply: succ_injective1. Qed. (** ** EIII-3-5 Exponentiation of cardinals *) Definition cpow a b := cardinal (functions b a). Notation "x ^c y" := (cpow x y) (at level 30). Lemma CS_pow a b: cardinalp (a ^c b). Proof. apply:CS_cardinal. Qed. Hint Resolve CS_pow: fprops. Lemma cpow_pr a b a' b': a \Eq a' -> b \Eq b' -> a ^c b = a' ^c b'. Proof. move=> [f [bf sf tf]] ebb'; apply /card_eqP. have [g [bg sg tg]] := (EqS ebb'). exists (compose3function g f); hnf. rewrite {2 3} /compose3function - sf -tf - sg -tg; aw. by split => //;apply: c3f_fb. Qed. Lemma cpowcl a b: (cardinal a) ^c b = a ^c b. Proof. apply: cpow_pr;fprops. Qed. Lemma cpowcr a b: a ^c (cardinal b) = a ^c b. Proof. apply: cpow_pr; fprops. Qed. Theorem cpow_pr1 x y: cardinal (functions y x) = (cardinal x) ^c (cardinal y). Proof. apply: cpow_pr; fprops. Qed. Lemma cpow_pr2 a b: cprod (cst_graph b a) = a ^c b. Proof. symmetry;apply/card_eqP. rewrite (setXb_eq_gfunctions (f:= (cst_graph b a)) (x:=a));bw. apply: Eq_fun_set. move=> i isc;bw. Qed. Theorem cpow_pr3 a b j: cardinal j = b -> cprod (cst_graph j a) = a ^c b. Proof. by move=> <-; rewrite cpow_pr2 cpowcr. Qed. Lemma cpow_sum a f: a ^c (csum f) = cprodb (domain f) (fun i => a ^c (Vg f i)). Proof. transitivity (a ^c (disjointU (Lg (domain f) (Vg f)))). apply: cpow_pr; [fprops | rewrite - (csum_gr); apply: cardinal_pr ]. rewrite -cpow_pr2 /disjointU. set S:= disjointU_fam _; set f0:= cst_graph _ _. have pfa:partition_w_fam S (domain f0). move: (partition_disjointU (Lg (domain f) (Vg f))); rewrite /f0; bw. rewrite (cprod_An pfa) /S /disjointU_fam ! Lg_domain;apply cprodb_exten. move=> x xdf /=; bw; rewrite /cprodb. have ->: (Lg (Vg f x *s1 x) (Vg f0)) = (Lg (Vg f x *s1 x) (fun _ => a)). rewrite /f0;apply: Lg_exten => t tw; bw. apply /setUb_P; rewrite /S /disjointU_fam;bw; ex_tac; bw. by rewrite cpow_pr2 - cpowcr cardinal_indexed cpowcr. Qed. Lemma cpow_prod b f: (cprod f) ^c b = cprodb (domain f) (fun i => (Vg f i) ^c b). Proof. rewrite - cpow_pr2. set (g:= Lg (product (domain f) b)(fun z=> Vg f (P z))). set (h0:= Lg (domain f) (fun i => product (singleton i) b)). have fph0: partition_w_fam h0 (domain g). hnf; rewrite /h0; split; fprops. apply: mutually_disjoint_prop2; move=> i j y _ _. by move => /setX_P [_ /set1_P <- _] /setX_P [_ /set1_P <- _]. set_extens t. move => /setUb_P; bw; move => [y yd]; rewrite /g; bw. move /setX_P => [pa /set1_P pb pc]; apply:setX_i => //; ue. rewrite /g; bw => /setX_P [pa pb pc]; apply /setUb_P; bw; ex_tac. bw; apply /setX_P; split;fprops. rewrite /cprodb. have <-: (Lg (domain f) (fun l => cprodb (Vg h0 l) (Vg g))= Lg (domain f) (fun i => (Vg f i) ^c b)). apply: Lg_exten. move=> x xsf; rewrite /h0; bw; rewrite /cprodb. set (T:= indexedr x b). have ->: (Lg (singleton x \times b) (Vg g)) = cst_graph T (Vg f x). rewrite /g; apply: fgraph_exten; fprops; bw => t ts. move /setX_P: (ts) => [pa /set1_P pb pc]; bw; first by ue. by apply /setX_P;split => //; rewrite pb. rewrite cpow_pr2; apply: (cpow_pr (EqR _)); apply:EqS; apply: Eq_rindexed. have dh0: domain h0 = domain f by rewrite /h0; bw. move: (cprod_An fph0). rewrite dh0 /cprodb => <-; clear dh0. pose h:= Lg b (fun i => (domain f) *s1 i). have pfa: (partition_w_fam h (domain g)). rewrite/ h;split; fprops. apply: mutually_disjoint_prop2; move=> i j y _ _. by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-]. set_extens t; rewrite /g; bw. move => /setUb_P; bw; move => [y yd]; bw; move /setX_P => [pa pb]. move /set1_P => pc; apply: setX_i;fprops; ue. move => /setX_P [pa pb pc]; apply /setUb_P; bw; ex_tac; bw. apply:setX_i; fprops. rewrite (cprod_An pfa). have ->: (domain h = b) by rewrite /h; bw. symmetry; apply: cprodb_exten =>// x xb; rewrite /cprodb. have ->: (Lg (Vg h x) (Vg g)) = Lg ((domain f) *s1 x) (fun z => Vg f(P z)). rewrite /h; bw; apply: Lg_exten => t ts; rewrite /g; bw. move /setX_P: ts => [pa pb /set1_P pc]; apply /setX_P;split => //; ue. set (ff:=Lf (fun u=> J u x) (domain f) ( (domain f) *s1 x)). set (X :=Lg (product (domain f) (singleton x)) (fun z => Vg f (P z))). have fgX: fgraph X by rewrite /X; fprops. have tff: target ff = domain X by rewrite / ff/X; aw; bw. have bff: (bijection ff). rewrite /ff/indexed; apply: lf_bijective. - by move=> t xa /=; aw; fprops. - by move=> u v _ _; apply: pr1_def. - by move=> y /setX_P [py Pya /set1_P <-]; ex_tac; aw. rewrite (cprod_Cn tff bff) -(cprod_gr f). have -> //: (X \cf (graph ff) = Lg (domain f) (Vg f)). have fff:=(bij_function bff). rewrite /composef /ff; aw; bw. apply: fgraph_exten; fprops; bw. have lfa: lf_axiom (J^~ x) (domain f) (domain f *s1 x). by move=> z; aw=> zf; apply: setXp_i; fprops. move => t tf /=; bw; rewrite -/(Vf ff t) (lf_V lfa tf) /X; bw;aw; fprops. Qed. Lemma cpow_sum2 a b c: a ^c (b +c c) = (a ^c b) *c (a ^c c). Proof. rewrite /csum2 cpow_sum; symmetry; apply: cprod2_pr; bw. move: (doubleton_fam_canon (fun i => cpow a (Vg (variantLc b c) i))). bw. Qed. Lemma cpow_prod2 a b c: (a *c b) ^c c = (a ^c c) *c (b ^c c). Proof. rewrite {2} /cprod2 cpow_prod; bw; symmetry; apply: cprod2_pr. move: (doubleton_fam_canon (fun i => cpow (Vg (variantLc a b) i) c)). bw. Qed. Lemma cpow_pow a b c: a ^c (b *c c) = (a ^c b) ^c c. Proof. rewrite -csum_of_same cpow_sum -cpow_pr2; bw. apply:cprodb_exten => x xc; bw. Qed. Lemma cpowx0 a: a ^c \0c = \1c. Proof. by rewrite /cpow functions_empty cardinal_set1. Qed. Lemma cpow00: \0c ^c \0c = \1c. Proof. apply: cpowx0. Qed. Lemma cpowx1c a: a ^c \1c = cardinal a. Proof. have h: inc \0c \1c by apply:set1_1. rewrite -cpowcl - cpow_pr2 (cprod_trivial2 (x := \0c)); bw;fprops. Qed. Lemma cpowx1 a: cardinalp a -> a ^c \1c = a. Proof. by move=> /card_card ac; rewrite cpowx1c. Qed. Lemma cpow1x a: \1c ^c a = \1c. Proof. move: fgraph_set0 domain_set0 => eg de. by rewrite - (cprod_trivial de) cpow_prod // de /cprodb /Lg funI_set0. Qed. Lemma cpow0x a: a <> \0c -> \0c ^c a = \0c. Proof. move=>naz;rewrite/cpow. suff: (functions a \0c = emptyset) by move => ->; apply: cardinal_set0. apply /set0_P => y /functionsP [fy sy tg]. case: naz; case: (emptyset_dichot a) => // [][x]. by rewrite - sy => /(Vf_target fy); rewrite tg => /in_set0. Qed. Lemma cpowx2 a: a ^c \2c = a *c a. Proof. by rewrite -card_two_pr cpow_sum2 cpowx1c cprod2cl cprod2cr. Qed. Definition char_fun A B := Lf (varianti A \1c \0c) B (doubleton \1c \0c). Lemma char_fun_axioms A B: lf_axiom (varianti A \1c \0c) B (doubleton \1c \0c). Proof. move=> z zB; rewrite /varianti;Ytac zA; fprops. Qed. Lemma char_fun_f A B: function (char_fun A B). Proof. rewrite/char_fun; apply: lf_function; apply: char_fun_axioms. Qed. Lemma char_fun_V A B x : inc x B -> Vf (char_fun A B) x = (varianti A \1c \0c x). Proof. move=> xB; rewrite /char_fun; aw; apply: char_fun_axioms. Qed. Lemma char_fun_V_cardinal A B x: inc x B -> cardinalp (Vf (char_fun A B) x). Proof. move => h; rewrite (char_fun_V A h) /varianti; Ytac h'; fprops. Qed. Lemma char_fun_V_a A B x: sub A B -> inc x A -> Vf (char_fun A B) x = \1c. Proof. move=> AB xA; rewrite (char_fun_V A (AB _ xA)). by apply: varianti_in. Qed. Lemma char_fun_V_b A B x: sub A B -> inc x (B -s A) -> Vf (char_fun A B) x = \0c. Proof. move=> AB /setC_P [xB nxA]; rewrite (char_fun_V _ xB). by apply: varianti_out. Qed. Lemma char_fun_injectiveP A A' B: sub A B -> sub A' B -> ((A=A') <-> (char_fun A B = char_fun A' B)). Proof. move=> AB A'B; split => scf; first by rewrite scf. set_extens x => xs; ex_middle u. have xc:= (char_fun_V_b A'B (setC_i (AB _ xs) u)). by case: card1_nz; rewrite -(char_fun_V_a AB xs) scf. have xc:= (char_fun_V_b AB (setC_i (A'B _ xs) u)). by case: card1_nz; rewrite -(char_fun_V_a A'B xs) - scf. Qed. Lemma char_fun_surjective X f: function f -> source f = X -> target f = (doubleton \1c \0c) -> exists2 A, sub A X & char_fun A X = f. Proof. move => fy <- ty. set W := Zo (source f) (fun z => Vf f z = \1c). have WX: sub W (source f) by apply: Zo_S. exists W => //. symmetry;rewrite/char_fun;apply: function_exten => //; aw. apply: char_fun_f. move => s sX /=; case: (inc_or_not s W) => ws. rewrite (char_fun_V_a WX ws); exact: (Zo_hi ws). rewrite (char_fun_V_b WX (setC_i sX ws)). move: (Vf_target fy sX); rewrite ty. by case /set2_P => // f1; case: ws; apply/Zo_P. Qed. Theorem card_setP X: cardinal (powerset X) = \2c ^c X. Proof. rewrite - (cardinal_set2 C1_ne_C0) cpowcl /cpow. set K:= functions X _. apply/card_eqP; exists (Lf (char_fun ^~ X) (powerset X) K); hnf;aw;split => //. apply:lf_bijective. - move => y /setP_P yX; apply /functionsP;split => //; rewrite /char_fun; aw. by apply:char_fun_f. - by move => u v /setP_P uX /setP_P vX /(char_fun_injectiveP uX vX). - move => y /functionsP [fy sy ty]. move: (char_fun_surjective fy sy ty)=> [A pa pb]; exists A => //. by apply /setP_P. Qed. (** ** EIII-3-6 Order relation and operations on cardinals *) Definition cdiff a b := cardinal (a -s b). Notation "x -c y" := (cdiff x y) (at level 50). Lemma CS_diff a b: cardinalp (a -c b). Proof. apply CS_cardinal. Qed. Lemma cardinal_setC A E: sub A E -> (cardinal A) +c (E -c A) = cardinal E. Proof. by move=> AE; rewrite /cdiff csum2cl csum2cr - cardinal_setC2. Qed. Lemma cdiff_pr a b: b <=c a -> b +c (a -c b) = a. move=> [cb ca sab]. by rewrite -{1} (card_card cb) cardinal_setC // (card_card ca). Qed. Theorem cardinal_le_setCP a b: cardinalp a -> cardinalp b -> ((b <=c a) <-> (exists2 c, cardinalp c & b +c c = a)). Proof. move=> ca cb; split. by exists (cardinal (a -s b)); fprops;apply: cdiff_pr. move=> [c cc pbc];move: (disjointU2_pr3 b c C0_ne_C1); rewrite pbc. set b1 := b *s1 _; set d := _ \cup _ => aux. apply /cardinal_le_aux2P => //. have bb1: equipotent b1 b by apply/Eq_indexed2. have h1: equipotent_to_subset b1 d by exists b1; fprops; apply: subsetU2l. apply: (eq_subset_pr2 bb1 (EqS aux) h1). Qed. Theorem csum_increasing f g: domain f = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x)) -> (csum f) <=c (csum g). Proof. move=> dfdg ale; apply: sub_smaller => t. rewrite /disjointU /disjointU_fam. move /setUb_P; bw; move => [y ydf]; bw. move /setX_P => [pt Pt /set1_P Qt]; apply/setUb_P; bw; rewrite -dfdg. ex_tac; bw; rewrite -{2} Qt;apply :setX_i; fprops. by move: (ale _ ydf) => [_ _];apply. Qed. Theorem cprod_increasing f g: domain f = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x)) -> (cprod f) <=c (cprod g). Proof. move=> dfdg alle. by apply: sub_smaller; apply: setXb_monotone1 =>// i /alle [_ _]. Qed. Lemma csum_increasing1 f j: cardinal_fam f -> sub j (domain f) -> (csum (restr f j)) <=c (csum f). Proof. move=> alc sjd. apply: sub_smaller => t. rewrite /disjointU /disjointU_fam. move /setUb_P; bw; move=> [y yd]; bw => /setX_P [pa pb /set1_P pc]. apply /setUb_P; bw; move: (sjd _ yd) => yf; ex_tac; bw. apply /setX_P;split => //; rewrite pc; fprops. Qed. Lemma cprod_increasing1 f j: cardinal_fam f -> card_nz_fam f -> sub j (domain f) -> (cprod (restr f j)) <=c (cprod f). Proof. move=> alc alne sjd. set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) \1c)). have fgg: fgraph g by rewrite /g; fprops. have dgdf : domain g = domain f by rewrite /g; bw. have cs: (cprod g = cprodb j (Vg g)). apply: cprod_one_unit=>//; rewrite dgdf //. by move=> i /setC_P [idf nij]; rewrite /g; bw; rewrite Y_false. have drf: domain (restr f j) = j by bw. have ->: (restr f j = Lg j (Vg g)). apply: fgraph_exten; fprops; rewrite! drf; bw=>//. move=> x xj; move: (sjd _ xj) => xdf. by bw; rewrite /g; bw; Ytac0. rewrite -/(cprodb _ _) - cs; apply: cprod_increasing=> //. move=> x xdg; rewrite /g; bw; try ue. Ytac h; fprops; apply: cge1; [ apply: alc;ue | apply: alne; ue]. Qed. Lemma csum_increasing6 f j: cardinal_fam f -> inc j (domain f) -> (Vg f j) <=c (csum f). Proof. move=> cf jd. move: (csum_increasing1 cf (set1_sub jd)). by rewrite csum_trivial4 (card_card (cf _ jd)). Qed. Lemma cprod_increasing6 f j: cardinal_fam f -> card_nz_fam f -> inc j (domain f) -> (Vg f j) <=c (cprod f). Proof. move=> cf alnz jd. move: (cprod_increasing1 cf alnz (set1_sub jd)). by rewrite cprod_trivial4 (card_card (cf _ jd)). Qed. Lemma csum_Mlele a b a' b': a <=c a' -> b <=c b' -> (a +c b) <=c (a' +c b'). Proof. move=> aa' bb'; apply: csum_increasing; fprops; bw => x xtp; try_lvariant xtp. Qed. Lemma csum_Meqle a b b': b <=c b' -> (a +c b) <=c (a +c b'). Proof. move => h; rewrite -(csum2cl a b) -(csum2cl a b'). apply:csum_Mlele; fprops. Qed. Lemma csum_Mleeq a b b': b <=c b' -> (b +c a) <=c (b' +c a). Proof. by move => h; rewrite (csumC _ a)(csumC _ a); apply: csum_Meqle. Qed. Lemma cprod_Mlele a b a' b': a <=c a' -> b <=c b' -> (a *c b) <=c (a' *c b'). Proof. move=> aa' bb';apply: cprod_increasing;fprops; bw => x xtp; try_lvariant xtp. Qed. Lemma cprod_Meqle a b b': b <=c b' -> (a *c b) <=c (a *c b'). Proof. move => h; rewrite -(cprod2cl a b) -(cprod2cl a b'). apply:cprod_Mlele;fprops. Qed. Lemma cprod_Mleeq a b b': b <=c b' -> (b *c a) <=c (b' *c a). Proof. by move => h; rewrite (cprodC _ a)(cprodC _ a); apply: cprod_Meqle. Qed. Lemma csum_M0le a b: cardinalp a -> a <=c (a +c b). Proof. move=> ca. rewrite -{1}(csum0r ca) - (csum2cr a b). apply: csum_Meqle; fprops;apply: czero_least. Qed. Lemma csum2_pr6 a b: cardinal (a \cup b) <=c a +c b. Proof. rewrite - (setU2Cr2 a b) (csum2_pr5 (set_I2Cr b a)) - (csum2cr a b). rewrite - (csum2cr a); apply: csum_Meqle; apply: sub_smaller; apply: sub_setC. Qed. Lemma cprod_M1le a b: cardinalp a -> b <> \0c -> a <=c (a *c b). Proof. move=> ca nbz. rewrite -{1}(cprod1r ca) - (cprod2cr a b). apply: cprod_Mlele; fprops; apply: cge1; fprops. by apply: card_nonempty0. Qed. Lemma csum_eq1 a b: cardinalp a -> cardinalp b -> a +c b = \1c -> (a = \0c \/ b = \0c). Proof. move => ca cb eq. case: (equal_or_not a \0c) => anz; first by left. case: (equal_or_not b \0c) => bnz; first by right. move:(csum_Mlele (cge1 ca anz) (cge1 cb bnz)). by rewrite card_two_pr eq => /(cltNge clt_12). Qed. Lemma cprod_eq1 a b: cardinalp a -> cardinalp b -> a *c b = \1c -> (a = \1c /\ b = \1c). Proof. move => ca cb eq. case: (equal_or_not a \0c) => az. by move: eq; rewrite az cprod0l => bad; case: card1_nz. case: (equal_or_not b \0c) => bz. by move: eq; rewrite bz cprod0r => bad; case: card1_nz. case: (equal_or_not a \1c) => px1; first by rewrite - {2} eq px1 (cprod1l cb). move: (cprod_Mlele (cge2 ca az px1) (cge1 cb bz)). by rewrite (cprod1r CS2) eq => /(cltNge clt_12). Qed. Lemma cpow_Mleeq x y z: x <=c y -> x <> \0c -> x ^c z <=c y ^c z. Proof. move=> xy xz. rewrite - cpow_pr2 - cpow_pr2; apply: cprod_increasing; fprops;bw. move => t tx; bw. Qed. Lemma cpow_Meqle x a b: x <> \0c -> a <=c b -> x ^c a <=c x ^c b. Proof. move => /card_nonempty0 xnz leab. move: (cardinal_le_aux1 leab) => [t tb ebt]. have ->: (x ^c a = x ^c t) by apply: cpow_pr; fprops. rewrite - cpowcl -(cpowcl x b) - 2! cpow_pr2 / cst_graph. rewrite - (restr_Lg (fun _ => (cardinal x)) tb). apply: cprod_increasing1;hnf; bw => z zx; bw; fprops. Qed. Lemma cpow_Mlele a b a' b': a <> \0c -> a <=c a' -> b <=c b' -> (a ^c b) <=c (a' ^c b'). Proof. move=> nz aa' bb'; apply: (cleT (cpow_Mleeq b aa' nz)). by apply:cpow_Meqle bb'; dneg az; apply:cle0; rewrite -az. Qed. Lemma cpow_M2le x y: x <=c y -> \2c ^c x <=c \2c ^c y. Proof. move=> h; apply: cpow_Meqle; fprops. Qed. Lemma cpow_Mle1 a b: cardinalp a -> b <> \0c -> a <=c (a ^c b). Proof. move=> ca l1b. case: (equal_or_not a \0c). move => ->; apply: czero_least; fprops. move=> anz;rewrite - cpowcr - {1} (cpowx1 ca); apply:(cpow_Meqle anz). by apply:(cge1 (CS_cardinal b)); apply: card_nonempty0. Qed. Theorem cantor a: cardinalp a -> a ca; rewrite - card_setP. rewrite - {1} (card_card ca). split. apply /eq_subset_cardP1 /eq_subset_ex_injP. exists (Lf singleton a (powerset a)); hnf; aw; split => //. apply: lf_injective. by move=> t ta /=; apply/setP_P => v /set1_P ->. by move=> u v ua va; apply: set1_inj. apply/ card_eqP; move => [f [[_ suf] sf tf]]. set (X:= Zo a (fun x => (~ inc x (Vf f x)))). have Xt: (inc X (target f)) by rewrite tf; apply /setP_P; apply: Zo_S. move: ((proj2 suf) _ Xt) => [y ysf Wy]. have:(~ (inc y X)) by move=> yX; move: (yX) => /Zo_hi;rewrite Wy. move=> h;case: (h); apply: Zo_i; ue. Qed. Lemma infinite_powerset x: infinite_c x -> infinite_c (\2c ^c x). Proof. move => oo; exact (ge_infinite_infinite oo (proj1 (cantor (proj1 oo)))). Qed. Lemma cantor_bis: non_coll cardinalp. Proof. move=> [a ap]. have ca: cardinal_set a by move => t /ap. case: (cltNge (cantor (CS_sup ca))); apply: (card_sup_ub ca); apply/ap; fprops. Qed. Definition cnext c := Zo (\2c ^c c) (fun z => cardinal z <=c c). Lemma cnextP c: cardinalp c -> forall x, (inc x (cnext c) <-> (ordinalp x /\ cardinal x <=c c)). Proof. move => cc x. move:(cantor cc) => ncc; move: (ncc) => [[_ cc1 _] _]; move: (cc1) => [oc _]. split; first by move /Zo_P =>[/(ordinal_hi oc) h1 h2]. move => [h1 h2];apply: Zo_i => //. move: (cle_ltT h2 ncc) => h3. by move /(ocle2P cc1 h1): h3 => /oltP0 []. Qed. Lemma cnext_pr1 c (a:= cnext c): cardinalp c -> [/\ cardinalp a, c a <=c c']. Proof. move => cc. have H:= (cnextP cc). have ose: ordinal_set a by move => t /H [pa pb]. have oe: ordinalp a. apply: ordinal_pr => // t /H [pa pb] s st. apply/H; split; first by exact: (ordinal_hi pa st). exact:(cleT (sub_smaller (ordinal_transitive pa st)) pb). case: (cleT_el (CS_cardinal a) cc) => pa. by case /H: (ordinal_irreflexive oe). have pb: forall c', c sub a c'. move => c' cc'; move:(proj32_1 cc') => h2 t /H [sa sb]. by move /(ocle2P h2 sa): (cle_ltT sb cc') => /olt_i. have cp: cardinalp a. split => // z oz /card_eqP hh; rewrite hh in pa. move: (card_ord_le oz) => [_ _ s3]; exact: (sub_trans (pb _ pa) s3). rewrite -{2} (card_card cp); split => //. by move => c' cc'; split => //; [ exact:proj32_1 cc' | apply: pb]. Qed. Lemma CS_cnext x: cardinalp x -> cardinalp (cnext x). Proof. by move/cnext_pr1 /proj31. Qed. Lemma cnext_pr4 x y: cardinalp y -> x x <=c y. Proof. move => pa pb. case: (cleT_el (proj31_1 pb) pa) => // h. case: (cltNge pb (proj33 (cnext_pr1 pa) _ h)). Qed. Lemma cnext_pr2 x: cardinalp x -> x ic; exact (proj32 (cnext_pr1 ic)). Qed. Lemma cnext_pr3 x: cardinalp x -> cnext x <=c \2c ^c x. Proof. by move=> ic; move: (cnext_pr1 ic) => [pa pb]; apply; apply: cantor. Qed. Lemma cnext_pr5P x : cardinalp x -> forall y, (x cnext x <=c y). Proof. move => cx; split => h. by apply: (proj33 (cnext_pr1 cx)). exact:(clt_leT (cnext_pr2 cx) h). Qed. Lemma cnext_pr4P y: cardinalp y -> forall x, (x x <=c y). Proof. move => cy x; split; first by apply: cnext_pr4. move => sb; exact:(cle_ltT sb (cnext_pr2 cy)). Qed. Lemma cnext_pr6 x y: x <=c y -> cnext x <=c cnext y. Proof. move => xy. move: (xy) => [cx cy _]. by apply/cnext_pr5P => //; apply/cnext_pr4P. Qed. End CardinalOps. Export CardinalOps. Module FiniteSets. (** ** EIII-4-1 Definition of integers *) Definition Nat := omega0. Definition natp x := inc x Nat. Theorem finite_succP x: cardinalp x -> (finite_c (csucc x) <-> finite_c x). Proof. case /finite_dichot. move => h; rewrite (succ_of_finite h); exact: finite_oP. by move /csucc_inf => ->. Qed. Lemma infinite_Nat: infinite_set Nat. Proof. hnf; rewrite (card_card CS_omega); exact OIS_omega. Qed. Lemma NatP a: natp a <-> finite_c a. Proof. exact: omega_P2. Qed. Lemma Nat_i a: finite_c a -> natp a. Proof. by move /NatP. Qed. Lemma Nat_hi a: natp a -> finite_c a. Proof. by move /NatP. Qed. Hint Resolve Nat_i Nat_hi: fprops. Lemma CS_nat x: natp x -> cardinalp x. Proof. fprops. Qed. Lemma card_nat n: natp n -> cardinal n = n. Proof. by move/CS_nat =>/card_card. Qed. Lemma finite_set_nat n: natp n -> finite_set n. Proof. by move => nN; rewrite /finite_set (card_nat nN); apply/NatP. Qed. Lemma NS_succ x: natp x -> natp (csucc x). by move => /NatP h;rewrite (succ_of_finite h); apply/NatP/finite_oP. Qed. Lemma NS_nsucc x: cardinalp x -> natp (csucc x) -> natp x. Proof. by move => xs /NatP/(finite_succP xs) /NatP. Qed. Hint Resolve CS_nat : fprops. Hint Resolve NS_succ: fprops. Lemma Nsucc_rw x: natp x -> csucc x = x +c \1c. Proof. by move=> fx; apply: csucc_pr4; fprops. Qed. Lemma succ_of_Nat n: natp n -> csucc n = osucc n. Proof. by move => /NatP nN;rewrite succ_of_finite. Qed. Lemma OS_nat x: natp x -> ordinalp x. Proof. move => xN;apply: OS_cardinal; fprops. Qed. Lemma NS_inc_nat a: natp a -> forall b, inc b a -> natp b. Proof. move => ha b hb; exact:(ordinal_transitive OS_omega ha hb). Qed. Lemma Nsum0r x: natp x -> x +c \0c = x. Proof. by move=> xN; apply: csum0r; fprops. Qed. Lemma Nsum0l x: natp x -> \0c +c x = x. Proof. by move=> xN; apply: csum0l; fprops. Qed. Lemma Nprod1l x: natp x -> \1c *c x = x. Proof. by move=> xN; apply: cprod1l; fprops. Qed. Lemma Nprod1r x: natp x -> x *c \1c = x. Proof. by move=> xN; apply: cprod1r; fprops. Qed. Lemma NS_le_nat a b: a <=c b -> natp b -> natp a. Proof. move=> ab /NatP bi; apply/NatP; apply: (le_finite_finite bi ab). Qed. Lemma NS_lt_nat a b: a natp b -> natp a. Proof. by move => [h _]; apply: (NS_le_nat). Qed. Lemma Nat_dichot x: cardinalp x -> natp x \/ infinite_c x. Proof. by move=> h; case: (finite_dichot h); [ move/NatP; left | right]. Qed. Lemma Nat_le_infinite a b: natp a -> infinite_c b -> a <=c b. Proof. by move/NatP; apply finite_le_infinite. Qed. Lemma Nmax_p1 x y: natp x -> natp y -> [/\ natp (cmax x y), x <=c (cmax x y) & y <=c (cmax x y)]. Proof. move => xN yN. have ha : natp (cmax x y) by rewrite /cmax; Ytac w. by move:(cmax_p1 (CS_nat xN) (CS_nat yN)) => [hb hc]. Qed. Lemma NltP a: natp a -> forall x, x inc x a. Proof. move => aN x; split; first by move /oclt; apply: olt_i. move => xa. apply: (oclt3 (CS_nat (NS_inc_nat aN xa)) (CS_nat aN)). by apply/(oltP (OS_nat aN)). Qed. Lemma NleP a: natp a -> forall x, (x <=c a <-> inc x (csucc a)). Proof. move=> aN x; rewrite (succ_of_Nat aN). split; first by move=> /ocle/(oleP (OS_nat aN)). case/setU1_P;first by case/(NltP aN). move => ->; apply: (cleR (CS_nat aN)). Qed. Lemma Nsucc_i a: natp a -> inc a (csucc a). Proof. move => aN; exact:(proj1 (NleP aN a) (cleR (CS_nat aN))). Qed. Lemma nat_irreflexive n: natp n -> ~(inc n n). Proof. move => nN; apply:(ordinal_irreflexive (OS_nat nN)). Qed. Definition card_three := csucc card_two. Definition card_four := csucc card_three. Notation "\3c" := card_three. Notation "\4c" := card_four. Lemma NS0: natp \0c. Proof. apply: Nat_i; apply: finite_zero. Qed. Lemma NS1: natp \1c. Proof. move: NS0; rewrite - succ_zero; fprops. Qed. Lemma NS2: natp \2c. Proof. move: NS1; rewrite - succ_one; fprops. Qed. Lemma NS3: natp \3c. Proof. move: NS2; rewrite /card_three; fprops. Qed. Lemma NS4: natp \4c. Proof. move: NS3; rewrite /card_four; fprops. Qed. Hint Resolve NS0 NS1 NS2: fprops. Lemma finite_0: finite_c \0c. Proof. fprops. Qed. Lemma finite_1: finite_c \1c. Proof. fprops. Qed. Lemma finite_2: finite_c \2c. Proof. fprops. Qed. Hint Resolve finite_0 finite_1 finite_2 : fprops. Lemma two_plus_two: \2c +c \2c = \4c. Proof. rewrite /card_four (Nsucc_rw NS3). rewrite /card_three (Nsucc_rw NS2) - csumA - card_two_pr //. Qed. Lemma two_times_two: \2c *c \2c = \4c. Proof. rewrite - two_plus_two; apply: two_times_n. Qed. Lemma power_2_4: \2c ^c \4c = \4c ^c \2c. Proof. by rewrite -{2} two_times_two cpow_prod2 -two_plus_two cpow_sum2. Qed. Lemma cardinal_tripleton x y z: x <> y -> x <> z -> y <> z -> cardinal (tripleton x y z) = \3c. Proof. move => xy xz yz. rewrite /tripleton csucc_pr ? cardinal_set2 //. by move /set2_P; case; apply: nesym. Qed. Lemma cardinal_ge3 E: \3c <=c cardinal E -> exists a b c, [/\ inc a E, inc b E, inc c E & [/\ a <> b, a <> c & b <> c]]. Proof. rewrite /card_three - (card_card (CS_succ \2c)) (succ_of_Nat NS2). move /eq_subset_cardP1 /eq_subset_ex_injP => [f [[ff injf] sf tf]]. exists (Vf f \0c); exists (Vf f \1c); exists (Vf f \2c). have zs: inc \0c (source f) by rewrite sf; apply /set3_P; in_TP4. have os: inc \1c (source f) by rewrite sf; apply /set3_P; in_TP4. have ts: inc \2c (source f) by rewrite sf; apply /set3_P; in_TP4. rewrite -tf;split; fprops; split=> h. by move: (injf _ _ zs os h); fprops. by move: (injf _ _ zs ts h); fprops. by move: (injf _ _ os ts h); fprops. Qed. Lemma cardinal_doubleton x y: cardinal (doubleton x y) <=c \2c. Proof. case: (equal_or_not x y) => eq. rewrite eq; rewrite cardinal_set1; apply: cle_12. rewrite (cardinal_set2 eq); fprops. Qed. Lemma Nat_in_suml a b: cardinalp a -> natp (a +c b) -> natp a. Proof. move => /(csum_M0le b) sa; exact:NS_le_nat. Qed. Lemma Nat_in_sumr a b: cardinalp b -> natp (a +c b) -> natp b. Proof. rewrite csumC;exact:Nat_in_suml. Qed. Lemma Nat_in_product a b: cardinalp a -> b <> \0c -> natp (a *c b) -> natp a. Proof. move=> ca nzb. have on: (\1c <=c (cardinal b)). apply: cge1; [fprops | by apply: card_nonempty0]. rewrite -(cprod2cr a b) -(cdiff_pr on) cprodDl (cprod1r ca). apply: (Nat_in_suml ca). Qed. Lemma cdiff_le1 a b: cardinalp a -> a -c b <=c a. Proof. by move => /card_card h; move: (sub_smaller (@sub_setC a b)); rewrite h. Qed. Lemma cdiff_nz a b: b (a -c b) <> \0c. Proof. move => [lea nea] cs; case: nea. by rewrite -(cdiff_pr lea) cs (csum0r (proj31 lea)). Qed. Lemma NS_diff a b: natp a -> natp (a -c b). Proof. move => h; apply:(NS_le_nat (cdiff_le1 b (CS_nat h)) h). Qed. Hint Resolve NS_diff: fprops. Lemma cpred0 : cpred \0c = \0c. Proof. exact: setU_0. Qed. Lemma cpred1: cpred \1c = \0c. Proof. rewrite - succ_zero (succ_of_finite finite_0); apply: (succo_K OS0). Qed. Lemma cpred_inf a: infinite_c a -> cpred a = a. Proof. exact: infinite_card_limit1. Qed. Lemma cpred_pr n: natp n -> n <> \0c -> (natp (cpred n) /\ n = csucc (cpred n)). Proof. move/NatP; rewrite /finite_c finite_succ => p1 p2. case: p1 => // -[y fy ns]. rewrite ns /cpred -/opred (succo_K (proj1 fy)) (succ_of_finite fy). split; fprops. Qed. Lemma NS_pred a: natp a -> natp (cpred a). Proof. move => aN; case: (equal_or_not a \0c) => az. by rewrite az cpred0 -az. exact: (proj1 (cpred_pr aN az)). Qed. Lemma CS_pred a: cardinalp a -> cardinalp (cpred a). Proof. move => h; case: (finite_dichot h); last by move/cpred_inf => ->. move/NatP => aN; exact: (CS_nat (NS_pred aN)). Qed. Lemma cpred_pr2 n: natp n -> cpred (csucc n) = n. Proof. by move/NatP => h; rewrite succ_of_finite //; apply: succo_K; case:h. Qed. Lemma cpred_pr1 n: cardinalp n -> cpred (csucc n) = n. Proof. case /finite_dichot; first by move/NatP/cpred_pr2. by move => ifn;move: (ifn) => /csucc_inf ->;apply: cpred_inf. Qed. Lemma cpred_pr5 x y: inc x y -> cpred (cardinal y) = cardinal (y -s1 x). Proof. move => nxy;move:(f_equal cpred (csucc_pr2 nxy)); rewrite cpred_pr1 //; fprops. Qed. Lemma cpred_pr3 n: natp n -> n = \0c \/ exists2 m, natp m & n = csucc m. Proof. move=> nN; case: (equal_or_not n \0c); first by left. by move /(cpred_pr nN) => [pa pb];right; exists (cpred n). Qed. Lemma cpred_nz n: cardinalp n -> cpred n <> \0c -> \0c pa pb; exact:(card_ne0_pos (CS_pred pa) pb). Qed. Lemma cleS0 a: cardinalp a -> a <=c (csucc a). Proof. by move=> ca; rewrite (csucc_pr4 ca); apply: csum_M0le. Qed. Lemma cleS a: natp a -> a <=c (csucc a). Proof. by move=> /CS_nat /cleS0. Qed. Lemma cltS a: natp a -> a aN; apply/(NltP (NS_succ aN)); rewrite (succ_of_Nat aN);fprops. Qed. Hint Resolve cleS cltS: fprops. Lemma cpred_le a: cardinalp a -> cpred a <=c a. Proof. move => ca; move:(CS_pred ca) => cpa; split => //. exact (proj33 (opred_le (proj1 ca))). Qed. Lemma cle_24: \2c <=c \4c. Proof. exact: (cleT (cleS NS2)(cleS NS3)). Qed. Lemma clt_24: \2c forall a, (a a <=c n). Proof. move => nN a. apply:(iff_trans (NltP (NS_succ nN) a) (iff_sym (NleP nN a))). Qed. Lemma cleSS a b : a <=c b -> csucc a <=c csucc b. Proof. move => h; move:(h) => [ca cb _]. rewrite ! csucc_pr4 //;apply: (csum_Mlele h (cleR CS1)). Qed. Lemma cleSSP a b: cardinalp a -> cardinalp b -> (csucc a <=c csucc b <-> a <=c b). Proof. move => ca cb; split => h; last by apply: cleSS. case: (Nat_dichot cb) => bN; last first. rewrite (csucc_inf bN) in h. case: (Nat_dichot ca) => aN; first by apply: Nat_le_infinite. by rewrite -(csucc_inf aN). have le1 := (cleS0 ca). apply/(cltSleP bN);split;first by apply: (cleT le1 h). move=> aux; rewrite -aux in h; have asa:=(cleA h le1). move: (NS_succ bN); rewrite -aux => /NatP /finite_cP [_] []//. Qed. (* alternate proof removed *) Lemma ordinal_incSS a b: ordinalp b -> (inc a b <-> inc (osucc a) (osucc b)). Proof. move =>ob; split. by move => /(oltP ob) /oltSSP /(oltP (OS_succ ob)). by move /(oltP (OS_succ ob)) /oltSSP /(oltP ob). Qed. Lemma cleSlt0P a b: cardinalp a -> natp b -> (csucc a <=c b <-> a ca bN; apply:iff_trans (iff_sym(NltP bN a)). apply: (iff_trans (NleP bN (csucc a))). case: (p_or_not_p (natp a)) => aN. rewrite (succ_of_Nat aN) (succ_of_Nat bN); apply: iff_sym. apply:(ordinal_incSS _ (OS_nat bN)). split=> h;case: aN; first exact:(NS_nsucc ca (NS_inc_nat (NS_succ bN) h)). exact:(NS_inc_nat bN h). Qed. Lemma cleSltP a: natp a -> forall b, (csucc a <=c b <-> a aN b. case (p_or_not_p (cardinalp b)) => h; last first. split => lt;case: h; [ exact :proj32 lt | exact :proj32_1 lt]. case: (Nat_dichot h) => H; first by apply /(cleSlt0P (CS_nat aN) H). split => _. by apply:(finite_lt_infinite (Nat_hi aN)). apply:(finite_le_infinite (Nat_hi (NS_succ aN)) H). Qed. Lemma cltSS a b : a csucc a [pa pb]; split; first by apply:cleSS. by move/(succ_injective1 (proj31 pa) (proj32 pa)). Qed. Lemma cltSSP n m: cardinalp n -> cardinalp m -> ((csucc n (n cn cm; split; last by apply:cltSS. move => [pa pb]; split; first by move/(cleSSP cn cm) : pa. by move => h; case: pb; rewrite h. Qed. Lemma cpred_pr6 k i: natp k -> \1c <=c i -> i <=c csucc k -> [/\ natp (cpred i), i = csucc (cpred i) & cpred i <=c k]. Proof. move => kN sa sb. have inz : i <> \0c by move => iz; case:(cltNge clt_01); rewrite -iz. move: (cpred_pr (NS_le_nat sb (NS_succ kN)) inz) => [ra rb]; split => //. by move: sb; rewrite {1} rb; move /(cleSSP (CS_nat ra)( (CS_nat kN))). Qed. Lemma cpred_lt n: natp n -> n <> \0c -> cpred n nN nz. move: (cpred_pr nN nz) =>[sa sb]. apply /(cleSltP sa); rewrite - sb; fprops. Qed. Lemma cmax_succ a b: cardinalp a -> cardinalp b -> cmax (csucc a) (csucc b) = csucc (cmax a b). Proof. wlog: a b / a <=c b. move => H ca cb; case: (cleT_ee ca cb) => H'; first by apply:H. by rewrite (cmaxC ca cb)(cmaxC (CS_succ _) (CS_succ _)); apply: H. by move => lab ca cb;rewrite /cmax (Y_true (cleSS lab)) (Y_true lab). Qed. Lemma inf_Nat E (x:= intersection E): sub E Nat -> nonempty E -> inc x E /\ (forall y, inc y E -> x <=c y). Proof. by move => pa; apply:cle_wor' => // t /pa /CS_nat. Qed. Lemma NS_inf_Nat E (x:= intersection E): sub E Nat -> natp x. Proof. move => h; case (emptyset_dichot E) => h1. rewrite /x h1 setI_0; fprops. exact: (h _ (proj1 (inf_Nat h h1))). Qed. Lemma card_finite_setP x: finite_set x <-> natp (cardinal x). Proof. apply: iff_sym;apply:NatP. Qed. Lemma emptyset_finite: finite_set emptyset. Proof. apply/NatP; rewrite cardinal_set0; apply: NS0. Qed. Lemma strict_sub_smaller x y: ssub x y -> finite_set y -> (cardinal x) ssxy fsy. move: (setC_ne ssxy) =>[u uc]. move /setC_P : uc => [uy ux]. set (z:= y -s1 u). have ->: (cardinal y = csucc (cardinal z)) by rewrite /z - csucc_pr1 setC1_K. move: ssxy => [sxy _]. have szy: sub z y by rewrite /z; apply: sub_setC. have /sub_smaller lexz: sub x z. move=> t tx; apply /setC1_P; split; [ by apply: sxy | dneg tu; ue]. apply /cltSleP => //; apply /NatP; apply: (sub_finite_set szy fsy). Qed. Lemma strict_sub_smaller1 y: (forall x, ssub x y -> (cardinal x) finite_set y. Proof. split; last by move => fsy x ss; apply: strict_sub_smaller. move=> h. case: (emptyset_dichot y); first by move => ->; apply: emptyset_finite. move=> [u uy]. set (z:=complement y (singleton u)). have ssy: ssub z y. split; first by apply: sub_setC. by move=> ezy; move: uy; rewrite -ezy; move /setC1_P => [_]. have yt: y = z +s1 u by rewrite setC1_K. move: (csucc_pr1 y u); rewrite -/z -yt => cy. have cz := (CS_cardinal z). rewrite /finite_set cy. apply /(finite_succP cz) /finite_cP;split => //. rewrite - cy; exact: (proj2 (h _ ssy)). Qed. Lemma finite_range f: fgraph f -> finite_set (domain f) -> finite_set (range f). Proof. move=> /range_smaller => pa pb; apply :(le_finite_finite pb pa). Qed. Lemma finite_image f: function f -> finite_set (source f) -> finite_set (Imf f). Proof. move=> ff fs; move: (image_smaller ff)=> cle. apply: (le_finite_finite fs cle). Qed. Lemma finite_image_by f A: function f -> finite_set A -> finite_set (Vfs f A). Proof. move=> ff fsA; move:(image_smaller1 A ff) => cle. apply: (le_finite_finite fsA cle). Qed. Lemma finite_fun_image a f: finite_set a -> finite_set (fun_image a f). Proof. move=> fsa;move: (fun_image_smaller a f) => h. apply: (le_finite_finite fsa h). Qed. Lemma finite_graph_domain f: fgraph f -> (finite_set f <-> finite_set (domain f)). Proof. by move=> /Eq_domain /card_eqP; rewrite /finite_set /finite_c => ->. Qed. Lemma bijective_if_same_finite_c_inj f: cardinal (source f) = cardinal (target f) -> finite_set (source f) -> injection f -> bijection f. Proof. move=> csftf fs injf; split=>//; apply: surjective_pr1; first by fct_tac. have fst: (finite_set (target f)) by hnf; ue. have sit: (sub (Imf f) (target f)). apply: fun_image_Starget; fct_tac. ex_middle it. move:(strict_sub_smaller (conj sit it) fst) => [cle ne]. case: ne; transitivity (cardinal (source f))=>//. symmetry; apply /card_eqP. exists (restriction_to_image f); red. rewrite {2 3} /restriction_to_image /restriction2; aw. split => //; by apply: (restriction_to_image_fb injf). Qed. Lemma bijective_if_same_finite_c_surj f: cardinal (source f) = cardinal (target f) -> finite_set (source f) -> surjection f -> bijection f. Proof. move=> cstf fsf sf. move: (exists_right_inv_from_surj sf)=> [g rig]. move: (right_i_source rig) =>sg. move: (right_inverse_fi rig)=> ig. move: rig =>[co c]; move: (co) => [_ s t]. have csftf: (cardinal (source g) = cardinal (target g)) by rewrite sg -t. have fss: finite_set (source g) by hnf; rewrite sg - cstf. have bg :=(bijective_if_same_finite_c_inj csftf fss ig). have bc: (bijection (compose f g)) by rewrite c; apply: identity_fb. apply: (left_compose_fb co bc bg). Qed. (** ** EIII-6-1 The set of natural integers *) Lemma sub_natI_prop X (x := intersection X): sub X Nat -> [/\ natp x, forall t, t ~ (inc t X) & nonempty X -> inc x X]. Proof. move => ha; have hb := (NS_inf_Nat ha). case: (emptyset_dichot X) => Xe. by rewrite Xe;split =>//; [ move => t _ /in_set0 | move/nonemptyP ]. move: (inf_Nat ha Xe) => [hc hd]; split => //. by move => t aa /hd /cleNgt;apply. Qed. Lemma wleast_int_prop (prop:property): (exists2 x, natp x & prop x) -> prop \0c \/ (exists x, [/\ natp x, prop (csucc x) & ~ prop x]). Proof. move=> [x xn xp]. set (X:=Zo Nat prop). have sX: sub X Nat by apply: Zo_S. have nX: nonempty X by exists x; apply: Zo_i. move:(sub_natI_prop sX); set y := intersection _. move => [pa pb pc]; move:(pc nX) => /Zo_P [yN yp]. case: (equal_or_not y \0c) => eq; [ by rewrite - eq; left | right]. move: (cpred_pr yN eq) => [sa sb]; exists (cpred y); rewrite - sb; split => //. by move:(cltS sa); rewrite - sb => /pb sc sd; case:sc; apply: Zo_i. Qed. Definition Nat_order := graph_on cardinal_le Nat. Definition Nat_le x y := [/\ natp x, natp y & x <=c y]. Definition Nat_lt x y := Nat_le x y /\ x<>y. Notation "x <=N y" := (Nat_le x y) (at level 60). Notation "x x <=N y. Proof. apply: graph_on_P1. Qed. Lemma Nat_wordered X: sub X Nat -> nonempty X -> inc \0c X \/ (exists a, [/\ natp a, inc (csucc a) X & ~ (inc a X)]). Proof. move=> Xb neX. have [wor sr] := Nat_order_wor. have aux: sub X (substrate Nat_order) by rewrite sr. move: (worder_prop wor aux neX) => [x xX xle]. case: (cpred_pr3 (Xb _ xX)) => h. by left; rewrite -h. move: h => [c cn xs]; right; exists c; split=>//; first by ue. move=> xC; move: (xle _ xC) => /Nat_order_leP [xN cN lexc]. by move: (cltS cN); rewrite -xs=> /(cleNgt lexc). Qed. Section NatIinterval. Variables (a b: Set). Hypotheses (aN: natp a) (bN: natp b). Lemma Nint_ccP x: (inc x (interval_cc Nat_order a b) <-> (a <=N x /\ x <=N b)). Proof. rewrite /interval_cc (proj2 Nat_order_wor); split. by move /Zo_P => [xb [/Nat_order_leP pa /Nat_order_leP pb]]. move => [pa pb]; apply /Zo_i; first by move: pa => [_]. by split; apply /Nat_order_leP. Qed. Lemma Nint_coP x: (inc x (interval_co Nat_order a b) <-> (a <=N x /\ x [xb []] /Nat_order_leP pa [] /Nat_order_leP pb xnb. move => [pa [pb pc]]; apply /Zo_i; first by move: pa => [_]. by split; [| split => // ];apply /Nat_order_leP. Qed. Lemma Nint_ccP1 x: (inc x (interval_cc Nat_order a b) <-> (a <=c x /\ x <=c b)). Proof. apply: (iff_trans (Nint_ccP x)); split. by move=> [[_ _ pa] [_ _ pb]]. move=> [ax bx]; move:(NS_le_nat bx bN) => xN //. Qed. Lemma Nint_coP1 x: (inc x (interval_co Nat_order a b) <-> (a <=c x /\ x [[_ _ pa] [[_ _ pb] pc]]. move=> [ax [bx xb]]; move:(NS_le_nat bx bN) => xN //. Qed. End NatIinterval. (** ** EIII-4-3 The principle of induction *) Lemma Nat_induction (r:property): (r \0c) -> (forall n, natp n -> r n -> r (csucc n)) -> (forall n, natp n -> r n). Proof. move=> r0 ri n nN. case: (p_or_not_p (r n)) => // nrn. have pa: (exists2 x, natp x & ~ r x) by exists n. case:(wleast_int_prop pa) => // [] [x [xN nsr /excluded_middle rx]]. by case: nsr; apply: ri. Qed. Lemma Nat_induction1 (r:property): let s:= fun n => forall p, natp n -> natp p -> p r p in (forall n, natp n -> s n -> r n) -> (forall n, natp n -> r n). Proof. move=> s si n nN; apply: (si)=>//. move: n nN; apply: Nat_induction. move=> p f0 fp np; case: (clt0 np). move=> m fm sm p fsp fp lp. case: (equal_or_not p m); first by move=>->; apply: si =>//. by move=> pm; apply: sm=>//; split=>//; move: lp => /(cltSleP fm). Qed. Lemma Nat_induction2 (r:property) k: natp k -> r k -> (forall n, natp n -> k <=c n -> r n -> r (csucc n)) -> (forall n, natp n -> k <=c n -> r n). Proof. move=> fk rk ri n fn kn. move: n fn kn; apply: Nat_induction; first by move=> h; rewrite - (cle0 h). move=> m fm sm; case: (equal_or_not k (csucc m)); first by move => <-. move => ks ksm. move/(cltSleP fm):(conj ksm ks) => lekm. by apply: ri=>//; apply: sm. Qed. Lemma Nat_induction3 (r:property) a b: natp a -> natp b -> r a -> (forall n, a <=c n -> n r n -> r (csucc n)) -> (forall n, a <=c n -> n <=c b -> r n). Proof. move=> aN bN ra ri n an nb. have nN:= NS_le_nat nb bN. move: n nN an nb; apply: Nat_induction. by move => az _; rewrite -(cle0 az). move=> m mN sm am; move/(cleSltP mN) => mb. case: (equal_or_not a (csucc m));[ by move => <- | move=> asm]. move/(cltSleP mN): (conj am asm) => leam. apply: (ri _ leam mb (sm leam (proj1 mb))). Qed. Lemma Nat_induction4 (r:property) a b: natp a -> natp b -> r b -> (forall n, a <=c n -> n r (csucc n) -> r n) -> (forall n, a <=c n -> n <=c b -> r n). Proof. move=> aN bN rb ti n an nb. set (q := fun n => ~ (r n)). case: (p_or_not_p (r n))=>// nrn. have nN:= NS_le_nat nb bN. have qi: (forall m, n <=c m -> m q m -> q (csucc m)). rewrite /q;move=> m nm mb qm; dneg rs; apply: ti=> //; exact: cleT an nm. by move: ((Nat_induction3 nN bN nrn qi) _ nb (cleR (proj32 nb))). Qed. Lemma Nat_induction6 (P: property): P \0c -> (forall n, natp n -> (forall k, k<=c n -> P k) -> P (csucc n)) -> (forall n, natp n -> P n). Proof. move => ha hb. suff: forall n, natp n -> forall m, m <=c n -> P m. move => H n nN; exact: (H n nN n (cleR (CS_nat nN))). apply: Nat_induction ; first by move => m /cle0 ->. move => n nN Hrec m le1. case: (equal_or_not m (csucc n)) => lt1 //. by rewrite lt1; apply: (hb _ nN). by move /(cltSleP nN): (conj le1 lt1) => /Hrec. Qed. Lemma Nat_induction3_v (r:property) a b: natp a -> natp b -> r a -> (forall n, inc n (interval_co Nat_order a b) -> r n -> r (csucc n)) -> (forall n, inc n (interval_cc Nat_order a b) -> r n). Proof. move=> aN bN ra ri m. have ri': (forall n, a <=c n -> n r n -> r (csucc n)). by move=> n an nb;apply: ri; apply /Nint_coP1. move/(Nint_ccP1 aN bN) => [am mb]. by apply: (Nat_induction3 aN bN). Qed. Lemma setU1_finite X x: finite_set X -> finite_set (X +s1 x). Proof. move=>fX; case: (inc_or_not x X) => h; first by rewrite (setU1_eq h). rewrite/finite_set (csucc_pr h); apply /finite_succP; fprops. Qed. Lemma set1_finite x: finite_set(singleton x). Proof. apply/ card_finite_setP; rewrite cardinal_set1; apply: NS1. Qed. Lemma set2_finite x y: finite_set (doubleton x y). Proof. rewrite -(setU2_11 x y); apply: setU1_finite; apply: set1_finite. Qed. Lemma finite_set_scdo: finite_set (substrate canonical_doubleton_order). Proof. rewrite (proj2 cdo_wor); apply: set2_finite. Qed. Lemma setU1_succ_card x n: cardinalp n -> cardinal x = csucc n -> exists u v, [/\ x = u +s1 v, ~(inc v u) & cardinal u = n]. Proof. move=> cn cx. case: (emptyset_dichot x) => h. by case:(@succ_nz n); rewrite - cx h cardinal_set0. move: h=> [y yx]. have xt:= (setC1_K yx). exists (x -s1 y), y;split =>//;first by apply: setC1_1. apply: succ_injective1; fprops. by rewrite - cx -xt (csucc_pr1 x y) xt. Qed. Lemma finite_set_induction0 (s:property): s emptyset -> (forall a b, s a -> ~(inc b a) -> s (a +s1 b)) -> forall x, finite_set x -> s x. Proof. move=> se si x /card_finite_setP cxN. pose r n := forall x, cardinal x = n -> s x. have r0: r \0c by move => y h; rewrite (card_nonempty h). apply: (Nat_induction r0 _ cxN _ (erefl (cardinal x))) => n nN rn y yp. move: (setU1_succ_card (CS_nat nN) yp) => [u [v [yt nvu cu]]]. by rewrite yt; apply: si=>//; apply: rn. Qed. Lemma finite_set_induction (s:property): s emptyset -> (forall a b, s a -> s (a +s1 b)) -> forall x, finite_set x -> s x. Proof. move => se si x fs; apply: (finite_set_induction0 (s:=s))=>//. by move=> a b sa _; apply: si. Qed. Lemma finite_set_induction1 (A B:property) x: (A emptyset -> B emptyset) -> (forall a b, (A a -> B a) -> A(a +s1 b) -> B(a +s1 b)) -> finite_set x -> A x -> B x. Proof. move=> h1 h2 fs. by pose s x := A x -> B x; apply: (finite_set_induction (s:=s) h1). Qed. Lemma finite_set_induction2 (A B:property) x: (forall a, A (singleton a) -> B (singleton a)) -> (forall a b, (A a -> nonempty a -> B a) -> nonempty a -> A(a +s1 b) -> B(a +s1 b)) -> finite_set x -> A x -> nonempty x -> B x. Proof. move=> fA fr. pose s x := A x -> nonempty x -> B x. apply: (finite_set_induction (s:=s)). by move=> _ [t /in_set0]. move=> a b sa. case: (emptyset_dichot a) => pa. have ->: (a +s1 b = singleton b) by rewrite pa; exact: set0_U2. by move => h _; apply: fA. by move=> h h'; apply: fr. Qed. Lemma csum_via_succ a b: cardinalp b -> a +c (csucc b) = csucc (a +c b). Proof. move => cb; rewrite (csucc_pr4 cb) csumA (csucc_pr4) //; fprops. Qed. Lemma cprod_via_sum a b: cardinalp b -> a *c (csucc b) = (a *c b) +c a. Proof. move=> cb; rewrite (csucc_pr4 cb) cprodDl. rewrite - (csum2cr (a *c b) a) - (cprod1l (CS_cardinal a)). by rewrite (cprod2cr \1c a) (cprodC \1c). Qed. Lemma cpow_succ' a b: cardinalp b -> a ^c (csucc b) = (a ^c b) *c a. Proof. by move=> cb; rewrite (csucc_pr4 cb) cpow_sum2 (cpowx1c a) cprod2cr. Qed. Lemma csum_nS a b: natp b -> a +c (csucc b) = csucc (a +c b). Proof. move => /CS_nat; apply: csum_via_succ. Qed. Lemma csum_Sn a b: natp a -> (csucc a) +c b = csucc (a +c b). Proof. by move=> aN; rewrite csumC (csum_nS _ aN) csumC. Qed. Lemma cprod_nS a b: natp b -> a *c (csucc b) = (a *c b) +c a. Proof. move => /CS_nat; apply: cprod_via_sum. Qed. Lemma cpow_succ a b: natp b -> a ^c (csucc b) = (a ^c b) *c a. Proof. move => /CS_nat; apply: cpow_succ'. Qed. Lemma NS_sum a b: natp a -> natp b -> natp (a +c b). Proof. move=> aN bN. move: b bN; apply: Nat_induction; first by aw;fprops. move=> n fn fan; rewrite (csum_nS a fn); fprops. Qed. Lemma NS_prod a b: natp a -> natp b -> natp (a *c b). Proof. move=> aN bN. move: b bN; apply: Nat_induction; first by rewrite cprod0r; fprops. by move=> n nN mN; rewrite cprod_nS; fprops; apply: NS_sum. Qed. Lemma NS_pow a b: natp a -> natp b -> natp (a ^c b). Proof. move=> aN bN. move: b bN; apply: Nat_induction; first by rewrite cpowx0; fprops. by move=> n nN mN; rewrite cpow_succ => //;apply: NS_prod. Qed. Lemma NS_pow2 n: natp n -> natp (\2c ^c n). Proof. apply: NS_pow; fprops. Qed. Hint Resolve NS_sum NS_prod: fprops. Hint Resolve NS_pow NS_pow2: fprops. Lemma finite_prod2 u v: finite_set u -> finite_set v -> finite_set (u \times v). Proof. move =>/card_finite_setP ha /card_finite_setP hb. apply /card_finite_setP; rewrite - cprod2_pr1 - cprod2cl - cprod2cr. fprops. Qed. Lemma cdiff_n0 a: natp a -> a -c \0c = a. Proof. by move => ca;rewrite /cdiff setC_0 (card_nat ca). Qed. Lemma cdiff_wrong a b: a <=c b -> a -c b = \0c. Proof. by move => [_ _ ab]; rewrite /cdiff (setC_T ab) cardinal_set0. Qed. Lemma csum_fin_infin a b: finite_c a -> infinite_c b -> a +c b = b. Proof. move/NatP => aN ifb; move: a aN; apply:Nat_induction. by aw; exact: (proj1 ifb). by move => a aN hr; rewrite (csum_Sn _ aN) hr (csucc_inf ifb). Qed. Lemma cdiff_fin_infin a b: finite_c a -> infinite_c b -> b -c a = b. Proof. move => ha hb; move: (cdiff_pr (finite_le_infinite ha hb)) => ea. case: (finite_dichot (CS_diff b a)) => fd. move: ha fd => /NatP aN /NatP dN; move:(NS_sum aN dN); rewrite ea => /NatP fb. case:(infinite_dichot1 fb hb). by move: ea; rewrite (csum_fin_infin ha fd). Qed. Lemma cdiff_succ_aux a b: b cardinal ((a +s1 a) -s (b +s1 b)) = cardinal (a -s b). Proof. move => h; move/olt_i: (h) => iba; move:h=> [[ob oa sab] anb]. have aa:= (ordinal_irreflexive oa). set E := (a -s (b +s1 b)). have naE: ~inc a E by move /setC_P => [/aa]. have nbE: ~inc b E by move /setC_P => [_] /setU1_P; case; right. have -> : a -s b = E +s1 b. set_extens t. move/setC_P => [ta tb]; case: (equal_or_not t b) => tc. - rewrite tc; fprops. - by apply:setU1_r; apply/setC_P ; split => //; case/setU1_P. case/setU1_P. move/setC_P => [ta ntb]; apply /setC_P; split => // itb. - case: ntb; fprops. - move => ->; apply/setC_P; split => //; apply:(ordinal_irreflexive ob). have -> : ((a +s1 a) -s (b +s1 b)) = E +s1 a. set_extens t. move/setC_P => [ta tb]; case/setU1_P: ta => ta. - by apply:setU1_r;apply/setC_P. - by rewrite ta; apply:setU1_1. case/setU1_P. - move/setC_P => [ta tb]; apply/setC_P; split => //; fprops. - move ->; apply/setC_P; split => //; fprops => w. by move: (extensionality sab (ordinal_sub3 ob w)). by rewrite (csucc_pr naE) (csucc_pr nbE). Qed. Lemma cdiff_succ a b: cardinalp a -> cardinalp b -> (csucc a) -c (csucc b) = a -c b. Proof. move => ca cb. case :(cleT_el ca cb) => lea. by move:(cleSS lea) => leb; rewrite (cdiff_wrong leb)(cdiff_wrong lea). case /finite_dichot: cb => fb. case /finite_dichot: ca => fa. move: fa fb => /NatP aN /NatP bN. rewrite (succ_of_Nat aN) (succ_of_Nat bN) /cdiff /osucc. apply:(cdiff_succ_aux (oclt lea)). move/(finite_succP (proj31_1 lea)):(fb) => fsb. by rewrite (csucc_inf fa) (cdiff_fin_infin fsb fa)(cdiff_fin_infin fb fa). move:(ge_infinite_infinite fb (proj1 lea)) => ifa. by rewrite (csucc_inf ifa)(csucc_inf fb). Qed. Lemma cdiff_pr1' a b: cardinalp a -> natp b -> (a +c b) -c b = a. Proof. move=> aN bN. have aa: a -c \0c = a by rewrite /cdiff setC_0 (card_card aN). move: b bN; apply:Nat_induction. by rewrite (csum0r aN) aa. move => n nN hr. by rewrite (csum_nS _ nN) (cdiff_succ (CS_sum2 a n) (CS_nat nN)). Qed. Lemma cdiff_pr1 a b: natp a -> natp b -> (a +c b) -c b = a. Proof. by move=> /CS_nat aN bN; apply: cdiff_pr1'. Qed. (** ** EIII-4-4 Finite subsets of ordered sets *) Lemma finite_set_induction3 (p: Set -> Set -> Prop) E X: (forall a b, inc a E -> inc b E -> exists y, p (doubleton a b) y) -> (forall a b x y, sub a E -> inc b E -> p a x -> p (doubleton x b) y-> p (a +s1 b) y) -> (forall X x, sub X E -> nonempty X -> p X x -> inc x E) -> nonempty X -> finite_set X -> sub X E -> exists x, p X x. Proof. move=> p1 p2 p3 neX fsX XE. apply: (@finite_set_induction2 (fun X=> sub X E) (fun X => exists x, p X x)) => //. move=> a aE; have ae:= (aE _ (set1_1 a)). exact:(p1 a a ae ae). move=> a b p4 nea st. have saE: sub a E by apply: sub_trans st; fprops. have bE: inc b E by apply: st;fprops. have [y py] := (p4 saE nea). have yE:= (p3 _ _ saE nea py). have [z pz] := (p1 _ _ yE bE). exists z; apply: p2 saE bE py pz. Qed. Lemma finite_subset_directed_bounded r X: right_directed r ->finite_set X -> sub X (substrate r) -> nonempty X -> bounded_above r X. Proof. move=> [or rr] fsX sX neX. move: neX fsX sX. apply: finite_set_induction3 => //; last by move => Y x Ysr neY [sr uYx]. move=> a b x y asr bsr [xsr ubx] [yser upy]. split =>//. have xy := (upy _ (set2_1 x b)). have lyb:= (upy _ (set2_2 x b)). move=> t /setU1_P; case; last by move=>->. move => ta; move: (ubx _ ta)=> aux; order_tac. Qed. Lemma finite_subset_lattice_inf r X: lattice r ->finite_set X -> sub X (substrate r) -> nonempty X -> exists x, greatest_lower_bound r X x. Proof. move=> [or lr] fsX Xsr neX. move: neX fsX Xsr. apply: finite_set_induction3. + by move=>a b asr bsr; move: (lr _ _ asr bsr)=> [p1 p2]. + move=> a b x y asr bsr. move /(glbP or asr)=> [[xsr lb] glex]. have st: sub (a +s1 b) (substrate r) by apply: setU1_sub. have sd: sub (doubleton x b) (substrate r) by apply: sub_set2. move=> /(glbP or sd) [[ysr lby] lgley]. have xy := (lby _ (set2_1 x b)). have lbyy:= (lby _ (set2_2 x b)). apply /(glbP or st); split. split =>// z /setU1_P; case; last by move=> ->. move=>za; move: (lb _ za)=> xa; order_tac. move=> z [ze xx]. apply: lgley; split=>//; move=> t /set2_P [] ->. apply: glex; split=>//. move=> u ua; apply: xx; fprops. apply: xx; fprops. + by move=> Z x Zr _ /(glbP or Zr) [[xsr _] _]. Qed. Lemma finite_subset_lattice_sup r X: lattice r ->finite_set X -> sub X (substrate r) -> nonempty X -> exists x, least_upper_bound r X x. Proof. move=> [or lr] fsX Xsr neX. move: neX fsX Xsr. apply: finite_set_induction3. + by move=>a b asr bsr; move: (lr _ _ asr bsr)=> [p1 p2]. + move=> a b x y asr bsr. move /(lubP or asr)=> [[xsr lb] glex]. have st: sub (a +s1 b) (substrate r) by apply: setU1_sub. have sd: sub (doubleton x b) (substrate r) by apply: sub_set2. move=> /(lubP or sd) [[ysr lby] lgley]. have xy:= (lby _ (set2_1 x b)). have lbyy := (lby _ (set2_2 x b)). apply /(lubP or st); split. split =>// z /setU1_P; case; last by move=> ->. move=>za; move: (lb _ za)=> xa; order_tac. move=> z [ze xx]. apply: lgley; split=>//; move=> t /set2_P [] ->. apply: glex; split=>//. move=> u ua; apply: xx; fprops. apply: xx; fprops. by move=> Z x Zr _ /(lubP or Zr) [[xsr _] _]. Qed. Lemma finite_subset_torder_greatest r X: total_order r ->finite_set X -> sub X (substrate r) -> nonempty X -> has_greatest (induced_order r X). Proof. move=> [or tor] fsX Xsr neX. move: neX fsX Xsr. apply: (finite_set_induction3 (p:=fun X x => greatest (induced_order r X) x)). + move=> a b asr bsr. have sd: sub (doubleton a b) (substrate r) by apply: sub_set2. by case: (tor _ _ asr bsr)=> cp; [exists b | exists a]; hnf; aw; split; fprops; move=> x /set2_P [] ->; apply/iorder_gleP; fprops; order_tac. + move=> a b x y asr bsr;rewrite /greatest. have sta: (sub (a +s1 b) (substrate r)) by apply: setU1_sub. rewrite iorder_sr //; move=> [xa xp]. have xsr := (asr _ xa). have sd: sub (doubleton x b) (substrate r) by apply: sub_set2. move: xp; aw; move=> xp [yd yp]; split. move: yd => /set2_P []->; fprops. have xy:= (iorder_gle1 (yp _ (set2_1 x b))). have lby:= (iorder_gle1 (yp _ (set2_2 x b))). have yt: inc y (a +s1 b) by case /set2_P: yd => ->; fprops. move=> z zi; apply /iorder_gleP => //. case /setU1_P: zi => h; last by ue. have zx:=(iorder_gle1 (xp _ h)) ; order_tac. + move=> Z x Zs neZ [h gex]; apply: (Zs). move: h; aw. Qed. Lemma finite_subset_torder_least r X: total_order r ->finite_set X -> sub X (substrate r) -> nonempty X -> has_least (induced_order r X). Proof. move=> tor fsX Xsr neX. have or: order r by move: tor=> []. have rtor:=(total_order_opposite tor). move: (opp_osr or) => [aa so]; move: (Xsr); rewrite - so => rXsr. move: (finite_subset_torder_greatest rtor fsX rXsr neX)=> [x []]; aw; fprops. move=> xX xg; exists x; hnf;aw;split => //. move=> a aX; move: (iorder_gle1 (xg _ aX)) => /igraph_pP h. by apply /iorder_gleP. Qed. Lemma finite_set_torder_greatest r: total_order r -> finite_set (substrate r) -> nonempty (substrate r) -> has_greatest r. Proof. move=> tor fss nes; move: (tor)=> [or _]. rewrite - (iorder_substrate or). apply: finite_subset_torder_greatest; fprops. Qed. Lemma finite_set_torder_least r: total_order r -> finite_set (substrate r) -> nonempty (substrate r) -> has_least r. Proof. move=> tor fss nes; move: (tor)=> [or _]. rewrite - (iorder_substrate or). apply: finite_subset_torder_least; fprops. Qed. Lemma finite_set_torder_wor r: total_order r -> finite_set (substrate r) -> worder r. Proof. move=> tor fse; move: (tor)=> [or _]. split=>// z zs zne. apply: finite_subset_torder_least =>//. apply: (sub_finite_set zs fse). Qed. Lemma finite_subset_Nat X: sub X Nat -> finite_set X -> nonempty X -> exists2 n, inc n X & forall m, inc m X -> m <=c n. Proof. move => pa pb pc. move: Nat_order_wor => [wor sr]. have pd: sub X (substrate Nat_order) by rewrite sr. move: (finite_subset_torder_greatest (worder_total wor) pb pd pc). move => [n []]; rewrite (iorder_sr (proj1 wor) pd) => pe pf; ex_tac. by move => m /pf /iorder_gle1 /Nat_order_leP []. Qed. Lemma finite_set_maximal r: order r ->finite_set (substrate r) -> nonempty (substrate r) -> exists x, maximal r x. Proof. move=> or fse nes; apply: Zorn_lemma=>//. move => X Xsr toX. case: (emptyset_dichot X)=> xe. rewrite xe;move: nes=> [z zE]; exists z; split=>//; move=> y; case; case. set (s:= induced_order r X) in toX. have sr: (substrate s = X) by rewrite /s; aw. have fs: (finite_set (substrate s)). by rewrite sr; apply: (sub_finite_set Xsr fse). have nse: (nonempty (substrate s)) by rewrite sr. move: (finite_set_torder_greatest toX fs nse)=> [x [xsr xge]]. rewrite - sr in Xsr. rewrite - sr; exists x; split; first by apply: Xsr. move=> y yX; exact (iorder_gle1 (xge _ yX)). Qed. Section LatticeProps. Variable (r: Set). Hypothesis lr: lattice r. Let E := substrate r. Lemma lattice_finite_sup2 x: finite_set x -> sub x E -> nonempty x -> has_supremum r x. Proof. apply: (finite_set_induction2 (A:=fun x => (sub x (substrate r)))). move => a asr;rewrite -/(singleton a). have ar: inc a (substrate r) by apply: asr; fprops. by move: lr => [or lr1]; move: (lr1 _ _ ar ar) =>[p1 p2]. move=> a b xx yy zz. have p1: sub a (substrate r) by apply: sub_trans zz; fprops. have p2: inc b (substrate r) by apply: zz; fprops. have [c cs] := (xx p1 yy). exists (sup r c b);apply: (lattice_finite_sup1 lr p1 cs p2). Qed. Lemma lattice_finite_inf2 x: finite_set x -> sub x E -> nonempty x -> has_infimum r x. Proof. apply: (finite_set_induction2 (A:=fun x => (sub x (substrate r)))). move => a asr;rewrite -/(singleton a). have ar: inc a (substrate r) by apply: asr; fprops. by move: lr => [or lr1]; move: (lr1 _ _ ar ar) =>[p1 p2]. move=> a b xx yy zz. have p1: sub a (substrate r) by apply: sub_trans zz; fprops. have p2: (inc b (substrate r)) by apply: zz; fprops. have [c cs]:= (xx p1 yy). exists (inf r c b); apply: (lattice_finite_inf1 lr p1 cs p2). Qed. Lemma lattice_finite_sup3P x y: finite_set x -> nonempty x -> sub x E -> (gle r (supremum r x) y <-> (forall z, inc z x -> gle r z y)). Proof. move=> fsx nex xsr. have hs:= (lattice_finite_sup2 fsx xsr nex). have or: order r by case:lr. move: (supremum_pr or xsr hs) => [[p1 p2] p3]; split. move=> p4 z zx; move: (p2 _ zx) => p5; order_tac. move=> p4; apply: p3; split => //. move: nex=> [u ux]; move: (p4 _ ux) => p5; order_tac. Qed. Lemma lattice_finite_inf3P x y: finite_set x -> nonempty x -> sub x E -> (gle r y (infimum r x) <-> (forall z, inc z x -> gle r y z)). Proof. move=> fsx nex xsr. have hs:= (lattice_finite_inf2 fsx xsr nex). have or: order r by move: lr => [ok _]. have [[p1 p2] p3] := (infimum_pr or xsr hs). split; first by move=> p4 z zx; move: (p2 _ zx) => p5; order_tac. move=> p4; apply: p3; split => //. move: nex=> [u ux]; move: (p4 _ ux) => p5; order_tac. Qed. Lemma supremum_setU1 a b: sub a E -> has_supremum r a -> inc b E -> supremum r (a +s1 b) = sup r (supremum r a) b. Proof. move=> asr hsa bsr; move: lr => [or _]; symmetry; apply: supremum_pr2 =>//. by apply: lattice_finite_sup1 => //;apply: supremum_pr1. Qed. Lemma infimum_setU1 a b: sub a E -> has_infimum r a -> inc b E -> infimum r (a +s1 b) = inf r (infimum r a) b. Proof. move: lr => [or _]; move=> asr hsa bsr; symmetry; apply: infimum_pr2 => //. by apply: lattice_finite_inf1 => //;apply: infimum_pr1. Qed. Lemma sup_setU1 X a: sub X E -> nonempty X -> finite_set X -> inc a E -> supremum r (X +s1 a) = sup r (supremum r X) a. Proof. move => pb pc pd pe; apply:supremum_setU1 => //. by apply: lattice_finite_sup2. Qed. Lemma inf_setU1 X a: sub X E -> nonempty X -> finite_set X -> inc a E -> infimum r (X +s1 a) = inf r (infimum r X) a. Proof. move => pb pc pd pe; apply:infimum_setU1 => //. by apply: lattice_finite_inf2. Qed. End LatticeProps. (** ** EIII-4-5 Properties of finite character *) Definition finite_character s:= forall x, (inc x s) <-> (forall y, (sub y x /\ finite_set y) -> inc y s). Lemma finite_character_example r: order r -> finite_character(Zo (powerset (substrate r)) (fun z => total_order (induced_order r z))). Proof. move=> or s; split. move /Zo_P => [] /setP_P sr tor y [ys fsy];apply: Zo_i. have sys: (sub y (substrate r)) by apply: sub_trans sr. by apply /setP_P. have ->: (induced_order r y) = (induced_order (induced_order r s) y). by rewrite iorder_trans. apply: total_order_sub =>//; aw. move=> h. have p1: sub s (substrate r). move=> t ts; set (y:= singleton t). have p1: (sub y s) by rewrite/y; apply: set1_sub. have p2: (finite_set y) by rewrite /y; apply: set1_finite. have p3: (sub y s /\ finite_set y) by split => //. move: (h _ p3) => /Zo_P [] /setP_P ysr _. apply: ysr; rewrite /y; fprops. apply: Zo_i; first by apply /setP_P. move: (iorder_osr or p1) => [pa pb]. split => //; rewrite pb. move=> x y xs ys; rewrite /ocomparable. set (z:= doubleton x y). have p2: (sub z s /\ finite_set z). by split; rewrite /z; [ apply: sub_set2 |apply: set2_finite]. move: (h _ p2) => /Zo_P [] /setP_P zsr [oz]; aw => toz. case: (toz _ _ (set2_1 x y) (set2_2 x y)) => h1; [left | right]; apply /iorder_gleP => //; exact: (iorder_gle1 h1). Qed. Lemma maximal_inclusion s: finite_character s -> nonempty s -> exists x, maximal (sub_order s) x. Proof. move=>fs nes. have es: inc emptyset s. move: nes=> [x]; rewrite fs=> aux; apply: aux. split; [ fprops | apply: emptyset_finite]. set (E:=union s). have sp: (sub s (powerset E)) by move=> t ts; apply /setP_P; apply: setU_s1. apply: (maximal_in_powerset(A:=s) (F:=E)) =>//. move=> u tou us. rewrite fs; move=> y [ysu fsy]. case: (emptyset_dichot y) => yne; try ue. set(Zy:= fun a => choose (fun b=> inc a b /\ inc b u)). have Zyp: (forall a, inc a y -> (inc a (Zy a) /\ inc (Zy a) u)). move=> a ay; rewrite /Zy; apply choose_pr. by move: (ysu _ ay)=> aux; move: (setU_hi aux) => [v pa pb]; exists v. set (Zz:= fun_image y Zy). have fsZz: (finite_set Zz) by rewrite /Zz; apply: finite_fun_image. move: (sub_osr Zz) => []; set r:=(sub_order Zz) => pa pb. have tor: (total_order r). split => //; rewrite pb /r /ocomparable;move=> a b aZz bZz. have au: (inc a u) by move: aZz => /funI_P [z /Zyp [_ zy] ->]. have bu: (inc b u) by move: bZz => /funI_P [z /Zyp [_ zy] ->]. case: (tou _ _ au bu) =>h; [left | right]; apply /ordo_leP;split => //. have fsr: (finite_set (substrate r)) by ue. have ner: nonempty (substrate r). move: yne=> [w wy]; exists (Zy w) ; rewrite pb; apply /funI_P; ex_tac. move: (finite_set_torder_greatest tor fsr ner) => [x [xsr xgr]]. have ysr: (sub y x). move => t ty. have aux: (inc (Zy t)(substrate r)) by rewrite pb; apply /funI_P; ex_tac. move /ordo_leP: (xgr _ aux). move: (Zyp _ ty)=> [tZ _] [_ _ Zx]; apply: Zx =>//. rewrite fs; move=> z [zy fsz]; move: (sub_trans zy ysr) => zx. move: xsr; rewrite pb; move /funI_P=> [w wy Zyw]. move: (Zyp _ wy); rewrite - Zyw; move => [_ xu]. by move: (us _ xu); rewrite fs; apply. Qed. Lemma maximal_inclusion_aux: let s := emptyset in finite_character s /\ ~ (exists x, maximal (sub_order s) x). Proof. split. move=> x; split; first by move => /in_set0. move=> h; have: (inc emptyset emptyset). apply: h;split; [ fprops | apply: emptyset_finite]. by move /in_set0. by move=> [x [xe _]]; move: xe;rewrite (proj2 (sub_osr _))=> /in_set0. Qed. Fixpoint nat_to_B (n:nat) := if n is m.+1 then csucc (nat_to_B m) else \0c. Lemma nat_to_B_succ n: csucc (nat_to_B n) = (nat_to_B n.+1). Proof. by done. Qed. Lemma nat_to_B_Nat n: natp (nat_to_B n). Proof. elim :n; first by simpl; fprops. by move=> n nN /=; apply: NS_succ. Qed. Lemma nat_to_B_injective: injective nat_to_B. Proof. elim. elim => // n h /= es; move: (@succ_nz (nat_to_B n)); rewrite -es //. move => n h; elim => [/= es | m h1 /= aux]. by move: (@succ_nz (nat_to_B n)); rewrite es. have cn := (CS_nat (nat_to_B_Nat n)). have cm:= (CS_nat (nat_to_B_Nat m)). congr (_ .+1); apply: h;exact: (succ_injective1 cn cm aux). Qed. Lemma nat_to_B_surjective x: natp x -> exists n, x = nat_to_B n. Proof. move: x; apply: Nat_induction. by exists 0. by move=> n nN [m mv]; exists m.+1 ; rewrite mv //. Qed. (* Inverse function of nat_to_B via the axiom of choice *) Fact nonempty_nat: inhabited nat. Proof. exact (inhabits 0). Qed. Definition B_to_nat x := (chooseT (fun y => x = nat_to_B y) nonempty_nat). Lemma B_to_nat_pa x: natp x -> (nat_to_B (B_to_nat x)) = x. Proof. move => H; symmetry. apply:(chooseT_pr nonempty_nat (nat_to_B_surjective H)). Qed. Lemma B_to_nat_pb p : B_to_nat (nat_to_B p) = p. Proof. exact: (nat_to_B_injective (B_to_nat_pa (nat_to_B_Nat p))). Qed. Lemma nat_to_B_sum x y: nat_to_B (x + y) = nat_to_B x +c nat_to_B y. Proof. elim: y => [|n hrec /=]. rewrite addn0 csum0r //; exact (CS_nat (nat_to_B_Nat x)). by rewrite (csum_nS _ (nat_to_B_Nat n)) addnS - hrec. Qed. Lemma nat_to_B_prod x y: nat_to_B (x * y) = nat_to_B x *c nat_to_B y. Proof. elim: y =>[| n hrec /=]; first by rewrite muln0 cprod0r. by rewrite (cprod_nS _ (nat_to_B_Nat n)) mulnS nat_to_B_sum hrec csumC. Qed. Lemma nat_to_B_pow x y: nat_to_B (x ^ y) = nat_to_B x ^c nat_to_B y. Proof. elim: y =>[| n hrec /=]; first by rewrite cpowx0 //=; exact succ_zero. by rewrite (cpow_succ _ (nat_to_B_Nat n)) expnS nat_to_B_prod hrec cprodC. Qed. Lemma nat_to_B_le x y: x <=y <-> nat_to_B x <=c nat_to_B y. Proof. split. move /subnKC => h; move: (nat_to_B_sum x (y - x)); rewrite h => ->. apply: csum_M0le; apply: CS_nat; apply: nat_to_B_Nat. move/cdiff_pr. set z := (nat_to_B y -c nat_to_B x). have zb: natp z by apply: NS_diff; apply: nat_to_B_Nat. have [u ->]:= (nat_to_B_surjective zb). rewrite - nat_to_B_sum => /nat_to_B_injective <-. apply:leq_addr. Qed. Lemma nat_to_B_lt x y: x < y <-> nat_to_B x // /clt0. move => y; rewrite ltnS /=; apply: (iff_trans ( nat_to_B_le x y)). apply:iff_sym;apply:(cltSleP (nat_to_B_Nat y)). Qed. Lemma nat_to_B_diff x y: nat_to_B (x - y) = nat_to_B x -c nat_to_B y. Proof. case: (ltnP x y) => p1. move: (ltnW p1) => p2. have -> /= : x -y = 0 by apply /eqP. rewrite /cdiff. by move / nat_to_B_le : p2 => [_ _ /setC_T ->]; rewrite cardinal_set0. rewrite - {2}(subnK p1) nat_to_B_sum cdiff_pr1 //; apply:nat_to_B_Nat. Qed. Lemma nat_to_B_max a b: nat_to_B (maxn a b) = cmax (nat_to_B a) (nat_to_B b). Proof. case /orP: (leq_total a b) => lab;move/nat_to_B_le: (lab) => lac. by rewrite (cmax_xy lac); move/maxn_idPr: lab => ->. by rewrite (cmax_yx lac); move/maxn_idPl: lab => ->. Qed. Lemma nat_to_B_min a b: nat_to_B (minn a b) = cmin (nat_to_B a) (nat_to_B b). Proof. case /orP: (leq_total a b) => lab;move/nat_to_B_le: (lab) => lac. by rewrite (cmin_xy lac); move/minn_idPl: lab => ->. by rewrite (cmin_yx lac); move/minn_idPr: lab => ->. Qed. (** Canonical ordering of pairs of ordinals *) Definition ordinal_pair x := [/\ pairp x, ordinalp (P x) & ordinalp (Q x)]. Definition ord_pair_le x y:= [/\ ordinal_pair x, ordinal_pair y & ((P x) \cup (Q x) ((P x <=o Q x) /\ ((P x) \cup (Q x) = Q x)) \/ ((Q x <=o P x) /\ ((P x) \cup (Q x) = P x)). Proof. move=> [px op oq]; case:(oleT_ee op oq)=> h ; [left | right ]; split => //. move: h => [_ _ ss]; by apply /setU2id_Pl. move: h => [_ _ ss]; by apply /setU2id_Pr. Qed. Lemma ordering_pair2 x: ordinal_pair x -> ordinalp ((P x) \cup (Q x)). Proof. by move=> h; case: (ordering_pair1 h) => [][[ ha hb _] pb]; rewrite pb. Qed. Lemma ordering_pair3 x y : ord_pair_le x y -> inc x (coarse (osucc (((P y) \cup (Q y))))). Proof. move=> [px py le]; apply /setX_P. move: (ordering_pair2 py) => oo; move: (OS_succ oo) => soo. suff: inc (P x) (osucc (P y \cup Q y)) /\ inc (Q x) (osucc (P y \cup Q y)). by move => [pa pb]; split => //;move:px => [ok _]. case: le => [][le aux]. case: (ordering_pair1 px); move => [pa pb]; rewrite pb in le; split;apply /(oltP soo); apply /oltSleP => //; apply:(oleT pa le). case: (ordering_pair1 px); move=> [pa pb]; split;apply /(oltP soo); apply /oltSleP => //; rewrite -le pb => //;apply:(oleR (proj32 pa)). Qed. Lemma ordering_pair4 x: ordinal_pair x -> ord_pair_le x x. Proof. move => op; hnf; split => //; right; split => //; right; split => //. by move:op => [_ _ ok]; apply: oleR. Qed. Lemma well_ordering_pair: worder_r ord_pair_le. Proof. move: ordering_pair4 => or1. have oR: reflexive_rr ord_pair_le. by move => x y [p1 p2 _]; split; apply: or1. have oA: antisymmetric_r ord_pair_le. move => x y [p1 p2 p3] [_ _ q3]; case: p3 => p3; case: q3 => q3. + by move: q3 => [q3 _]; case: (oltNge p3 q3). + by move: q3 => [q3 _]; rewrite q3 in p3; case: p3. + by move: p3 => [p3 _]; rewrite p3 in q3; case: q3. + move: p3 => [p31 p32]; move: q3 => [q31 q32]. case: p32 => p32; case: q32 => q32. - by move: q32 => [q32 _];case: (oltNge p32 q32). - by move: q32 => [q32 _]; rewrite q32 in p32; case: p32. - by move: p32 => [p32 _]; rewrite p32 in q32; case: q32. - move: p32 => [pa pb]; move: q32 => [_ pc]. move: p1 p2 => [px _ _][py _ _]; apply: pair_exten => //. by apply:oleA pb pc. split. split => //. move => a b c [p1 p2 p3] [q1 q2 q3]. split ; [exact | exact | ]. case: p3 => p3; case: q3 => q3. - by left; apply: (olt_ltT p3 q3). - move: q3 => [q3a q3b];case: q3b => q3b; first by rewrite q3a in p3; left. move: q3b => [q4 q5]; left;ue. - by move: p3 => [p31 p32]; rewrite -p31 in q3; left. - move: p3 q3 => [p3 p4] [q3 q4]; right; split => //; first by ue. case:p4=> p4. left; case: q4; move => [q4 q5]; [ apply:olt_leT p4 q4 |ue ]. move: p4 => [ -> p4]. case: q4; [by left| move=> [p5 p6];right;split => //;apply:oleT p4 p6]. move => x cx [x0 x0x]. set S1:= fun_image x (fun z => (P z) \cup (Q z)). have os1: ordinal_set S1. move=> t /funI_P [z zx ->]. move:(cx _ zx) => [pz _ _]; case: (ordering_pair1 pz); move=> [[pa1 pa2 _] pb]; rewrite pb //. have nes1: nonempty S1 by exists ((P x0) \cup (Q x0)); apply /funI_P; ex_tac. move: (ordinal_setI nes1 os1); set gamma:= intersection S1 => gs1. have g1: forall z, inc z x -> gamma <=o ((P z) \cup (Q z)). move => z zx. have aa: inc ((P z) \cup (Q z)) S1 by apply /funI_P; ex_tac. move: (os1 _ aa) => ou; split => //. by apply os1. by apply: setI_s1. move: gs1 => /funI_P [g0 g0x g0v]. set S2:= fun_image (Zo x (fun z => (P z) \cup (Q z) = gamma)) P. have nes2: nonempty S2. by apply: funI_setne; exists g0 => //; apply: Zo_i. have os2: ordinal_set S2. move =>t /funI_P [z /Zo_S zx]. by move: (cx _ zx) => [[ _ aa _] _ _] ->. move: (ordinal_setI nes2 os2); set alpha:= intersection S2 => as1. have a1: forall z, inc z x ->(gamma z zx; move: (g1 _ zx) => le1. case: (equal_or_not gamma ((P z) \cup (Q z))) => eq; last by left. have pa: inc (P z) S2 by apply/funI_P; exists z => //; apply: Zo_i => //. by right;split => //; hnf; split; fprops;apply: setI_s1. move: as1 => /funI_P [a0 /Zo_P [a0x ba] qa]. set S3 := fun_image (Zo x (fun z => (P z) \cup (Q z) = gamma /\ (P z) = alpha)) Q. have neS3: nonempty S3. by apply: funI_setne; exists a0 => //; apply: Zo_i. have os3: ordinal_set S3. move =>t /funI_P [z /Zo_P [pa _] ->]. by move: (cx _ pa) => [[_ qb qc] _]. move: (ordinal_setI neS3 os3); set beta:= intersection S3 => as2. move: as2 => /funI_P [b0 /Zo_P [b0x [pd pb]] pc]. exists b0; hnf. rewrite (graph_on_sr cx); split => //. move=> t tx; apply /graph_on_P1;split => //;split => //. by move: (cx _ b0x) => [ok _]. by move: (cx _ tx) => [ok _]. case: (a1 _ tx); first by rewrite pd => h; left. rewrite pd; move=> [pe pf]; right; split => //. rewrite pb; case: (equal_or_not alpha (P t)) => eq1; last by left. right; split => //; hnf; split => //. by move: (cx _ b0x) => [[_ _ ra] _]. by move: (cx _ tx) => [[_ _ ra] _]. have pg: inc (Q t) S3 by apply/funI_P; exists t => //; apply: Zo_i => //. rewrite - pc; apply (setI_s1 pg). Qed. Lemma infinite_product_aux k: infinite_c k -> (forall z, infinite_c z -> z z *c z = z) -> let lo:= graph_on ord_pair_le (product k k) in k *c k = k /\ exists2 f, bijection_prop f (product k k) k & (forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) ik hrec lo. move: (ik) => [[ok _] _]; move: (ik) => [ck _]. have pa: (forall a, inc a (product k k) -> ord_pair_le a a). move => a /setX_P [pa p1a p2a]; apply: ordering_pair4; hnf;split => //. apply: (ordinal_hi ok p1a). apply: (ordinal_hi ok p2a). move: (wordering_pr well_ordering_pair pa); rewrite -/lo; move=> [los low]. move: (OS_ordinal los) (ordinal_o_is los)=> ot [f oisf]. move: (oisf) => [or1 or2 [bf sf tf] isf]. rewrite (ordinal_o_sr (ordinal lo)) in tf. move: (bf) => [injf [ff sjf]]. have fp1: forall a, inc a (source f) -> ordinalp (Vf f a). move => a asf; move: (Vf_target ff asf); rewrite tf. apply: (ordinal_hi ot). have oifp: forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) a b asf bsf; apply:(iff_trans (order_isomorphism_siso oisf asf bsf)). split. move => [] /ordo_leP [_ _ qa] pb; split => //;split;fprops. move => [[_ _ qd] qa]; split => //. by apply/ordo_leP;split => //;rewrite - tf; apply: (Vf_target ff). have otf: ordinalp (target f) by ue. have pb: forall t, inc t (source f) -> cardinal (Vf f t) = cardinal (Zo (source f) (fun z => (glt lo z t))). move => t tsf; symmetry;apply /card_eqP. set A := (Zo (source f) ((glt lo)^~ t)). have As: sub A (source f) by apply Zo_S. move: (Vf_target ff tsf) => wt. have ra: restriction2_axioms f A (Vf f t). split => //; [by apply (ordinal_transitive otf wt) | move => w ]. move => /(Vf_image_P ff As) [u /Zo_P [usf lt] ->]. by move: lt; rewrite (oifp _ _ usf tsf); move /oltP0 =>[_ _]. move: (restriction2_fi injf ra). set g := restriction2 f A (Vf f t) => injg. have sg: source g = A by rewrite /g/restriction2; aw. have tg: target g = Vf f t by rewrite /g/restriction2; aw. exists g; split => //; split => //; split; first by fct_tac. rewrite sg tg; move=> y ytg. move: (ordinal_transitive otf wt ytg) => ytf. move: (sjf _ ytf) => [w wsf wv]; move: (fp1 _ tsf) => ow. have wa: inc w A. by apply: Zo_i => //; rewrite (oifp _ _ wsf tsf) wv; apply /oltP. exists w => //; rewrite restriction2_V //. have pc: forall t, inc t (source f) -> cardinal (Vf f t) t tsf; rewrite (pb _ tsf). set S := (Zo (source f) ((glt lo)^~ t)). have qa: sub S (coarse (osucc (((P t) \cup (Q t))))). move => v /Zo_P [vs [/graph_on_P1 [_ _ le] _]]; exact (ordering_pair3 le). move: (sub_smaller qa). move: tsf; rewrite sf low => tsf1. set a := (osucc ((P t) \cup (Q t))). rewrite /coarse - cprod2_pr1 - cprod2cl - cprod2cr. move=> le1; apply: (cle_ltT le1). case: (finite_dichot (CS_cardinal a)) => fca. apply: finite_lt_infinite => //. by apply /NatP; apply: NS_prod; fprops. have ak : a //. move: (infinite_card_limit2 ik) => [_ _]; apply. move: (tsf1) => /setX_P [_ i1 i2]. by case: (ordering_pair1 (proj31 (pa _ tsf1))); move => [cd ->]. move: ak (ak) => [[oa _ _] _]. move/ (ocle2P ck oa) => cak. move: (oclt cak) => lt1. by rewrite (hrec _ fca lt1). have pd: sub (ordinal lo) k. move => t; rewrite - tf => ttf; move: (sjf _ ttf) => [v vsf <-]. apply/(oltP ok) /(ocle2P ck (fp1 _ vsf)). exact: (pc _ vsf). move: (card_bijection bf); rewrite sf low - cprod2_pr1 => pe. have okok: ordinal lo = k. ex_middle xx. have /(ocle2P ck otf) : target f //; rewrite tf => //. move: (cleNgt (cprod_M1le ck (infinite_nz ik))); rewrite pe //. rewrite tf okok (card_card ck) in pe. split => //;exists f => //; split => //; ue. Qed. Lemma infinite_product_alt x : infinite_c x -> x *c x = x. Proof. move => ic; ex_middle bad. pose p z:= infinite_c z /\ z *c z <> z. have px: p x by split. have ox: ordinalp x by move: ic => [[ox _] _]. move: (least_ordinal4 ox px); set k := least_ordinal p x. move=> [ok [ik nkk kl]]; case: nkk. have kl0: forall z, infinite_c z -> z z *c z = z. move => z icz zk; ex_middle neq. case: (oltNge zk (kl _ (proj1 (proj1 icz)) (conj icz neq))). by move: (infinite_product_aux ik kl0) => [ xx _ ]. Qed. Lemma infinite_product_prop2 k: infinite_c k -> let lo:= graph_on ord_pair_le (product k k) in exists2 f, bijection_prop f (product k k) k & (forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) ik. have pa: (forall z, infinite_c z -> z z *c z = z). by move =>z iz _ ; apply: infinite_product_alt. by move: (infinite_product_aux ik pa) => [ _ ]. Qed. Lemma succ_study (r: relation) x (r' := fun a b => r a b /\ a <> b) (Ap := fun y A => forall t, inc t A <-> [/\ r x t, r t y & t <> x]) (Ax:= fun y => exists A, Ap y A) (Ay := fun y => choose (Ap y)) (ly := fun y => the_least (graph_on r (Ay y))): worder_r r -> (forall y, r' x y -> Ax y) -> [/\ (r x x -> ~ (exists y, r' x y) -> forall t, r t t -> r t x), (forall y, r' x y -> r' x (ly y)) , (forall y, r' x y -> forall t, r' x t -> r (ly y) t) & (forall y y', r' x y -> r' x y' -> ly y = ly y')]. Proof. move => wor; move: (wor) => [[ha hb hc] hd] h2. have h3: forall y, r' x y -> Ap y (Ay y). by move => y /h2 ax; apply: choose_pr. have h4: forall y, r' x y -> inc y (Ay y). move => y ya; move:(h3 _ ya) => h; apply/h. by move: ya => [rxy /nesym xny]; split => //; move: (hc _ _ rxy)=> []. have h5: forall y, r' x y -> has_least (graph_on r (Ay y)). move => y ya; move: (h3 _ ya) (h4 _ ya) => yb yc. apply:hd; [by move => t /yb [/hc []] | ex_tac ]. have h6: forall y, r' x y -> order_on (graph_on r (Ay y)) (Ay y). move => y ya; move: (h3 _ ya) => yb. have rr:{inc (Ay y), reflexive_r r} by move => t /yb [/hc []]. by move:(wordering_pr wor rr) => [[qa _] qb]. have h7:forall y, r' x y -> least (graph_on r (Ay y)) (ly y). move => y ya; move: (h6 _ ya) => [oR sR]; apply: the_least_pr => //. exact: h5. have h8: forall y, r' x y -> r' x (ly y). move => y ya; move: (h7 _ ya); rewrite /least (proj2 (h6 _ ya)). by move =>[ /(h3 _ ya) [ua _ /nesym ub] _]; split. have h9: forall y, r' x y -> forall t, r' x t -> r (ly y) t. move => y ya t ta. move: (h7 _ ya); rewrite /least (proj2 (h6 _ ya)); move => [_ yb]. move: (yb _ (h4 _ ya)) => /graph_on_P1 [_ _ yc]. have ryy:=(proj2 (hc _ _ (proj1 ya))). have rtt:= (proj2 (hc _ _ (proj1 ta))). case: (worderr_total wor ryy rtt) => cyt. exact (ha _ _ _ yc cyt). have: inc t (Ay y) by move:ta => [t1 /nesym t2];apply/(h3 _ ya). by move/yb => /graph_on_P1 [_ _]. split => //. + move => rxx ney t rtt. case:(equal_or_not x t) => exy; first by rewrite exy. case: (worderr_total wor rxx rtt) => // rxt. by case: ney; exists t; split. + move => y y' ya yb. exact (hb _ _ (h9 _ ya _ (h8 _ yb)) (h9 _ yb _ (h8 _ ya))). Qed. Lemma limit_study (r: relation) y B (C := B +s1 y) (R := (graph_on r C)) (x := supremum R B): (forall a, inc a B <-> r a y /\ a <> y) -> worder_r r -> r y y -> [/\ (least_upper_bound R B x /\ r x y), (B = emptyset -> forall t, r t t -> r y t), ( x <> y -> [/\ inc x B, x = the_greatest (graph_on r B), (forall z, r x z -> r z y -> z = x \/ z = y) & (forall z, r z z -> r z x \/ r y z)]) & (x = y -> forall B1, nonempty B1 -> finite_set B1 -> sub B1 B -> inc (the_greatest (graph_on r B1)) B)]. Proof. move => hB wor ryy. move:(wor) => [ [ha hb hc] _]. have hd: {inc B, reflexive_r r} by move => t /hB [/hc []]. have he: {inc C, reflexive_r r}. move => t /setU1_P []; [by apply:hd | by move -> ]. have sBC: sub B C by apply:sub_setU1. have yC: inc y C by rewrite /C; fprops. have srB:= (graph_on_sr hd). move:(wordering_pr wor he) => [woR sr]. have oR := proj1 woR. have pa: sub B (substrate (graph_on r C)) by rewrite graph_on_sr. have uy: upper_bound (graph_on r C) B y. split; first by rewrite sr. move => t tB;apply /graph_on_P1; split => //; first by apply sBC. by move/(hB t): tB => []. have hs:has_supremum (graph_on r C) B. by apply:(worder_hassup woR pa); exists y. have xp: least_upper_bound R B x by apply: (supremum_pr1 oR). move:(supremum_pr1 oR hs) => /(lubP oR pa) []; rewrite -/x => h1 h2. move: (h2 _ uy) => /graph_on_P1 [_ _ rxy]. have pb: forall t, inc t B -> r t x. by move => t /(proj2 h1) /graph_on_P1 []. have pc: x <> y -> [/\ inc x B, x = the_greatest (graph_on r B), (forall z, r x z -> r z y -> z = x \/ z = y) & (forall z, r z z -> r z x \/ r y z)]. move => xz. have xB: inc x B by apply/hB. move:(supremum_pr1 oR hs) => /(lubP oR pa) [hh _]. move: hh; rewrite -/x; move => [_ hx]. have orB: order (graph_on r B) by apply: (order_from_rel B (proj1 wor)). have xgr: x = the_greatest (graph_on r B). symmetry;apply: (the_greatest_pr2 orB); hnf; rewrite srB; split => //. move => t tB; move/hB: (tB)=> [qa qb]; apply /graph_on_P1; split => //. by move:(hx _ tB) => /graph_on_P1 []. have hh:forall z, r z z -> r z x \/ r y z. move => z rzz; case (equal_or_not z y) => ezy; first by rewrite ezy; right. case: (worderr_total wor ryy rzz) => czy; first by right. have zB: inc z B by apply/hB. by move: (hx _ zB) => /graph_on_P1 [ _ _ rzx]; left. split => // t t1 t2; case (equal_or_not t y) => ty; first by right. have tB: inc t B by apply /hB. by move:(hx _ tB) => /graph_on_P1 [_ _ t3]; rewrite (hb _ _ t1 t3); left. have pd: B = emptyset -> forall t, r t t -> r y t. move => be t rtt. case (equal_or_not t y) => ty; first by ue. case: (worderr_total wor ryy rtt) => // czy. empty_tac1 t; by apply/hB. split => // exy B1 neB1 fsB1 sb1. have hf : {inc B1, reflexive_r r} by move => t/sb1 /hd. move:(wordering_pr wor hf) => [wos ss]. move:(worder_total wos) => tos. have ss1: sub B1 (substrate (graph_on r B1)) by rewrite ss. move: (finite_subset_torder_greatest tos fsB1 ss1 neB1). rewrite -{2} ss (iorder_substrate (proj1 tos)) => hgt. move:(the_greatest_pr (proj1 tos) hgt) => []; rewrite ss => r0 _. by apply: sb1. Qed. End FiniteSets. Export FiniteSets.