(** * Theory of Sets EIII-4 Natural integers. Finite sets Copyright INRIA (2009) Apics Team (Jose Grimm). *) Require Export set2. Require Export set3. Require Export set4. Require Export set5. Require Export set6. Require Export set7. Set Implicit Arguments. (* $Id: set8.v,v 1.64 2010/08/02 07:30:56 grimm Exp $ *) Import Correspondence. Import Bfunction. Import Border. Import Worder. Import Cardinal. Module FiniteSets. (** ** EIII-4-1 Definition of integers *) Definition succ x := card_plus x card_one. Definition is_finite_c x := is_cardinal x & x <> succ x. Definition is_finite_set x := is_finite_c (cardinal x). Definition card_three := succ card_two. Definition card_four := succ card_three. Lemma integer_is_cardinal: forall x, is_finite_c x -> is_cardinal x. Proof. ir. nin H. am. Qed. Hint Resolve integer_is_cardinal: fprops. Lemma cardinal_succ_pr0: forall a b, equipotent a b -> succ a = succ b. Proof. ir. uf succ. app cardinal_sum_pr2. fprops. Qed. Lemma succ_is_cardinal: forall a, is_cardinal (succ a). Proof. ir. uf succ. fprops. Qed. Lemma cardinal_succ: forall a, cardinal (succ a) = succ a. Proof. ir. pose (succ_is_cardinal a). fprops. Qed. Lemma is_finite_succ1: forall x, is_finite_c x -> is_finite_c (succ x). Proof. ir. nin H. pose (succ_is_cardinal x). split. am. dneg. ap (succ_injective H i H1). Qed. Theorem is_finite_succ: forall x, is_cardinal x -> (is_finite_c x) = (is_finite_c (succ x)). Proof. ir. ap iff_eq; ir. app is_finite_succ1. nin H0. split. am. dneg. wrr H2. Qed. Lemma succ_cardinal: forall z, succ (cardinal z) = succ z. Proof. ir. app cardinal_succ_pr0. fprops. Qed. Lemma is_finite_succ2: forall x, is_finite_set x -> is_finite_c (succ x). Proof. ir. wr (succ_cardinal x). app is_finite_succ1. Qed. Lemma succ_zero: succ card_zero = card_one. Proof. ir. uf succ. aw. app cardinal1. Qed. Lemma is_finite0: is_finite_c card_zero. Proof. split. ap cardinal0. rw succ_zero. red. ir. symmetry in H. app (card_one_not_zero). Qed. Lemma is_finite1: is_finite_c card_one. Proof. wr succ_zero. app is_finite_succ1. app is_finite0. Qed. Lemma is_finite2: is_finite_c card_two. Proof. rw card_two_pr. change (is_finite_c (succ card_one)). app is_finite_succ1. app is_finite1. Qed. Lemma is_finite3: is_finite_c card_three. Proof. uf card_three. app is_finite_succ1. app is_finite2. Qed. Lemma is_finite4: is_finite_c card_four. Proof. uf card_four. app is_finite_succ1. app is_finite3. Qed. (** ** EIII-4-2 Inequalities between integers *) Lemma cardinal_le_when_complement1: forall a b, cardinal_le b a -> (exists c, is_cardinal c & card_plus b c = a). Proof. ir. assert (is_cardinal a). co_tac. assert (is_cardinal b). co_tac. rwii (cardinal_le_when_complement H0 H1) H. Qed. Lemma is_less_than_succ: forall a, is_cardinal a -> cardinal_le a (succ a). Proof. ir. uf succ. rww cardinal_le_when_complement. exists card_one. split. ap cardinal1. tv. fprops. Qed. Lemma is_finite_in_sum: forall a b, is_cardinal b -> is_finite_c (card_plus a b) -> is_finite_c b. Proof. ir. split. am. nin H0. dneg. uf succ. wr card_plus_associative. ufi succ H2. wrr H2. Qed. Lemma is_finite_in_sum2: forall a b, is_cardinal a -> is_finite_c (card_plus a b) -> is_finite_c a. Proof. ir. rwi card_plus_commutative H0. app (is_finite_in_sum H H0). Qed. Theorem le_int_is_int: forall a b, is_finite_c b -> cardinal_le a b -> is_finite_c a. Proof. ir. nin (cardinal_le_when_complement1 H0). nin H1. wri H2 H. assert (is_cardinal a). co_tac. ap (is_finite_in_sum2 H3 H). Qed. Definition predc n := choose (fun m => is_cardinal m & n = succ m). Lemma predc_pr0: forall n, is_cardinal n -> n <> card_zero -> (is_cardinal (predc n) & n = succ (predc n)). Proof. ir. uf predc. app choose_pr. assert (cardinal_le card_one n). app one_small_cardinal. nin (cardinal_le_when_complement1 H1). nin H2. symmetry in H3. exists x. split. am. uf succ. rww card_plus_commutative. Qed. Lemma predc_pr: forall n, is_finite_c n -> n <> card_zero -> (is_finite_c (predc n) & n = succ (predc n)). Proof. ir. assert (is_cardinal n). fprops. nin (predc_pr0 H1 H0). split. rww is_finite_succ. ue. am. Qed. Theorem exists_predc: forall n, is_finite_c n -> n <> card_zero -> exists_unique (fun m => is_finite_c m & n = succ m). Proof. ir. split. exists (predc n). app predc_pr. ir. ee. rwi H4 H3. ap succ_injective; fprops. Qed. Lemma finite_in_product: forall a b, is_cardinal a -> is_cardinal b -> b <> card_zero -> is_finite_c (card_mult a b) -> is_finite_c a. Proof. ir. nin (predc_pr0 H0 H1). rwi H4 H2. ufi succ H2. rwi cardinal_distrib_prod_sum3 H2. rwii one_unit_prodr H2. app (is_finite_in_sum H H2). Qed. Theorem lt_is_le_succ: forall a n, is_finite_c n -> cardinal_lt a (succ n) = cardinal_le a n. Proof. ir. ap iff_eq. ir. nin H0. nin (cardinal_le_when_complement1 H0). nin H2. assert (x <> card_zero). red. ir. rwi H4 H3. rwi zero_unit_sumr H3. au. co_tac. nin (predc_pr0 H2 H4). rwi H6 H3. assert (card_plus a (predc x) = n). app succ_injective. fprops. fprops. wrr card_plus_associative. wr H7. app sum_increasing3. co_tac. ir. red. nin H. pose (is_less_than_succ H). ee. co_tac. dneg. rwi H2 H0. co_tac. Qed. Hint Rewrite lt_is_le_succ : sw. Lemma is_lt_succ: forall n, is_finite_c n -> cardinal_lt n (succ n). Proof. ir. rww lt_is_le_succ. fprops. Qed. Lemma lt_is_le_succ1: forall a b, is_finite_c b -> cardinal_le a (succ b) -> a <> (succ b) -> cardinal_le a b. Proof. ir. wrr lt_is_le_succ. split; am. Qed. Lemma lt_n_succ_le1: forall a b, is_cardinal a -> is_finite_c b -> cardinal_le a b = cardinal_le (succ a) (succ b). Proof. ir. ap iff_eq. ir. uf succ. app sum_increasing2. cp cardinal1. fprops. ir. assert (cardinal_le a (succ a)). app is_less_than_succ. wrr lt_is_le_succ. split. co_tac. nin H0. dneg. wri H4 H1. assert (a = succ a). co_tac. wr H4. rwi H5 H4. sy. app succ_injective. Qed. Lemma succ_nonzero1:forall n, cardinal_le card_one (succ n). Proof. ir. wr succ_cardinal. uf succ. rw card_plus_commutative. app sum_increasing3. app cardinal1. fprops. Qed. Lemma succ_nonzero:forall n, succ n <> card_zero. Proof. ir. cp (succ_nonzero1 n). red. ir. rwi H0 H. apply zero_smallest1 with card_one. red. ee. am. ap card_one_not_zero. Qed. Lemma predc_pr1: forall n, is_cardinal n -> predc (succ n) = n. Proof. ir. cp (predc_pr0 (succ_is_cardinal n) (succ_nonzero (n:=n))). sy. ee. app succ_injective. Qed. Lemma succ_positive: forall a, cardinal_lt card_zero (succ a). Proof. ir. red. ee. app zero_smallest. app succ_is_cardinal. red. ir. symmetry in H. ap (succ_nonzero H). Qed. Lemma zero_lt_one: cardinal_lt card_zero card_one. Proof. wr succ_zero. app succ_positive. Qed. Lemma lt_n_succ_le0: forall a b, is_cardinal a -> is_finite_c b -> cardinal_le (succ a) b = cardinal_lt a b. Proof. ir. sy. nin (equal_or_not b card_zero). rw H1. ap iff_eq. ir. elim (zero_smallest1 H2). ir. assert (cardinal_lt (succ a) card_zero). split. am. ap (succ_nonzero (n:=a)). elim (zero_smallest1 H3). nin (predc_pr H0 H1). rw H3. wrr lt_n_succ_le1. srw. Qed. Hint Rewrite lt_n_succ_le0 : sw. Lemma sub_finite_set: forall x y, sub x y -> is_finite_set y -> is_finite_set x. Proof. uf is_finite_set. ir. app (le_int_is_int H0 (sub_smaller H)). Qed. Lemma cardinal_succ_pr: forall a b, ~ (inc b a) -> cardinal (tack_on a b) = succ a. Proof. ir. wr (succ_cardinal a). cp (disjoint_with_singleton H). uf succ. uf tack_on. assert (equipotent a (cardinal a)). fprops. app card_plus_pr1. uf card_one. eqtrans (singleton emptyset). app singletons_equipotent. fprops. Qed. Lemma cardinal_succ_pr1: forall a b, cardinal (tack_on (complement a (singleton b)) b) = succ (cardinal (complement a (singleton b))). Proof. ir. rww cardinal_succ_pr. app cardinal_succ_pr0. fprops. app not_inc_complement_singleton. Qed. Lemma strict_sub_smaller: forall x y, sub x y -> is_finite_set y -> x<> y -> cardinal_lt (cardinal x) (cardinal y). Proof. ir. assert (strict_sub x y). split; am. nin (strict_sub_nonempty_complement H2). srwi H3. nin H3. set (z:= complement y (singleton y0)). assert (sub x z). red. ir. uf z. srw. split. app H. dneg. wrr (singleton_eq H6). pose (sub_smaller H5). assert (cardinal y = succ (cardinal z)). uf z. wr cardinal_succ_pr1. wrr tack_on_complement. rw H6. srw. assert (sub z y). uf z. app sub_complement. ap (sub_finite_set H7 H0). Qed. Lemma emptyset_finite: is_finite_set emptyset. Proof. red. rw cardinal_zero. app is_finite0. Qed. Lemma strict_sub_smaller1: forall y, (forall x, sub x y -> x<> y -> cardinal_lt (cardinal x) (cardinal y)) -> is_finite_set y. Proof. ir. nin (emptyset_dichot y). rw H0. app emptyset_finite. nin H0. set (z:=complement y (singleton y0)). assert (sub z y). uf z. app sub_complement. assert (y = tack_on z y0). uf z. app tack_on_complement. cp (cardinal_succ_pr1 y y0). fold z in H3. wri H2 H3. assert (z <> y). red. ir. assert (inc y0 z). ue. ufi z H5. srwi H5. ee. elim H6. fprops. cp (H _ H1 H4). rwi H3 H5. nin H5. red. rw H3. wrr is_finite_succ. split; fprops. fprops. Qed. Lemma finite_image: forall f, is_function f -> is_finite_set (source f) -> is_finite_set (image_of_fun f). Proof. ir. cp (image_smaller_cardinal H). red. red in H0. ap (le_int_is_int H0 H1). Qed. Lemma finite_image_by: forall f A, is_function f -> sub A (source f) -> is_finite_set A -> is_finite_set (image_by_fun f A). Proof. ir. set (g:= restriction1 f A). assert (surjective g). uf g. app restriction1_surjective. nin H2. assert (image_of_fun g = image_by_fun f A). ue. uf g. uf restriction1. aw. wr H4. app finite_image. uf g. uf restriction1. aw. Qed. Lemma finite_fun_image: forall a f, is_finite_set a -> is_finite_set (fun_image a f). Proof. ir. assert (surjective (BL f a (fun_image a f))). app bl_surjective. red. ir. aw. exists c. auto. ir. awi H0. am. nin H0. awi H1. wr H1. app finite_image. aw. Qed. Lemma finite_range: forall f, fgraph f -> is_finite_set(domain f) -> is_finite_set(range f). Proof. ir. assert (is_function (corresp (domain f) (range f) f)). app is_function_pr. fprops. assert (range f = image_of_fun (corresp (domain f)(range f) f)). uf image_of_fun. aw. wrr image_by_graph_domain. fprops. rw H2. app finite_image. aw. Qed. Lemma finite_graph_domain: forall f, fgraph f -> is_finite_set f -> is_finite_set (domain f). Proof. ir. uf domain. app finite_fun_image. Qed. Lemma finite_graph_range: forall f, fgraph f -> is_finite_set f -> is_finite_set (range f). Proof. ir. uf range. app finite_fun_image. Qed. Lemma finite_domain_graph: forall f, fgraph f -> is_finite_set (domain f) -> is_finite_set f. Proof. ir. wrr L_recovers. uf L. app finite_fun_image. Qed. Lemma bijective_if_same_finite_c_inj: forall f, cardinal (source f) = cardinal (target f) -> is_finite_set (source f) -> injective f -> bijective f. Proof. ir. split. am. split. fct_tac. ex_middle. assert (sub (image_of_fun f) (target f)). nin H1. app sub_image_target. assert (is_finite_set (target f)). red. wr H. exact H0. cp (strict_sub_smaller H3 H4 H2). nin H5. elim H6. transitivity (cardinal (source f)). symmetry. aw. red. exists (restriction_to_image f). ee. ap (restriction_to_image_bijective H1). uf restriction_to_image. uf restriction2. aw. uf restriction_to_image. uf restriction2. aw. am. Qed. Lemma sub_image_of_fun: forall f x, is_function f -> sub x (source f) -> sub (image_by_fun f x) (image_of_fun f). Proof. ir. uf image_by_fun. uf image_of_fun. app image_by_increasing. fprops. Qed. Lemma bijective_if_same_finite_c_surj: forall f, cardinal (source f) = cardinal (target f) -> is_finite_set (source f) -> surjective f -> bijective f. Proof. ir. nin (exists_right_inv_from_surj H1). cp (source_right_inverse H2). cp (right_inverse_injective H2). assert (source f = target x). nin H2. red in H2. ee; am. assert (cardinal (source x) = cardinal (target x)). rw H3. sy. ue. assert (is_finite_set (source x)). red. ue. ue. cp (bijective_if_same_finite_c_inj H6 H7 H4). nin H2. ee. assert (bijective (compose f x)). rw H9. app identity_bijective. app (bij_left_compose H2 H10 H8). Qed. (** ** EIII-6-1 The set of natural integers *) Definition is_infinite_c a := is_cardinal a & ~ (is_finite_c a). Definition infinite_set E := is_infinite_c (cardinal E). Lemma finite_lt_infinite: forall a b, is_finite_c a -> is_infinite_c b -> cardinal_lt a b. Proof. ir. nin H0. assert (is_cardinal a). fprops. nin (cardinal_le_total_order2 H0 H2). elim H1. ap (le_int_is_int H H3). am. Qed. Lemma finite_le_infinite: forall a b, is_finite_c a -> is_infinite_c b -> cardinal_le a b. Proof. ir. nin (finite_lt_infinite H H0). am. Qed. Lemma S_inj_not_bij: injective (acreate S) & (~ surjective (acreate S)). Proof. split. red. split. app acreate_function. aw. ir. nin H. nin H0. subst. rwi acreate_W H1. rwi acreate_W H1. cp (R_inj H1). rww (eq_add_S _ _ H). red. ir. assert (inc (Ro 0) (target (acreate S))). aw. exists 0. tv. nin (surjective_pr2 H H0). simpl in H1. ee. symmetry in H2. awi H1. nin H1. subst. awi H0. rwi acreate_W H2. elim (O_S x0). ap (R_inj H2). Qed. Lemma nat_infinite_set: is_infinite_c (cardinal nat). Proof. red. split. fprops. red. ir. assert (cardinal (source (acreate S)) = cardinal (target (acreate S))). aw. fprops. assert (is_finite_set (source (acreate S))). aw. nin S_inj_not_bij. nin (bijective_if_same_finite_c_inj H0 H1 H2). auto. Qed. Definition Bnat := Zo(set_of_cardinals_le (cardinal nat)) (fun z => is_finite_c z). Lemma inc_Bnat: forall a, inc a Bnat = is_finite_c a. Proof. ir. uf Bnat. ap iff_eq; ir;Ztac. am. assert (is_cardinal (cardinal nat)). fprops. rw (set_of_cardinals_pr a H0). cp nat_infinite_set. ap (finite_le_infinite H H1). Qed. Opaque Bnat. Hint Rewrite inc_Bnat : bw. Lemma inc_Bnat_prop: forall a, inc a Bnat -> is_finite_c a. Proof. ir. bwi H. am. Qed. Definition Bnat_order := graph_on cardinal_le Bnat. Definition Bnat_le x y := inc x Bnat & inc y Bnat & cardinal_le x y. Definition Bnat_lt x y := Bnat_le x y & x<>y. Lemma Bnat_is_cardinal: forall x, inc x Bnat -> is_cardinal x. Proof. ir. bwi H. nin H. am. Qed. Hint Resolve Bnat_is_cardinal inc_Bnat_prop : fprops. Lemma Bnat_order_substrate: substrate Bnat_order = Bnat. Proof. ir. assert (forall x, inc x Bnat -> is_cardinal x). ir. fprops. nin (wordering_cardinal_le_pr H). am. Qed. Lemma Bnat_order_worder: worder Bnat_order. Proof. ir. assert (forall x, inc x Bnat -> is_cardinal x). ir. fprops. nin (wordering_cardinal_le_pr H). am. Qed. Lemma Bnat_order_le: forall x y, gle Bnat_order x y = Bnat_le x y. Proof. ir. uf Bnat_order. aw. rww graph_on_rw1. Qed. Lemma inc0_Bnat: inc card_zero Bnat. Proof. bw. ap is_finite0. Qed. Lemma inc1_Bnat: inc card_one Bnat. Proof. bw. ap is_finite1. Qed. Lemma inc2_Bnat: inc card_two Bnat. Proof. bw. ap is_finite2. Qed. Lemma inc_succ_Bnat: forall x, inc x Bnat -> inc (succ x) Bnat. Proof. ir. bw. ap is_finite_succ1. fprops. Qed. Lemma le_int_in_Bnat: forall a b, cardinal_le a b -> inc b Bnat -> inc a Bnat. Proof. ir. bw. bwi H0. app (le_int_is_int H0 H). Qed. Hint Resolve inc0_Bnat inc1_Bnat inc2_Bnat inc_succ_Bnat: fprops. Lemma predc_pr2: forall n, inc n Bnat -> predc (succ n) = n. Proof. ir. assert (is_cardinal n). fprops. app predc_pr1. Qed. Lemma predc_pr3: forall n, inc n Bnat -> n = card_zero \/ exists m, inc m Bnat & n = succ m. Proof. ir. nin (equal_or_not n card_zero). au. bwi H. nin (predc_pr H H0). right. exists (predc n). split. bw. am. Qed. (** ** EIII-4-3 The principle of induction *) Lemma Bnat_wordered : forall X, sub X Bnat -> nonempty X -> inc card_zero X \/ (exists a, inc a Bnat & inc (succ a) X & ~ (inc a X)). Proof. ir. nin Bnat_order_worder. wri Bnat_order_substrate H. nin (H2 _ H H0). red in H3. awii H3. ee. rwi Bnat_order_substrate H. nin (predc_pr3 (H _ H3)). wr H5. au. right. nin H5. nin H5. ex_tac. wr H6. split. am. red. ir. cp (H4 _ H7). awii H8. rwi Bnat_order_le H8. red in H8. ee. bwi H5. cp (is_lt_succ H5). rwi H6 H10. co_tac. Qed. Lemma cardinal_c_induction_v: forall r:EP, (r card_zero) -> (forall n, inc n Bnat-> r n -> r (succ n)) -> (forall n, inc n Bnat -> r n). Proof. ir. set (X:= Zo Bnat (fun z => ~ (r z))). assert (sub X Bnat). uf X. app Z_sub. nin (p_or_not_p (r n)). am. assert (nonempty X). exists n. uf X. Ztac. nin (Bnat_wordered H2 H4). ufi X H5. Ztac. contradiction. nin H5. ufi X H5. ee. elim H7. Ztac. Qed. Lemma cardinal_c_induction: forall r:EP, (r card_zero) -> (forall n, is_finite_c n -> r n -> r (succ n)) -> (forall n, is_finite_c n -> r n). Proof. ir. assert (forall n, inc n Bnat -> r n -> r (succ n)). ir. app H0. fprops. app cardinal_c_induction_v. bw. Qed. Lemma cardinal_c_induction1: forall r:EP, let s:= fun n => forall p, is_finite_c n -> is_finite_c p -> cardinal_lt p n -> r p in (forall n, is_finite_c n -> s n -> r n) -> (forall n, is_finite_c n -> r n). Proof. ir. app H. app cardinal_c_induction. uf s. ir. elim (zero_smallest1 H3). ir. red. ir. srwi H5. nin (equal_or_not p n0). app H. rww H6. red in H2. app H2. red. au. am. Qed. Lemma cardinal_c_induction2: forall (r:EP) k, is_finite_c k -> r k -> (forall n, is_finite_c n -> cardinal_le k n -> r n -> r (succ n)) -> (forall n, is_finite_c n -> cardinal_le k n -> r n). Proof. ir. set (s:= fun n => (cardinal_le k n -> r n)). assert (s n). ap cardinal_c_induction. uf s. ir. wrr (zero_smallest2 H4). ir. red. nin (equal_or_not k (succ n0)). wr H6. ir. am. ir. cp (lt_is_le_succ1 H4 H7 H6). app H1. app H5. am. app H4. Qed. Lemma cardinal_c_induction3: forall (r:EP) a b, is_finite_c a -> is_finite_c b -> r a -> (forall n, cardinal_le a n -> cardinal_lt n b -> r n -> r (succ n)) -> (forall n, cardinal_le a n -> cardinal_le n b -> r n). Proof. ir. set (s:= fun n => (cardinal_le a n -> cardinal_le n b -> r n)). assert (s n). ap cardinal_c_induction. uf s. ir. wrr (zero_smallest2 H5). red. ir. nin (equal_or_not a (succ n0)). ue. cp (lt_is_le_succ1 H5 H7 H9). srwi H8; tv. app H2. app H6. red in H8. ee. am. fprops. ap (le_int_is_int H0 H4). app H5. Qed. Lemma cardinal_c_induction4: forall (r:EP) a b, is_finite_c a -> is_finite_c b -> r b -> (forall n, cardinal_le a n -> cardinal_lt n b -> r (succ n) -> r n) -> (forall n, cardinal_le a n -> cardinal_le n b -> r n). Proof. ir. set (q := fun n => ~ (r n)). nin (p_or_not_p (r n)). am. assert (is_finite_c n). app (le_int_is_int H0 H4). assert (forall m, cardinal_le n m -> cardinal_lt m b -> q m -> q (succ m)). ir. uf q. red. ir. elim H9. assert (cardinal_le a m). co_tac. ap (H2 _ H11 H8 H10). cp (cardinal_c_induction3 _ H6 H0 H5 H7). assert (q b). app H8. red in H0. ee. fprops. elim H9. am. Qed. Lemma Bnat_interval_cc_pr: forall a b x, inc a Bnat -> inc b Bnat -> inc x (interval_cc Bnat_order a b) = (Bnat_le a x & Bnat_le x b). Proof. ir. uf interval_cc. rw Bnat_order_substrate. app iff_eq. ir. Ztac. repeat wrr Bnat_order_le. ir. Ztac. ee. red in H1; ee; am. repeat rww Bnat_order_le. Qed. Lemma Bnat_interval_co_pr: forall a b x, inc a Bnat -> inc b Bnat -> inc x (interval_co Bnat_order a b) = (Bnat_le a x & Bnat_lt x b). Proof. ir. uf Bnat_lt. uf interval_co. rw Bnat_order_substrate. ap iff_eq. ir. Ztac. repeat wrr Bnat_order_le. ir. Ztac. ee. red in H1; ee; am. uf glt. repeat rww Bnat_order_le. Qed. Lemma Bnat_interval_cc_pr1: forall a b x, inc a Bnat -> inc b Bnat -> inc x (interval_cc Bnat_order a b) = (cardinal_le a x & cardinal_le x b). Proof. ir. rww Bnat_interval_cc_pr. uf Bnat_le. ap iff_eq. ir. intuition. ir. nin H1. set (le_int_in_Bnat H2 H0). intuition. Qed. Lemma Bnat_interval_co_pr1: forall a b x, inc a Bnat -> inc b Bnat -> inc x (interval_co Bnat_order a b) = (cardinal_le a x & cardinal_lt x b). Proof. ir. rww Bnat_interval_co_pr. uf Bnat_lt. uf Bnat_le. uf cardinal_lt. ap iff_eq. ir. intuition. ir. nin H1. nin H2. set (le_int_in_Bnat H2 H0). intuition. Qed. Lemma cardinal_c_induction3_v: forall (r:EP) a b, inc a Bnat -> inc b Bnat -> r a -> (forall n, inc n (interval_co Bnat_order a b) -> r n -> r (succ n)) -> (forall n, inc n (interval_cc Bnat_order a b) -> r n). Proof. ir. assert (forall n, cardinal_le a n -> cardinal_lt n b -> r n -> r (succ n)). ir. app H2. rw Bnat_interval_co_pr1. ee; am. am. am. rwii Bnat_interval_cc_pr1 H3. nin H3. bwi H. bwi H0. app (cardinal_c_induction3 r H H0). Qed. Lemma cardinal_c_induction4_v: forall (r:EP) a b, inc a Bnat -> inc b Bnat -> r b -> (forall n, inc n (interval_co Bnat_order a b) -> r (succ n) -> r n) -> (forall n, inc n (interval_cc Bnat_order a b) -> r n). Proof. ir. assert (forall n, cardinal_le a n -> cardinal_lt n b -> r (succ n) -> r n). ir. app H2. rw Bnat_interval_co_pr1. ee; am. am. am. rwii Bnat_interval_cc_pr1 H3. nin H3. bwi H. bwi H0. app (cardinal_c_induction4 r H H0). Qed. Lemma tack_on_finite: forall X x, is_finite_set X -> is_finite_set (tack_on X x). Proof. ir. nin (inc_or_not x X). ir. assert (tack_on X x= X). set_extens. rwi tack_on_inc H1. nin H1. am. rww H1. fprops. rww H1. ir. red. rww cardinal_succ_pr. red in H. app is_finite_succ2. Qed. Lemma singleton_finite: forall x, is_finite_set(singleton x). Proof. ir. red. rw cardinal_singleton. app is_finite1. Qed. Lemma doubleton_finite: forall x y, is_finite_set(doubleton x y). Proof. ir. assert (doubleton x y = tack_on (singleton x) y). set_extens. nin (doubleton_or H). rw H0. fprops. rw H0. fprops. rwi tack_on_inc H. nin H. rw (singleton_eq H). fprops. rw H. fprops. rw H. app tack_on_finite. ap singleton_finite. Qed. Lemma tack_if_succ_card: forall x n, is_cardinal n -> cardinal x = succ n -> exists u, exists v, x = tack_on u v & ~(inc v u) & cardinal u = n. Proof. ir. nin (emptyset_dichot x). rwi H1 H0. rwi cardinal_emptyset H0. symmetry in H0. elim (succ_nonzero H0). nin H1. assert (x = tack_on (complement x (singleton y)) y). app tack_on_complement. exists (complement x (singleton y)). exists y. ee. am. app not_inc_complement_singleton. cp (cardinal_succ_pr1 x y). wri H2 H3. rwi H0 H3. sy. app succ_injective. fprops. Qed. Lemma finite_set_induction0: forall s:EP, s emptyset -> (forall a b, s (a) -> ~(inc b a) -> s (tack_on a b)) -> forall x, is_finite_set x -> s x. Proof. ir. set (r:= fun n => forall x, cardinal x = n-> s x). assert (r card_zero). uf r. ir. rww (cardinal_nonemptyset H2). assert (forall n, is_finite_c n -> r n -> r (succ n)). ir. assert (is_cardinal n). fprops. red. ir. cp (tack_if_succ_card H5 H6). nin H7. nin H7. ee. rw H7. app H0. app H4. cp (cardinal_c_induction r H2 H3). cp (H4 _ H1). app H5. Qed. Lemma finite_set_induction: forall s:EP, s emptyset -> (forall a b, s (a) -> s (tack_on a b)) -> forall x, is_finite_set x -> s x. Proof. ir. app (finite_set_induction0 s). ir. app H0. Qed. Lemma finite_set_induction1: forall (A B:EP) x, (A emptyset -> B emptyset) -> (forall a b, (A a -> B a) -> A(tack_on a b) -> B(tack_on a b)) -> is_finite_set x -> A x -> B x. Proof. ir. set (s:= fun x => A x -> B x). app (finite_set_induction s). Qed. Lemma finite_set_induction2: forall (A B:EP) x, (forall a, A (singleton a) -> B (singleton a)) -> (forall a b, (A a -> nonempty a -> B a) -> nonempty a -> A(tack_on a b) -> B(tack_on a b)) -> is_finite_set x -> A x -> nonempty x -> B x. Proof. ir. set (s:= fun x => A x -> nonempty x -> B x). app (finite_set_induction s). uf s. ir. nin H5. elim (emptyset_pr H5). ir. nin (emptyset_dichot a). assert (tack_on a b = singleton b). set_extens. rwi tack_on_inc H6. nin H6. rwi H5 H6. elim (emptyset_pr H6). rw H6. fprops. rw (singleton_eq H6). fprops. rw H6. uf s. ir. app H. red. ir. app H0. Qed. Definition set_of_finite_subsets E := Zo(powerset E)(fun X => is_finite_set X). Definition set_of_finite_subsets_prop E F:= inc emptyset F & forall x X, inc x E -> inc X F -> inc (tack_on X x) F. Lemma set_of_finite_subsets_pr: forall E, set_of_finite_subsets_prop E (set_of_finite_subsets E) & (forall F, set_of_finite_subsets_prop E F -> sub (set_of_finite_subsets E) F). Proof. ir. split. uf set_of_finite_subsets. red. split. Ztac. app powerset_inc. app emptyset_sub_any. app emptyset_finite. ir. Ztac. clear H0. Ztac. app powerset_inc. app tack_on_sub. ap (powerset_sub H1). app tack_on_finite. ir. red in H. ee. red. ir. ufi set_of_finite_subsets H1. Ztac. set (powerset_sub H2). app (finite_set_induction1 (fun x=> sub x E)(fun x=> inc x F)). ir. app H0. app H5. fprops. app H4. app (sub_trans (a:=a) (b:= tack_on a b)). fprops. Qed. Lemma finite_union2: forall x y, is_finite_set x -> is_finite_set y -> is_finite_set (union2 x y). Proof. ir. set (E:=union2 x y). set (t:= Zo (powerset E) (fun a=> is_finite_set (union2 x a))). assert(set_of_finite_subsets_prop E t). red. ee. uf t. Ztac. app powerset_inc. app emptyset_sub_any. assert(union2 x emptyset = x). set_extens. nin (union2_or H1). am. elim (emptyset_pr H2). inter2tac. rww H1. ir. ufi t H2. Ztac. clear H2. Ztac. uf t. Ztac. app powerset_inc. app tack_on_sub. ap (powerset_sub H3). uf tack_on. rw union2assoc. change (is_finite_set (tack_on (union2 x X) x0)). app tack_on_finite. nin (set_of_finite_subsets_pr E). cp (H3 _ H1). assert (inc y t). app H4. uf set_of_finite_subsets. Ztac. app powerset_inc. uf E. ap union2sub_second. ufi t H5. Ztac. am. Qed. Lemma finite_powerset: forall x, is_finite_set x -> is_finite_set (powerset x). Proof. ir. set (t:= Zo (powerset x) (fun a=> is_finite_set (powerset a))). assert (set_of_finite_subsets_prop x t). red. ee. uf t. Ztac. app powerset_inc. app emptyset_sub_any. rw powerset_emptyset. app singleton_finite. ir. ufi t H1. Ztac. clear H1. uf t. Ztac. app powerset_inc. cp (powerset_sub H2). red. ir. rwi tack_on_inc H4. nin H4. app H1. rww H4. nin (inc_or_not x0 X). ir. rww (tack_on_when_inc H1). ir. set (w:= fun_image (powerset X) (fun t => tack_on t x0)). assert (equipotent (powerset X) w). set (f:= BL (fun t => tack_on t x0) (powerset X) w). assert (transf_axioms (fun t => tack_on t x0) (powerset X) w). red. ir. uf w. aw. exists c. ee. am. tv. assert (is_function f). uf f. app bl_function. exists f. ee. red. ee. uf f. app bl_injective. ir. set_extens. assert (inc x1 (tack_on u x0)). fprops. rwi H8 H10. rwi tack_on_inc H10. nin H10. am. rwi H10 H9. elim H1. cp (powerset_sub H6). app H11. assert (inc x1 (tack_on u x0)). rw H8. fprops. rwi tack_on_inc H10. nin H10. am. rwi H10 H9. elim H1. cp (powerset_sub H7). app H11. uf f. app bl_surjective. ir. ufi w H6. awi H6. nin H6. exists x1. ee. am. am. uf f. aw. uf f; aw. assert(powerset (tack_on X x0)= union2 (powerset X) w). set_extens. cp (powerset_sub H5). nin (inc_or_not x0 x1). ir. ap union2_second. uf w. aw. exists (intersection2 X x1). ee. app powerset_inc. app intersection2sub_first. set_extens. rwi tack_on_inc H8. nin H8. ap (intersection2_second H8). rww H8. nin (equal_or_not x2 x0). rw H9. fprops. assert (inc x2 (intersection2 X x1)). app intersection2_inc. cp (H6 _ H8). rwi tack_on_inc H10. nin H10. am. elim H9. ee. am. fprops. ir. ap union2_first. app powerset_inc. red. ir. cp (H6 _ H8). rwi tack_on_inc H9. nin H9. am. rwi H9 H8. elim H7. am. nin (union2_or H5). cp (powerset_sub H6). app powerset_inc. red. ir. assert (inc x2 X). app H7. fprops. ufi w H6. awi H6. nin H6. nin H6. wr H7. app powerset_inc. app tack_on_sub. cp (powerset_sub H6). red. ir. cp (H8 _ H9). fprops. fprops. rw H5. app finite_union2. red. assert (cardinal (powerset X) = cardinal w). aw. wr H6. am. cp (set_of_finite_subsets_pr x). nin H1. cp (H2 _ H0). red in H3. assert (inc x t). app H3. uf set_of_finite_subsets. Ztac. ap inc_x_powerset_x. ufi t H4. Ztac. am. Qed. (** ** EIII-4-4 Finite subsets of ordered sets *) Lemma finite_set_induction3: forall (p:EEP) 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 (tack_on a b) y) -> (forall X x, sub X E -> nonempty X -> p X x -> inc x E) -> nonempty X -> is_finite_set X -> sub X E -> exists x, p X x. Proof. ir. app (finite_set_induction2( fun X=> sub X E) (fun X => exists x, p X x)). ir. wr doubleton_singleton. assert (inc a E). app H5. fprops. app H. ir. assert (sub a E). apply sub_trans with (tack_on a b). fprops. am. assert (inc b E). app H7. fprops. cp (H5 H8 H6). nin H10. cp (H1 _ _ H8 H6 H10). nin (H _ _ H11 H9). exists x0. ee. app (H0 _ _ _ _ H8 H9 H10 H12). Qed. Lemma finite_subset_directed_bounded: forall r X, right_directed r ->is_finite_set X -> sub X (substrate r) -> nonempty X -> bounded_above r X. Proof. ir. red. app (finite_set_induction3( fun X x => upper_bound r X x) (E:=(substrate r))). red in H. ee. ir. app H3. ir. red in H5; red in H6. ee. red. ir. ee. am. ir. rwi tack_on_inc H9. nin H9. apply order_transitivity with x. red in H; ee; am. app H8. app H7. fprops. rw H9. app H7. fprops. ir. red in H5. intuition. Qed. Lemma finite_subset_lattice_inf: forall r X, lattice r ->is_finite_set X -> sub X (substrate r) -> nonempty X -> exists x, greatest_lower_bound r X x. Proof. ir. assert (order r). red in H; ee; am. app (finite_set_induction3 (fun X x => greatest_lower_bound r X x)(E:= substrate r)). ir. red in H. ee. cp (H6 _ _ H4 H5). ee. nin H8. exists x. am. ir. rwi greatest_lower_bound_pr H6. rwi greatest_lower_bound_pr H7. ee. red in H6; red in H7. ee. rw greatest_lower_bound_pr. ee. red. ee. am. ir. rwi tack_on_inc H12. nin H12. apply order_transitivity with x. am. ap H10. fprops. app H11. rw H12. app H10. fprops. ir. ap H8. red. red in H12; ee. am. ir. nin (doubleton_or H14). rw H15. app H9. red. ee. am. ir. app H13. fprops. rw H15. app H13. fprops. am. app tack_on_sub. am. red. ir. nin (doubleton_or H8). rw H9. ee. red in H6; ee; am. rww H9. am. am. ir. red in H6. red in H6. ee. awi H6. Ztac. am. am. ap Z_sub. Qed. Lemma finite_subset_lattice_sup: forall r X, lattice r ->is_finite_set X -> sub X (substrate r) -> nonempty X -> exists x, least_upper_bound r X x. Proof. ir. assert (order r). red in H; ee; am. app (finite_set_induction3 (fun X x => least_upper_bound r X x)(E:= substrate r)). ir. red in H. ee. cp (H6 _ _ H4 H5). ee. nin H7. exists x. am. ir. rwi least_upper_bound_pr H6. rwi least_upper_bound_pr H7. ee. red in H6; red in H7. ee. rw least_upper_bound_pr. ee. red. ee. am. ir. rwi tack_on_inc H12. nin H12. apply order_transitivity with x. am. app H11. ap H10. fprops. rw H12. app H10. fprops. ir. ap H8. red. red in H12; ee. am. ir. nin (doubleton_or H14). rw H15. app H9. red. ee. am. ir. app H13. fprops. rw H15. app H13. fprops. am. app tack_on_sub. am. red. ir. nin (doubleton_or H8). rw H9. ee. red in H6; ee; am. rww H9. am. am. ir. red in H6. red in H6. ee. awi H6. Ztac. am. am. ap Z_sub. Qed. Lemma finite_subset_torder_greatest: forall r X, total_order r ->is_finite_set X -> sub X (substrate r) -> nonempty X -> exists x, greatest_element (induced_order r X) x. Proof. ir. red in H; ee. app (finite_set_induction3 (fun X x => greatest_element (induced_order r X) x)(E:= substrate r)). ir. nin (H3 _ _ H4 H5). exists b. red. aw. ee. fprops. ir. aw. nin (doubleton_or H7). rw H8. am. rw H8. order_tac. fprops. red. ir. nin (doubleton_or H7). rww H8. rww H8. exists a. red. aw. ee. fprops. ir. aw. nin (doubleton_or H7). rw H8. order_tac. rw H8. am. fprops. red. ir. nin (doubleton_or H7). rww H8. rww H8. uf greatest_element. intros a b x y H4 H5. assert (sub (tack_on a b) (substrate r)). red. ir. rwi tack_on_inc H6. nin H6. app H4. rww H6. ir. nin H7. awi H7; try am. assert (sub (doubleton x b) (substrate r)). red. ir. nin (doubleton_or H10). rw H11. fprops. rww H11. nin H8. awi H11; awi H8; try am. assert (inc y (tack_on a b)). nin (doubleton_or H8). rw H12. fprops. rw H12. fprops. ee. aw. awi H12. am. ir. aw. awi H13. nin H13. apw order_transitivity x. awii H9. cp (H9 _ H13). awii H14. assert (inc x (doubleton x b)). fprops. cp (H11 _ H14). awii H15. rw H13. assert (inc b (doubleton x b)). fprops. cp (H11 _ H14). awii H15. am. am. awii H13. awi H12. am. ir. red in H6. awii H6. ee. app H4. Qed. Lemma finite_subset_torder_least: forall r X, total_order r ->is_finite_set X -> sub X (substrate r) -> nonempty X -> exists x, least_element (induced_order r X) x. Proof. ir. cp (total_order_opposite H). assert (sub X (substrate (opposite_order r))). aw. red in H; ee; am. nin (finite_subset_torder_greatest H3 H0 H4 H2). exists x. nin H;nin H3. ee. clear H7. red in H5. ee. awii H5. awii H7. red. ee. aw. ir. awii H8. cp (H7 _ H8). awii H9. aw. Qed. Lemma finite_set_torder_greatest: forall r, total_order r ->is_finite_set (substrate r) -> nonempty (substrate r) -> exists x, greatest_element r x. Proof. ir. cp H. nin H. wr (induced_order_substrate H). app finite_subset_torder_greatest. fprops. Qed. Lemma finite_set_torder_worder: forall r, total_order r ->is_finite_set (substrate r) -> worder r. Proof. ir. red. ee. red in H. ee. am. ir. app finite_subset_torder_least. app (sub_finite_set H1 H0). Qed. Lemma finite_set_maximal: forall r, order r ->is_finite_set (substrate r) -> nonempty (substrate r) -> exists x, maximal_element r x. Proof. ir. app Zorn_lemma. red. ir. nin (emptyset_dichot X). nin H1. exists y. red. ee. am. ir. rwi H4 H5. elim (emptyset_pr H5). set (s:= induced_order r X). fold s in H3. assert (substrate s = X). uf s; aw. assert (is_finite_set (substrate s)). rw H5. app (sub_finite_set H2 H0). assert (nonempty (substrate s)). rww H5. nin (finite_set_torder_greatest H3 H6 H7). exists x. red. red in H8. nin H8. rwi H5 H8. ee. app H2. ir. rwi H5 H9. ufi s H9. cp (H9 _ H10). awi H11. am. am. am. Qed. (** ** EIII-4-5 Properties of finite character *) Definition of_finite_character s:= forall x, (inc x s) = (forall y, (sub y x & is_finite_set y) -> inc y s). Lemma of_finite_character_example: forall r, order r -> of_finite_character(Zo (powerset (substrate r)) (fun z => total_order (induced_order r z))). Proof. ir. red. ir. app iff_eq. ir. nin (Z_all H0). clear H0. awi H2. nin H1. assert (sub y (substrate r)). apw sub_trans x. Ztac. aw. split. fprops. aw. ir. nin H3. awi H7. nin (H7 _ _ (H0 _ H5) (H0 _ H6)); cp (related_induced_order1 H8). left. aw. right. red. aw. am. am. ir. assert (sub x (substrate r)). red. ir. set (y:= singleton x0). assert (sub y x). uf y. red. ir. rww (singleton_eq H2). assert (is_finite_set y). uf y. app singleton_finite. assert (sub y x & is_finite_set y). intuition. cp (H0 _ H4). Ztac. ee. cp (powerset_sub H6). app H9. uf y. fprops. Ztac. aw. split. fprops. aw. ir. set (z:= doubleton x0 y). assert(sub z x & is_finite_set z). ee. uf z. red. ir. nin (doubleton_or H4); rww H5. uf z. app doubleton_finite. cp (H0 _ H4). Ztac. nin H4. assert (sub z (substrate r)). apw sub_trans x. nin H7. awii H10. assert (inc x0 z). uf z. fprops. assert (inc y z). uf z. fprops. nin (H10 _ _ H11 H12); cp (related_induced_order1 H13). left. aw. right; red. aw. Qed. Lemma maximal_inclusion: forall s, of_finite_character s -> nonempty s -> exists x, maximal_element (inclusion_suborder s) x. Proof. ir. rename H0 into Ha. assert (Hb:inc emptyset s). nin Ha. red in H. rwi H H0. app H0. ee. app emptyset_sub_any. app emptyset_finite. set (E:=union s). assert (sub s (powerset E)). red. ir. aw. uf E. app union_sub. app (maximal_in_powerset(A:=s) (F:=E)). ir. red in H. rename H2 into Hs. rw H. ir. ee. nin (emptyset_dichot y). rww H4. rename H4 into Hc. set(Zy:= fun a => choose (fun b=> inc a b & inc b So)). assert (forall a, inc a y -> (inc a (Zy a) & inc (Zy a) So)). ir. uf Zy. app choose_pr. cp (H2 _ H4). app (union_exists H5). set (Zz:= fun_image y Zy). assert (is_finite_set Zz). uf Zz. app finite_fun_image. set (r:=inclusion_suborder Zz). assert (total_order r). uf r; red. ee. fprops. aw. ir. assert (inc x So). ufi Zz H6. awi H6. nin H6. nin H6. wr H8. nin (H4 _ H6). am. assert (inc y0 So). ufi Zz H7. awi H7. nin H7. nin H7. wr H9. nin (H4 _ H7). am. nin (H1 _ _ H8 H9). left. aw. ee; am. right. red; aw. ee;am. assert (Hd:substrate r = Zz). uf r. aw. assert(is_finite_set (substrate r)). rww Hd. assert(nonempty (substrate r)). rw Hd. nin Hc. exists (Zy y0). uf Zz. aw. exists y0. ee. am. tv. nin (finite_set_torder_greatest H6 H7 H8). red in H9. nin H9. assert (sub y x). red. ir. nin (H4 _ H11). assert (inc (Zy x0)(substrate r)). uf r. aw. uf Zz. aw. exists x0. ee. am. tv. cp (H10 _ H14). ufi r H15. awi H15. ee. app H17. rwi Hd H9. ufi Zz H9. awi H9. nin H9. nin H9. cp (H4 _ H9). nin H13. rwi H12 H14. rw H. ir. ee. cp (sub_trans H15 H11). cp (Hs _ H14). rwi H H18. app H18. ee; am. Qed. (** ** Pseudo Ordinals*) Definition transitive_set X:= forall x, inc x X -> sub x X. Definition pseudo_ordinal X:= forall Y, sub Y X -> transitive_set Y -> Y <> X -> inc Y X. Definition decent_set x := forall y, inc y x -> ~ (inc y y). Lemma transitive_tack_on_itself: forall y, transitive_set y -> transitive_set (tack_on y y). Proof. ir. red. ir. rwi tack_on_inc H0. nin H0. cp (H _ H0). red. ir. set (H1 _ H2). fprops. rw H0. red. ir. fprops. Qed. Lemma transitive_union: forall x, (forall y, inc y x -> transitive_set y) -> transitive_set (union x). Proof. ir. red. ir. nin (union_exists H0). ee. cp ((H _ H2) _ H1). red. ir. set (H3 _ H4). union_tac. Qed. Lemma transitive_intersection: forall x, (forall y, inc y x -> transitive_set y) -> nonempty x -> transitive_set (intersection x). Proof. ir. red. ir. red. ir. app intersection_inc. ir. app ((H _ H3) _ (intersection_forall H1 H3)). Qed. Lemma pseudo_ordinal_transitive1: forall x, pseudo_ordinal x -> (transitive_set x & decent_set x). Proof. ir. set (y:=Zo (powerset x)(fun z=> transitive_set z & decent_set z)). assert (transitive_set (union y)). app transitive_union. ir. ufi y H0. Ztac. ee. am. assert (decent_set (union y)). red. ir. nin (union_exists H1). nin H2. ufi y H3. Ztac. ee. red in H6. app (H6 _ H2). red in H. assert (sub (union y) x). app sub_union. ir. ufi y H2. app powerset_sub. Ztac. am. nin (p_or_not_p (union y = x)). ir. wr H3. ee; am. ir. cp (H _ H2 H0 H3). assert (transitive_set (tack_on (union y) (union y))). app transitive_tack_on_itself. assert (decent_set (tack_on (union y) (union y))). red. ir. rwi tack_on_inc H6. nin H6. app H1. red. ir. assert (inc y0 (union y)). wrr H6. nin (union_exists H8). ee. ufi y H10. Ztac. ee. red in H13. elim (H13 _ H9). am. set (u:=tack_on (union y) (union y)). assert (inc u y). uf y. uf u. Ztac. app powerset_inc. red. ir. rwi tack_on_inc H7. nin H7. app H2. rww H7. red in H1. assert (sub u (union y)). app union_sub. set (t:= union y). assert (inc t u). uf u. rw tack_on_inc. right. tv. assert (inc t t). app H8. fold u in H6. nin (H6 _ H9). am. Qed. Lemma pseudo_ordinal_transitive: forall x, pseudo_ordinal x -> transitive_set x. Proof. ir. nin (pseudo_ordinal_transitive1 H). am. Qed. Lemma pseudo_ordinal_tack_on: forall x, pseudo_ordinal x -> pseudo_ordinal (tack_on x x). Proof. ir. red. ir. nin (inc_or_not x Y). elim H2. set (H1 _ H3). set_extens. rwi tack_on_inc H4. nin H4. app s. ue. ir. assert (sub Y x). red. ir. set (H0 _ H4). rwi tack_on_inc i. nin i. am. elim H3. ue. nin (equal_or_not Y x). rw H5. fprops. rw tack_on_inc. left. app H. Qed. Lemma pseudo_ordinal_emptyset: pseudo_ordinal emptyset. Proof. red. ir. elim H1. app extensionality. ap emptyset_sub_any. Qed. Lemma pseudo_not_inc_itself: forall x, pseudo_ordinal x -> ~ (inc x x). Proof. ir. cp (pseudo_ordinal_transitive1 H). ee. red in H1. red. ir. cp (H1 _ H2). au. Qed. Lemma pseudo_ordinal_dichotomy : forall x y, pseudo_ordinal x -> pseudo_ordinal y -> (inc x y \/ inc y x \/ x = y). Proof. ir. cp (pseudo_ordinal_transitive1 H). cp (pseudo_ordinal_transitive1 H0). ee. set (z:=intersection2 x y). assert (transitive_set z). uf z. uf intersection2. app transitive_intersection. ir. nin (doubleton_or H5); ue. app nonempty_doubleton. assert (~ (inc z z)). red. ir. red in H4. assert (inc z (intersection2 x y)). am. cp (intersection2_first H7). app (H4 _ H8). nin (equal_or_not x y). au. assert (y <> x). intuition. assert (sub z x). uf z; app intersection2sub_first. nin (equal_or_not z x). assert (sub x y). red. ir. wri H10 H11. ufi z H11. ap (intersection2_second H11). cp (H0 _ H11 H1 H7). au. cp (H _ H9 H5 H10). nin (equal_or_not z y). wr H12. au. assert (sub z y). uf z; app intersection2sub_second. cp (H0 _ H13 H5 H12). assert (inc z (intersection2 x y)). app intersection2_inc. elim H6. am. Qed. Lemma pseudo_ordinal_pr: forall x, transitive_set x -> (forall y, inc y x -> pseudo_ordinal y) -> pseudo_ordinal x. Proof. ir. red. ir. nin (emptyset_dichot (complement x Y)). elim H3. app extensionality. app empty_complement. nin H4. srwi H4. ee. cp (H0 _ H4). assert (sub Y y). red. ir. cp (H0 _ (H1 _ H7)). nin (pseudo_ordinal_dichotomy H6 H8). elim H5. app (H2 _ H7). nin H9. am. elim H5. rww H9. nin (equal_or_not Y y). rww H8. ap (H _ H4). app H6. Qed. Lemma pseudo_ordinal_empty: pseudo_ordinal emptyset. Proof. red. ir. elim H1. app extensionality. app emptyset_sub_any. Qed. Lemma inc_pseudo_pseudo: forall x y, pseudo_ordinal x -> inc y x -> pseudo_ordinal y. Proof. ir. set (t:= union (Zo(powerset x) (fun y=> transitive_set y & forall a, inc a y -> pseudo_ordinal a))). assert (pseudo_ordinal t). red. app pseudo_ordinal_pr. uf t. app transitive_union. ir. Ztac. ee. am. uf t. ir. nin (union_exists H1). ee. Ztac. ee. app H6. assert (t=x). nin (pseudo_ordinal_dichotomy H H1). ufi t H2. nin (union_exists H2). ee. Ztac. ee. cp (powerset_sub H5). cp (H8 _ H3). elim (pseudo_not_inc_itself H H9). nin H2. cp (pseudo_ordinal_transitive H). set (a:= tack_on t t). assert (sub a x). uf a. red. ir. rwi tack_on_inc H4. nin H4. app (H3 _ H2). ue. assert (sub a t). uf t. red. ir. apply union_inc with a. am. Ztac. app powerset_inc. ee. cp (pseudo_ordinal_tack_on H1). ap (pseudo_ordinal_transitive H6). ir. ufi a H6. rwi tack_on_inc H6. nin H6. ufi t H6. nin (union_exists H6). ee. Ztac. ee. app H11. rww H6. assert (inc t a). uf a. fprops. cp (H5 _ H6). elim (pseudo_not_inc_itself H1 H7). sy; am. wri H2 H0. ufi t H0. nin (union_exists H0). ee. Ztac. ee. app H7. Qed. Lemma intersection_of_pseudo_ordinals: forall x, nonempty x -> (forall a, inc a x -> pseudo_ordinal a) -> inc (intersection x) x. Proof. ir. set (u:= intersection x). assert (pseudo_ordinal u). uf u. app pseudo_ordinal_pr. app transitive_intersection. ir. ap pseudo_ordinal_transitive. app H0. ir. nin H. cp (intersection_forall H1 H). apply inc_pseudo_pseudo with y0. app H0. am. assert (forall a, inc a x -> sub u a). uf u. red. ir. app (intersection_forall H3 H2). assert (forall a, inc a x -> inc u a \/ a =u). ir. cp (H0 _ H3). nin (pseudo_ordinal_dichotomy H4 H1). cp (H2 _ H3). cp (H6 _ H5). elim (pseudo_not_inc_itself H4 H7). am. assert (exists a, inc a x & a = u). app exists_proof. red. ir. assert(forall a, inc a x -> inc u a). ir. cp (H4 a). nin (H3 _ H5). am. elim H6. ee; am. assert (inc u (intersection x)). app intersection_inc. elim (pseudo_not_inc_itself H1 H6). nin H4. ee. ue. Qed. Lemma worder_sub_ordinal: forall x, pseudo_ordinal x -> worder (inclusion_suborder x). Proof. ir. red. ee. fprops. aw. ir. assert (inc (intersection x0) x0). app intersection_of_pseudo_ordinals. ir. apply inc_pseudo_pseudo with x. am. app H0. cp (intersection_is_least H2). set (t:= (intersection x0)) in *. exists t. red. aw. ee. am. nin H3. ir. aw. awi H4. ee. app H0. app H0. cp (H4 _ H5). awi H6. ee; am. fprops. Qed. Lemma pseudo_ordinal_isomorphism_unique: forall x y f, pseudo_ordinal x -> pseudo_ordinal y -> order_isomorphism f (inclusion_suborder x)(inclusion_suborder y) -> x = y. Proof. ir. set (A:=Zo x(fun z => W z f <> z)). nin H1. ee. awi H4. awi H5. assert (Ha:is_function f). app bij_is_function. assert (Hb: forall a, inc a x -> inc (W a f) y). ir. rw H5. app inc_W_target. wrr H4. nin (emptyset_dichot A). assert (forall a, inc a x -> W a f = a). ir. ex_middle. empty_tac1 a. uf A. Ztac. set_extens. wr (H8 _ H9). app Hb. rwi H5 H9. nin H3. cp (surjective_pr2 H10 H9). nin H11. ee. wri H4 H11. rwi (H8 _ H11) H12. ue. assert (Hc:forall a b, inc a x -> inc b x -> sub a b = sub (W a f) (W b f)). wri H4 H6. ir. cp (H6 _ _ H8 H9). awi H10. cp (Hb _ H8). cp (Hb _ H9). app iff_eq. ir. assert (inc a x & inc b x & sub a b). ee; am. rwi H10 H14. ee; am. ir. assert (inc a x & inc b x & sub a b). rw H10. ee; am. ee; am. assert (Hd:forall a b, inc a x -> inc b x -> inc a b = inc (W a f) (W b f)). ir. cp (inc_pseudo_pseudo H H8). cp (inc_pseudo_pseudo H H9). cp (Hb _ H8). cp (Hb _ H9). cp (inc_pseudo_pseudo H0 H12). cp (inc_pseudo_pseudo H0 H13). nin (pseudo_ordinal_dichotomy H10 H11). app iff_eq. ir. nin (pseudo_ordinal_dichotomy H14 H15). am. nin H18. cp (pseudo_ordinal_transitive H14 H18). wri Hc H19. cp (H19 _ H17). elim (pseudo_not_inc_itself H10 H20). am. am. red in H3. ee. red in H3. ee. wri H4 H20. rwi (H20 _ _ H8 H9 H18) H17. elim (pseudo_not_inc_itself H11 H17). nin H16. cp (pseudo_ordinal_transitive H10 H16). app iff_eq. ir. cp (H17 _ H18). elim (pseudo_not_inc_itself H10 H19). ir. rwi Hc H17. cp (H17 _ H18). elim (pseudo_not_inc_itself H14 H19). am. am. rw H16. app iff_eq. ir. elim (pseudo_not_inc_itself H11 H17). ir. elim (pseudo_not_inc_itself H15 H17). assert (sub A x). uf A. app Z_sub. cp (worder_sub_ordinal H). nin H9. ee. awi H10. cp (H10 _ H8 H7). nin H11. red in H11. nin H11. awi H11. awi H12. assert (forall x1, inc x1 A -> sub x0 x1). ir. cp (H12 _ H13). awi H14. ee. am. am. am. clear H10; clear H12. assert (forall u, inc u x0 -> W u f= u). ir. ex_middle. assert (inc u x). assert (inc x0 x). app H8. cp (pseudo_ordinal_transitive H). red in H15. app (H15 _ H14). assert (inc u A). uf A. Ztac. cp (inc_pseudo_pseudo H H14). cp (H13 _ H15). cp (H17 _ H10). elim (pseudo_not_inc_itself H16 H18). assert(forall u b, inc b x -> inc u (W b f) -> exists v, inc v b & u =W v f). ir. red in H3. ee. cp (Hb _ H12). cp (pseudo_ordinal_transitive H0 H16). cp (H17 _ H14). rwi H5 H18. cp (surjective_pr2 H15 H18). nin H19. nin H19. symmetry in H20. rwi H20 H14. wri Hd H14. exists x1. ee; am. rww H4. am. assert (sub (W x0 f) x0). red. ir. cp (H12 _ _ (H8 _ H11) H14). nin H15. nin H15. rw H16. rww H10. cp (inc_pseudo_pseudo H (H8 _ H11)). cp (inc_pseudo_pseudo H0 (Hb _ (H8 _ H11))). assert (He:W x0 f <> x0). ufi A H11. Ztac. am. nin (pseudo_ordinal_dichotomy H15 H16). elim (pseudo_not_inc_itself H15 (H14 _ H17)). nin H17. cp (H10 _ H17). red in H3. ee; red in H3. ee. wri H4 H20. cp (H8 _ H11). cp ( (pseudo_ordinal_transitive H H21) _ H17). elim He. app H20. elim He. sy; am. am. aw. am. aw. Qed. Lemma pseudo_ordinal_isomorphism_exists: forall r, worder r -> exists y, exists f, (pseudo_ordinal y & order_isomorphism f r (inclusion_suborder y)). Proof. ir. set (p:= fun f => target f). cp (transfinite_definition p H). nin H0. clear H1. nin H0. rename x into f. red in H0. ee. ufi p H2. exists (target f). exists f. set (todo:= pseudo_ordinal (target f) & order_isomorphism f r (inclusion_suborder (target f))). set (E:= substrate r). fold E in H2. fold E in H1. assert (Ha: is_function f). red in H0; ee; am. assert (forall a b, gle r a b -> sub (W a f) (W b f)). ir. assert (inc a E). uf E. order_tac. assert (inc b E). uf E. order_tac. rww H2. rww H2. uf restriction_to_segment. uf restriction1. aw. uf image_by_fun. app image_by_increasing. fprops. app segment_monotone. red in H; ee;am. assert (forall a b, glt r a b -> inc (W a f) (W b f)). ir. assert (inc b E). uf E. order_tac. rw (H2 _ H5). uf restriction_to_segment. uf restriction1. aw. exists a. ee. app segment_inc. tv. rw H1. uf E. app sub_segment. assert(He:forall a b, inc a E -> inc b (W a f) -> sub b (W a f)). red. ir. rwi (H2 _ H5) H6. ufi restriction_to_segment H6. ufi restriction1 H6. awi H6. nin H6. nin H6. cp (inc_segment H6). red in H9. ee. cp (H3 _ _ H9). app H11. ue. fprops. rw H1. uf segment. uf interval_uo. app Z_sub. assert (forall a, inc a E -> ~ (inc (W a f) (W a f))). set (Bad:= Zo E (fun a => inc (W a f) (W a f))). nin (emptyset_dichot Bad). ir. red. ir. empty_tac1 a. uf Bad. Ztac. red in H. ee. fold E in H6. assert (sub Bad E). uf Bad. app Z_sub. nin (H6 _ H7 H5). red in H8. ee. awi H8. awi H9. cp H8. ufi Bad H8. Ztac. clear H8. set (w:= W x f). assert (inc w (W x f)). tv. rwi (H2 _ H11) H8. ufi restriction_to_segment H8. ufi restriction1 H8. awi H8. nin H8. nin H8. cp (inc_segment H8). assert (inc x0 (source f)). rw H1. uf E. order_tac. assert (inc x0 Bad). uf Bad. Ztac. wrr H1. rww H13. cp (H9 _ H16). awi H17. order_tac. am. am. am. rw H1. uf E. app sub_segment. am. am. am. am. assert (injective f). red. ee. red in H0. ee. am. ir. rwi H1 H6; rwi H1 H7. cp (worder_total H). cp (total_order_pr1 H9 H6 H7). nin H10. cp (H4 _ _ H10). rwi H8 H11. elim (H5 _ H7). am. nin H10. assert (glt r y x). red in H10; ee. red in H10. red. ee. am. intuition. cp (H4 _ _ H11). rwi H8 H12. elim (H5 _ H7). am. am. assert (order_isomorphism f r (inclusion_suborder (target f))). red. ee. red in H. ee. am. fprops. red. ee;am. rww H1. aw. ir. aw. app iff_eq. ir. ee. app inc_W_target. app inc_W_target. app H3. ir. ee. cp (worder_total H). rwi H1 H7; rwi H1 H8. cp (total_order_pr1 H12 H7 H8). nin H13. red in H13; ee; am. nin H13. red in H13. ee. red in H13. cp (H3 _ _ H13). assert ( (W y f)= (W x f)). app extensionality. elim H14. red in H6. ee. app H17. rww H1. rww H1. sy; am. rw H13. wrr order_reflexivity. red in H; ee;am. assert (forall a, inc a E -> transitive_set (W a f)). ir. red. ir. app He. assert (forall a, inc a E -> pseudo_ordinal (W a f)). set (Bad:= Zo E (fun z => (~ (pseudo_ordinal (W z f))))). nin (emptyset_dichot Bad). ir. nin (p_or_not_p (pseudo_ordinal (W a f))). am. assert (inc a emptyset). wr H9. uf Bad. Ztac. elim (emptyset_pr H12). red in H. ee. assert (sub Bad E). uf Bad. app Z_sub. cp (H10 _ H11 H9). nin H12. red in H12. ee. awi H12. awi H13. assert (Hd: inc x Bad). am. ufi Bad H12. Ztac. clear H12. elim H15. app pseudo_ordinal_pr. app H8. ir. rwi (H2 _ H14) H12. simpl in H12. ufi image_by_fun H12. ufi restriction_to_segment H12. ufi restriction1 H12. awi H12. nin H12. nin H12. cp (inc_segment H12). wr H16. nin (p_or_not_p (pseudo_ordinal (W x0 f))). am. assert (inc x0 Bad). uf Bad. Ztac. uf E. order_tac. cp (H13 _ H19). awi H20. order_tac. am. am. am. rw H1. uf E. app sub_segment. am. am. am. am. assert (transitive_set (target f)). red. ee. ir. cp (surjective_pr2 H0 H10). nin H11. ee. red. ir. rwi H1 H11. cp (H2 _ H11). ufi restriction_to_segment H14. ufi restriction1 H14. awi H14. wri H12 H13. rwi H14 H13. ufi image_by_fun H13. awi H13. nin H13. nin H13. graph_tac. red. ee. app pseudo_ordinal_pr. ir. cp (surjective_pr2 H0 H11). nin H12. nin H12. wr H13. app H9. wrr H1. am. Qed. Lemma pseudo_ordinal_pr1: forall x, exists y, pseudo_ordinal y & equipotent x y & (forall z, pseudo_ordinal z -> equipotent x z -> sub y z). Proof. ir. nin (Zermelo x). nin H. destruct (pseudo_ordinal_isomorphism_exists H) as [u [f [H1 H2]]]. assert (equipotent x u). red in H2. ee. awi H6. rwi H0 H5. exists f. ee. am. sy; am. sy; am. set (t:=Zo u (fun z=> equipotent x z)). nin (emptyset_dichot t). exists u. ee. am. am. ir. nin (pseudo_ordinal_dichotomy H1 H5). cp (pseudo_ordinal_transitive H5). red in H8. app H8. nin H7. empty_tac1 z. uf t. Ztac. rw H7. fprops. assert (sub t u). uf t. app Z_sub. cp (worder_sub_ordinal H1). red in H6. ee. awi H7. cp (H7 _ H5 H4). nin H8. nin H8. awi H8. cp H8. ufi t H8. Ztac. clear H8. cp (inc_pseudo_pseudo H1 H11). exists x1. ee. am. am. ir. nin (pseudo_ordinal_dichotomy H1 H13). red. ir. cp (pseudo_ordinal_transitive H13). red in H17. cp(H17 _ H15). app H18. cp (pseudo_ordinal_transitive H1). red in H19. cp(H19 _ H11). app H20. nin H15. assert (inc z t). uf t. Ztac. awi H9. cp (H9 _ H16). awi H17. ee; am. am. am. fprops. aw. wr H15. cp (pseudo_ordinal_transitive H1). red in H16. app H16. fprops. aw. Qed. (** Link between pseudo-ordinal and nat *) Fixpoint natR (n:nat) := match n with 0 => emptyset | S p => tack_on (natR p) (natR p) end. Lemma value_R_0: natR 0 = emptyset. Proof. tv. Qed. Lemma value_R_1: natR 1 = singleton emptyset. Proof. simpl. set_extens. rwi tack_on_inc H. nin H. elim (emptyset_pr H). rw H. fprops. rw (singleton_eq H). fprops. Qed. Lemma value_R_2: natR 2 = doubleton (singleton emptyset) emptyset. Proof. simpl. cp value_R_1. simpl in H. rw H. set_extens. rwi tack_on_inc H0. nin H0. rw (singleton_eq H0). fprops. rw H0. fprops. nin (doubleton_or H0). rw H1. fprops. rw H1. fprops. Qed. Lemma value_R_3: let tripleton a b c := tack_on (doubleton a b) c in natR 3 = tripleton (doubleton (singleton emptyset) emptyset) (singleton emptyset) emptyset. Proof. simpl. cp value_R_2. simpl in H. rw H. set_extens. rwi tack_on_inc H0. nin H0. nin (doubleton_or H0). rw H1. fprops. rw H1. fprops. rw H0. fprops. rwi tack_on_inc H0. nin H0. nin (doubleton_or H0). rw H1. fprops. rw H1. fprops. rw H0. fprops. Qed. Lemma pseudo_ordinal_Rnat: forall i, pseudo_ordinal (natR i). Proof. ir. nin i. simpl. app pseudo_ordinal_emptyset. simpl. app pseudo_ordinal_tack_on. Qed. Lemma finite_Rnat: forall i, is_finite_set (natR i). Proof. ir. nin i. simpl. app emptyset_finite. simpl. app tack_on_finite. Qed. Lemma Rnat_le_implies_sub : forall i j, i <= j -> sub (natR i) (natR j). Proof. ir. nin H. fprops. apply sub_trans with (natR m). am. red. ir. simpl. fprops. Qed. Lemma Rnat_lt_implies_inc : forall i j, i < j -> inc (natR i) (natR j). Proof. ir. red in H. cp (Rnat_le_implies_sub H). app H0. simpl. fprops. Qed. Lemma Rnat_lt_implies_strict_sub : forall i j, i < j -> strict_sub (natR i) (natR j). Proof. ir. cp (Rnat_lt_implies_inc H). cp (pseudo_ordinal_Rnat j). red. ee. red. ir. rwi H2 H0. ap (pseudo_not_inc_itself H1). am. app pseudo_ordinal_transitive. Qed. Lemma Rnat_sub_le : forall i j, sub (natR i) (natR j) = (i <= j). Proof. ir. ap iff_eq; ir. cp (le_or_lt i j). nin H0. am. cp (Rnat_lt_implies_inc H0). cp (H _ H1). elim (pseudo_not_inc_itself (pseudo_ordinal_Rnat j)). am. app Rnat_le_implies_sub. Qed. Lemma Rnot_inc_itself:forall i, ~ (inc (natR i)(natR i)). Proof. ir. ap (pseudo_not_inc_itself (pseudo_ordinal_Rnat i)). Qed. Lemma Rnat_inc_lt : forall i j, inc (natR i) (natR j) = (i < j). Proof. ir. ap iff_eq; ir. nin (le_or_lt j i). cp (Rnat_le_implies_sub H0). elim (Rnot_inc_itself _ (H1 _ H)). am. app Rnat_lt_implies_inc. Qed. Lemma cardinal_Rnat_lt: forall i j, i< j -> cardinal_lt (cardinal (natR i)) (cardinal (natR j)). Proof. ir. cp (Rnat_lt_implies_strict_sub H). nin H0. app strict_sub_smaller. app (finite_Rnat j). Qed. Lemma cardinal_Rnat_inj: forall i j, cardinal (natR i) = cardinal (natR j) -> i = j. Proof. ir. nin (p_or_not_p (i = j)). am. nin (nat_total_order _ _ H0). cp (cardinal_Rnat_lt H1). red in H2. ee. elim H3. am. cp (cardinal_Rnat_lt H1). red in H2. ee. elim H3. sy; am. Qed. Lemma exists_nat_cardinal: forall a, is_finite_c a -> exists_unique(fun i => cardinal (natR i) = a). Proof. ir. red. split. app (cardinal_c_induction (fun n => exists i:nat, cardinal (natR i) =n)). exists 0. simpl. rw cardinal_zero. tv. ir. nin H1. exists (S x). simpl. wr H1. rw succ_cardinal. app cardinal_succ_pr. ap Rnot_inc_itself. ir. wri H1 H0. app cardinal_Rnat_inj. Qed. Definition cardinal_nat x := choosenat(fun i => cardinal (natR i) = cardinal x). Lemma cardinal_nat_cardinal: forall x, cardinal_nat (cardinal x) = cardinal_nat x. Proof. uf cardinal_nat. ir. set (t := cardinal x). assert (is_cardinal t). uf t. fprops. rww (cardinal_of_cardinal H). Qed. Hint Rewrite cardinal_nat_cardinal: aw. Lemma cardinal_nat_pr: forall x, is_finite_set x -> cardinal (natR (cardinal_nat x)) = cardinal x. Proof. ir. uf cardinal_nat. ap choosenat_pr. nin (exists_nat_cardinal H). am. Qed. Lemma cardinal_nat_pr1: forall i, cardinal_nat(natR i) = i. Proof. ir. cp (finite_Rnat i). cp (cardinal_nat_pr H). app cardinal_Rnat_inj. Qed. Lemma cardinal_nat_finite_eq: forall a b, is_finite_set a -> cardinal a = cardinal b -> cardinal_nat a = cardinal_nat b. Proof. ir. assert (is_finite_set b). red. ue. wri (cardinal_nat_pr H) H0. wri(cardinal_nat_pr H1) H0. app cardinal_Rnat_inj. Qed. Lemma cardinal_nat_finite_eq1: forall a b, is_finite_set a -> is_finite_set b -> cardinal_nat a = cardinal_nat b -> cardinal a = cardinal b. Proof. ir. wr (cardinal_nat_pr H). wr (cardinal_nat_pr H0). ue. Qed. Lemma cardinal_nat_emptyset: cardinal_nat emptyset = 0. Proof. ir. change(cardinal_nat (natR 0) = 0). ap cardinal_nat_pr1. Qed. Lemma cardinal_nat_singleton: forall x, cardinal_nat (singleton x) = 1. Proof. ir. wr (cardinal_nat_pr1 1). rw value_R_1. app cardinal_nat_finite_eq. app singleton_finite. aw. app singletons_equipotent. Qed. Lemma cardinal_nat_doubleton: forall x y, x <> y -> cardinal_nat (doubleton x y) = 2. Proof. ir. wr (cardinal_nat_pr1 2). rw value_R_2. app cardinal_nat_finite_eq. app doubleton_finite. aw. ap doubleton_equipotent1. am. fprops. Qed. Lemma cardinal_nat_zero: cardinal_nat card_zero = 0. Proof. ir. rw zero_is_emptyset. app cardinal_nat_emptyset. Qed. Lemma cardinal_nat_one: cardinal_nat card_one = 1. Proof. ir. cp cardinal_one_is_singleton. nin H. rw H. app cardinal_nat_singleton. Qed. Lemma cardinal_nat_two: cardinal_nat card_two = 2. Proof. ir. uf card_two. cp (two_points_distinct). wr (cardinal_nat_doubleton H). aw. rww two_points_pr2. Qed. (** Bijection between nat and the integers *) Lemma plus_via_succ: forall a n, card_plus a (succ n) = succ (card_plus a n). Proof. ir. uf succ. app card_plus_associative. Qed. Lemma Bnat_stable_plus: forall a b, inc a Bnat -> inc b Bnat -> inc (card_plus a b) Bnat. Proof. ir. bw. bwi H. bwi H0. app (cardinal_c_induction (fun b => is_finite_c (card_plus a b))). aw. fprops. ir. rw plus_via_succ. app is_finite_succ1. Qed. Lemma mult_via_plus: forall a b, is_cardinal a -> card_mult a (succ b) = card_plus (card_mult a b) a. Proof. ir. uf succ. rw cardinal_distrib_prod_sum3. aw. Qed. Lemma Bnat_stable_mult: forall a b, inc a Bnat -> inc b Bnat -> inc (card_mult a b) Bnat. Proof. ir. app (cardinal_c_induction_v (fun b => inc (card_mult a b) Bnat)). aw. rw zero_prod_absorbing. fprops. ir. rw mult_via_plus. app Bnat_stable_plus. fprops. Qed. Hint Resolve Bnat_stable_plus Bnat_stable_mult: fprops. Hint Rewrite succ_zero:aw. Fixpoint nat_to_B (n:nat) := match n with 0 => card_zero | S m => succ (nat_to_B m) end. Lemma nat_B_0: nat_to_B 0 = card_zero. Proof. tv. Qed. Lemma nat_B_1: nat_to_B 1 = card_one. Proof. simpl. aw. Qed. Lemma nat_B_S: forall n, nat_to_B (S n) = succ (nat_to_B n). Proof. tv. Qed. Lemma inc_nat_to_B: forall n, inc (nat_to_B n) Bnat. Proof. ir. induction n. simpl. fprops. simpl. fprops. Qed. Hint Resolve inc_nat_to_B: fprops. Lemma nat_B_plus: forall a b, nat_to_B (a+b) = card_plus (nat_to_B a) (nat_to_B b). Proof. ir. induction b. rw plus_0_r. sy. app zero_unit_sumr. cp (inc_nat_to_B a). fprops. assert (a+ S b = S(a+b)). auto with arith. rw H. rw nat_B_S. rw IHb. rw nat_B_S. uf succ. rww card_plus_associative. Qed. Lemma nat_B_2: nat_to_B 2 = card_two. Proof. rw card_two_pr. wr nat_B_1. wrr nat_B_plus. Qed. Lemma nat_B_mult: forall a b, nat_to_B (a*b) = card_mult (nat_to_B a) (nat_to_B b). Proof. ir. induction b. rw mult_0_r. rw nat_B_0. sy. ap zero_prod_absorbing. assert (a* S b = a*b+a). auto with arith. rw H. rw nat_B_plus. rw IHb. rw nat_B_S. uf succ. rw cardinal_distrib_prod_sum3. rww one_unit_prodr. cp (inc_nat_to_B a). fprops. Qed. Lemma nat_to_B_surjective: forall n, inc n Bnat -> exists m, nat_to_B m = n. Proof. ir. app (cardinal_c_induction_v (fun b => exists m, nat_to_B m = b)). ir. exists 0. ap nat_B_0. ir. nin H1. exists (S x). wr H1. ap nat_B_S. Qed. Lemma nat_B_inj: forall a b, nat_to_B a = nat_to_B b -> a = b. Proof. intro a. induction a. ir. rwi nat_B_0 H. induction b. tv. rwi nat_B_S H. cp (succ_positive (nat_to_B b)). red in H0. ee. elim H1. am. ir. induction b. rwi nat_B_S H. rwi nat_B_0 H. cp (succ_positive (nat_to_B a)). red in H0. ee. elim H1. sy;am. rwi nat_B_S H. rwi nat_B_S H. assert (a=b). app IHa. app succ_injective. cp (inc_nat_to_B a). fprops. cp (inc_nat_to_B b). fprops. rww H0. Qed. Lemma nat_B_le: forall a b, (a<= b) = cardinal_le (nat_to_B a) (nat_to_B b). Proof. ir. app iff_eq. ir. cp (inc_nat_to_B a). induction H. fprops. apply cardinal_le_transitive with (nat_to_B m). am. rw nat_B_S. app is_less_than_succ. cp (inc_nat_to_B m). fprops. ir. cp (inc_nat_to_B a). cp (inc_nat_to_B b). assert (is_cardinal (nat_to_B a)). fprops. assert (is_cardinal (nat_to_B b)). fprops. rwi (cardinal_le_when_complement H3 H2) H. nin H. ee. bwi H1. wri H4 H1. cp (is_finite_in_sum H H1). wri inc_Bnat H5. nin (nat_to_B_surjective H5). wri H6 H4. wri nat_B_plus H4. cp (nat_B_inj _ _ H4). wr H7. auto with arith. Qed. Lemma nat_B_lt: forall a b, (a< b) = cardinal_lt (nat_to_B a) (nat_to_B b). Proof. ir. app iff_eq. ir. red. ee. wr nat_B_le. app lt_le_weak. red. ir. rwi (nat_B_inj _ _ H0) H. elim (lt_irrefl _ H). ir. nin H. wri nat_B_le H. nin (le_lt_or_eq _ _ H). am. elim H0. ue. Qed. Lemma nat_B_lt0: forall b, (0 nat_to_B (cardinal_nat n) = n. Proof. ir. app (cardinal_c_induction_v (fun b => nat_to_B (cardinal_nat b) = b)). rw cardinal_nat_zero. app nat_B_0. ir. assert (cardinal_nat (succ n0) = S (cardinal_nat n0)). wr (cardinal_nat_pr1 (S (cardinal_nat n0))). assert (is_finite_set (succ n0)). red. rw cardinal_succ. wr inc_Bnat. fprops. app cardinal_nat_finite_eq. awi H0. assert (cardinal n0 = n0). red in H0; ee. fprops. assert (is_finite_set n0). red. rw H3. bwi H0. am. cp (cardinal_nat_pr H4). rw cardinal_succ. simpl. fprops. rw cardinal_succ_pr. set (m:= cardinal_nat n0) in *. wr H3. wr H5. rw succ_cardinal. tv. app Rnot_inc_itself. rw H2. rw nat_B_S. ue. Qed. Lemma nat_to_B_pr1: forall n, cardinal_nat(nat_to_B n) = n. Proof. ir. app nat_B_inj. rww nat_to_B_pr. fprops. Qed. Hint Rewrite nat_to_B_pr nat_to_B_pr1: aw. Hint Rewrite <- nat_B_lt nat_B_le nat_B_S nat_B_lt0 nat_B_plus nat_B_mult :bw. Hint Rewrite nat_B_lt nat_B_S nat_B_lt0 nat_B_plus nat_B_mult :aw. Fixpoint pow (n m:nat) {struct m} : nat := match m with | O => 1 | S p => (pow n p) * n end where "n ^ m" := (pow n m) : nat_scope. End FiniteSets. Export FiniteSets.