Require Export func. Set Implicit Arguments. Unset Strict Implicit. Module Order_notation. Import Universe. Open Local Scope string_scope. Definition Less_Than := R "LessThan". Definition less_than (x a b : E) := V a (V b (V Less_Than x)). Definition leq (x a b : E) := A (inc a (U x)) (A (inc b (U x)) (nonempty (less_than x a b))). Definition lt (a x y : E) := A (leq a x y) (x <> y). Section Construction. Variables (x : E) (lq : E2P). Definition create := denote Underlying x ( denote Less_Than (binary x lq) stop). Lemma inc_create_u : forall u, Universe.axioms u -> inc x u -> inc create u. Proof. ir. uf create. app inc_denote_u. incdu. incdu. app inc_binary_u. ir. app inc_a_prop_u. drw_solve. Qed. Lemma underlying_create : U create = x. ir; uf U; uf create. drw. Qed. Lemma less_than_rw : forall a b : E, inc a x -> inc b x -> less_than create a b = lq a b. ir; uf less_than; uf create. drw. aw. Qed. Lemma leq_create : forall a b : E, inc a x -> inc b x -> leq create a b = lq a b. ir. uf leq. rw less_than_rw. ap iff_eq; ir. ee. nin H3. exact (B H3). rw underlying_create. ee. am. am. sh (R H1). ap R_inc. am. am. Qed. Lemma leq_create_all : forall a b : E, leq create a b = A (inc a x) (A (inc b x) (lq a b)). ir. ap iff_eq. uf leq. rw underlying_create. ir; ee. am. am. rwi less_than_rw H1. nin H1. exact (B H1). am. am. ir. rw leq_create; ee; am. Qed. End Construction. Definition like (a : E) := a = create (U a) (leq a). Lemma create_like : forall a : E, like (create (U a) (leq a)). ir. uf like. assert (U (create (U a) (leq a)) = U a). ap underlying_create. rw H. assert (leq (create (U a) (leq a)) = leq a). ap arrow_extensionality; ir. ap arrow_extensionality; ir. ap iff_eq; ir. rwi leq_create_all H0; ee; am. ufi leq H0. ee. rw leq_create_all; ee. am. am. uf leq; ee; am. rw H0. tv. Qed. Ltac cluc := match goal with | id1:?X1 |- _ => rwi underlying_create id1; cluc | |- ?X1 => rw underlying_create | _ => idtac end. Lemma leq_create_then : forall (a : E) (l : E2P) (x y : E), leq (create a l) x y -> A (inc x a) (A (inc y a) (l x y)). ir. rwi leq_create_all H. am. Qed. Lemma leq_create_if : forall (a : E) (l : E2P) (x y : E), inc x a -> inc y a -> l x y -> leq (create a l) x y. ir. rw leq_create; am. Qed. End Order_notation. Module Order. Import Universe. Module Definitions. Export Order_notation. Definition property (a : E) (l : E2P) := A (forall x : E, inc x a -> l x x) (A (forall x y : E, inc x a -> inc y a -> l x y -> l y x -> x = y) (forall x y z : E, inc x a -> inc y a -> inc z a -> l x y -> l y z -> l x z)). Definition axioms (a : E) := A (forall x : E, inc x (U a) -> leq a x x) (A (forall x y : E, leq a x y -> inc x (U a)) (A (forall x y : E, leq a x y -> inc y (U a)) (A (forall x y : E, leq a x y -> leq a y x -> x = y) (forall x y z : E, leq a x y -> leq a y z -> leq a x z)))). Lemma create_axioms : forall (a : E) (l : E2P), property a l -> axioms (create a l). ir. uf axioms. dj. cluc. ap leq_create_if; try am. ufi property H. ee. ap H; am. ufi leq H1. xe. ufi leq H2; xe. assert (inc x a). lapply (H1 x y). ir. cluc. am. am. assert (inc y a). lapply (H2 x y). ir; cluc; am. am. ufi property H; ee. ap H7. am. am. rwi leq_create_all H3; xe. rwi leq_create_all H4; xe. assert (inc x a). lapply (H1 x y); ir. cluc; am. am. assert (inc y a). lapply (H2 x y). ir. cluc; am. am. assert (inc z a). lapply (H2 y z); ir. cluc; am. am. ufi property H; ee. ap leq_create_if. am. am. apply H10 with y. am. am. am. rwi leq_create_all H4; xe. rwi leq_create_all H5; xe. Qed. Lemma lt_leq_trans : forall a x y z : E, axioms a -> lt a x y -> leq a y z -> lt a x z. ir. uf lt; ufi lt H0; ee. ufi axioms H; ee. apply H6 with y; au. uf not; ir. rwi H3 H0. ufi axioms H; ee. ap H2. rw H3. ap H6; au. Qed. Lemma leq_lt_trans : forall a x y z : E, axioms a -> leq a x y -> lt a y z -> lt a x z. ir. uf lt; ufi lt H1; ee. ufi axioms H; ee. apply H6 with y; au. uf not; ir. ap H2. wr H3. wri H3 H1. ufi axioms H; ee. ap H6. exact H1. exact H0. Qed. Lemma leq_refl : forall a x : E, axioms a -> inc x (U a) -> leq a x x. ir. ufi axioms H; xe. ap H; am. Qed. Lemma leq_trans : forall a x y z : E, axioms a -> leq a x y -> leq a y z -> leq a x z. ir. ufi axioms H; ee. apply H5 with y. exact H0. exact H1. Qed. Lemma leq_leq_eq : forall a x y : E, axioms a -> leq a x y -> leq a y x -> x = y. intros. unfold axioms in H; xe. ap H4; am. Qed. Lemma no_lt_leq : forall a x y : E, axioms a -> lt a x y -> leq a y x -> False. ir. ufi axioms H; ufi lt H0; xe. ap H2; ap H5; am. Qed. Lemma leq_eq_or_lt : forall a x y : E, axioms a -> leq a x y -> x = y \/ lt a x y. ir. apply by_cases with (x = y). ir. ap or_introl; am. ir. ap or_intror. uf lt; xe. Qed. End Definitions. Export Definitions. Module SetOfOrders. Section orders_on_section. Variable x : E. Definition is_order_on (a : E) := A (axioms a) (A (U a = x) (like a)). Definition little_leq (lq : x -> x -> Prop) (u v : E) := A (inc u x) (A (inc v x) (forall (hu : inc u x) (hv : inc v x), lq (B hu) (B hv))). Definition lit_lq (a : E) (m n : x) := leq a (R m) (R n). Lemma create_little_leq : forall a : E, is_order_on a -> a = create x (little_leq (lit_lq a)). ir. assert (leq a = little_leq (lit_lq a)). ap arrow_extensionality; intro u. ap arrow_extensionality; intro v. ap iff_eq; ir. ufk leq H0; ee. ufk is_order_on H; ee. uhg; ee. wr H3; am. wr H3; am. ir. uhg. rw B_eq. rw B_eq. am. ufi little_leq H0; ee. cp (H2 H0 H1). ufi lit_lq H3. rwi B_eq H3. rwi B_eq H3. am. wr H0. uh H. ee. wr H1. exact H2. Qed. Lemma is_order_bounded : Bounded.axioms is_order_on. ir. apply Bounded.little_criterion with (x -> x -> Prop) (fun lq : x -> x -> Prop => create x (little_leq lq)). ir. sh (lit_lq y). sy; ap create_little_leq. am. Qed. Definition orders_on := Bounded.create is_order_on. Lemma inc_orders_on : forall a : E, inc a orders_on = is_order_on a. ir. uf orders_on. ap Bounded.inc_create. ap is_order_bounded. Qed. End orders_on_section. End SetOfOrders. Export SetOfOrders. Module Morphisms. Definition mor_axioms (u : E) := A (axioms (source u)) (A (axioms (target u)) (A (strong_axioms u) (forall x y : E, leq (source u) x y -> leq (target u) (ev u x) (ev u y)))). Lemma mor_Umor : forall u : E, mor_axioms u -> strong_axioms u. intros. unfold mor_axioms in H; ee. exact H1. Qed. Coercion mor_Umor_C := mor_Umor. Lemma identity_axioms : forall a : E, axioms a -> mor_axioms (identity a). ir. cx. uf mor_axioms; ee; clst. am. am. ap identity_strong_axioms. ir. rw ev_identity. rw ev_identity. am. lu. lu. Qed. Definition composable (u v : E) := A (mor_axioms u) (A (mor_axioms v) (source u = target v)). Lemma compose_axioms : forall u v : E, composable u v -> mor_axioms (compose u v). intros. unfold composable in H; ee. unfold mor_axioms in H; ee. unfold mor_axioms in H0; ee. unfold mor_axioms in |- *; ee. rewrite source_compose; au. rewrite target_compose; au. apply compose_strong_axioms. unfold Umorphism.composable in |- *; ee. apply axioms_from_strong; am. apply axioms_from_strong; am. am. intros. rewrite target_compose. rewrite ev_compose. rewrite ev_compose. rewrite source_compose in H8. apply H4. rewrite H1. apply H7. am. unfold axioms in H0; ee. rewrite source_compose in H8. lu. rewrite source_compose in H8. unfold axioms in H0; ee. lu. Qed. End Morphisms. Export Morphisms. Module Suborders. Definition suborder (b a : E) := Order_notation.create b (leq a). Lemma suborder_axioms : forall a b : E, axioms a -> sub b (U a) -> axioms (suborder b a). intros. unfold suborder in |- *. apply create_axioms. unfold property in |- *. unfold axioms in H. ee. ir; au. ir. ap H3. exact H7. exact H8. intros. apply H4 with y; au. Qed. Lemma underlying_suborder : forall a b : E, U (suborder b a) = b. intros. unfold suborder in |- *; rewrite underlying_create; tv. Qed. Lemma leq_suborder_if : forall a b x y : E, inc x b -> inc y b -> sub b (U a) -> leq a x y -> leq (suborder b a) x y. intros. unfold suborder in |- *. apply leq_create_if; au. Qed. Lemma leq_suborder_then : forall a b x y : E, axioms a -> sub b (U a) -> leq (suborder b a) x y -> A (inc x b) (A (inc y b) (leq a x y)). intros. ee. unfold suborder in H1. pose (leq_create_then H1). ee; am. unfold suborder in H1. pose (leq_create_then H1); ee; am. unfold suborder in H1. pose (leq_create_then H1); ee; am. Qed. Lemma leq_suborder_all : forall a b x y : E, axioms a -> sub b (U a) -> leq (suborder b a) x y = A (inc x b) (A (inc y b) (leq a x y)). intros. apply iff_eq; intros. pose (leq_suborder_then H H0 H1). ee; am. apply leq_suborder_if; ee; am. Qed. Definition suborder_inclusion (b a : E) := inclusion (suborder b a) a. Lemma suborder_inclusion_mor_axioms : forall a b : E, axioms a -> sub b (U a) -> mor_axioms (suborder_inclusion b a). intros. unfold suborder_inclusion in |- *. unfold mor_axioms in |- *; ee. unfold inclusion in |- *; rewrite source_create. apply suborder_axioms; au. unfold inclusion in |- *; rewrite target_create. am. unfold inclusion in |- *. apply create_strong_axioms. unfold Umorphism.property in |- *. unfold Transformation.axioms in |- *. intros. rewrite underlying_suborder in H1. apply H0; au. intros. unfold inclusion in |- *. rewrite target_create. repeat rewrite ev_create. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1. ee. am. am. am. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1; au. ee. rewrite underlying_suborder; am. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1; au. ee. rewrite underlying_suborder; au. Qed. Definition is_suborder (a b : E) := A (axioms a) (A (axioms b) (A (sub (U a) (U b)) (mor_axioms (inclusion a b)))). Lemma is_suborder_leq : forall a b x y : E, is_suborder a b -> leq a x y -> leq b x y. ir. ufi is_suborder H. ee. ufi mor_axioms H3; ee. assert (b = target (inclusion a b)). uf inclusion; rw target_create. tv. rw H7. assert (x = ev (inclusion a b) x). uf inclusion; rw ev_create; tv. ufi leq H0. ee. am. assert (y = ev (inclusion a b) y). uf inclusion; rw ev_create; tv. ufi leq H0; xe. rw H8; rw H9. ap H6. uf inclusion; rw source_create; am. Qed. Lemma show_is_suborder : forall a b : E, axioms a -> axioms b -> (forall x y : E, leq a x y -> leq b x y) -> is_suborder a b. ir. uf is_suborder; ee. am. am. uf sub; ir. assert (leq b x x). ap H1. ap leq_refl; am. ufi leq H3; xe. uf inclusion. uf mor_axioms. rw source_create. rw target_create. ee. am. am. ap create_strong_axioms. uf Umorphism.property. uf Transformation.axioms. ir. assert (leq b x x). ap H1. ap leq_refl; am. ufi leq H3; xe. ir. rw ev_create. rw ev_create. ap H1; am. ufi leq H2; xe. ufi leq H2; xe. Qed. (*** note that this doesn't imply that the order on (U a) is the same as that induced by the order on (U b) ****) Lemma suborder_is_suborder : forall a b : E, axioms a -> sub b (U a) -> is_suborder (suborder b a) a. ir. uf is_suborder. ee. ap suborder_axioms; am. uf suborder. am. uf suborder. rw underlying_create. am. change (mor_axioms (suborder_inclusion b a)) in |- *. ap suborder_inclusion_mor_axioms; am. Qed. Lemma is_suborder_refl : forall a : E, axioms a -> is_suborder a a. ir. uf is_suborder; dj. am. am. uf sub; ir; am. uf mor_axioms; dj. uf inclusion; rw source_create. am. uf inclusion; rw target_create; am. uf inclusion; ap create_strong_axioms. uf Umorphism.property. uf Transformation.axioms; ir; am. uf inclusion; rw ev_create. rw ev_create. rw target_create. ufi inclusion H6. rwi source_create H6. am. ufi inclusion H6; rwi source_create H6. ufi leq H6; ee. am. ufi inclusion H6; rwi source_create H6. ufi leq H6; ee; am. Qed. Lemma is_suborder_trans : forall a b c : E, is_suborder a b -> is_suborder b c -> is_suborder a c. ir. ap show_is_suborder. ufi is_suborder H; xe. ufi is_suborder H0; xe. ir. apply is_suborder_leq with b. am. apply is_suborder_leq with a. exact H. exact H1. Qed. Definition same_order (a b : E) := A (is_suborder a b) (is_suborder b a). Lemma same_order_refl : forall a : E, axioms a -> same_order a a. ir. uf same_order; ee. ap is_suborder_refl. am. ap is_suborder_refl; am. Qed. Lemma same_order_symm : forall a b : E, same_order a b -> same_order b a. ir. ufi same_order H. uf same_order. ee. am. exact H. Qed. Lemma same_order_trans : forall a b c : E, same_order a b -> same_order b c -> same_order a c. ir. ufi same_order H. ufi same_order H0. uf same_order. ee. apply is_suborder_trans with b. exact H. exact H0. apply is_suborder_trans with b. exact H1. exact H2. Qed. Lemma same_underlying : forall a b : E, same_order a b -> U a = U b. ir. ufi same_order H; ee. ufi is_suborder H. ufi is_suborder H0. ee. ap extensionality. am. am. Qed. Lemma same_leq_eq : forall a b x y : E, same_order a b -> leq a x y = leq b x y. ir. ap iff_eq; ir. ufi same_order H. ee. apply is_suborder_leq with a; am. ufi same_order H; ee. apply is_suborder_leq with b; am. Qed. Lemma same_order_extens : forall a b : E, same_order a b -> like a -> like b -> a = b. ir. assert (U a = U b). ap same_underlying; am. assert (leq a = leq b). ap arrow_extensionality. ir. ap arrow_extensionality. ir. ap same_leq_eq. am. uh H0. rw H0. rw H2. rw H3. sy. exact H1. Qed. Lemma same_as_suborder_is_suborder : forall a b x : E, sub x (U b) -> axioms b -> same_order a (suborder x b) -> is_suborder a b. ir. apply is_suborder_trans with (suborder x b). ufi same_order H1; ee. exact H1. ap suborder_is_suborder. exact H0. am. Qed. Lemma suborder_trans : forall a b c : E, axioms c -> sub a b -> sub b (U c) -> same_order (suborder a (suborder b c)) (suborder a c). ir. uf same_order; ee; ap show_is_suborder. ap suborder_axioms. ap suborder_axioms. am. am. uf suborder; rw underlying_create. am. ap suborder_axioms. am. uf sub; ir; au. ir. ap leq_suborder_if. rwi leq_suborder_all H2. ee; am. ap suborder_axioms; am. uf suborder; rw underlying_create. am. rwi leq_suborder_all H2; ee. am. ap suborder_axioms; am. uf suborder; rw underlying_create. am. uf sub; ir; au. rwi leq_suborder_all H2; ee. rwi leq_suborder_all H4; ee. am. am. am. ap suborder_axioms; am. uf suborder; rw underlying_create; uf sub; ir; au. ap suborder_axioms. am. uf sub; ir; au. ap suborder_axioms. ap suborder_axioms; am. uf suborder; rw underlying_create. am. ir. rwi leq_suborder_all H2; ee. ap leq_suborder_if; au. uf suborder; rw underlying_create; am. ap leq_suborder_if. au. au. am. am. am. uf sub; ir; au. Qed. End Suborders. Export Suborders. Module Linear. Definition is_linear (a : E) := A (axioms a) (forall x y : E, inc x (U a) -> inc y (U a) -> leq a x y \/ leq a y x). Lemma linear_axioms : forall a : E, is_linear a -> axioms a. intros. unfold is_linear in H; ee; am. Qed. Coercion linear_axioms_C := linear_axioms. Lemma linear_not_lt_leq : forall a x y : E, is_linear a -> inc x (U a) -> inc y (U a) -> (lt a x y -> False) -> leq a y x. intros. unfold is_linear in H; ee. pose (H3 _ _ H0 H1). induction o. pose (leq_eq_or_lt H H4). induction o. rewrite H5. unfold axioms in H; ee. ap H; am. elim (H2 H5). am. Qed. Lemma injective_lt_lt : forall u x y : E, mor_axioms u -> injective u -> lt (source u) x y -> lt (target u) (ev u x) (ev u y). ir. ufi lt H1. uf lt; ee. ufi mor_axioms H; xe. ap H5. am. uf not; intros. ufi injective H0; ee. ufi Transformation.injective H4. ee. ufi Transformation.injects H5. ap H2. ap H5. ufi mor_axioms H; ee. ufi axioms H; ee. apply H9 with y. am. ufi mor_axioms H; ee. ufi axioms H; ee. apply H10 with x; au. am. Qed. Lemma linear_injective_leq_back : forall u x y : E, mor_axioms u -> injective u -> is_linear (source u) -> inc x (U (source u)) -> inc y (U (source u)) -> leq (target u) (ev u x) (ev u y) -> leq (source u) x y. intros. apply linear_not_lt_leq; au. intros. pose (injective_lt_lt H H0 H5). apply no_lt_leq with (target u) (ev u y) (ev u x). assert (mor_axioms u). am. unfold mor_axioms in H6; ee. am. am. am. Qed. Lemma linear_injective_lt_back : forall u x y : E, mor_axioms u -> injective u -> is_linear (source u) -> inc x (U (source u)) -> inc y (U (source u)) -> lt (target u) (ev u x) (ev u y) -> lt (source u) x y. intros. unfold lt in H4. unfold lt in |- *; ee. apply linear_injective_leq_back; au. unfold not in |- *; intros. apply H5. rewrite H6; tv. Qed. Definition is_linear_subset (a b : E) := A (axioms a) (A (sub b (U a)) (is_linear (suborder b a))). Lemma linear_sub : forall a b c : E, is_linear_subset a b -> sub c b -> is_linear_subset a c. ir. ufi is_linear_subset H; uf is_linear_subset; dj; ee. am. uf sub; ir; au. ufi is_linear H4; uf is_linear; dj; ee. ap suborder_axioms; am. assert (inc x (U (suborder b a))). rw underlying_suborder. ap H0. rwi underlying_suborder H6. am. assert (inc y (U (suborder b a))). rw underlying_suborder. ap H0. rwi underlying_suborder H7; am. cp (H8 x y H9 H10). nin H11. ap or_introl. rwi underlying_suborder H6. rwi underlying_suborder H7. ap leq_suborder_if; try am. rwi leq_suborder_all H11; ee. am. am. am. ap or_intror. rwi underlying_suborder H6. rwi underlying_suborder H7. rw leq_suborder_all. rwi leq_suborder_all H11. xd. am. am. am. am. Qed. End Linear. Export Linear. Module Bounds. Definition is_minimal (a b x : E) := A (axioms a) (A (sub b (U a)) (A (inc x b) (forall y : E, inc y b -> leq a y x -> y = x))). Lemma minimal_axioms : forall a b x : E, is_minimal a b x -> axioms a. intros. unfold is_minimal in H; ee; am. Qed. Coercion minimal_axioms_C := minimal_axioms. Definition is_maximal (a b x : E) := A (axioms a) (A (sub b (U a)) (A (inc x b) (forall y : E, inc y b -> leq a x y -> x = y))). Lemma maximal_axioms : forall a b x : E, is_maximal a b x -> axioms a. intros. unfold is_maximal in H; ee; am. Qed. Coercion maximal_axioms_C := maximal_axioms. Definition is_upper_bound (a b x : E) := A (axioms a) (A (sub b (U a)) (A (inc x (U a)) (forall y : E, inc y b -> leq a y x))). Lemma upper_bound_axioms : forall a b x : E, is_upper_bound a b x -> axioms a. intros. unfold is_upper_bound in H; ee; am. Qed. Coercion upper_bound_axiomsC := upper_bound_axioms. Definition is_lower_bound (a b x : E) := A (axioms a) (A (sub b (U a)) (A (inc x (U a)) (forall y : E, inc y b -> leq a x y))). Lemma lower_bound_axioms : forall a b x : E, is_lower_bound a b x -> axioms a. intros. unfold is_lower_bound in H; ee; am. Qed. Coercion lower_bound_axiomsC := lower_bound_axioms. Definition is_bottom_element (a b x : E) := A (is_lower_bound a b x) (inc x b). Lemma bottom_element_lower_bound : forall a b x : E, is_bottom_element a b x -> is_lower_bound a b x. intros. unfold is_bottom_element in H; ee; am. Qed. Coercion bottom_element_lower_boundC := bottom_element_lower_bound. Definition is_top_element (a b x : E) := A (is_upper_bound a b x) (inc x b). Lemma top_element_upper_bound : forall a b x : E, is_top_element a b x -> is_upper_bound a b x. intros. unfold is_top_element in H; ee; am. Qed. Coercion top_element_upper_boundC := top_element_upper_bound. Lemma top_element_maximal : forall a b x : E, is_top_element a b x -> is_maximal a b x. intros. unfold is_top_element in H. unfold is_upper_bound in H. unfold is_maximal in |- *. ee. intros. am. am. am. ir. ufi axioms H; ee. ap H8. am. ap H3; am. Qed. Coercion top_element_maximalC := top_element_maximal. Lemma bottom_element_minimal : forall a b x : E, is_bottom_element a b x -> is_minimal a b x. intros. unfold is_bottom_element in H. unfold is_lower_bound in H. unfold is_minimal in |- *. xe. intros. unfold axioms in H; xe. ap H8. am. ap H3. am. Qed. Coercion bottom_element_minimalC := bottom_element_minimal. Lemma top_element_unique : forall a b x y : E, is_top_element a b x -> is_top_element a b y -> x = y. intros. unfold is_top_element in H, H0; xe. unfold is_upper_bound in H, H0; xe. unfold axioms in H; xe. ap H11. ap H6; am. ap H8; am. Qed. Lemma bottom_element_unique : forall a b x y : E, is_bottom_element a b x -> is_bottom_element a b y -> x = y. intros. unfold is_bottom_element in H, H0; xe. unfold is_lower_bound in H, H0; xe. unfold axioms in H; xe. ap H11. ap H8; am. ap H6; am. Qed. Lemma linear_maximal_top_element : forall a b x : E, is_linear a -> is_maximal a b x -> is_top_element a b x. intros. unfold is_linear in H. unfold is_maximal in H0. unfold is_top_element in |- *. unfold is_upper_bound in |- *. xd. intros. assert (inc x (U a)). apply H1; au. assert (inc y (U a)). apply H1; au. pose (H2 _ _ H6 H7). induction o. uh H. ee. assert (x = y). apply H4; au. rewrite H13. ap H; am. am. Qed. Lemma linear_minimal_bottom_element : forall a b x : E, is_linear a -> is_minimal a b x -> is_bottom_element a b x. intros. unfold is_linear in H. unfold is_minimal in H0. unfold is_bottom_element in |- *. unfold is_lower_bound in |- *. xd. intros. assert (inc x (U a)). apply H1; au. assert (inc y (U a)). apply H1; au. pose (H2 _ _ H6 H7). induction o. unfold axioms in H; xe. assert (y = x). apply H4; au. rewrite H9. unfold axioms in H; ee. ap H. am. Qed. Definition downward_subset (a x : E) := Z (U a) (fun y : E => leq a y x). Definition punctured_downward_subset (a x : E) := Z (U a) (fun y : E => lt a y x). Definition downward_suborder (a x : E) := suborder (downward_subset a x) a. Definition punctured_downward_suborder (a x : E) := suborder (punctured_downward_subset a x) a. End Bounds. Export Bounds. Module WellOrdered. Definition is_well_ordered (a : E) := A (is_linear a) (forall b : E, sub b (U a) -> nonempty b -> ex (fun x : E => is_bottom_element a b x)). Lemma wo_linear : forall a : E, is_well_ordered a -> is_linear a. intros. unfold is_well_ordered in H; xe. Qed. Coercion wo_linear_C := wo_linear. Lemma bottom_element_no_lt : forall a b x y : E, is_bottom_element a b x -> lt a y x -> inc y b -> False. intros. unfold is_bottom_element in H; ee. unfold is_lower_bound in H; ee. assert (leq a x y). apply H5; am. apply no_lt_leq with a y x; au. Qed. Definition choose_bottom_element (a b : E) := choose (fun x : E => is_bottom_element a b x). Lemma wo_choose_bottom : forall a b : E, is_well_ordered a -> sub b (U a) -> nonempty b -> is_bottom_element a b (choose_bottom_element a b). intros. unfold is_well_ordered in H; ee. pose (H2 b H0 H1). pose (choose_pr e). am. Qed. Lemma wo_induction : forall (a : E) (H : is_well_ordered a) (p : EP), (forall x : E, inc x (U a) -> (forall y : E, inc y (U a) -> lt a y x -> p y) -> p x) -> forall x : E, inc x (U a) -> p x. ir. set (b := Z (U a) (fun z : E => ~ p z)). ap excluded_middle; uf not; ir. assert (nonempty b). apply nonempty_intro with x. uf b. Ztac. set (z := choose_bottom_element a b). assert (is_bottom_element a b z). uf z; ap wo_choose_bottom. am. uf b; ap Z_sub. am. assert (sub b (U a)). uf b; ap Z_sub. assert (inc z b). ufi is_bottom_element H4; ee. assert (inc z (U a)). ap H5; am. am. assert (~ p z). ufi b H6. Ztac. ap H7. ap H0; ir. au. ap excluded_middle; uf not; ir. assert (inc y b). uf b; Ztac. apply bottom_element_no_lt with a b z y; au. Qed. Definition is_wo_subset (a b : E) := A (is_linear_subset a b) (is_well_ordered (suborder b a)). Lemma wo_same_order : forall a b : E, same_order a b -> is_well_ordered a -> is_well_ordered b. ir. uhg; dj. uhg; dj. ufi same_order H; ee. ufi is_suborder H; ee. am. assert (leq b x y = leq a x y). sy; ap same_leq_eq. am. assert (leq b y x = leq a y x). sy; ap same_leq_eq; am. rw H4. rw H5. uh H0. ee. uh H0; ee. ap H7. assert (U a = U b). ap same_underlying. am. rw H8; am. assert (U a = U b). ap same_underlying; am. rw H8; am. assert (U a = U b). ap same_underlying; am. assert (sub b0 (U a)). rw H4; am. uh H0; ee. cp (H6 _ H5 H3). nin H7. sh x. uhg; ee. uhg; ee. uh H; ee. ufi is_suborder H; ee. am. am. uh H7; ee. ap H2; am. ir. assert (leq b x y = leq a x y). sy. ap same_leq_eq. am. rw H9. uh H7. ee. uh H7. ee. ap H13. am. uh H7. ee. am. Qed. (*** a scale is a morphism between well ordered subsets that starts at the bottom and is injective with no gaps ***) Definition is_scale (u : E) := A (mor_axioms u) (A (injective u) (A (is_well_ordered (source u)) (A (is_well_ordered (target u)) (forall x y : E, inc x (U (source u)) -> leq (target u) y (ev u x) -> ex (fun z : E => A (inc z (U (source u))) (ev u z = y)))))). Lemma scale_mor_axioms : forall u : E, is_scale u -> mor_axioms u. intros. unfold is_scale in H; ee; am. Qed. Coercion scale_mor_axiomsC := scale_mor_axioms. Lemma scale_injective : forall u : E, is_scale u -> injective u. intros. unfold is_scale in H; ee; am. Qed. Coercion scale_injectiveC := scale_injective. Lemma scale_leq_back : forall u x y : E, is_scale u -> inc x (U (source u)) -> inc y (U (source u)) -> leq (target u) (ev u x) (ev u y) -> leq (source u) x y. intros. unfold is_scale in H; ee. unfold is_well_ordered in H4; ee. apply linear_injective_leq_back; au. Qed. Lemma scale_lt_back : forall u x y : E, is_scale u -> inc x (U (source u)) -> inc y (U (source u)) -> lt (target u) (ev u x) (ev u y) -> lt (source u) x y. intros. unfold is_scale in H; ee. unfold is_well_ordered in H4; ee. apply linear_injective_lt_back; au. Qed. Lemma scale_leq_ev : forall u v x : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> inc x (U (source u)) -> leq (target v) (ev u x) (ev v x). intros. unfold is_scale in H, H0; ee. apply (wo_induction H9 (p:=fun w : E => leq (target v) (ev u w) (ev v w))). intros. unfold is_well_ordered in H10; ee. unfold is_linear in H10; ee. apply linear_not_lt_leq. unfold is_well_ordered in H7; xe. unfold mor_axioms in H0; ee. unfold strong_axioms in H17; ee; unfold Umorphism.axioms in H17. apply H17. rewrite <- H1; am. rewrite <- H2. unfold mor_axioms in H; ee. unfold strong_axioms in H17; ee. ap H17; exact H12. intros. unfold lt in H16; ee. rewrite <- H2 in H16. pose (H11 _ _ H12 H16). induction e. ee. assert (lt (source u) x1 x0). apply scale_lt_back. unfold is_scale in |- *; ee. am. exact H5. exact H9. rewrite H2; am. am. am. am. rewrite H19. unfold lt in |- *; xe. assert (lt (target v) (ev v x1) (ev v x0)). apply injective_lt_lt. am. am. rewrite <- H1; am. assert (leq (target v) (ev u x1) (ev v x1)). apply H13. am. am. unfold lt in H21; ee. apply H23. apply leq_leq_eq with (target v). wr H2. am. exact H21. wr H19. exact H22. exact H3. Qed. Lemma scale_same_ev : forall u v x : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> inc x (U (source u)) -> ev u x = ev v x. intros. apply leq_leq_eq with (target u). unfold is_scale in H; ee. unfold mor_axioms in H; xe. rewrite H2. apply scale_leq_ev; au. apply scale_leq_ev; au. rewrite <- H1; am. Qed. Lemma scale_unique : forall u v : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> u = v. intros. apply extens. unfold is_scale in H; ee. unfold mor_axioms in H; xe. unfold is_scale in H0; ee. unfold mor_axioms in H0; xe. am. am. intros. apply scale_same_ev; au. Qed. Definition scale_subset (a b : E) := A (is_well_ordered b) (A (sub a (U b)) (forall x y : E, inc y a -> leq b x y -> inc x a)). Lemma source_suborder_inclusion : forall a b : E, source (suborder_inclusion a b) = suborder a b. ir. uf suborder_inclusion. uf inclusion; rw source_create. tv. Qed. Lemma target_suborder_inclusion : forall a b : E, target (suborder_inclusion a b) = b. ir. uf suborder_inclusion. uf inclusion; rw target_create. tv. Qed. Lemma ev_suborder_inclusion : forall a b x : E, inc x a -> ev (suborder_inclusion a b) x = x. ir. uf suborder_inclusion. uf inclusion; rw ev_create. tv. rw underlying_suborder; am. Qed. Lemma suborder_well_ordered : forall a b : E, sub a (U b) -> is_well_ordered b -> is_well_ordered (suborder a b). ir. ufk is_well_ordered H0; ee. ufk is_linear H0; ee. uf is_well_ordered; dj. uf is_linear; dj. ap suborder_axioms; am. rw leq_suborder_all. rw leq_suborder_all. cp (H2 x y). lapply H6. ir. lapply H7; ir. nin H8. ap or_introl. ee. rwi underlying_suborder H4. exact H4. rwi underlying_suborder H5; ap H5. am. ap or_intror. ee. rwi underlying_suborder H5; ap H5. rwi underlying_suborder H4; ap H4. am. ap H. rwi underlying_suborder H5; ap H5. ap H. rwi underlying_suborder H4; ap H4. am. am. am. am. assert (sub b0 (U b)). uf sub; ir; ap H. rwi underlying_suborder H4; ap H4. am. cp (H1 b0 H6 H5). nin H7. sh x. uf is_bottom_element; dj. uf is_lower_bound; dj. ap suborder_axioms. am. am. am. ap H9. ufi is_bottom_element H7; ee. am. rw leq_suborder_all; dj. rwi underlying_suborder H9. ap H9. ufi is_bottom_element H7; ee. am. rwi underlying_suborder H9; ap H9; am. ufi is_bottom_element H7; ee. ufi is_lower_bound H7; ee. ap H17. am. am. am. ufi is_bottom_element H7; ee; am. Qed. Lemma wo_sub : forall a b c : E, is_wo_subset a b -> sub c b -> is_wo_subset a c. ir. uh H. ee. uhg. dj. apply linear_sub with b. am. am. apply wo_same_order with (suborder c (suborder b a)). ap suborder_trans. uh H. ee. am. am. uh H. ee. am. ap suborder_well_ordered. rw underlying_suborder. am. am. Qed. Lemma wo_sub_bottom : forall a b : E, is_wo_subset a b -> nonempty b -> is_bottom_element a b (choose_bottom_element a b). ir. assert (ex (fun x : E => is_bottom_element a b x)). uh H; ee. set (y := choose_bottom_element (suborder b a) b). assert (is_bottom_element (suborder b a) b y). uf y. ap wo_choose_bottom. am. rw underlying_suborder. uf sub; ir; am. am. sh y. uh H2. ee. uh H2; ee. uhg. ee. uhg; ee. uh H; ee. am. uh H; ee. am. uh H; ee. ap H7; am. ir. cp (H6 _ H7). rwi leq_suborder_all H8; ee. am. uh H; ee; am. uh H; ee; am. am. cp (choose_pr H1). exact H2. Qed. Lemma scale_suborder_inclusion : forall a b : E, scale_subset a b -> is_scale (suborder_inclusion a b). ir. ufi scale_subset H; ee. ufk is_well_ordered H. ee. ufk is_linear H; ee. ufk axioms H; ee. uf is_scale; dj. ap suborder_inclusion_mor_axioms. am. am. uf injective. dj. ufi mor_axioms H8; ee. ufi strong_axioms H10; ee. exact H10. uf Transformation.injective. rw source_suborder_inclusion. rw target_suborder_inclusion. rw underlying_suborder. dj. uf Transformation.axioms. ir. rw ev_suborder_inclusion. ap H0; am. am. uf Transformation.injects. ir. rwi ev_suborder_inclusion H13; try am. rw H13. rw ev_suborder_inclusion. tv. am. rw source_suborder_inclusion. ap suborder_well_ordered. am. am. rw target_suborder_inclusion. am. sh y. dj. rw source_suborder_inclusion. rw underlying_suborder. apply H1 with x. rwi source_suborder_inclusion H12. rwi underlying_suborder H12. exact H12. rwi target_suborder_inclusion H13. rwi ev_suborder_inclusion H13. exact H13. rwi source_suborder_inclusion H12. rwi underlying_suborder H12. exact H12. rw ev_suborder_inclusion. tv. rwi source_suborder_inclusion H14. rwi underlying_suborder H14. exact H14. Qed. (* Lemma empty_scale_subset : (a:E)(is_well_ordered a) -> (scale_subset emptyset a). Save. Lemma scale_subset_intersection2 : (a,u,v:E)(scale_subset u a) -> (scale_subset v a) -> (scale_subset (intersection2 u v) a). Save. Definition is_scale_between := [a,b,f:E] (A (is_well_ordered a) (A (is_well_ordered b) (A (is_scale f) (A (source f) == a (target f) == b )). Lemma scale_between_compose : (a,b,c,f,g:E)(is_scale_between a b f) -> (is_scale_between b c g) -> (is_scale_between a c (Umorphism.compose g f)). Save. Lemma scale_between_identity : (a,f:E)(is_scale_between a a f) -> f == (Umorphism.identity a). Save. Lemma scale_between_inverse : (a,b,f,g:E)(is_scale_between a b f) -> (is_scale_between b a g) -> (Umorphism.are_inverse f g). Save. Lemma scale_between_surjective_inverse : (a,b,f:E)(is_scale_between a b f) -> (Umorphism.surjective f) -> (is_scale_between b a (Umorphism.inverse f)). Save. Definition ordinal_leq := [a,b:E] (exists [f:E](is_scale_between a b f)). Lemma ordinal_leq_refl : (a:E)(is_well_ordered a) -> (ordinal_leq a a). Save. Lemma ordinal_leq_trans : (a,b,c:E)(ordinal_leq a b) -> (ordinal_leq b c) -> (ordinal_leq a c). Save. Definition same_ordinal := [a,b:E] (A (ordinal_leq a b) (ordinal_leq b a)). Lemma same_ordinal_refl : (a:E)(is_well_ordered a) -> (same_ordinal a a). Save. Lemma same_ordinal_symm : (a,b:E)(same_ordinal a b) -> (same_ordinal b a). Save. Lemma same_ordinal_trans : (a,b,c:E)(same_ordinal a b) -> (same_ordinal b c) -> (same_ordinal a c). Save. Definition correspond := [a,b,x,y:E] (A (is_well_ordered a) (A (is_well_ordered b) (A (inc x (U a)) (A (inc y (U b)) (same_ordinal (downward_suborder a x) (downward_suborder b y)) )))). Definition corresponding := [a,b,x:E](choose [y:E](correspond a b x y)). Definition has_correspondant := [a,b,x:E](exists [y:E](correspond a b x y)). Lemma correspond_symm : (a,b,x,y:E)(correspond a b x y) -> (correspond b a y x). Save. Lemma correspond_refl : (a,x:E)(is_well_ordered a) -> (inc x (U a)) -> (correspond a a x x). Save. Lemma correspond_trans : (a,b,c,x,y,z:E)(correspond a b x y) -> (correspond b c y z) -> (correspond a c x z). Save. Lemma corresponding_unique : (a,b,x,y:E)(correspond a b x y) -> (corresponding a b x) == y. Save. Lemma scale_correspond : (a,b,f,x:E)(is_scale_between a b f) -> (inc x (U a)) -> (correspond a b x (ev f x)). Save. Lemma has_correspondant_leq : (a,b,x,u:E)(has_correspondant a b x) -> (leq a u x) -> (has_correspondant a b u). Save. Lemma has_correspondant_scale_subset : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) -> (scale_subset (Z (U a) [x:E](has_correspondant a b x)) a). Save. Lemma have_correspondants_disj : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) -> ((x:E)(inc x (U a)) -> (has_correspondant a b x)) \/ ((y:E)(inc y (U b)) -> (has_correspondant b a y)). Save. Lemma ordinal_leq_disj : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) -> (ordinal_leq a b) \/ (ordinal_leq b a). Save. *) End WellOrdered. Export WellOrdered. Module Zorn. Definition is_ultra_bound (a b x : E) := A (is_upper_bound a b x) (~ inc x b). Definition ultra_bound (a b : E) := choose (fun x : E => is_ultra_bound a b x). (*** here a is the order and b is the subset ***) Definition eq_ultra_bound (a b x : E) := A (is_ultra_bound a b x) (ultra_bound a b = x). Definition is_ultra_zorn (a : E) := A (axioms a) (forall b : E, is_linear_subset a b -> is_ultra_bound a b (ultra_bound a b)). Definition is_ultra_linear_subset (a b : E) := A (is_wo_subset a b) (forall x : E, inc x b -> eq_ultra_bound a (intersection2 b (punctured_downward_subset a x)) x). Definition coincide_at (a b c x : E) := A (inc x b) (A (inc x c) (A (forall y : E, inc y b -> leq a y x -> inc y c) (forall y : E, inc y c -> leq a y x -> inc y b))). Definition coinciders (a b c : E) := Z b (fun x : E => coincide_at a b c x). Lemma coinciders_symm : forall a b c : E, coinciders a b c = coinciders a c b. assert (forall a b c x : E, coincide_at a b c x -> coincide_at a c b x). ir. uh H; uhg; xd. assert (forall a b c : E, sub (coinciders a b c) (coinciders a c b)). ir. uf sub; ir. uf coinciders. ufi coinciders H0. Ztac. ap Z_inc. uh H2; xd. ap H. am. ir. ap extensionality. ap H0. ap H0. Qed. Definition downward_saturated (a b c : E) := A (axioms a) (A (sub b (U a)) (A (sub c b) (forall x y : E, inc x c -> inc y b -> leq a y x -> inc y c))). Lemma coinciders_saturated : forall a b c : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b (coinciders a b c). ir. uhg. dj. uh H; ee. uh H; ee. uh H; ee. am. uh H; ee. uh H; ee. uh H; ee. am. uhg; ir. ufi coinciders H3; Ztac. uf coinciders; ap Z_inc. am. uhg; ee. am. ufi coinciders H4. Ztac. uh H8; ee. au. ir. ufi coinciders H4; Ztac. uh H10. ee. ap H12. am. uh H1; ee. apply H17 with y. am. am. ir. ufi coinciders H4. Ztac. uh H10; ee. ap H13. am. uh H1; ee. apply H17 with y. am. am. Qed. Lemma scale_next : forall a b c z : E, is_ultra_linear_subset a b -> downward_saturated a b c -> is_bottom_element a (complement b c) z -> eq_ultra_bound a c z. ir. assert (intersection2 b (punctured_downward_subset a z) = c). ap extensionality; uf sub; ir. apply use_complement with b. cp (intersection2_first H2). am. uf not; ir. assert (inc x (punctured_downward_subset a z)). cp (intersection2_second H2). am. ufi punctured_downward_subset H4; Ztac. uh H1; ee. uh H1; ee. cp (H10 _ H3). apply no_lt_leq with a x z. am. am. am. ap intersection2_inc. uh H0; ee. ap H4; am. uf punctured_downward_subset; ap Z_inc. uh H0; ee. ap H3. ap H4; am. uh H. ee. uh H. ee. uh H; ee. uh H6; ee. assert (inc x (U (suborder b a))). rw underlying_suborder. uh H0; ee. ap H9; am. assert (inc z (U (suborder b a))). rw underlying_suborder. uh H1; ee. uh H1; ee. rwi inc_complement H9; ee. am. cp (H7 _ _ H8 H9). nin H10. rwi leq_suborder_all H10. ee. cp (leq_eq_or_lt H H12). nin H13. uh H1; ee. rwi inc_complement H14. ee. assert False. ap H15. wr H13. am. elim H16. am. am. am. rwi leq_suborder_all H10; ee. uh H0. ee. assert (inc z c). apply H15 with x. am. am. am. uh H1. ee. rwi inc_complement H17; ee. assert False. ap H18; am. elim H19. am. am. wr H2. uh H; ee. ap H3. uh H1. ee. rwi inc_complement H4. ee. am. Qed. Lemma next_eq : forall a b c d x y : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b d -> downward_saturated a c d -> is_bottom_element a (complement b d) x -> is_bottom_element a (complement c d) y -> x = y. ir. cp (scale_next H H1 H3). cp (scale_next H0 H2 H4). ufi eq_ultra_bound H5. ufi eq_ultra_bound H6. ee. wr H8; am. Qed. Lemma next_or : forall a b c x y : E, is_ultra_linear_subset a b -> downward_saturated a b c -> is_bottom_element a (complement b c) x -> inc y b -> leq a y x -> x = y \/ inc y c. ir. assert (axioms a). uh H. ee. uh H; ee. uh H; ee. am. cp (leq_eq_or_lt H4 H3). nin H5. ap or_introl. sy; am. assert (x <> y -> inc y c). ir. apply use_complement with b. am. uf not; ir. uh H1; ee. uh H1; ee. cp (H11 y H7). assert (x = y). apply leq_leq_eq with a. am. am. am. ap H6; am. ap excluded_middle. uf not; ir. ap H7. ap or_introl. ap excluded_middle. uf not; ir. ap H7. ap or_intror. ap H6; am. Qed. Lemma next_coincide : forall a b c d x y : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b d -> downward_saturated a c d -> is_bottom_element a (complement b d) x -> is_bottom_element a (complement c d) y -> coincide_at a b c x. ir. assert (x = y). apply next_eq with a b c d; am. uhg. dj. ufi is_bottom_element H3; ee. rwi inc_complement H6; ee. am. ufi is_bottom_element H4; ee. rwi inc_complement H7; ee. rw H5; am. cp (next_or H H1 H3 H8 H9). nin H10. wr H10. am. ufi downward_saturated H2; ee. ap H12; am. assert (leq a y0 y). wr H5. am. cp (next_or H0 H2 H4 H9 H11). nin H12. wr H12. wr H5; am. ufi downward_saturated H1; ee. ap H14. am. Qed. Lemma show_sub_or : forall b c : E, (nonempty (complement b c) -> nonempty (complement c b) -> False) -> sub b c \/ sub c b. exact (fun (b c : E) (H : nonempty (complement b c) -> nonempty (complement c b) -> False) => excluded_middle (fun H0 : sub b c \/ sub c b -> False => H (excluded_middle (fun H1 : nonempty (complement b c) -> False => H0 (or_introl (sub c b) (fun (x : E) (H2 : inc x b) => excluded_middle (fun H3 : inc x c -> False => H1 (nonempty_intro (eq_ind_r (fun P : Prop => P) ( conj H2 H3) (inc_complement b c x)))))))) (excluded_middle (fun H1 : nonempty (complement c b) -> False => H0 (or_intror (sub b c) (fun (x : E) (H2 : inc x c) => excluded_middle (fun H3 : inc x b -> False => H1 (nonempty_intro (eq_ind_r (fun P : Prop => P) ( conj H2 H3) (inc_complement c b x)))))))))). Qed. Lemma wo_subset_choose_bottom : forall a b : E, is_wo_subset a b -> nonempty b -> is_bottom_element a b (choose_bottom_element a b). ir. assert (ex (fun x : E => is_bottom_element a b x)). uh H. ee. uh H1; ee. assert (sub b (U (suborder b a))). rw underlying_suborder. uf sub; ir; am. cp (H2 b H3 H0). nin H4. sh x. uhg. ee. uhg; ee. uh H. ee; am. uh H; ee; am. uh H4; ee. uh H; ee. ap H6; am. ir. uh H4; ee. uh H4; ee. cp (H9 y H5). rwi leq_suborder_all H10; ee. am. uh H; ee; am. uh H; ee; am. uh H4; ee. am. cp (choose_pr H1). exact H2. Qed. Lemma uls_or : forall a b c : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> sub b c \/ sub c b. ir. set (d := coinciders a b c). assert (downward_saturated a b d). uf d; ap coinciders_saturated. am. am. assert (downward_saturated a c d). uf d. assert (coinciders a b c = coinciders a c b). ap coinciders_symm. rw H2. ap coinciders_saturated. am. am. apply show_sub_or; ir. assert (nonempty (complement b d)). nin H3. sh y. rw inc_complement; ee. rwi inc_complement H3; ee. am. uf not; ir. rwi inc_complement H3; ee. ap H6. uh H2; ee. ap H8; am. assert (nonempty (complement c d)). nin H4. sh y. rw inc_complement; ee. rwi inc_complement H4; ee; am. uf not; ir. rwi inc_complement H4; ee. ap H7. uh H1; ee. ap H9. am. ufk is_ultra_linear_subset H. ufk is_ultra_linear_subset H0. ee. assert (is_wo_subset a (complement b d)). apply wo_sub with b. am. uf sub; ir. rwi inc_complement H9; ee; am. assert (is_wo_subset a (complement c d)). apply wo_sub with c. am. uf sub; ir. rwi inc_complement H10; ee; am. cp (wo_sub_bottom H9 H5). cp (wo_sub_bottom H10 H6). set (x := choose_bottom_element a (complement b d)) in *. set (y := choose_bottom_element a (complement c d)) in *. cp (next_eq X0 X1 H1 H2 H11 H12). cp (next_coincide X0 X1 H1 H2 H11 H12). assert (inc x d). uf d. uf coinciders. ap Z_inc. ufi is_bottom_element H11; ee. rwi inc_complement H15; ee; am. am. ufi is_bottom_element H11. ee. rwi inc_complement H16. ee. ap H17; am. Qed. Lemma uls_sub_downward_saturated : forall (a b c : E) (hyp : sub c b), is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b c. ir. set (d := coinciders a b c). assert (downward_saturated a b d). uf d; ap coinciders_saturated. am. am. assert (downward_saturated a c d). uf d. assert (coinciders a b c = coinciders a c b). ap coinciders_symm. rw H2. ap coinciders_saturated. am. am. apply excluded_middle; uf not; ir. assert (nonempty (complement b d)). apply excluded_middle; uf not; ir. assert (sub b d). uf sub; ir. apply use_complement with b. am. uf not; ir. ap H4. sh x. am. assert (c = d). ap extensionality; uf sub; ir. ap H5. ap hyp. am. ufi downward_saturated H2; ee. ap H8; am. ap H3. rw H6. am. assert (nonempty (complement c d)). apply excluded_middle; uf not; ir. assert (sub c d). uf sub; ir. apply use_complement with c. am. uf not; ir. ap H5; sh x. am. assert (c = d). ap extensionality. am. ufi downward_saturated H2; ee. am. ap H3. rw H7; exact H1. ufk is_ultra_linear_subset H. ufk is_ultra_linear_subset H0. ee. assert (is_wo_subset a (complement b d)). apply wo_sub with b. am. uf sub; ir. rwi inc_complement H8; ee; am. assert (is_wo_subset a (complement c d)). apply wo_sub with c. am. uf sub; ir. rwi inc_complement H9; ee; am. cp (wo_sub_bottom H8 H4). cp (wo_sub_bottom H9 H5). set (x := choose_bottom_element a (complement b d)) in *. set (y := choose_bottom_element a (complement c d)) in *. cp (next_eq X0 X1 H1 H2 H10 H11). cp (next_coincide X0 X1 H1 H2 H10 H11). assert (inc x d). uf d. uf coinciders. ap Z_inc. ufi is_bottom_element H10; ee. rwi inc_complement H14; ee; am. am. ufi is_bottom_element H11. ee. rwi inc_complement H15. ee. ap H16. wr H12. am. Qed. Definition increasing_ds_family (a f : E) := forall x y : E, inc x f -> inc y f -> downward_saturated a x y \/ downward_saturated a y x. Lemma wo_subset_increasing_union : forall a f : E, axioms a -> increasing_ds_family a f -> (forall b : E, inc b f -> is_wo_subset a b) -> is_wo_subset a (union f). ir. uhg. dj. uhg; dj. am. uhg; ir. cp (union_exists H3). nin H4; ee. cp (H1 x0 H5). ufi is_wo_subset H6. ee. ufi is_linear_subset H6; ee. ap H8; am. uhg; dj. ap suborder_axioms. am. am. rwi underlying_suborder H5. rwi underlying_suborder H6. cp (union_exists H5). nin H7. cp (union_exists H6). nin H8. ee. ufi increasing_ds_family H0. cp (H0 _ _ H10 H9). nin H11. assert (inc y x0). ufi downward_saturated H11. ee. ap H13; am. cp (H1 x0 H10). ufi is_wo_subset H13. ee. ufi is_linear_subset H13; ee. ufi is_linear H16; ee. assert (inc x (U (suborder x0 a))). rw underlying_suborder. am. assert (inc y (U (suborder x0 a))). rw underlying_suborder. am. cp (H17 x y H18 H19). nin H20. ap or_introl. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. ap or_intror. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. assert (inc x x1). ufi downward_saturated H11. ee. ap H13; am. cp (H1 x1 H9). ufi is_wo_subset H13. ee. ufi is_linear_subset H13; ee. ufi is_linear H16; ee. assert (inc x (U (suborder x1 a))). rw underlying_suborder. am. assert (inc y (U (suborder x1 a))). rw underlying_suborder. am. cp (H17 x y H18 H19). nin H20. ap or_introl. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. ap or_intror. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. uhg; dj. ufi is_linear_subset H2; ee. am. nin H5. assert (inc y (union f)). rwi underlying_suborder H4. ap H4. am. cp (union_exists H6). nin H7. ee. assert (is_wo_subset a x). ap H1; am. ufi is_wo_subset H9. ee. assert (nonempty (intersection2 b x)). sh y. ap intersection2_inc. am. am. set (z := choose_bottom_element (suborder x a) (intersection2 b x)). assert (is_bottom_element (suborder x a) (intersection2 b x) z). uf z. ap wo_choose_bottom. am. uf sub; ir. cp (intersection2_second H12). rw underlying_suborder. am. am. sh z. ufi is_bottom_element H12. ee. assert (sub (union f) (U a)). uf sub; ir. cp (union_exists H14). nin H15; ee. assert (is_wo_subset a x1). ap H1; am. ufi is_wo_subset H17; ee. ufi is_linear_subset H17; ee. ap H19. am. uf is_bottom_element; dj. ufi is_lower_bound H12; uf is_lower_bound; ee. ap suborder_axioms. am. am. am. rw underlying_suborder. apply union_inc with x. rwi underlying_suborder H16; am. am. ir. assert (inc y0 (union f)). rwi underlying_suborder H4. ap H4; am. cp (union_exists H19). nin H20; ee. ufi increasing_ds_family H0. cp (H0 x x0 H8 H21). nin H22. assert (leq (suborder x a) z y0). ap H17. ap intersection2_inc. am. ufi downward_saturated H22. ee. ap H24; am. rw leq_suborder_all. rwi leq_suborder_all H23. ee. apply union_inc with x. am. am. apply union_inc with x. am. am. am. am. ufi is_linear_subset H9; ee. am. am. am. ufi is_linear H3. ee. assert (leq (suborder (union f) a) z y0 \/ leq (suborder (union f) a) y0 z). ap H23. rw underlying_suborder. apply union_inc with x. apply intersection2_second with b. am. am. rw underlying_suborder. am. nin H24. am. assert (inc z x). apply intersection2_second with b. exact H13. assert (inc y0 x). ufi downward_saturated H22. ee. apply H28 with z. am. am. rwi leq_suborder_all H24; ee. am. am. am. assert (leq (suborder x a) z y0). ap H17. ap intersection2_inc. am. am. rw leq_suborder_all; ee. apply union_inc with x. am. am. apply union_inc with x. am. am. rwi leq_suborder_all H27; ee. am. am. ufi is_linear_subset H9; ee. exact H28. am. am. apply intersection2_first with x. am. Qed. Lemma uls_increasing_ds : forall a f : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> increasing_ds_family a f. ir. uhg. ir. assert (sub x y \/ sub y x). apply uls_or with a; ap H0; am. nin H3. ap or_intror. ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. ap or_introl. ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. Qed. Lemma uls_union_downward : forall a f z : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> inc z f -> downward_saturated a (union f) z. ir. uhg. ee. am. uf sub; ir. cp (union_exists H2). nin H3; ee. cp (H0 x0 H4). uh H5. ee. uh H5; ee. uh H5; ee. ap H8; am. uf sub; ir. apply union_inc with z. am. am. ir. cp (union_exists H3). nin H5. ee. assert (sub x0 z \/ sub z x0). apply uls_or with a. ap H0; am. ap H0; am. nin H7. ap H7; am. assert (downward_saturated a x0 z). ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. ufi downward_saturated H8. ee. apply H11 with x. am. am. am. Qed. Lemma uls_union_int_rw : forall a b x z : E, axioms a -> downward_saturated a b x -> inc z x -> intersection2 b (punctured_downward_subset a z) = intersection2 x (punctured_downward_subset a z). ir. ap extensionality; uf sub; ir; cp (intersection2_first H2); cp (intersection2_second H2). ap intersection2_inc. ufi downward_saturated H0; ee. apply H7 with z. am. am. ufi punctured_downward_subset H4. Ztac. ufi lt H9; ee. am. am. ap intersection2_inc. ufi downward_saturated H0; ee. ap H6; am. am. Qed. Lemma ultra_linear_subset_union : forall a f : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> is_ultra_linear_subset a (union f). ir. assert (increasing_ds_family a f). ap uls_increasing_ds. am. am. uhg; dj. ap wo_subset_increasing_union. am. am. ir. cp (H0 b H2). ufi is_ultra_linear_subset H3. ee. am. cp (union_exists H3). nin H4. ee. assert (intersection2 (union f) (punctured_downward_subset a x) = intersection2 x0 (punctured_downward_subset a x)). ap uls_union_int_rw. am. ap uls_union_downward. am. exact H0. am. am. rw H6. cp (H0 x0 H5). ufi is_ultra_linear_subset H7. ee. ap H8. am. Qed. Lemma wo_subset_new : forall a b x : E, is_wo_subset a b -> ~ inc x b -> is_upper_bound a b x -> is_wo_subset a (union2 b (singleton x)). ir. ufk is_wo_subset H. ufk is_upper_bound H1. ee. ufk is_well_ordered H3. ufk is_linear_subset H. ee. ufk is_linear H8. ee. uhg; dj. uhg; dj. am. uf sub; ir. cp (union2_or H11). nin H12. ap H2. am. cp (singleton_eq H12). rw H13; am. uhg; dj. ap suborder_axioms. am. am. rwi underlying_suborder H13. rwi underlying_suborder H14. cp (union2_or H13). cp (union2_or H14). nin H15. nin H16. ufi is_linear X4. ee. assert (leq (suborder b a) x0 y \/ leq (suborder b a) y x0). ap H18. rw underlying_suborder; am. rw underlying_suborder; am. nin H19. ap or_introl. rw leq_suborder_all; ee. am. am. rwi leq_suborder_all H19. ee. am. am. am. am. am. ap or_intror. rw leq_suborder_all; ee. am. am. rwi leq_suborder_all H19. ee; am. am. am. am. am. cp (singleton_eq H16). ap or_introl. rw leq_suborder_all; ee. am. am. rw H17. ap H5. am. am. am. cp (singleton_eq H15). ap or_intror. rw leq_suborder_all; ee. am. am. rw H17. nin H16. ap H5; am. cp (singleton_eq H16). rw H18. ufi axioms H; ee. ap H. am. am. am. uhg. dj. ufi is_linear_subset H10. ee. am. apply by_cases with (nonempty (intersection2 b0 b)). ir. ufi is_well_ordered X2. ee. set (b1 := intersection2 b0 b) in *. assert (sub b1 (U (suborder b a))). rw underlying_suborder. uf b1; uf sub; ir. apply intersection2_second with b0. am. cp (H16 b1 H17 H14). nin H18. sh x0. uhg; dj. uhg; dj. ap suborder_axioms. am. uf sub; ir. cp (union2_or H19). nin H20. ap H2; am. cp (singleton_eq H20). rw H21. am. am. rw underlying_suborder. apply union2_first. rwi underlying_suborder H17. ap H17. ufi is_bottom_element H18; ee. am. rw leq_suborder_all. ee. rwi underlying_suborder H21. exact H21. rwi underlying_suborder H20. ap H20. am. apply by_cases with (inc y b). ir. assert (inc y b1). uf b1; ap intersection2_inc; am. ufi is_bottom_element H18; ee. ufi is_lower_bound H18; ee. cp (H28 y H24). rwi leq_suborder_all H29. ee. am. am. am. ir. assert (inc y (union2 b (singleton x))). rwi underlying_suborder H20. ap H20. am. cp (union2_or H24). nin H25. assert False. ap H23; am. elim H26. cp (singleton_eq H25). rw H26. assert (inc x0 (union2 b (singleton x))). rwi underlying_suborder H21; exact H21. cp (union2_or H27). nin H28. ap H5. am. cp (singleton_eq H28). rw H29. ufi axioms H1; ee. ap H1; am. am. uf sub; ir. cp (union2_or H23). nin H24. ap H2; am. cp (singleton_eq H24). rw H25; am. ufi is_bottom_element H18. ee. ufi b1 H20. apply intersection2_first with b; am. ir. assert (sub b0 (singleton x)). uf sub; ir. rwi underlying_suborder H12. assert (inc x0 (union2 b (singleton x))). ap H12. am. cp (union2_or H16). nin H17. assert False. ap H14. sh x0. ap intersection2_inc; am. elim H18. am. assert (b0 = singleton x). ap extensionality. am. uf sub; ir. cp (singleton_eq H16). rw H17. nin H13. assert (inc y (singleton x)). ap H15; am. cp (singleton_eq H18). wr H19. am. rw H16. sh x. uhg; dj. uhg; dj. ap suborder_axioms. am. ufi is_linear_subset H10; ee. am. uf sub; ir. rw underlying_suborder. ap union2_second. am. rw underlying_suborder. ap union2_second. ap singleton_inc. cp (singleton_eq H20). rw H21. rw leq_suborder_all. dj. ap union2_second; ap singleton_inc. am. ufi axioms H1; ee; ap H1. am. am. ufi is_linear_subset H10; ee; am. ap singleton_inc. Qed. Lemma uls_new : forall a b x : E, is_ultra_linear_subset a b -> eq_ultra_bound a b x -> is_ultra_linear_subset a (union2 b (singleton x)). ir. uhg; dj. ap wo_subset_new. uh H; ee. am. uh H0; ee. uh H0; ee. am. uh H0; ee. uh H0; ee. am. cp (union2_or H2). nin H3. assert (intersection2 (union2 b (singleton x)) (punctured_downward_subset a x0) = intersection2 b (punctured_downward_subset a x0)). ap extensionality; uf sub; ir. cp (intersection2_first H4). cp (intersection2_second H4). ap intersection2_inc. cp (union2_or H5). nin H7. am. cp (singleton_eq H7). rw H8. ufi punctured_downward_subset H6. Ztac. uh H0; ee. uh H0; ee. uh H0; ee. cp (H15 x0 H3). rwi H8 H10. assert False. apply no_lt_leq with a x x0. am. am. am. elim H17. am. cp (intersection2_first H4). cp (intersection2_second H4). ap intersection2_inc. ap union2_first. am. am. rw H4. uh H; ee. ap H5. am. cp (singleton_eq H3). assert (intersection2 (union2 b (singleton x)) (punctured_downward_subset a x0) = b). ap extensionality; uf sub; ir. cp (intersection2_first H5). cp (intersection2_second H5). cp (union2_or H6). nin H8. am. cp (singleton_eq H8). ufi punctured_downward_subset H7. Ztac. ufi lt H11. ee. assert False. ap H12. rw H4; am. elim H13. ap intersection2_inc. ap union2_first; am. uf punctured_downward_subset; ap Z_inc. uh H; ee. uh H; ee. uh H; ee. ap H8; am. uh H0; ee. uh H0; ee. uh H0; ee. uf lt; ee. rw H4. ap H10; am. uf not; ir. ap H7. wr H4. wr H11. am. rw H5. rw H4. am. Qed. Definition uls_pool (a : E) := Z (powerset (U a)) (fun b : E => is_ultra_linear_subset a b). Lemma inc_uls_pool_rw : forall a b : E, inc b (uls_pool a) = is_ultra_linear_subset a b. ir. ap iff_eq; ir. ufi uls_pool H. Ztac. uf uls_pool. ap Z_inc. ap powerset_inc. uh H; ee. uh H; ee. uh H; ee. am. am. Qed. Definition max_uls (a : E) := union (uls_pool a). Lemma uls_sub_uls_pool : forall a b : E, is_ultra_linear_subset a b -> sub b (max_uls a). ir. uf sub; ir. uf max_uls. apply union_inc with b. am. rw inc_uls_pool_rw. am. Qed. Lemma max_uls_uls : forall a : E, axioms a -> is_ultra_linear_subset a (max_uls a). ir. uf max_uls. ap ultra_linear_subset_union. am. ir. rwi inc_uls_pool_rw H0. am. Qed. Lemma ub_inc_max_uls : forall a b x : E, is_ultra_linear_subset a b -> eq_ultra_bound a b x -> inc x (max_uls a). ir. assert (sub (union2 b (singleton x)) (max_uls a)). ap uls_sub_uls_pool. ap uls_new. am. am. ap H1. ap union2_second. ap singleton_inc. Qed. Lemma no_ultra_zorn : forall a : E, ~ is_ultra_zorn a. uf not; ir. uh H; ee. set (c := max_uls a) in *. assert (is_ultra_linear_subset a c). uf c; ap max_uls_uls. am. set (x := ultra_bound a c) in *. assert (is_ultra_bound a c x). uf x. ap H0. uh H1; ee. uh H1; ee. am. ufk is_ultra_bound H2. ee. ap H3. uf c. apply ub_inc_max_uls with c. am. uhg; ee. am. tv. Qed. Lemma zorn : forall a : E, axioms a -> (forall b : E, is_linear_subset a b -> ex (fun x : E => is_upper_bound a b x)) -> ex (fun z : E => is_maximal a (U a) z). ir. ap excluded_middle. uf not; ir. apply no_ultra_zorn with a. uhg; dj. am. cp (H0 b H3). apply by_cases with (ex (fun y : E => is_ultra_bound a b y)). ir. cp (choose_pr H5). am. ir. assert False. ap H1. nin H4. sh x. uhg; dj. am. uf sub; ir; am. uh H4; ee. am. assert (is_upper_bound a b y). uhg; ee. am. uh H3; ee. am. am. ir. uh H4; ee. uh H; ee. apply H18 with x. ap H14; am. am. ap excluded_middle; uf not; ir. assert (is_top_element a b x). uhg; ee. am. ap excluded_middle. uf not; ir. ap H5. sh x. uhg; ee. am. am. assert (is_top_element a b y). uhg; ee. am. ap excluded_middle. uf not; ir. ap H5. sh y. uhg; ee. am. am. cp (top_element_unique H13 H14). ap H12; am. elim H6. Qed. End Zorn. Export Zorn. End Order. (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) Module Transfinite. (*** we set up the basis for transfinite induction. given a transformation f:E->E, we use it to define a relation leq_gen f which is supposed to be the order generated by f. then, is_leq_gen_scale f y means that y is a "scale" for the order leq_gen f. The first application is that any set can be well ordered. ***) Import Universe. Export Order. Lemma linear_show_same : forall a b:E, (is_linear a) -> (is_linear b) -> (U a) = (U b) -> (forall (x y:E),(leq a x y) -> (leq b x y)) ->(same_order a b). ir. uhg; ee; ap show_is_suborder; ir. uh H; ee; am. uh H0; ee; am. ap H2; am. uh H0; ee; am. uh H; ee; am. uh H; ee. assert (inc x (U a)). rw H1. uh H0; ee. uh H0; ee. ap (H6 _ _ H3). assert (inc y (U a)). rw H1. uh H0; ee. uh H0; ee. ap (H8 _ _ H3). pose (H4 _ _ H5 H6). nin o. am. pose (H2 _ _ H7). uh H0; ee; uh H0; ee. assert (x = y). ap H11; am. rw H13. uh H; ee. ap H. am. Save. Lemma scale_subset_or : forall a y z:E, scale_subset y a -> scale_subset z a -> (sub y z) \/ (sub z y). Proof. ir. uh H. uh H0. ee. ap show_sub_or. ir. nin H5. nin H6. rwi inc_complement H5. rwi inc_complement H6. ee. uh H; ee. uh H; ee. assert (leq a y0 y1 \/ leq a y1 y0). ap H10. ap H2. am. ap H1; am. nin H11. ap H8. ap (H3 y0 y1). am. am. ap H7. ap (H4 y1 y0). am. am. Qed. Lemma union_sub : forall x z : E, (forall y:E, inc y z -> sub y x) -> sub (union z) x. Proof. ir. uhg; ir. pose (union_exists H0). nin e. ee. assert (sub x1 x). ap H; am. ap H3; am. Qed. Lemma scale_subset_union : forall a z:E, is_well_ordered a -> (forall y:E, inc y z -> scale_subset y a) -> scale_subset (union z) a. Proof. ir. uhg. ee. am. ap union_sub. ir. cp (H0 _ H1). uh H2. ee. am. ir. cp (union_exists H1). nin H3. ee. cp (H0 _ H4). uh H5; ee. apply union_inc with x0. apply H7 with y. am. am. am. Qed. Lemma scale_subset_union_exists : forall a z u v : E, is_well_ordered a -> (forall y: E, inc y z -> scale_subset y a) -> inc u (union z) -> inc v (union z) -> exists y : E, (inc y z & scale_subset y a & inc u y & inc v y). Proof. ir. cp (union_exists H1). cp (union_exists H2). nin H3. nin H4. ee. assert (sub x x0 \/ sub x0 x). apply scale_subset_or with a. ap H0; am. ap H0; am. nin H7. sh x0. xd. sh x. xd. Qed. Definition next (a y:E):= choose (is_bottom_element a (complement (U a) y)). Lemma strict_sub_nonempty_complement : forall x y : E, strict_sub x y -> nonempty (complement y x). Proof. ir. assert (nonemptyT (complement y x)). ap not_empty_nonemptyT. uhg; ir. uh H; ee. ap H. ap extensionality. am. uhg; ir. ap excluded_middle. uhg; ir. assert (inc x0 (complement y x)). rw inc_complement. xd. uh H0. ufi not H0. apply H0 with x0. am. nin H0. cp (R_inc X0). sh (R X0). am. Qed. Lemma sub_complement : forall x y : E, sub (complement x y) x. Proof. ir. uhg; ir. rwi inc_complement H. ee. am. Qed. Lemma next_bottom_element : forall a y:E, strict_sub y (U a) -> is_well_ordered a -> is_bottom_element a (complement (U a) y) (next a y). Proof. ir. uh H0; ee. assert (nonempty (complement (U a) y)). ap strict_sub_nonempty_complement. am. uh H; ee. assert (sub (complement (U a) y) (U a)). ap sub_complement. cp (H1 _ H4 H2). cp (choose_pr H5). cbv beta in H6. uf next. am. Qed. Lemma next_inc_U : forall a y:E, strict_sub y (U a) -> is_well_ordered a -> inc (next a y) (U a). Proof. ir. cp (next_bottom_element H H0). uh H1; ee. rwi inc_complement H2. ee; am. Qed. Lemma next_not_inc : forall a y:E, strict_sub y (U a) -> is_well_ordered a -> ~inc (next a y) y. Proof. ir. cp (next_bottom_element H H0). uh H1; ee. rwi inc_complement H2. ee. am. Qed. Lemma next_smallest : forall a y u:E, strict_sub y (U a) -> is_well_ordered a -> inc u (U a) -> ~ inc u y -> leq a (next a y) u. Proof. ir. cp (next_bottom_element H H0). uh H1; ee. uh H3; ee. uh H3; ee. ap H7. rw inc_complement; ee. am. am. Qed. Lemma scale_subset_next : forall a y : E, scale_subset y a -> strict_sub y (U a) -> scale_subset (tack_on y (next a y)) a. Proof. ir. uhg; dj. uh H; xd. uhg; ir. cp (tack_on_or H2). nin H3. uh H; xd. uh H; ee. rw H3; ap next_inc_U; am. cp (tack_on_or H3). nin H5. uh H; ee. rw tack_on_inc. ap or_introl. apply H7 with y0. am. am. rw tack_on_inc. apply by_cases with (inc x y). ir. ap or_introl; am. ir. ap or_intror. assert (leq a (next a y) x). ap next_smallest. am. am. uh H4; xd. am. apply leq_leq_eq with a. uh H; ee. uh H; ee. uh H. ee. am. wr H5; am. am. Qed. Lemma punctured_downward_scale : forall a x : E, is_well_ordered a -> inc x (U a) -> scale_subset (punctured_downward_subset a x) a. Proof. ir. uhg; dj. am. uf punctured_downward_subset. uhg; ir. Ztac. uf punctured_downward_subset. ap Z_inc. uh H4; xd. ufi punctured_downward_subset H3. Ztac. apply leq_lt_trans with y. uh H; ee; uh H; ee; am. am. am. Qed. Lemma punctured_downward_strict_sub : forall a x:E, axioms a -> inc x (U a) -> strict_sub (punctured_downward_subset a x) (U a). Proof. ir. uhg; ee. uhg; uhg; ir. assert (inc x (punctured_downward_subset a x)). rw H1; am. ufi punctured_downward_subset H2; Ztac. uh H4; xd. uhg; ir. ufi punctured_downward_subset H1; Ztac. Qed. Lemma next_punctured_downward : forall a x : E, is_well_ordered a -> inc x (U a) -> x = next a (punctured_downward_subset a x). Proof. ir. set (y:= punctured_downward_subset a x). apply leq_leq_eq with a. uh H; ee; uh H; ee; am. ap excluded_middle; uhg; ir. assert (lt a (next a y) x). ap excluded_middle; uhg; ir. ap H1. ap linear_not_lt_leq. uh H; ee. am. ap next_inc_U. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. am. assert (inc (next a y) (punctured_downward_subset a x)). uf punctured_downward_subset. ap Z_inc. ap next_inc_U. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. generalize H3. fold y. ap next_not_inc. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. ap next_smallest. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. uhg; ir. ufi y H1. ufi punctured_downward_subset H1. Ztac. uh H3; xd. Qed. Lemma scale_is_punctured_downward : forall a y : E, scale_subset y a -> strict_sub y (U a) -> punctured_downward_subset a (next a y)= y. Proof. ir. symmetry. ap extensionality; uhg; ir. uf punctured_downward_subset; ap Z_inc. uh H0; ee. ap H2. am. assert (inc x (U a)). uh H0; ee. ap H2; am. assert (inc (next a y) (U a)). ap next_inc_U. am. uh H; ee. am. uhg; ee. uh H; ee. uh H; ee. uh H; ee. cp (H7 _ _ H2 H3). nin H8. am. assert (inc (next a y) y). apply H5 with x. am. am. assert False. apply next_not_inc with a y. am. uhg; xd. uhg; xd. am. elim H10. uhg; ir. apply next_not_inc with a y. am. uh H; xd. wr H4; am. ap excluded_middle. uhg; ir. assert (leq a (next a y) x). ap next_smallest. am. uh H; xd. ufi punctured_downward_subset H1. Ztac. am. ufi punctured_downward_subset H1; Ztac. uh H5; xd. ap H6. uh H; ee; uh H; ee. uh H; ee. uh H; ee. apply H13. am. am. Qed. Definition next_compatible (f:E->E)(a:E) := is_well_ordered a & (forall (y:E),inc y (U a) -> (f (punctured_downward_subset a y)) = y). Definition scale_bisubset (a b y : E) := is_well_ordered a & is_well_ordered b & scale_subset y a & scale_subset y b & (forall u v:E, inc u y -> inc v y -> leq a u v = leq b u v). Lemma scale_bisubset_union : forall a b z : E, is_well_ordered a -> is_well_ordered b -> (forall y:E, inc y z -> scale_bisubset a b y) -> scale_bisubset a b (union z). Proof. ir. uhg. dj. am. am. ap scale_subset_union. am. ir. cp (H1 _ H4). uh H5; xd. ap scale_subset_union. am. ir. cp (H1 _ H5). uh H6; xd. assert (exists y : E, (inc y z & scale_subset y a & inc u y & inc v y)). ap scale_subset_union_exists. am. ir. cp (H1 _ H8). uh H9; xd. am. am. nin H8. ee. assert (scale_bisubset a b x). ap H1. am. uh H12; ee. ap H16. am. am. Qed. Lemma next_compatible_scale : forall (f:E1) (a y:E), next_compatible f a -> scale_subset y a -> strict_sub y (U a) -> next a y = f y. Proof. ir. uh H; ee. assert (inc (next a y) (U a)). ap next_inc_U. am. am. cp (H2 _ H3). wr H4. rw scale_is_punctured_downward. tv. am. am. Qed. Lemma next_compatible_lt : forall a y u:E, scale_subset y a -> strict_sub y (U a) -> inc u y -> lt a u (next a y). Proof. ir. cp (scale_is_punctured_downward H H0). wri H2 H1. ufi punctured_downward_subset H1. Ztac. Qed. Lemma scale_bicompatible_next : forall (f:E1) (a b y : E), scale_bisubset a b y -> strict_sub y (U a) -> strict_sub y (U b) -> next_compatible f a -> next_compatible f b -> scale_bisubset a b (tack_on y (f y)). Proof. ir. uhg. dj. uh H; ee. am. uh H; ee; am. assert (f y = next a y). uh H2; ee. uh H; ee. cp (scale_is_punctured_downward H8 H0). wr H11. rw H6. wr next_punctured_downward. trivial. am. ap next_inc_U. am. am. ap next_inc_U. am. am. rw H6. ap scale_subset_next. uh H; xd. am. assert (f y = next b y). uh H; ee. uh H; ee. assert (strict_sub y (U b)). am. cp (scale_is_punctured_downward H9 H12). wr H13. uh H3; ee. rw H14. wr next_punctured_downward. trivial. am. ap next_inc_U. am. am. ap next_inc_U. am. am. rw H7. ap scale_subset_next. uh H; xd. am. cp (tack_on_or H8). cp (tack_on_or H9). nin H10. nin H11. (*** the case inc u y and inc v y ***) uh H; ee. ap H15. am. am. (*** the case inc u y and v = f y ***) assert (v = next a y). rw H11; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (v = next b y). rw H11; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (lt a u v). rw H12. ap next_compatible_lt. uh H; ee; am. am. am. assert (lt b u v). rw H13. ap next_compatible_lt. uh H; ee; am. am. am. ap iff_eq. ir. uh H15; xd. ir; uh H14; xd. nin H11. (*** the case u = f y and inc v y ***) assert (u = next a y). rw H10; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (u = next b y). rw H10; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (lt a v u). rw H12. ap next_compatible_lt. uh H; ee; am. am. am. assert (lt b v u). rw H13. ap next_compatible_lt. uh H; ee; am. am. am. ap iff_eq. ir. assert False. apply no_lt_leq with a v u. uh H4; ee; uh H4; ee; am. am. am. elim H17. ir. assert False. apply no_lt_leq with b v u. uh H5; ee; uh H5; ee; am. am. am. elim H17. (*** the case u = f y and v = f y ***) assert (u = v). transitivity (f y). am. sy; am. rw H12. ap iff_eq; ir. ap leq_refl. uh H5; ee; uh H5; ee; am. assert (v = next b y). rw H11. sy; ap next_compatible_scale. am. uh H; ee; am. am. rw H14. ap next_inc_U. am. am. ap leq_refl. uh H4; ee; uh H4; ee; am. assert (v = next a y). rw H11. sy; ap next_compatible_scale. am. uh H; ee; am. am. rw H14; ap next_inc_U; am. Qed. Definition compatibility_scales a b:E:= Z (powerset (U a)) (fun y:E=> (scale_bisubset a b y)). Lemma compatibility_scales_inc : forall a b y : E, inc y (compatibility_scales a b) = scale_bisubset a b y. Proof. ir. ap iff_eq; ir. ufi compatibility_scales H; Ztac. uf compatibility_scales; ap Z_inc. ap powerset_inc. uh H; ee. uh H1; ee. am. am. Qed. Definition max_comp_scale (a b:E):= union (compatibility_scales a b). Lemma max_comp_scale_bisubset : forall (a b :E), is_well_ordered a -> is_well_ordered b -> scale_bisubset a b (max_comp_scale a b). Proof. ir. uf max_comp_scale. ap scale_bisubset_union. am. am. ir. rwi compatibility_scales_inc H1. am. Qed. Lemma max_comp_scale_or : forall (f:E1) (a b : E), next_compatible f a -> next_compatible f b -> (max_comp_scale a b = U a) \/ (max_comp_scale a b = U b). Proof. ir. ap excluded_middle. uhg; ir. assert (~(max_comp_scale a b = U a)). ap excluded_middle; uhg; ir. ap H1; ap or_introl. ap excluded_middle; am. assert (~(max_comp_scale a b = U b)). ap excluded_middle; uhg; ir. ap H1; ap or_intror. ap excluded_middle; am. set (y:= max_comp_scale a b). assert (scale_bisubset a b y). uf y. ap max_comp_scale_bisubset. uh H; ee. am. uh H0; ee; am. assert (strict_sub y (U a)). uhg; ee. am. uh H4; ee. uh H6; ee; am. assert (strict_sub y (U b)). uhg; ee. am. uh H4; ee. uh H8; ee; am. assert (scale_bisubset a b (tack_on y (f y))). ap scale_bicompatible_next; au. wri compatibility_scales_inc H7. assert (sub (tack_on y (f y)) y). uhg; ir. uf y. uf max_comp_scale. apply union_inc with (tack_on y (f y)). am. am. assert (inc (f y) y). ap H8. rw tack_on_inc. ap or_intror; tv. assert (next a y = f y). ap next_compatible_scale. am. uh H4; ee; am. am. apply next_not_inc with a y. am. uh H; ee; am. rw H10; am. Qed. Lemma full_bisubset_suborder : forall a b : E, scale_bisubset a b (U a) -> is_suborder a b. Proof. ir. ap show_is_suborder. uh H; ee. uh H; ee; uh H; ee; am. uh H; ee. uh H0; ee; uh H0; ee; am. ir. assert (inc x (U a)). uh H0; ee; am. assert (inc y (U a)). uh H0; ee; am. uh H; ee. wr H6. am. am. am. Qed. Lemma max_comp_scale_sym_sub: forall a b:E, sub (max_comp_scale a b) (max_comp_scale b a). Proof. ir. uhg; ir. ufi max_comp_scale H. cp (union_exists H). nin H0. ee. uf max_comp_scale; apply union_inc with x0. am. rwi compatibility_scales_inc H1. rw compatibility_scales_inc. uh H1; ee. uhg; xd. ir. sy. au. Qed. Lemma max_comp_scale_sym: forall a b:E, max_comp_scale a b = max_comp_scale b a. Proof. ir. ap extensionality; uhg; ir. ap max_comp_scale_sym_sub. am. ap max_comp_scale_sym_sub; am. Qed. Lemma next_compatible_or : forall (f : E1) (a b : E), next_compatible f a -> next_compatible f b -> (is_suborder a b \/ is_suborder b a). Proof. ir. cp (max_comp_scale_or H H0). nin H1. ap or_introl. ap full_bisubset_suborder. wr H1. ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. ap or_intror. ap full_bisubset_suborder. rwi max_comp_scale_sym H1. wr H1. ap max_comp_scale_bisubset. uh H0; ee; am. uh H; ee; am. Qed. Lemma next_compatible_same : forall (f:E1) (a b : E), next_compatible f a -> next_compatible f b -> U a = U b -> same_order a b. Proof. ir. cp (next_compatible_or H H0). nin H2. ap linear_show_same. uh H; ee. uh H; ee. am. uh H0; ee; uh H0; ee; am. am. ir. apply is_suborder_leq with a. am. am. ap linear_show_same. uh H; ee. uh H; ee. am. uh H0; ee; uh H0; ee; am. am. ir. ap linear_not_lt_leq. uh H0; ee; uh H0; ee; am. wr H1. uh H3; xd. wr H1; uh H3; xd. ir. assert (lt a y x). uhg; ee. uh H4; ee. apply is_suborder_leq with b; am. uh H4; ee; am. apply no_lt_leq with a y x. uh H; ee; uh H; ee; uh H; ee; am. am. am. Qed. Definition leq_gen (f:E1)(x y:E):= exists a:E, (next_compatible f a & leq a x y). Lemma linear_suborder_leq : forall a b x y : E, is_linear a -> is_suborder a b -> inc x (U a) -> inc y (U a) -> leq b x y -> leq a x y. Proof. ir. ap linear_not_lt_leq. am. am. am. ir. assert (lt b y x). uhg; ee. apply is_suborder_leq with a. am. uh H4; ee; am. uh H4; ee; am. apply no_lt_leq with b y x. uh H0; ee. am. am. am. Qed. Lemma leq_gen_leq : forall (f:E1)(a x y:E), next_compatible f a -> inc x (U a) -> inc y (U a) -> leq_gen f x y = leq a x y. Proof. ir. ap iff_eq; ir. uh H2. nin H2. ee. cp (next_compatible_or H H2). nin H4. apply linear_suborder_leq with x0. uh H; ee. uh H; ee; am. am. am. am. am. apply is_suborder_leq with x0. am. am. uhg. sh a. ee. am. am. Qed. Lemma leq_gen_trans : forall (f:E1)(x y z:E), leq_gen f x y -> leq_gen f y z -> leq_gen f x z. Proof. ir. cp H. cp H0. uh H; uh H0. nin H; nin H0. ee. cp (next_compatible_or H H0). nin H5. uh H5. ee. assert (inc x (U x1)). ap H7. uh H4; ee; am. assert (inc y (U x1)). uh H3; ee; am. assert (inc z (U x1)). uh H3; ee; am. cp (leq_gen_leq H0 H9 H10). cp (leq_gen_leq H0 H10 H11). cp (leq_gen_leq H0 H9 H11). rw H14. apply leq_trans with y. am. wr H12; am. am. uh H5; ee. assert (inc x (U x0)). uh H4; ee; am. assert (inc y (U x0)). uh H4; ee; am. assert (inc z (U x0)). ap H7; uh H3; ee; am. cp (leq_gen_leq H H9 H10). cp (leq_gen_leq H H9 H11). cp (leq_gen_leq H H10 H11). rw H13. apply leq_trans with y. am. am. wr H14; am. Qed. Lemma leq_gen_eq : forall (f:E1) (x y:E), leq_gen f x y -> leq_gen f y x -> x = y. Proof. ir. cp H; cp H0. uh H; uh H0. nin H; nin H0. ee. assert (inc x (U x0)). uh H4; ee; am. assert (inc y (U x0)). uh H4; ee; am. cp (leq_gen_leq H H6 H5). apply leq_leq_eq with x0. uh H; ee. uh H; ee; uh H; ee; am. am. wr H7; am. Qed. Lemma leq_gen_def1 : forall (f:E1) (x y:E), leq_gen f x y -> leq_gen f x x. Proof. ir. uh H; nin H. ee. assert (inc x (U x0)). uh H0; ee; am. cp (leq_gen_leq H H1 H1). rw H2. apply leq_refl. uh H; ee; uh H; ee; uh H; ee; am. am. Qed. Lemma leq_gen_def2 : forall (f:E1) (x y:E), leq_gen f x y -> leq_gen f y y. Proof. ir. uh H; nin H. ee. assert (inc y (U x0)). uh H0; ee; am. cp (leq_gen_leq H H1 H1). rw H2. apply leq_refl. uh H; ee; uh H; ee; uh H; ee; am. am. Qed. Lemma leq_gen_or : forall (f:E1) (x y:E), leq_gen f x x -> leq_gen f y y -> (leq_gen f x y \/ leq_gen f y x). Proof. ir. uh H; uh H0; nin H; nin H0; ee. cp (next_compatible_or H H0). nin H3. assert (inc x (U x1)). uh H3; ee. ap H5; uh H2; ee; am. assert (inc y (U x1)). uh H1; ee; am. rw (leq_gen_leq H0 H4 H5); rw (leq_gen_leq H0 H5 H4). uh H0; ee; uh H0; ee. uh H0; ee. ap H8; am. assert (inc y (U x0)). uh H3; ee. ap H5; uh H1; ee; am. assert (inc x (U x0)). uh H2; ee; am. rw (leq_gen_leq H H4 H5); rw (leq_gen_leq H H5 H4). uh H; ee; uh H; ee; uh H; ee. ap H8; am. Qed. Definition is_leq_gen_scale (f:E1)(y:E):= exists a:E, (U a = y & next_compatible f a). Lemma leq_gen_scale_or : forall (f:E1)(y z:E), is_leq_gen_scale f y -> is_leq_gen_scale f z -> (sub y z \/ sub z y). Proof. ir. uh H; uh H0; nin H; nin H0. ee. cp (next_compatible_or H1 H2). nin H3. ap or_intror. wr H; wr H0. uh H3; ee; am. ap or_introl. wr H; wr H0. uh H3; ee; am. Qed. Lemma next_comp_leq_gen_scale : forall (f:E1)(a:E), next_compatible f a -> is_leq_gen_scale f (U a). Proof. ir. uhg; sh a. ee. tv. am. Qed. Lemma next_comp_sub_scale : forall (f:E1) (a b:E), next_compatible f a -> next_compatible f b -> (sub (U a) (U b)) -> scale_subset (U a) b. Proof. ir. cp (max_comp_scale_or H H0). nin H2. wr H2. assert (scale_bisubset a b (max_comp_scale a b)). ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. uh H3; ee; am. assert (scale_bisubset a b (max_comp_scale a b)). ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. uh H3; ee. rwi H2 H5. uh H5; ee. assert (U a = U b). apply extensionality; am. rw H10. wr H2. am. Qed. Lemma leq_gen_scale_subset : forall (f:E1)(a y:E), next_compatible f a -> is_leq_gen_scale f y -> sub y (U a) -> scale_subset y a. Proof. ir. uh H0; nin H0; ee. wr H0. apply next_comp_sub_scale with f. am. am. rw H0; am. Qed. Lemma scale_subset_is_leq_gen_scale : forall (f:E1)(a y:E), next_compatible f a -> scale_subset y a -> is_leq_gen_scale f y. Proof. ir. uhg. sh (suborder y a). ee. uf suborder. rw underlying_create. tv. uhg; ee. ap suborder_well_ordered. uh H0; ee; am. uh H; ee; am. ir. assert (punctured_downward_subset (suborder y a) y0 = punctured_downward_subset a y0). ap extensionality; uhg; ir. uf punctured_downward_subset. ufi punctured_downward_subset H2. Ztac. ap Z_inc. uh H0; ee. ap H5. assert (U (suborder y a) = y). uf suborder; ap underlying_create. wr H7; am. uh H4; ee. uhg; ee; au. rwi leq_suborder_all H4. ee. am. uh H; ee; uh H; ee; uh H; ee; am. uh H0; ee; am. uf punctured_downward_subset. ufi punctured_downward_subset H2. Ztac. ap Z_inc. ufi suborder H1. rwi underlying_create H1. uf suborder; rw underlying_create. uh H0; ee. apply H6 with y0. am. uh H4; ee; am. uh H4; ee. uhg; ee; try am. rw leq_suborder_all; ee. uh H0; ee. apply H7 with y0; try am. ufi suborder H1; rwi underlying_create H1; am. ufi suborder H1; rwi underlying_create H1; am. am. uh H; ee; uh H; ee; uh H; ee; am. uh H0; ee; am. rw H2. uh H; ee. ap H3. uh H0; ee. ap H4. ufi suborder H1; rwi underlying_create H1; am. Qed. Lemma leq_gen_char : forall (f:E1)(x y:E), leq_gen f x y = ((exists w:E, (is_leq_gen_scale f w & inc y w))& (forall w:E, is_leq_gen_scale f w -> inc y w -> inc x w)). Proof. ir. ap iff_eq; ir. ee. uh H; nin H; ee. sh (U x0). ee. ap next_comp_leq_gen_scale. am. uh H0; ee; am. ir. uh H; nin H; ee. assert (is_leq_gen_scale f (U x0)). ap next_comp_leq_gen_scale. am. cp (leq_gen_scale_or H0 H3). nin H4. cp (leq_gen_scale_subset H H0 H4). uh H5; ee. apply H7 with y. am. am. ap H4. uh H2; ee; am. ee. nin H. ee. uh H; nin H; ee. pose (u := punctured_downward_subset x1 y). assert (scale_subset u x1). uf u. ap punctured_downward_scale. uh H2; ee; am. rw H; am. assert (next x1 u = y). uf u. sy; ap next_punctured_downward. uh H2; ee; am. rw H; am. pose (v:=tack_on u y). assert (scale_subset v x1). uf v. wr H4. ap scale_subset_next. am. uhg; ee. uhg; uhg; ir. assert (inc y u). rw H5; rw H; am. ufi u H6; ufi punctured_downward_subset H6; Ztac. uh H8; ee. ap H9; tv. uh H3; ee; am. assert (inc x v). ap H0. apply scale_subset_is_leq_gen_scale with x1. am. am. uf v. rw tack_on_inc. ap or_intror; tv. ufi v H6. rwi tack_on_inc H6. nin H6. ufi u H6; ufi punctured_downward_subset H6; Ztac. assert (leq x1 x y = leq_gen f x y). sy. ap leq_gen_leq. am. am. rw H; am. wr H9. uh H8; ee; am. rw H6. uhg; ee. sh x1; ee; try am. ap leq_refl. uh H2; ee; uh H2; ee; uh H2; ee; am. rw H; am. Qed. Lemma leq_gen_def_char : forall f x, (exists u, is_leq_gen_scale f u & inc x u) -> leq_gen f x x. Proof. ir. rw leq_gen_char. ee; try am. ir. am. Qed. Lemma leq_gen_bottom_elt : forall (f:E1)(y:E), (forall x:E, inc x y -> leq_gen f x x) -> nonempty y -> exists b:E, (inc b y & (forall x:E, inc x y -> leq_gen f b x)). Proof. ir. nin H0. cp (H _ H0). uh H1; nin H1; ee. pose (w:=(intersection2 y (U x))). cp H1. uh H3; ee. uh H3; ee. assert (nonempty w). sh y0. uf w. ap intersection2_inc. am. uh H2; ee; am. assert (sub w (U x)). uf w. uhg; ir. cp (intersection2_second H7). am. cp (H5 _ H7 H6). nin H8. sh x0. ee. uh H8. ee. ufi w H9. cp (intersection2_first H9). am. ir. rw leq_gen_char; ee. assert (leq_gen f x1 x1). ap H; am. uh H10; nin H10; ee. sh (U x2). ee. uhg. sh x2; ee. tv. am. uh H11; ee; am. ir. uh H10; nin H10; ee. cp (next_compatible_or H1 H12). nin H13. uh H13; ee. wr H10. ap H15. ap H7. uh H8; ee. am. assert (scale_subset w0 x). wr H10. apply next_comp_sub_scale with f. am. am. uh H13; ee; am. uh H14; ee. apply H16 with x1. am. uh H8. ee. uh H8; ee. apply H20. uf w; ap intersection2_inc. am. ap H15. am. Qed. Lemma next_compatible_next : forall a, is_well_ordered a -> next_compatible (next a) a. Proof. ir. uhg; ee. am. ir. wr next_punctured_downward. tv. am. am. Qed. Lemma next_leq_gen_leq : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> leq_gen (next a) x y = leq a x y. Proof. ir. ap leq_gen_leq. ap next_compatible_next; am. am. am. Qed. Lemma leq_gen_scale_union : forall (f:E1)(z:E), (forall y:E, inc y z -> is_leq_gen_scale f y) -> is_leq_gen_scale f (union z). Proof. ir. uhg. pose (a:= create (union z) (leq_gen f)). sh a. dj. uf a; ap underlying_create. uhg; dj. uhg; dj. uhg; dj. uf a; ap create_axioms. uhg; ee. ir. (*** reflexivity ***) cp (union_exists H1). nin H2. ee. cp (H _ H3). uh H4; nin H4; ee. assert (leq x1 x x = leq_gen f x x). sy. ap leq_gen_leq. am. rw H4; am. rw H4; am. wr H6. ap leq_refl. do 3 (uh H5; ee); am. rw H4; am. (*** equality property ***) ir. apply leq_gen_eq with f. am. am. (*** transitivity ***) ir. apply leq_gen_trans with y; am. (*** linearity ***) assert (leq a x x & leq a y y). ee; ap leq_refl; am. ufi a H4. do 2 (rwi leq_create_all H4); ee. cp (leq_gen_or H9 H8). nin H10. ap or_introl. uf a; rw leq_create. am. am. am. ap or_intror. uf a; rw leq_create; am. (*** well_ordered ***) assert (exists t:E, (inc t b & (forall x:E, inc x b -> leq_gen f t x))). ap leq_gen_bottom_elt. ir. assert (inc x (U a)). ap H2; am. ufi a H5. rwi underlying_create H5. cp (union_exists H5). nin H6; ee. cp (H _ H7). uh H8; nin H8; ee. wri H8 H6. cp (leq_gen_leq H9 H6 H6). rw H10. ap leq_refl. do 3 (uh H9; ee); am. am. am. nin H4; ee. sh x. uhg; ee. uhg; ee. uh H1; ee; am. am. ap H2; am. ir. uf a. rw leq_create_all; ee. wr H0; ap H2; am. wr H0; ap H2; am. ap H5. am. am. (*** now the proof of the next_compatible property ***) rwi H0 H2. cp (union_exists H2). nin H3; ee. cp (H _ H4). cp H5. uh H5; nin H5; ee. assert (punctured_downward_subset a y = punctured_downward_subset x0 y). uf punctured_downward_subset; ap extensionality; uhg; ir; Ztac; ap Z_inc. rwi H0 H9. cp (union_exists H9). nin H11; ee. cp (H _ H12). cp (leq_gen_scale_or H6 H13). nin H14. uh H13; nin H13; ee. assert (scale_subset x x3). apply leq_gen_scale_subset with f. am. am. rw H13; am. rw H5. uh H16; ee. apply H18 with y. am. rewrite<- leq_gen_leq with (f:=f). uh H10; ee. ufi a H10; rwi leq_create_all H10; ee; am. am. rw H13; am. rw H13; ap H14; am. rw H5; ap H14; am. uh H10; ee. uhg; ee; try am. rewrite <- leq_gen_leq with (f:=f). ufi a H10; rwi leq_create_all H10; ee; am. am. (*** repeat the same block as before ***) rwi H0 H9. cp (union_exists H9). nin H12; ee. cp (H _ H13). cp (leq_gen_scale_or H6 H14). nin H15. uh H14; nin H14; ee. assert (scale_subset x x3). apply leq_gen_scale_subset with f. am. am. rw H14; am. rw H5. uh H17; ee. apply H19 with y. am. rewrite<- leq_gen_leq with (f:=f). ufi a H10; rwi leq_create_all H10; ee; am. am. rw H14; am. rw H14; ap H15; am. rw H5; ap H15; am. rw H5; am. rw H0. apply union_inc with x. wr H5; am. am. uh H10; ee. uhg; ee; try am. uf a; rw leq_create_all; ee. apply union_inc with x. wr H5; am. am. apply union_inc with x; am. rewrite leq_gen_leq with (a:= x0). am. am. am. rw H5; am. rw H8. uh H7; ee. ap H9. rw H5; am. Qed. Definition new_order (a y u v:E):= (leq a u v) \/ (v = y). Lemma new_order_wo : forall a y:E, ~inc y (U a) -> is_well_ordered a -> (is_well_ordered (create (tack_on (U a) y) (new_order a y))). Proof. ir. set (b:= (create (tack_on (U a) y) (new_order a y))). assert (U b = tack_on (U a) y). uf b; rw underlying_create; tv. assert (forall u :E,inc u (U b) -> (inc u (U a) \/ u = y)). ir. rwi H1 H2. cp (tack_on_or H2). am. assert (forall u v:E, leq b u v = (leq a u v \/ (v = y & (inc u (U b))))). ir. ap iff_eq; ir. ufi b H3. rwi leq_create_all H3; ee. uh H5. nin H5. ap or_introl; am. ap or_intror; ee. am. rw H1; am. uf b; rw leq_create_all; dj. nin H3. rw tack_on_inc. ap or_introl; uh H3; ee; am. ee. rwi H1 H4. am. nin H3. rw tack_on_inc; ap or_introl; uh H3; ee; am. ee. rw tack_on_inc; ap or_intror; am. uhg. nin H3. ap or_introl; am. ee; ap or_intror; am. uhg; dj. uhg; dj. uhg; ee; ir. rw H3. nin (H2 _ H4). ap or_introl; ap leq_refl; try am. do 2 (uh H0; ee); am. ap or_intror; ee; am. rwi H3 H4. nin H4. rw H1. rw tack_on_inc. ap or_introl; uh H4; ee; am. ee; am. uh H4; ee; am. rwi H3 H4. rwi H3 H5. nin H4. nin H5. apply leq_leq_eq with a. do 2 (uh H0; ee); am. am. am. assert False. ap H. ee. wr H5; uh H4; ee; am. elim H6. nin H5. assert False. ap H. ee. wr H4. uh H5; ee; am. elim H6. ee. rw H5; rw H4; tv. rwi H3 H4. rwi H3 H5. nin H4. nin H5. rw H3; ap or_introl. apply leq_trans with y0; try am. do 2 (uh H0; ee); am. ee. rw H3. ap or_intror. ee; try am. rw H1; rw tack_on_inc; ap or_introl. uh H4; ee; am. nin H5; ee. rw H3. assert False. ap H. wr H4; uh H5; ee; am. elim H7. rw H3; ap or_intror; ee; am. cp (H2 _ H5); cp (H2 _ H6). nin H7; nin H8. uh H0; ee. uh H0; ee. cp (H10 _ _ H7 H8). nin H11. ap or_introl. rw H3; ap or_introl; am. ap or_intror. rw H3; ap or_introl; am. ap or_introl; rw H3; ap or_intror. ee; am. ap or_intror; rw H3; ap or_intror. ee; am. ap or_introl; rw H3; ap or_intror; ee; am. (**** now the wo property ***) set (c:= intersection2 b0 (U a)). assert (sub c b0). uhg; ir. ufi c H7. cp (intersection2_first H7). am. assert (sub c (U a)). uhg; ir. cp (intersection2_second H8); am. apply by_cases with (nonempty c); ir. uh H0; ee. cp (H10 c H8 H9). nin H11. sh x. uhg; ee. uhg; ee. uh H4; ee; am. am. uh H11; ee. ap H5; ap H7; am. ir. assert (inc y0 (U b)). ap H5; am. cp (H2 _ H13). nin H14. rw H3; ap or_introl. uh H11; ee. uh H11; ee. ap H18. uf c; ap intersection2_inc. am. am. rw H3; ap or_intror. ee; try am. uh H11; ee. ap H5; ap H7; am. ap H7; uh H11; ee; am. assert (forall u:E, inc u b0 = (u = y)). ir. ap iff_eq; ir. assert (inc u (U b)). ap H5; am. cp (H2 _ H11). nin H12. assert False. ap H9. sh u. uf c; ap intersection2_inc. am. am. elim H13. am. nin H6. assert (inc y0 (U b)). ap H5; am. nin (H2 _ H11). assert False. ap H9. sh y0. uf c; ap intersection2_inc. am. am. elim H13. rw H10; wr H12; am. sh y. uhg. ee. uhg; ee. uh H4; ee; am. am. rw H1; rw tack_on_inc; ap or_intror; tv. ir. rwi H10 H11. rw H11. rw H3. ap or_intror; ee; tv. rw H1; rw tack_on_inc; ap or_intror; tv. nin H6. rw H10; tv. Qed. Lemma inc_punctured_downward_subset : forall a x u: E, inc u (punctured_downward_subset a x) = (inc u (U a) & leq a u x & u <> x). Proof. ir. ap iff_eq; ir. ufi punctured_downward_subset H; Ztac. uh H1; ee; am. uh H1; ee; am. uf punctured_downward_subset; ap Z_inc. ee; am. uhg; xd. Qed. Lemma leq_gen_scale_tack_on : forall (f:E1)(y:E), is_leq_gen_scale f y -> ~inc (f y) y -> is_leq_gen_scale f (tack_on y (f y)). Proof. ir. uh H; nin H; ee. assert (forall u v:E, inc u y-> inc v y-> leq x u v = leq_gen f u v). ir; sy; ap leq_gen_leq; try am. rw H; am. rw H; am. uhg. pose (a:= create (tack_on (U x) (f y)) (new_order x (f y))). sh a; dj. uf a; rw underlying_create. rw H; tv. assert (forall u v:E, inc u (U a) -> inc v (U a) -> leq a u v = new_order x (f y) u v). ir. uf a. rw leq_create. tv. rw H; wr H3; am. rw H; wr H3; am. uhg; dj. uf a. ap new_order_wo. rw H; am. uh H1; ee; am. rwi H3 H6. rwi tack_on_inc H6; nin H6. assert (punctured_downward_subset a y0 = punctured_downward_subset x y0). ap extensionality; uhg. intro. do 2 (rw inc_punctured_downward_subset); ir. xd. rw H. rwi H3 H7; rwi tack_on_inc H7; nin H7. am. rwi H4 H8. uh H8. nin H8. wr H. uh H8; ee; am. rw H7; wr H8; am. uh H8; ee; am. uh H8; ee; am. rwi H4 H8; uh H8; nin H8. am. assert False. ap H0. wr H8; am. elim H10. ee. am. ee; am. intro. do 2 (rw inc_punctured_downward_subset); ir. xd. rw H3; rw tack_on_inc; ap or_introl; rwi H H7; am. assert (sub (U x) (U a)). rw H; uhg; ir; rw H3; rw tack_on_inc; ap or_introl; am. rw H4. uhg. ap or_introl; am. ap H10; am. ap H10; rw H; am. rw H7. uh H1; ee. ap H8. rw H; am. transitivity (f y); try (sy; am). assert (punctured_downward_subset a y0 = y). ap extensionality; uhg; intro; rw inc_punctured_downward_subset; ir. ee. rwi H3 H7; rwi tack_on_inc H7; nin H7. am. assert False. ap H9; rw H6; rw H7; tv. elim H10. dj. rw H3; rw tack_on_inc; ap or_introl; am. rw H4. uhg. ap or_intror; am. am. rw H6. rw H3; rw tack_on_inc. ap or_intror; tv. uhg; ir. ap H0. wr H6; wr H10. am. rw H7; tv. Qed. Definition max_leq_gen_scale (f:E1)(x:E) := union (Z (powerset x) (is_leq_gen_scale f)). Lemma max_is_subset : forall (f:E1)(x:E), (sub (max_leq_gen_scale f x) x). Proof. ir. uhg; ir. ufi max_leq_gen_scale H. cp (union_exists H). nin H0; ee. Ztac. cp (powerset_sub H2). ap H4; am. Qed. Lemma max_is_leq_gen_scale :forall (f:E1)(x:E), (is_leq_gen_scale f (max_leq_gen_scale f x)). Proof. ir. uf max_leq_gen_scale. ap leq_gen_scale_union. ir. Ztac. Qed. Lemma max_is_max : forall (f:E1)(x u:E), is_leq_gen_scale f u -> sub u x -> sub u (max_leq_gen_scale f x). Proof. ir. uhg; ir. uf max_leq_gen_scale. apply union_inc with u. am. ap Z_inc. ap powerset_inc; am. am. Qed. Lemma max_f_out : forall (f:E1)(x:E), let u := max_leq_gen_scale f x in ~inc (f u) (complement x u). Proof. ir. uhg; ir. pose (v:=tack_on u (f u)). assert (~inc (f u) u). ufi complement H. Ztac. assert (inc v (powerset x)). ap powerset_inc. uf v. uhg; ir. rwi tack_on_inc H1. nin H1. assert (sub u x). uf u; ap max_is_subset. ap H2. am. rw H1. ufi complement H. Ztac. assert (is_leq_gen_scale f v). uf v. ap leq_gen_scale_tack_on. uf u; ap max_is_leq_gen_scale. am. assert (sub v u). uf u. ap max_is_max. am. exact (powerset_sub H1). ap H0. ap H3. uf v. rw tack_on_inc. ap or_intror; tv. Qed. Definition complementary_choice (x y:E):= choose (fun z:E=>inc z (complement x y)). Lemma max_lgs_cc_full : forall x :E, max_leq_gen_scale (complementary_choice x) x = x. Proof. ir. pose (f:= complementary_choice x). pose (u:= max_leq_gen_scale f x). assert (~inc (f u) (complement x u)). exact (max_f_out (f:= f) (x:=x)). ap extensionality. uf u; ap max_is_subset. uhg; ir. ap excluded_middle; uhg; ir. ap H. uf f. uf complementary_choice. ap choose_pr. sh x0. uf complement; ap Z_inc. am. am. Qed. Lemma full_cc_leq_gen_scale : forall x:E, is_leq_gen_scale (complementary_choice x) x. Proof. ir. cp (max_lgs_cc_full x). pose (f:= complementary_choice x). fold f. wr H. fold f. ap max_is_leq_gen_scale. Qed. Theorem every_set_can_be_well_ordered : forall x:E, exists a:E,(is_well_ordered a & U a = x). Proof. ir. cp (full_cc_leq_gen_scale x). uh H. nin H. ee. uh H0. ee. sh x0. ee; am. Qed. Definition choose_lgs_containing (f:E1)(x:E):= choose (fun y:E => (is_leq_gen_scale f y & inc x y)). Definition downward_lgs (f:E1)(x:E):= Z (choose_lgs_containing f x) (fun y:E=>leq_gen f y x). Lemma downward_lgs_lgs : forall (f:E1)(x:E), leq_gen f x x -> is_leq_gen_scale f (downward_lgs f x). Proof. ir. pose (u:= choose_lgs_containing f x). assert (is_leq_gen_scale f u & inc x u). rwi leq_gen_char H; ee. cp (choose_pr H). cbv beta in H1. ee. am. cp (choose_pr H); cbv beta in H1; ee; am. ee. uh H0; nin H0; ee. pose (a:= downward_suborder x0 x). uhg; sh a; ee. uf a; uf downward_suborder. rw underlying_suborder. uf downward_subset; uf downward_lgs; ap extensionality; uhg; ir; Ztac; ap Z_inc. fold u. wr H0; am. rewrite leq_gen_leq with (a:=x0). am. am. am. rw H0; am. rw H0; uf u; am. rewrite <- leq_gen_leq with (f:=f). am. am. rw H0; uf u; am. rw H0; am. uhg; dj. uf a; uf downward_suborder; ap suborder_well_ordered. uf downward_subset. uhg; ir; Ztac. uh H2; ee; am. assert (punctured_downward_subset a y = punctured_downward_subset x0 y). assert (sub (U a) (U x0)). uhg; ir. ufi a H5; ufi downward_suborder H5; rwi underlying_suborder H5. ufi downward_subset H5; Ztac. assert (forall r s:E, leq a r s -> leq x0 r s). ir. ufi a H6; ufi downward_suborder H6; rwi leq_suborder_all H6. ee. am. do 3 (uh H2; ee). am. uf downward_subset; uhg; ir; Ztac. assert (ax: axioms x0). do 3 (uh H2; ee); am. assert (lem1 : leq x0 y x). ufi a H4; ufi downward_suborder H4; rwi underlying_suborder H4; ufi downward_subset H4; Ztac. assert (forall r s : E, leq x0 r s -> leq x0 s x -> leq a r s). ir. uf a. uf downward_suborder. rw leq_suborder_all; dj. uf downward_subset; ap Z_inc. uh H7; ee; am. apply leq_trans with s. am. am. am. uf downward_subset; ap Z_inc. uh H7; ee; am. am. am. am. uf downward_subset; uhg; ir; Ztac. uf punctured_downward_subset; ap extensionality; uhg; ir; Ztac; ap Z_inc. ap H5; am. uh H10; uhg; xd. assert (leq a x1 x1). ap H7. ap leq_refl. am. am. uh H10; ee. apply leq_trans with y; am. uh H11; ee; am. uh H10; uhg; xd. rw H5. uh H2; ee. ap H6. ufi a H4; ufi downward_suborder H4; rwi underlying_suborder H4. ufi downward_subset H4; Ztac. Qed. Lemma downward_lgs_inc_refl :forall (f:E1)(x:E), leq_gen f x x -> inc x (downward_lgs f x). Proof. ir. pose (u:= choose_lgs_containing f x). assert (inc x u). rwi leq_gen_char H; ee. cp (choose_pr H); cbv beta in H1; ee; am. ee. uf downward_lgs. ap Z_inc. am. am. Qed. Lemma leq_gen_scale_saturated : forall (f:E1)(x y u:E), leq_gen f x y -> is_leq_gen_scale f u -> inc y u -> inc x u. Proof. ir. cp H. uh H. nin H. ee. assert (is_leq_gen_scale f (U x0)). uhg; sh x0; xd. nin (leq_gen_scale_or H0 H4). assert (scale_subset u x0). apply leq_gen_scale_subset with f. am. am. am. uh H6; ee. apply H8 with y. am. am. ap H5. uh H3; ee; am. Qed. Lemma downward_lgs_minimal : forall (f:E1)(x y:E), is_leq_gen_scale f y -> inc x y -> sub (downward_lgs f x) y. Proof. ir. cp H. uh H1; nin H1; ee. assert (lem1:leq_gen f x x). rewrite leq_gen_leq with (a:=x0). ap leq_refl. do 3 (uh H2; ee); am. rw H1; am. am. rw H1; am. rw H1; am. pose (u:= downward_lgs f x). assert (is_leq_gen_scale f u). uf u; ap downward_lgs_lgs. am. cp H3. uh H4; nin H4; ee. nin (leq_gen_scale_or H H3). assert (scale_subset y x1). apply leq_gen_scale_subset with f. am. am. rw H4; am. uf u; uf downward_lgs; uhg; ir; Ztac. clear H8. apply leq_gen_scale_saturated with f x. am. am. am. am. Qed. Lemma lgs_smallest_with_property : forall (f:E1)(p:EP), (exists y:E, (is_leq_gen_scale f y & p y)) -> exists x : E, (is_leq_gen_scale f x & p x & (forall y :E, is_leq_gen_scale f y -> p y -> sub x y)). Proof. ir. nin H; ee. cp H; uh H; nin H; ee. apply by_cases with (exists y:E, (strict_sub y x & is_leq_gen_scale f y & p y)); ir. pose (b := Z x (fun v:E=> p (punctured_downward_subset x0 v))). assert (sub b (U x0)). rw H; uf b; uhg; ir; Ztac. assert (nonempty b). nin H3. ee. assert (scale_subset x1 x0). apply leq_gen_scale_subset with f. am. am. rw H; uh H3; ee; am. sh (next x0 x1). uf b; ap Z_inc. wr H; ap next_inc_U. rw H; am. uh H2; ee; am. rw scale_is_punctured_downward. am. am. rw H; am. cp H2. uh H6; ee. uh H6; ee. nin (H8 b H4 H5). sh (punctured_downward_subset x0 x1). dj. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale. uh H2; ee; am. uh H9; ee. ap H4; am. uh H9; ee. ufi b H11; Ztac. nin (leq_gen_scale_or H1 H12). uhg; ir; ap H14. wr H; ufi punctured_downward_subset H15; Ztac. pose (w:= next x0 y). assert (scale_subset y x0). apply leq_gen_scale_subset with f. am. am. rw H; am. apply by_cases with (y=x); ir. rw H16; wr H; uf punctured_downward_subset; uhg; ir; Ztac. assert (y= punctured_downward_subset x0 w). sy; uf w; ap scale_is_punctured_downward. am. uhg; ee. rw H; am. rw H; am. assert (inc w b). uf b; ap Z_inc. wr H; uf w; ap next_inc_U. uhg; ee. rw H; am. rw H; am. uh H2; ee; am. wr H17; am. assert (leq x0 x1 w). uh H9; ee. uh H9; ee. ap H22. am. uhg; ir. ufi punctured_downward_subset H20; Ztac; ee. rw H17; uf punctured_downward_subset; ap Z_inc. am. apply lt_leq_trans with x1. do 3 (uh H2; ee); am. am. am. sh x. ee. am. am. ir. nin (leq_gen_scale_or H1 H4). am. apply by_cases with (y = x). ir. rw H7; uhg; ir; am. ir. assert False. ap H3. sh y. ee. uhg; ee; am. am. am. elim H8. Qed. Lemma lgs_limit_or_tack : forall (f:E1)(y:E), is_leq_gen_scale f y -> (exists z:E, ((forall x:E, inc x z -> (is_leq_gen_scale f x & strict_sub x y)) & y = union z)) \/ (exists x :E, (is_leq_gen_scale f x & y = tack_on x (f x))& ~inc (f x) x). Proof. ir. pose (z:= Z (powerset y) (fun x:E=> (is_leq_gen_scale f x & strict_sub x y))). pose (w:= union z). assert (sub w y). uhg; ir. ufi w H0; cp (union_exists H0). nin H1; ee. ufi z H2; Ztac. uh H5; ee. ap H6; am. assert (is_leq_gen_scale f w). uf w. ap leq_gen_scale_union. ir. ufi z H1; Ztac; am. apply by_cases with (w = y); ir. ap or_introl; sh z; ee; ir. ufi z H3; Ztac. wr H2; tv. ap or_intror; sh w; ee. am. ap excluded_middle; uhg; ir. assert (~sub (tack_on w (f w)) w). uhg; ir. cp H; uh H; nin H; ee. assert (strict_sub w y). uhg; ee; am. apply next_not_inc with x w. rw H; am. uh H6; ee; am. util (next_compatible_scale (f:=f) (a:=x) (y:=w)). am. apply leq_gen_scale_subset with f. am. am. rw H; am. rw H; am. rw H8. ap H4. rw tack_on_inc. ap or_intror; tv. ap H4. uhg; ir. uf w; apply union_inc with (tack_on w (f w)). am. assert (sub (tack_on w (f w)) y). assert (strict_sub w y). uhg; ee; am. cp H. uh H7; nin H7; ee. util (next_compatible_scale (f:=f) (a:= x0) (y:= w)). am. apply leq_gen_scale_subset with f. am. am. rw H7; am. rw H7; am. uhg; ir. rwi tack_on_inc H10; nin H10. ap H0; am. rw H10. wr H9. wr H7. ap next_inc_U. rw H7; am. uh H8; ee; am. uf z; ap Z_inc. ap powerset_inc. am. ee. apply by_cases with (inc (f w) w); ir. assert (tack_on w (f w) = w). ap extensionality; uhg; ir. rwi tack_on_inc H8; nin H8. am. rw H8; am. rw tack_on_inc; ap or_introl; am. rw H8. am. ap leq_gen_scale_tack_on. am. am. uhg; ee. uhg; uhg; ir. ap H3; sy; am. am. cp H; uh H; nin H; ee. util (next_compatible_scale (f:=f) (a:= x) (y:= w)). am. apply leq_gen_scale_subset with f. am. am. rw H; am. rw H; uhg; ee; am. wr H5. ap next_not_inc. rw H; uhg; ee; am. uh H4; ee; am. Qed. Lemma lgs_induction : forall (f:E1)(p:EP), (forall z:E,(forall u:E, inc u z -> p u)-> p (union z)) -> (forall u :E, p u -> p (tack_on u (f u))) -> (forall y:E, is_leq_gen_scale f y -> p y). Proof. ir. ap excluded_middle; uhg; ir. util (lgs_smallest_with_property (f:=f) (p:=(fun t:E=>~p t))). sh y. xd. nin H3; ee. cp (lgs_limit_or_tack H3). nin H6; nin H6; ee. ap H4. rw H7; ap H. ir. cp (H6 _ H8); ee. ap excluded_middle; uhg; ir. util (H5 u). am. am. uh H10; ee. ap H10. apply extensionality; am. ap H4. rw H8; ap H0. ap excluded_middle; uhg; ir. util (H5 x0). am. am. ap H7. ap H10. rw H8; rw tack_on_inc. ap or_intror; tv. Qed. Lemma downward_lgs_inc : forall (f:E1)(x y:E), leq_gen f x x -> inc y (downward_lgs f x) = leq_gen f y x. Proof. ir. ap iff_eq; ir. ufi downward_lgs H0; Ztac. uf downward_lgs; ap Z_inc. pose (u:=choose_lgs_containing f x). assert (is_leq_gen_scale f u & inc x u). uf u. uf choose_lgs_containing. pose (p:=fun y0 : E => is_leq_gen_scale f y0 & inc x y0). assert (ex p). sh (downward_lgs f x). uf p; cbv beta. ee. ap downward_lgs_lgs. am. ap downward_lgs_inc_refl. am. cp (choose_pr H1). exact H2. apply leq_gen_scale_saturated with f x. am. ee; am. ee; am. am. Qed. Lemma leq_gen_is_next: forall (f:E1)(x y:E), leq_gen f x y -> x = y \/ exists u:E, (is_leq_gen_scale f u & inc x u & y = f u). Proof. ir. apply by_cases with (x=y); ir. ap or_introl; am. ap or_intror. cp H. uh H1. nin H1. ee. sh (punctured_downward_subset x0 y). ee. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale; try am. uh H1; ee; am. uh H2; ee; am. uf punctured_downward_subset; ap Z_inc; ee. uh H2; ee; am. uhg; ee; am. uh H1; ee. sy. ap H3. uh H2; ee; am. Qed. (*** in general, in transfinite.v we need more stuff explaining what leq_gen f x y means in terms of inclusion of x and y in leq_gen_scales... ***) (*** this stuff should go in the basic Transfinite module ***) Definition chenille (f:E1)(x:E):= Z (downward_lgs f x) (fun y=> y<>x). Lemma chenille_inc : forall (f:E1)(x y:E), leq_gen f x x -> inc y (chenille f x) = (leq_gen f y x & y<>x). Proof. ir. ap iff_eq; ir. ufi chenille H0; Ztac. rwi downward_lgs_inc H1; try am. uf chenille; ap Z_inc. rw downward_lgs_inc; xd. ee; am. Qed. Lemma chenille_leq_gen_scale : forall (f:E1)(x:E), leq_gen f x x -> is_leq_gen_scale f (chenille f x). Proof. ir. pose (u:= downward_lgs f x). assert (is_leq_gen_scale f u). uf u; ap downward_lgs_lgs; am. cp H0. uh H0; nin H0. ee. assert (chenille f x = punctured_downward_subset x0 x). ap extensionality; uhg; ir. ufi chenille H3; Ztac. uf punctured_downward_subset; ap Z_inc. rw H0; am. uhg; ee; try am. rewrite <- leq_gen_leq with (f:=f). rwi downward_lgs_inc H4; am. am. rw H0; uf u; am. rw H0; uf u; ap downward_lgs_inc_refl. am. uf chenille; ap Z_inc. fold u. wr H0. ufi punctured_downward_subset H3; Ztac. ufi punctured_downward_subset H3; Ztac. uh H5; ee; am. rw H3. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale. uh H2; ee; am. rw H0; uf u; ap downward_lgs_inc_refl; am. Qed. Lemma next_compatible_saturated : forall (f:E1)(a b x y:E), next_compatible f a -> next_compatible f b -> inc y (U b) -> leq a x y -> inc x (U b). Proof. ir. nin (next_compatible_or H H0). uh H3; ee. ap H5. uh H2; ee; am. uh H3; ee. util (next_comp_sub_scale (f:= f) (a:=b) (b:=a)). am. am. am. uh H7; ee. apply H9 with y. am. am. Qed. Lemma weak_leq_gen_leq : forall (f:E1)(a x y:E), next_compatible f a -> inc y (U a) -> leq_gen f x y = leq a x y. Proof. ir. ap iff_eq; ir. uh H1. nin H1. ee. cp (next_compatible_or H H1). nin H3. apply linear_suborder_leq with x0. uh H; ee. uh H; ee; am. am. apply next_compatible_saturated with (f:=f)(a:= x0)(y:=y). am. am. am. am. am. am. apply is_suborder_leq with x0. am. am. uhg. sh a. ee. am. am. Qed. Lemma chenille_punctured_downward : forall (f:E1)(a x:E), next_compatible f a -> inc x (U a) -> chenille f x = punctured_downward_subset a x. Proof. ir. ap extensionality; uhg; ir. rwi chenille_inc H1. ee. rewrite weak_leq_gen_leq with (a:= a) in H1. uf punctured_downward_subset; ap Z_inc. uh H1; ee; am. uhg; ee; am. am. am. rewrite weak_leq_gen_leq with (a:=a). ap leq_refl. do 3 (uh H; ee); am. am. am. am. rw chenille_inc. ee. rewrite leq_gen_leq with (a:=a). ufi punctured_downward_subset H1; Ztac. uh H3; ee; am. am. ufi punctured_downward_subset H1; Ztac. am. ufi punctured_downward_subset H1; Ztac. uh H3; ee; am. rewrite leq_gen_leq with (a:=a). ap leq_refl. do 3 (uh H; ee); am. am. am. am. am. Qed. Lemma chenille_next : forall (f:E1)(x:E), leq_gen f x x -> f (chenille f x) = x. Proof. ir. cp H; uh H. nin H. ee. rewrite chenille_punctured_downward with (a:=x0). uh H; ee. ap H2. uh H1; ee; am. am. uh H1; ee; am. Qed. Lemma leq_gen_scale_chenille : forall (f:E1)(u:E), is_leq_gen_scale f u -> (exists v:E, (is_leq_gen_scale f v & strict_sub u v)) -> chenille f (f u) = u. Proof. ir. nin H0. ee. uh H0; nin H0; ee. rewrite chenille_punctured_downward with (a:= x0). assert (f u = next x0 u). sy; ap next_compatible_scale. am. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. rw H3. ap scale_is_punctured_downward. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. am. assert (f u = next x0 u). sy; ap next_compatible_scale. am. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. rw H3. ap next_inc_U. rw H0; am. uh H2; ee; am. Qed. Lemma chenille_tack_on : forall (f:E1)(x:E), leq_gen f x x -> tack_on (chenille f x) x = downward_lgs f x. Proof. ir. ap extensionality; uhg; ir. rwi tack_on_inc H0. nin H0. ufi chenille H0. Ztac. rw H0. ap downward_lgs_inc_refl. am. apply by_cases with (x0 = x); ir. rw tack_on_inc. ap or_intror; am. rw tack_on_inc; ap or_introl. uf chenille; ap Z_inc. am. am. Qed. End Transfinite. Module Transfinite_Mapping. Import Universe. Export Transfinite. (** now we start on the stuff needed to compare leq_gen_scales for different functions ****) Export Function. Definition tandem f g r:= (pair (f (domain r)) (g (range r))). Definition is_leq_gen_mapping f g r := (is_leq_gen_scale (tandem f g) r & Function.axioms r). Lemma leq_gen_mapping_domain : forall f g r, is_leq_gen_mapping f g r -> is_leq_gen_scale f (domain r). Proof. intros f g. pose (p:= fun r => is_leq_gen_scale f (domain r)). util (lgs_induction (f:=tandem f g) (p:=p)). ir. uf p; cbv beta. ee; ir. rw domain_union. ap leq_gen_scale_union. ir. rwi Image.inc_rw H0; nin H0; ee. wr H1. cp (H _ H0). ufi p H2; cbv beta in H2; ee. am. ir. uf tandem. uf p; cbv beta. rw domain_tack_on. apply by_cases with (inc (f (domain u)) (domain u)). ir. assert (tack_on (domain u) (f (domain u))= domain u). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc; ap or_introl; am. rw H1. ufi p H; cbv beta in H. am. ir. ap leq_gen_scale_tack_on. ufi p H; cbv beta in H; am. am. ir. uh H0. ee. cp (H _ H0). am. Qed. Lemma leq_gen_mapping_range : forall f g r, is_leq_gen_mapping f g r -> is_leq_gen_scale g (range r). Proof. intros f g. pose (p:= fun r => is_leq_gen_scale g (range r)). util (lgs_induction (f:=tandem f g) (p:=p)). ir. uf p; cbv beta. ee; ir. rw range_union. ap leq_gen_scale_union. ir. rwi Image.inc_rw H0; nin H0; ee. wr H1. cp (H _ H0). ufi p H2; cbv beta in H2; ee. am. ir. uf tandem. uf p; cbv beta. rw range_tack_on. apply by_cases with (inc (g (range u)) (range u)). ir. assert (tack_on (range u) (g (range u))= range u). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc; ap or_introl; am. rw H1. ufi p H; cbv beta in H. am. ir. ap leq_gen_scale_tack_on. ufi p H; cbv beta in H; am. am. ir. uh H0. ee. cp (H _ H0). am. Qed. Lemma leq_gen_mapping_sub : forall f g r s, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> sub (domain r) (domain s) -> sub r s. Proof. ir. uh H; uh H0; ee. cp (leq_gen_scale_or H H0). nin H4; try am. util (function_sub_eq (r:=s)(s:=r)). am. am. am. am. rw H5. uhg; ir; am. Qed. Lemma leq_gen_mapping_unique : forall f g r s, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> domain r = domain s -> r = s. Proof. ir. ap extensionality. apply leq_gen_mapping_sub with f g; try am. rw H1; uhg; ir; am. apply leq_gen_mapping_sub with f g; try am; rw H1; uhg; ir; am. Qed. Lemma leq_gen_mapping_union : forall f g z, (forall r, inc r z -> is_leq_gen_mapping f g r) -> is_leq_gen_mapping f g (union z). Proof. ir. uhg; ee. ap leq_gen_scale_union. ir. cp (H _ H0). uh H1; ee; am. ap function_glueing. ir. cp (H _ H0). uh H1; ee; am. ir. cp (H _ H0); cp (H _ H1). uh H4; uh H5; ee. nin (leq_gen_scale_or H4 H5). ap function_sub_V; am. sy; ap function_sub_V; try am. Qed. Lemma leq_gen_mapping_tack_on : forall f g r, is_leq_gen_mapping f g r -> ~inc (f (domain r)) (domain r) -> is_leq_gen_mapping f g (tack_on r (tandem f g r)). Proof. ir. uhg; ee. ap leq_gen_scale_tack_on. uh H; ee; am. uhg; ir. uh H; ee. cp (Function.lem2 H2 H1). ap H0. ufi tandem H3. rwi pr1_pair H3. am. uf tandem. ap function_tack_on_axioms. uh H; ee; am. am. Qed. Definition lgmaps f g u r := (is_leq_gen_mapping f g r & domain r = u). Definition lgmap f g u := choose (lgmaps f g u). Lemma lgmaps_exists_pr : forall f g u, (exists r, lgmaps f g u r )-> (lgmaps f g u (lgmap f g u)). Proof. ir. cp (choose_pr H). am. Qed. Lemma leq_gen_mapping_exists : forall f g u, is_leq_gen_scale f u -> exists r, lgmaps f g u r. Proof. intros f g. util (lgs_induction (f:=f) (p:= fun u=> exists r, (lgmaps f g u r))); ir. pose (pool := Image.create z (lgmap f g)). pose (r:= union pool). sh r; uhg; ee; ir. uf r. ap leq_gen_mapping_union. ir. ufi pool H0. rwi Image.inc_rw H0. nin H0. ee. cp (H _ H0). cp (lgmaps_exists_pr H2). rwi H1 H3. uh H3; ee; am. uf r; rw domain_union. ap extensionality; uhg; ir. cp (union_exists H0). nin H1; ee. rwi Image.inc_rw H2. nin H2; ee. ufi pool H2. rwi Image.inc_rw H2; nin H2; ee. cp (H _ H2). cp (lgmaps_exists_pr H5). rwi H4 H6. uh H6; ee. apply union_inc with x0. am. wr H3; rw H7; am. cp (union_exists H0). nin H1; ee. apply union_inc with x0. am. rw Image.inc_rw. sh (lgmap f g x0). ee. uf pool. rw Image.inc_rw. sh x0. ee; try am; try tv. cp (H _ H2). cp (lgmaps_exists_pr H3). uh H4; ee; am. apply by_cases with (inc (f u) u); ir. nin H. sh x. assert (tack_on u (f u) = u). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc; ap or_introl; am. rw H1; am. nin H. sh (tack_on x (tandem f g x)). uhg; ee. ap leq_gen_mapping_tack_on. uh H; ee; am. uh H; ee. rw H1. am. uf tandem. rw domain_tack_on. uh H; ee. rw H1; tv. ap H. am. Qed. Lemma lgmap_lgmaps : forall f g u, is_leq_gen_scale f u -> lgmaps f g u (lgmap f g u). Proof. ir. ap lgmaps_exists_pr. ap leq_gen_mapping_exists. am. Qed. Lemma lgmap_domain : forall f g u, is_leq_gen_scale f u -> domain (lgmap f g u) = u. Proof. ir. util (lgmap_lgmaps (f:=f) g (u:=u)). am. uh H0; ee; am. Qed. Lemma lgmap_lgmapping : forall f g u, is_leq_gen_scale f u -> is_leq_gen_mapping f g (lgmap f g u). Proof. ir. util (lgmap_lgmaps (f:=f) g (u:=u)). am. uh H0; ee; am. Qed. Lemma leq_gen_mapping_restr : forall f g r u, is_leq_gen_mapping f g r -> is_leq_gen_scale f u -> sub u (domain r) -> is_leq_gen_mapping f g (restr r u). Proof. ir. cp (lgmap_lgmaps g H0). util (leq_gen_mapping_sub (f:=f) (g:=g) (r:=(lgmap f g u))(s:= r)). uh H2; ee; am. am. rw lgmap_domain. am. am. assert (u = domain (lgmap f g u)). sy; ap lgmap_domain. am. rw H4. rw restr_to_domain. uh H2; ee; am. uh H2; ee. uh H2; ee. am. uh H; ee; am. am. Qed. Lemma lgmap_unique : forall f g r, is_leq_gen_mapping f g r -> lgmap f g (domain r) = r. Proof. ir. apply leq_gen_mapping_unique with f g. ap lgmap_lgmapping. apply leq_gen_mapping_domain with g. am. am. rw lgmap_domain; tv. apply leq_gen_mapping_domain with g. am. Qed. Definition avatar f g x := g (range (lgmap f g (chenille f x))). Lemma leq_gen_mapping_same_ev : forall f g r s x, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> inc x (domain r) -> inc x (domain s) -> V x r = V x s. Proof. ir. cp (leq_gen_mapping_domain H). cp (leq_gen_mapping_domain H0). cp (leq_gen_scale_or H3 H4). nin H5. pose (t:= restr s (domain r)). assert (V x s = V x t). uf t. sy. ap restr_ev. uh H0; ee; am. am. am. assert (t = r). apply leq_gen_mapping_unique with f g. uf t. ap leq_gen_mapping_restr. am. am. am. am. uf t. rw restr_domain. ap extensionality; uhg; ir. apply intersection2_second with (domain s); am. ap intersection2_inc. ap H5; am. am. uh H0; ee; am. wr H7. sy; am. pose (t:= restr r (domain s)). assert (V x r = V x t). uf t. sy. ap restr_ev. uh H; ee; am. am. am. assert (t = s). apply leq_gen_mapping_unique with f g. uf t. ap leq_gen_mapping_restr. am. am. am. am. uf t. rw restr_domain. ap extensionality; uhg; ir. apply intersection2_second with (domain r); am. ap intersection2_inc. ap H5; am. am. uh H; ee; am. wr H7. am. Qed. Lemma leq_gen_def_from_scale : forall f x, (exists u, is_leq_gen_scale f u & inc x u) -> leq_gen f x x. Proof. ir. nin H. ee. uh H. nin H. ee. rewrite weak_leq_gen_leq with (a:= x1). ap leq_refl. uh H1; ee. uh H1; ee. uh H1; ee. am. rw H; am. am. rw H; am. Qed. Lemma leq_gen_mapping_avatar : forall f g r x, is_leq_gen_mapping f g r -> inc x (domain r) -> V x r = avatar f g x. Proof. ir. uf avatar. assert (lem1 : leq_gen f x x). ap leq_gen_def_from_scale. sh (domain r); ee; try am. apply leq_gen_mapping_domain with g. am. set (u:= chenille f x). set (s := lgmap f g u). assert (is_leq_gen_mapping f g s). uf s. ap lgmap_lgmapping. uf u. ap chenille_leq_gen_scale. assert (is_leq_gen_scale f (domain r)). apply leq_gen_mapping_domain with g. am. am. assert (is_leq_gen_mapping f g (tack_on s (tandem f g s))). ap leq_gen_mapping_tack_on. am. uf s. rw lgmap_domain. uf u. rw chenille_inc. uhg; ir. ee. ap H3. ap chenille_next. am. ap leq_gen_def_from_scale. sh (domain r); ee; try am. apply leq_gen_mapping_domain with g. am. uf u. ap chenille_leq_gen_scale. am. set (t:= tack_on s (tandem f g s)). fold t in H2. assert (inc (pair x (g (range s))) t). uf t; rw tack_on_inc; ap or_intror. uf tandem. assert (x=f(domain s)). uf s. rw lgmap_domain. uf u. sy; ap chenille_next. am. uf u; ap chenille_leq_gen_scale; am. rw H3. tv. cp (Function.pr2_V (f:=t) (x:=(pair x (g (range s))))). rwi pr2_pair H4. rw H4. rw pr1_pair. apply leq_gen_mapping_same_ev with f g. am. am. am. uf t. uf tandem. rw domain_tack_on. rw tack_on_inc; ap or_intror. uf s. rw lgmap_domain. uf u. rw chenille_next. tv. am. uf u. ap chenille_leq_gen_scale. am. ufi t H2. uh H2; ee. am. uf t. rw tack_on_inc. ap or_intror. uf tandem. assert (x = f (domain s)). uf s. rw lgmap_domain; try am. uf u. rw chenille_next; try tv; try am. uf u. ap chenille_leq_gen_scale; try am. rw H5. tv. Qed. Lemma lgmap_avatar : forall f g u x, is_leq_gen_scale f u -> inc x u -> V x (lgmap f g u) = avatar f g x. Proof. ir. ap leq_gen_mapping_avatar. ap lgmap_lgmapping. am. rw lgmap_domain. am. am. Qed. Lemma lgmap_avatar_create : forall f g u, is_leq_gen_scale f u -> lgmap f g u = Function.create u (avatar f g). Proof. ir. util (Function.create_recovers (f:=lgmap f g u)). assert (is_leq_gen_mapping f g (lgmap f g u)). ap lgmap_lgmapping. am. uh H0; ee; am. wr H0. ap Function.create_extensionality. rw lgmap_domain. tv. am. ir. ap lgmap_avatar. am. am. Qed. Lemma avatar_image : forall f g u, is_leq_gen_scale f u -> Image.create u (avatar f g) = range (lgmap f g u). Proof. ir. rw lgmap_avatar_create. rw Function.create_range. ap Image.same. tv. ir. tv. am. Qed. Lemma lgs_avatar_image : forall f g u, is_leq_gen_scale f u -> is_leq_gen_scale g (Image.create u (avatar f g)). Proof. ir. rw avatar_image. apply leq_gen_mapping_range with f. ap lgmap_lgmapping. am. am. Qed. Lemma avatar_image_chenille : forall f g x, leq_gen f x x -> avatar f g x = g (Image.create (chenille f x) (avatar f g)). Proof. ir. rw avatar_image. tv. ap chenille_leq_gen_scale. am. Qed. Definition is_leq_gen_subscale f u := (is_leq_gen_scale f u & ~inc (f u) u). Definition is_expansive f := forall u, is_leq_gen_scale f u -> ~inc (f u) u. Lemma expansive_scale_chenille : forall f u, is_expansive f -> is_leq_gen_scale f u -> chenille f (f u) = u. Proof. ir. ap leq_gen_scale_chenille. am. sh (tack_on u (f u)). ee. ap leq_gen_scale_tack_on. am. uh H; ee. ap H. am. uhg; ee. uhg; uhg; ir. uh H. ap (H _ H0). set (v:= f u). rw H1; rw tack_on_inc; ap or_intror. tv. uhg; ir. rw tack_on_inc; ap or_introl; am. Qed. Lemma leq_gen_induction: forall f (p:EP), (forall x, leq_gen f x x -> (forall y, leq_gen f y x -> y<>x -> p y) -> p x) -> (forall z, leq_gen f z z -> p z). Proof. ir. cp H0; uh H0. nin H0; ee. apply wo_induction with (a:=x) (p:=p). do 5 (uh H0; ee; try am). ir. assert (leq_gen f x0 x0). rewrite weak_leq_gen_leq with (a:= x). ap leq_refl. do 5 (uh H0; ee; try am). am. am. am. cp (H _ H5). ap H6. ir. assert (leq x y x0). rewrite <- weak_leq_gen_leq with (f := f). am. am. am. ap H4. uh H9; ee; am. uhg; ee; am. uh H2; ee; am. Qed. Lemma chenille_induction : forall f (p:EP), (forall x, leq_gen f x x -> (forall y, inc y (chenille f x) -> p y) -> p x) -> (forall z, leq_gen f z z -> p z). Proof. ir. apply leq_gen_induction with (f:= f) (p:= p). ir. ap H. am. ir. ap H2. rwi chenille_inc H3. xd. am. rwi chenille_inc H3; xd. am. Qed. Lemma avatar_char : forall f g a y, (forall x, leq_gen f x x -> a x = g (Image.create (chenille f x) a)) -> leq_gen f y y -> a y = avatar f g y. Proof. ir. util (leq_gen_induction (f:= f) (p:= fun z => a z = avatar f g z)). ir. rw avatar_image_chenille. rw H. assert (forall e f, e=f -> (g e = g f)). ir. rw H3. tv. ap H3. ap Image.same. tv. ir. ap H2. rwi chenille_inc H4. xd. am. rwi chenille_inc H4; xd. am. am. ap H1. am. Qed. Lemma avatar_refl : forall f x, leq_gen f x x -> avatar f f x = x. Proof. ir. rewrite <- avatar_char with (a:= fun (i:E) => i). tv. ir. assert (Image.create (chenille f x0) (fun i : E => i) = (chenille f x0)). ap extensionality; uhg; ir. rwi Image.inc_rw H1. nin H1. ee. wr H2; am. rw Image.inc_rw. sh x1; ee; try am; try tv. rw H1. rw chenille_next. tv. am. am. Qed. Lemma avatar_chenille : forall f g x, is_expansive g -> leq_gen f x x -> chenille g (avatar f g x) = Image.create (chenille f x) (avatar f g). Proof. ir. rw avatar_image_chenille. rw expansive_scale_chenille. tv. am. ap lgs_avatar_image. ap chenille_leq_gen_scale. am. am. Qed. Lemma avatar_leq_gen_def : forall f g x, leq_gen f x x -> leq_gen g (avatar f g x) (avatar f g x). Proof. ir. rwi leq_gen_char H. ee. nin H. ap leq_gen_def_char. sh (Image.create x0 (avatar f g)). ee. ap lgs_avatar_image. am. rw Image.inc_rw. sh x. ee; try am; try tv. Qed. Lemma avatar_trans : forall f g h x, is_expansive g -> leq_gen f x x -> avatar g h (avatar f g x) = avatar f h x. Proof. ir. util (chenille_induction (f:=f) (p:= fun z => avatar g h (avatar f g z) = avatar f h z)). ir. set (u:= avatar f g x0). rw avatar_image_chenille. rw avatar_image_chenille. ap uneq. uf u. rw avatar_chenille. rw Image.trans. ap Image.same. tv. ir. ap H2. am. am. am. am. uf u. ap avatar_leq_gen_def. am. ap H1. am. Qed. Lemma avatar_inv : forall f g x, is_expansive g -> leq_gen f x x -> avatar g f (avatar f g x) = x. Proof. ir. rw avatar_trans. rw avatar_refl. tv. am. am. am. Qed. Lemma avatar_inj : forall f g x y, is_expansive g -> leq_gen f x x -> leq_gen f y y -> (avatar f g x) = (avatar f g y) -> x = y. Proof. ir. rewrite <- avatar_inv with (f:=f) (g:= g). wr H2. rw avatar_inv. tv. am. am. am. am. Qed. Lemma avatar_leq_gen : forall f g x y, is_expansive g -> leq_gen f x y -> leq_gen g (avatar f g x) (avatar f g y). Proof. ir. apply by_cases with (x = y); ir. rw H1. ap avatar_leq_gen_def. rwi H1 H0. am. assert (inc (avatar f g x) (chenille g (avatar f g y))). rw avatar_chenille. rw Image.inc_rw. sh x; ee; try tv. rw chenille_inc. ee; am. apply leq_gen_def2 with x. am. am. apply leq_gen_def2 with x. am. rwi chenille_inc H2; ee. am. ap avatar_leq_gen_def. apply leq_gen_def2 with x. am. Qed. Lemma next_compatible_avatar : forall a f g x, next_compatible f a -> inc x (U a) -> avatar f g x = avatar (next a) g x. Proof. ir. cp H; uh H; ee. util (wo_induction (a:= a) H (p:= (fun x => avatar f g x = avatar (next a) g x))). ir. rw avatar_image_chenille. rw avatar_image_chenille. ap uneq. ap extensionality; uhg; ir. rwi Image.inc_rw H5. rw Image.inc_rw. nin H5. sh x2; xd. rewrite chenille_punctured_downward with (a:= a). rewrite chenille_punctured_downward with (a:=a) in H5. am. am. am. ap next_compatible_next; am. am. wr H4. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. am. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. am. am. rwi Image.inc_rw H5. rw Image.inc_rw. nin H5. sh x2; xd. rewrite chenille_punctured_downward with (a:= a). rewrite chenille_punctured_downward with (a:=a) in H5. am. ap next_compatible_next; am. am. am. am. rw H4. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. ap next_compatible_next. am. am. rewrite chenille_punctured_downward with (a:=a) in H5. ufi punctured_downward_subset H5; Ztac. ap next_compatible_next. am. am. rw next_leq_gen_leq. ap leq_refl; try lu. am. am. am. rewrite leq_gen_leq with (a:=a). ap leq_refl; lu. am. am. am. exact (H3 _ H0). Qed. End Transfinite_Mapping. (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) Module Ordinal. Import Universe. Export Transfinite. Definition ID (y:E):= y. Definition is_ordinal (o:E):=is_leq_gen_scale ID o. Lemma ordinal_union : forall z:E, (forall u:E, inc u z -> is_ordinal u) -> is_ordinal (union z). Proof. ir. uhg. ap leq_gen_scale_union. ir. exact (H y H0). Qed. Lemma emptyset_ordinal : is_ordinal emptyset. Proof. assert (emptyset = union emptyset). ap extensionality; uhg; ir. elim (B H). cp (union_exists H). nin H0. ee. elim (B H1). rw H. ap ordinal_union; ir. elim (B H0). Qed. Lemma ordinal_tack_on : forall o:E, is_ordinal o -> is_ordinal (tack_on o o). Proof. ir. uhg. apply by_cases with (inc o o); ir. assert (tack_on o o = o). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc. ap or_introl; am. rw H1; am. change (is_leq_gen_scale ID (tack_on o (ID o))). ap leq_gen_scale_tack_on. exact H. am. Qed. Lemma ordinal_sub_or : forall a o:E, is_ordinal a -> is_ordinal o -> (sub a o \/ sub o a). Proof. ir. uh H; uh H0. cp (leq_gen_scale_or H H0). am. Qed. Lemma ordinal_induction : forall (p:EP), (forall z:E,(forall u:E, inc u z -> p u)-> p (union z)) -> (forall u :E, p u -> p (tack_on u u)) -> (forall o:E, is_ordinal o -> p o). Proof. ir. util (lgs_induction (f:=ID) (p:= p)). am. am. ap H2. am. Qed. Definition is_smallest_ordinal_with (p:EP)(o:E):= (is_ordinal o & p o & (forall x:E, is_ordinal x -> p x -> sub o x)). Lemma exists_smallest_ordinal_with : forall (p:EP), (exists x:E, (is_ordinal x&p x)) -> exists o:E, is_smallest_ordinal_with p o. Proof. ir. util (lgs_smallest_with_property (f:=ID)(p:=p)). am. am. Qed. Lemma ordinal_not_inc : forall x o:E, is_ordinal o -> inc x o -> ~inc x x. Proof. ir. util (ordinal_induction (p:= fun y:E=>(forall u:E, inc u y -> ~inc u u))). ir. cp (union_exists H2). nin H3; ee. cp (H1 x0 H4 u H3). am. ir. rwi tack_on_inc H2; nin H2. ap H1; am. uhg; ir. util (H1 u0). wr H2; am. ap H4; am. cbv beta in H1. apply H1 with o. am. am. Qed. Lemma ordinal_inc_ordinal : forall x o:E, is_ordinal o -> inc x o -> is_ordinal x. Proof. ir. util (ordinal_induction (p:= fun y:E=>(is_ordinal y & forall u:E, inc u y -> is_ordinal u))); ir. ee. ap ordinal_union. ir. cp (H1 u H2). ee; am. ir. nin (union_exists H2). ee. cp (H1 x0 H4). ee. ap H6; am. ee. ap ordinal_tack_on; am. ir. rwi tack_on_inc H3; nin H3. ap H2; am. rw H3; am. cbv beta in H1. cp (H1 o H); ee. ap H3; am. Qed. Lemma ordinal_not_inc_itself :forall o:E, is_ordinal o -> ~inc o o. Proof. ir. uhg; ir. apply ordinal_not_inc with o o. am. am. am. Qed. Lemma ordinal_strict_sub_inc : forall a o:E, is_ordinal a -> is_ordinal o -> strict_sub a o -> inc a o. Proof. ir. uh H; uh H0. cp H; cp H0. uh H; uh H0; nin H; nin H0. ee. assert (next x0 a= ID a). ap next_compatible_scale. am. apply leq_gen_scale_subset with ID. am. am. rw H0; uh H1; ee; am. rw H0; am. wr H0. ufi ID H6. wr H6. ap next_inc_U. rw H0; am. uh H4; ee; am. Qed. Lemma ordinal_inc_rw : forall x o:E, is_ordinal o -> (inc x o = (is_ordinal x & strict_sub x o)). Proof. ir. ap iff_eq; ir. dj. apply ordinal_inc_ordinal with o; am. uhg; ee. uhg; uhg; ir. apply ordinal_not_inc_itself with o. am. rwi H2 H0. am. nin (ordinal_sub_or H H1). assert (inc x x). ap H2; am. assert False. apply ordinal_not_inc_itself with x; am. elim H4. am. ee. ap ordinal_strict_sub_inc; am. Qed. Lemma ordinal_inc_sub : forall a o:E, is_ordinal o -> inc a o -> sub a o. Proof. ir. rwi ordinal_inc_rw H0. ee. uh H1; ee; am. am. Qed. Definition ordinal_leq a o:= (is_ordinal a & is_ordinal o& sub a o). Definition ordinal_lt a o:= (ordinal_leq a o & a <> o). Lemma ordinal_lt_rw : forall a o:E, ordinal_lt a o = (is_ordinal o&inc a o). Proof. ir. uf ordinal_lt. uf ordinal_leq; ap iff_eq; ir; xd. rw ordinal_inc_rw. uf strict_sub; xd. am. rwi ordinal_inc_rw H0; ee; am. rwi ordinal_inc_rw H0; ee. uh H1; ee; am. am. rwi ordinal_inc_rw H0; ee. uh H1; ee; am. am. Qed. Lemma ordinal_leq_leq_or : forall a o:E, is_ordinal a -> is_ordinal o -> (ordinal_leq a o \/ ordinal_leq o a). Proof. ir. nin (ordinal_sub_or H H0). ap or_introl. uhg; ee; am. ap or_intror; uhg; ee; am. Qed. Lemma ordinal_leq_leq_eq : forall a b, ordinal_leq a b -> ordinal_leq b a -> a = b. Proof. ir. ap extensionality; lu. Qed. Lemma ordinal_leq_trans : forall a b, (exists c, ordinal_leq a c & ordinal_leq c b)-> ordinal_leq a b. Proof. ir. nin H. ee. uhg; ee. lu. lu. apply sub_trans with x; lu. Qed. Lemma ordinal_if_leq_or : forall a o:E, ordinal_leq a o -> (ordinal_lt a o \/ a = o). Proof. ir. apply by_cases with (a = o); ir. ap or_intror; am. ap or_introl. uhg; uh H; xd. uhg; ee; am. Qed. Lemma ordinal_lt_lt_eq_or : forall a o:E, is_ordinal a -> is_ordinal o -> (ordinal_lt a o \/ ordinal_lt o a \/ a=o). Proof. ir. nin (ordinal_leq_leq_or H H0). nin (ordinal_if_leq_or H1). ap or_introl. am. ap or_intror. ap or_intror. am. nin (ordinal_if_leq_or H1). ap or_intror. ap or_introl; am. ap or_intror; ap or_intror; sy; am. Qed. Lemma ordinal_lt_tack_on_leq : forall a o:E, is_ordinal a -> (ordinal_lt a o = ordinal_leq (tack_on a a) o). Proof. ir. ap iff_eq; ir. cp H0. rwi ordinal_lt_rw H1. ee. uhg; ee. ap ordinal_tack_on; am. am. uhg; ir. rwi tack_on_inc H3; nin H3. uh H0; ee. uh H0; ee. ap H6; am. rw H3; am. uhg; ee. uhg; ee; try am. uh H0; ee; am. uh H0; ee. uhg; ir. ap H2. rw tack_on_inc. ap or_introl; am. uhg; ir. uh H0; ee. apply ordinal_not_inc_itself with a. am. rw H1. ap H3. rw tack_on_inc. ap or_intror; sy; am. Qed. Lemma exists_smallest_ordinal_without : forall (p:EP), (exists x : E, (is_ordinal x & ~ p x))-> exists o:E, (is_ordinal o & ~ p o & forall y : E, inc y o -> p y). Proof. ir. util (exists_smallest_ordinal_with (p:= fun x => (is_ordinal x &~p x))). nin H; ee. sh x; ee; am. nin H0. uh H0. ee. sh x. ee; try am. ir. ap excluded_middle; uhg; ir. assert (x = y). ap extensionality. ap H2. apply ordinal_inc_ordinal with x. am. am. ee. apply ordinal_inc_ordinal with x; am. am. ap ordinal_inc_sub. am. am. apply ordinal_not_inc_itself with x. am. wri H6 H4; am. Qed. Definition is_sow (p:EP) o := is_ordinal o & (exists x, is_ordinal x & p x) -> is_smallest_ordinal_with p o. Definition sow (p:EP) := choose (is_sow p). Lemma sow_exists : forall p, exists o, is_sow p o. Proof. ir. apply by_cases with (exists x, is_ordinal x & p x). ir. sh (choose (is_smallest_ordinal_with p)). cp (exists_smallest_ordinal_with H). cp (choose_pr H0). cbv beta in H1. uhg; ee. uh H1; ee. am. ir. am. ir. sh emptyset. uhg; ee. ap emptyset_ordinal. ir. elim (H H0). Qed. Lemma sow_is_sow : forall p, is_sow p (sow p). Proof. ir. cp (sow_exists p). cp (choose_pr H). am. Qed. Lemma sow_ordinal : forall p, is_ordinal (sow p). Proof. ir. cp (sow_is_sow p). uh H; ee. am. Qed. Lemma sow_property : forall p, (exists x:E, (is_ordinal x & p x)) -> p (sow p). Proof. ir. cp (sow_is_sow p). uh H0; ee. cp (H1 H). uh H2; ee. am. Qed. Lemma sow_smallest : forall (p:EP) o, is_ordinal o -> p o -> ordinal_leq (sow p) o. Proof. ir. cp (sow_is_sow p). uh H1; ee. util H2. sh o; ee; am. uh H3; ee. cp (H5 _ H H0). uhg; ee. ap sow_ordinal. am. am. Qed. Lemma ordinal_leq_gen_refl : forall o:E, is_ordinal o -> leq_gen ID o o. Proof. ir. pose (q:= tack_on o o). assert (is_ordinal q). uf q; ap ordinal_tack_on. am. uh H0. uh H0. nin H0; ee. assert (inc o (U x)). rw H0; uf q; rw tack_on_inc. ap or_intror; tv. rw (leq_gen_leq (f:=ID) (a:= x)). ap leq_refl. do 3 (uh H1; ee); am. am. am. am. am. Qed. Lemma ordinal_leq_gen_tack_on : forall o:E, is_ordinal o -> leq_gen ID o (tack_on o o). Proof. ir. pose (u:=tack_on o o). assert (is_ordinal u). uf u; ap ordinal_tack_on; am. assert (ordinal_lt o u). rw ordinal_lt_rw. ee; try am. uf u; rw tack_on_inc; ap or_intror; tv. pose (q:= tack_on u u). assert (is_ordinal q). uf q; ap ordinal_tack_on; am. assert (ordinal_lt u q). rw ordinal_lt_rw. ee; try am. uf q; rw tack_on_inc; ap or_intror; tv. cp H2; uh H4; uh H4; nin H4; ee. assert (u = next x u). sy; transitivity (ID u). apply (next_compatible_scale (f:= ID)). am. cp H0. uh H6; uh H6; nin H6; ee. wr H6. apply next_comp_sub_scale with (f:= ID). am. am. rw H6; rw H4. uh H3; ee. uh H3; ee; am. rw H4. rwi ordinal_lt_rw H3; ee. rwi ordinal_inc_rw H6; ee; am. tv. rw (leq_gen_leq (f:=ID)(a:=x)). assert (lt x o u). rw H6; ap next_compatible_lt. uh H0; uh H0; nin H0; ee. wr H0; apply next_comp_sub_scale with (f:= ID). am. am. rw H0; rw H4. uh H3; ee. uh H3; ee; am. rwi ordinal_lt_rw H3. ee. rwi ordinal_inc_rw H7. ee. rw H4; am. am. rwi ordinal_lt_rw H1; ee; am. uh H7; ee; am. am. rw H4. uf q; rw tack_on_inc; ap or_introl. uf u; rw tack_on_inc; ap or_intror; tv. rw H4; uf q; rw tack_on_inc; ap or_intror; tv. Qed. Lemma leq_gen_ordinal : forall o:E, leq_gen ID o o -> is_ordinal o. Proof. ir. uh H. nin H; ee. assert (is_ordinal (U x)). uhg. uhg. sh x; ee; try tv; try am. apply ordinal_inc_ordinal with (U x). am. uh H0; ee; am. Qed. Lemma leq_gen_ordinal_leq : forall a o:E, leq_gen ID a o -> ordinal_leq a o. Proof. ir. uhg; dj. ap leq_gen_ordinal. apply leq_gen_def1 with o; am. ap leq_gen_ordinal; apply leq_gen_def2 with a; am. nin (leq_gen_is_next H). rw H2; uhg; ir; am. nin H2. ee. ap ordinal_inc_sub. am. ufi ID H4. rw H4; am. Qed. Lemma ordinal_leq_leq_gen : forall a o:E, ordinal_leq a o = leq_gen ID a o. Proof. ir. ap iff_eq; ir. assert (leq_gen ID a a). ap ordinal_leq_gen_refl. uh H; ee; am. assert (leq_gen ID o o). ap ordinal_leq_gen_refl. uh H; ee; am. cp (leq_gen_or H0 H1). nin H2. am. assert (ordinal_leq o a). ap leq_gen_ordinal_leq. am. assert (a = o). ap extensionality. uh H; ee; am. uh H3; ee; am. rw H4; am. ap leq_gen_ordinal_leq; am. Qed. Definition obi x := create x sub. Lemma obi_U : forall x:E, (U (obi x)) = x. Proof. ir. uf obi. rw underlying_create; tv. Save. Lemma obi_leq : forall x u v:E, leq (obi x) u v = (inc u x & inc v x & sub u v). Proof. ir. uf obi; rw leq_create_all. tv. Qed. Lemma obi_axioms : forall x:E, axioms (obi x). Proof. ir. uf obi. ap create_axioms. uf property; dj. uhg; ir; am. ap extensionality; am. apply sub_trans with y; am. Qed. Lemma ordinal_obi_leq : forall x u v:E, is_ordinal x -> leq (obi x) u v = (inc u x & inc v x & ordinal_leq u v). Proof. ir. rw obi_leq; uf ordinal_leq; ap iff_eq; ir; xd. apply ordinal_inc_ordinal with x; am. apply ordinal_inc_ordinal with x; am. Qed. Lemma ordinal_leq_inc_tack_on : forall o x:E, is_ordinal o -> ordinal_leq x o = inc x (tack_on o o). Proof. ir. ap iff_eq; ir. nin (ordinal_if_leq_or H0). rw tack_on_inc; ap or_introl. rwi ordinal_lt_rw H1. ee; am. rw tack_on_inc; ap or_intror. am. rwi tack_on_inc H0. nin H0. rwi ordinal_inc_rw H0. ee. uh H1; ee. uhg; ee; am. am. rw H0; uhg; ee. am. am. uhg; ir; am. Qed. Lemma ordinal_container : forall z:E, (forall u:E, inc u z -> is_ordinal u) -> exists o:E, (is_ordinal o & sub z o). Proof. ir. pose (q:= (union z)). assert (is_ordinal q). uf q; ap ordinal_union; am. sh (tack_on q q). ee. ap ordinal_tack_on; am. uhg; ir. assert (ordinal_leq x q). uhg; ee. ap H; am. am. uhg; ir. uf q; apply union_inc with x. am. am. wr ordinal_leq_inc_tack_on. am. am. Qed. Lemma ordinal_leq_obi : forall a x y, next_compatible ID a -> inc x (U a) -> inc y (U a) -> leq (obi (U a)) x y = leq a x y. Proof. ir. assert (is_ordinal (U a)). uhg; ee. uhg. sh a; ee; try tv; try am. ap iff_eq; ir. wr (leq_gen_leq (f:=ID)). rwi ordinal_obi_leq H3. ee. wr ordinal_leq_leq_gen. am. am. am. am. am. rw ordinal_obi_leq. ee; try am. wri (leq_gen_leq (f:=ID)) H3. rw ordinal_leq_leq_gen. am. am. am. am. am. Qed. Lemma ordinal_next : forall a x, next_compatible ID a -> inc x (U a) -> next a x = x. Proof. ir. uh H; ee. cp (H1 _ H0). ufi ID H2. wr H2. wr next_punctured_downward. sy; am. am. am. Qed. Lemma punctured_downward_for_ord : forall a x, next_compatible ID a -> inc x (U a) -> punctured_downward_subset a x = x. Proof. ir. util (ordinal_next (a:=a) (x:=x)). am. am. uh H. ee. ufi ID H2. ap H2. am. Qed. Lemma ordinal_obi_lt : forall o x y, is_ordinal o -> lt (obi o) x y = (inc x y & inc y o). Proof. ir. ap iff_eq; ir. ee. uh H0; ee. rwi obi_leq H0. ee. ap ordinal_strict_sub_inc. apply ordinal_inc_ordinal with o; am. apply ordinal_inc_ordinal with o; am. uhg; ee; am. uh H0; ee. uh H0; ee. rwi obi_U H2; am. ee. uhg; ee. rw obi_leq. ee; try am. cp ordinal_inc_sub. ufi sub H2. apply H2 with y. am. am. am. ap ordinal_inc_sub. apply ordinal_inc_ordinal with o; am. am. uhg; ir. apply ordinal_not_inc_itself with x. apply ordinal_inc_ordinal with o. am. rw H2; am. wri H2 H0; am. Qed. Lemma ordinal_inc_trans: forall o x, (exists y, inc x y & inc y o) -> is_ordinal o -> inc x o. Proof. ir. cp ordinal_inc_sub. ufi sub H1. nin H. ee. apply H1 with x0. am. am. am. Qed. Lemma ordinal_punctured_downward : forall o x, is_ordinal o -> inc x o -> punctured_downward_subset (obi o) x = x. Proof. ir. uf punctured_downward_subset; ap extensionality; uhg; ir. Ztac. rwi ordinal_obi_lt H3. ee; am. am. ap Z_inc. rw obi_U. ap ordinal_inc_trans. sh x. ee; am. am. rw ordinal_obi_lt. ee; am. am. Qed. Lemma ordinal_obi_next_compatible : forall o:E, is_ordinal o -> next_compatible ID (obi o). Proof. ir. cp H; uh H. uh H. nin H. ee. assert (same_order x (obi o)). uhg; ee; ap show_is_suborder. do 5 (uh H1; ee; try am). ap obi_axioms. ir. wr H. rw ordinal_leq_obi. am. am. uh H2; ee; am. uh H2; ee; am. ap obi_axioms. do 5 (uh H1; ee; try am). ir. wr ordinal_leq_obi. rw H; am. am. uh H2; ee. rwi obi_U H2; rw H; am. uh H2; ee. rwi obi_U H3; rw H; am. uhg; dj. apply wo_same_order with x. am. uh H1; ee; am. rw ordinal_punctured_downward. tv. am. rwi obi_U H4; am. Qed. Lemma ordinal_inc : forall o x:E, is_ordinal o -> inc x o = (leq_gen ID x o & x <> o). Proof. ir. ap iff_eq; ir. ee. wr ordinal_leq_leq_gen. uhg. ee; try am. apply ordinal_inc_ordinal with o; am. ap ordinal_inc_sub; am. uhg; ir. rwi H1 H0. apply ordinal_not_inc_itself with o; am. ee. wri ordinal_leq_leq_gen H0. uh H0. ee. ap ordinal_strict_sub_inc. am. am. uhg; ee; am. Qed. Lemma ordinal_chenille : forall o, is_ordinal o -> chenille ID o = o. Proof. ir. ap extensionality; uhg; ir. rwi chenille_inc H0. wri ordinal_inc H0. am. am. rwi chenille_inc H0. ap ordinal_leq_gen_refl; am. ap ordinal_leq_gen_refl; am. rw chenille_inc. rwi ordinal_inc H0. am. am. ap ordinal_leq_gen_refl; am. Qed. Lemma ordinal_downward_lgs : forall o:E, is_ordinal o -> downward_lgs ID o = tack_on o o. Proof. ir. wr chenille_tack_on. rw ordinal_chenille. tv. am. ap ordinal_leq_gen_refl; am. Qed. Export Transfinite_Mapping. Lemma ordinal_inc_induction : forall (p:EP)(o:E), (forall u:E, (forall x:E, inc x u -> p x)-> p u) -> is_ordinal o -> p o. Proof. ir. util (chenille_induction (f:=ID) (p:=p)). ir. ap H. ir. ap H2. rw ordinal_chenille. am. ap leq_gen_ordinal. am. ap H1. ap ordinal_leq_gen_refl; am. Qed. Lemma ID_expansive : is_expansive ID. Proof. uhg. ir. uf ID. ap ordinal_not_inc_itself. am. Qed. Definition wo_avatar a := avatar (next a) ID. Definition wo_ordinal a := (Image.create (U a) (wo_avatar a)). Lemma wo_avatar_surjective : forall a, is_well_ordered a -> Transformation.surjective (U a) (wo_ordinal a) (wo_avatar a). Proof. ir. uhg; ee. uhg. ir. uf wo_ordinal; rw Image.inc_rw. sh x; ee; try am. tv. uhg. ir. ufi wo_ordinal H0; rwi Image.inc_rw H0. nin H0. ee. sh x0; ee; am. Qed. Lemma wo_avatar_injective : forall a, is_well_ordered a -> Transformation.injective (U a) (wo_ordinal a) (wo_avatar a). Proof. ir. uhg; ee. uhg. ir. uf wo_ordinal; rw Image.inc_rw. sh x; ee; try am. tv. uhg. ir. transitivity (avatar ID (next a) (wo_avatar a x)). uf wo_avatar. rw avatar_trans. rw avatar_refl. tv. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. ap ID_expansive. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. rw H2. uf wo_avatar. rw avatar_trans. rw avatar_refl. tv. rw next_leq_gen_leq; try am. ap leq_refl; lu. ap ID_expansive. rw next_leq_gen_leq; try am. ap leq_refl; lu. Qed. Lemma wo_avatar_bijective : forall a, is_well_ordered a -> Transformation.bijective (U a) (wo_ordinal a) (wo_avatar a). Proof. ir. uhg; ee. uhg; ir. uf wo_ordinal; rw Image.inc_rw. sh x; ee; try am. tv. ap wo_avatar_surjective; am. ap wo_avatar_injective; am. Qed. Lemma wo_avatar_is_ordinal : forall a x, is_well_ordered a -> inc x (U a) -> is_ordinal (wo_avatar a x). Proof. ir. uf wo_avatar. ap leq_gen_ordinal. ap avatar_leq_gen_def. rw next_leq_gen_leq; try am. ap leq_refl; lu. Qed. Lemma wo_ordinal_is_ordinal : forall a, is_well_ordered a -> is_ordinal (wo_ordinal a). Proof. ir. uf wo_ordinal. uhg. uf wo_avatar. ap lgs_avatar_image. apply scale_subset_is_leq_gen_scale with a. ap next_compatible_next. am. uhg; ee; try am. ap sub_refl. ir. uh H1; ee; am. Qed. Lemma wo_avatar_ordinal_leq : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> leq a x y -> ordinal_leq (wo_avatar a x) (wo_avatar a y). Proof. ir. uf wo_avatar. ap leq_gen_ordinal_leq; try am. ap avatar_leq_gen; try am. ap ID_expansive. rw next_leq_gen_leq; try am. Qed. Lemma wo_avatar_obi_id : forall o x, is_ordinal o -> inc x o -> wo_avatar (obi o) x = x. Proof. ir. cp (ordinal_obi_next_compatible H). uf wo_avatar. rewrite<- next_compatible_avatar with (f:=ID). ap avatar_refl. ap ordinal_leq_gen_refl. apply ordinal_inc_ordinal with o; am. am. rw obi_U. am. Qed. Lemma wo_ordinal_obi_rw : forall o, is_ordinal o -> wo_ordinal (obi o) = o. Proof. ir. uf wo_ordinal. ap extensionality; uhg; ir. rwi Image.inc_rw H0. nin H0. ee. rwi wo_avatar_obi_id H1. wr H1. rwi obi_U H0. am. am. rwi obi_U H0; am. rw Image.inc_rw. sh x. ee. rw obi_U; am. ap wo_avatar_obi_id. am. am. Qed. (*** thought we needed these for cardinal.v but didn't... ******************************************************* Lemma wo_avatar_same_order : forall a b x, is_well_ordered a -> same_order a b -> inc x (U b) -> wo_avatar a x = wo_avatar b x. Proof. Qed. Lemma wo_ordinal_same_order : forall a b, is_well_ordered a -> same_order a b -> wo_ordinal a = wo_ordinal b. Proof. Qed. Lemma obi_suborder_same_order : forall o u, is_ordinal o -> sub u o -> same_order (obi u) (suborder u (obi o)). Proof. Qed. ***********************************************) Lemma wo_leq_rw : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> leq a x y = ordinal_leq (wo_avatar a x) (wo_avatar a y). Proof. ir. ap iff_eq; ir. ap wo_avatar_ordinal_leq; try am. cp H. uh H; ee. uh H; ee. cp (H5 _ _ H0 H1). nin H6. am. assert (ordinal_leq (wo_avatar a y) (wo_avatar a x)). ap wo_avatar_ordinal_leq; try am. uh H2. uh H7. ee. assert (x = y). util (wo_avatar_injective (a:=a)). am. uh H12; ee. uh H13. ap H13. am. am. ap extensionality; am. rw H12. ap leq_refl; try am; try lu. Qed. Lemma wo_lt_rw : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> lt a x y = ordinal_lt (wo_avatar a x) (wo_avatar a y). Proof. ir. ap iff_eq; ir. uhg; ee. wr wo_leq_rw. uh H2; ee; am. am. am. am. uhg; ir. uh H2; ee. ap H4. util (wo_avatar_injective (a:= a)). am. uh H5; ee. ap H6. am. am. am. uhg; ee. rw wo_leq_rw. uh H2; ee; am. am. am. am. uhg; ir. uh H2. ee. ap H4. rw H3; tv. Qed. Lemma wo_punctured_downward : forall a x, is_well_ordered a -> inc x (U a) -> Image.create (punctured_downward_subset a x) (wo_avatar a) = wo_avatar a x. Proof. ir. rewrite<- chenille_punctured_downward with (f:=next a). uf wo_avatar. wr avatar_chenille. ap ordinal_chenille. change (is_ordinal (wo_avatar a x)). ap wo_avatar_is_ordinal. am. am. ap ID_expansive. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. ap next_compatible_next; am. am. Qed. Lemma suborder_wo_avatar_decreasing : forall u a x, is_well_ordered a -> sub u (U a) -> inc x u -> ordinal_leq (wo_avatar (suborder u a) x) (wo_avatar a x). Proof. ir. set (b:=suborder u a). assert (lem1: U b = u). uf b; rw underlying_suborder; tv. assert (lem2 : is_well_ordered b). uf b; ap suborder_well_ordered. am. am. util (wo_induction lem2 (p:= fun y=> (ordinal_leq (wo_avatar b y) (wo_avatar a y)))). ir. uhg; ee. ap wo_avatar_is_ordinal. am. am. ap wo_avatar_is_ordinal. am. ap H0. wr lem1; am. uhg; ir. wri wo_punctured_downward H4. rwi Image.inc_rw H4. nin H4. ee. ufi punctured_downward_subset H4. Ztac. cp (H3 _ H6 H7). rwi H5 H8. assert (lt a x2 x0). uh H7. uhg; ee; try am. ufi b H7. rwi leq_suborder_all H7. ee. am. lu. am. assert (ordinal_lt x1 (wo_avatar a x0)). uhg; ee. uhg; ee. uh H8; ee; am. ap wo_avatar_is_ordinal. am. ap H0. wr lem1; am. apply sub_trans with (wo_avatar a x2). uh H8; ee; am. uh H9; ee. rwi wo_leq_rw H9. lu. am. ap H0; wr lem1; am. lu. uhg; ir. rwi wo_lt_rw H9. uh H9; ee. ap H11. ap extensionality. lu. wr H10. lu. am. ap H0; wr lem1; am. ap H0; wr lem1; am. rwi ordinal_lt_rw H10. ee; am. am. am. wri lem1 H1. cp (H2 _ H1). am. Qed. Lemma ordinal_saturated : forall a b c, is_ordinal c -> inc b c -> ordinal_leq a b -> inc a c. Proof. ir. assert (ordinal_lt a c). uhg; ee. uhg; ee. lu. am. uh H1. ee. rwi ordinal_inc_rw H0. ee. uh H4. ee. apply sub_trans with b; am. am. uhg; ir. uh H1; ee. rwi H2 H4. apply ordinal_not_inc_itself with b. am. ap H4; am. rwi ordinal_lt_rw H2. ee; am. Qed. Lemma wo_avatar_ordinal_inc : forall a x, is_well_ordered a -> inc x (U a) -> inc (wo_avatar a x) (wo_ordinal a). Proof. ir. uf wo_ordinal. rw Image.inc_rw. sh x; ee; try am; try tv. Qed. Lemma suborder_wo_ordinal_decreasing : forall u a, is_well_ordered a -> sub u (U a)-> ordinal_leq (wo_ordinal (suborder u a)) (wo_ordinal a). Proof. ir. uhg; ee. ap wo_ordinal_is_ordinal. ap suborder_well_ordered; am. ap wo_ordinal_is_ordinal; am. uhg; ir. ufi wo_ordinal H1. rwi Image.inc_rw H1. nin H1. ee. wr H2. apply ordinal_saturated with (wo_avatar a x0). ap wo_ordinal_is_ordinal. am. ap wo_avatar_ordinal_inc. am. ap H0. rwi underlying_suborder H1. am. ap suborder_wo_avatar_decreasing. am. am. rwi underlying_suborder H1. am. Qed. End Ordinal. (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) Module Cardinal. Import Universe. Import Transformation. Import Map. Export Ordinal. Definition iso_sub x y := exists u, (are_isomorphic x u & sub u y). Lemma iso_sub_trans_rw : forall x y, iso_sub x y = (exists f, Transformation.injective x y f). Proof. ir. ap iff_eq; ir. uh H; nin H. ee. sh (isotrans x x0). rwi iso_isotrans_rw H. uh H; ee. cp (subidentity_injective H0). cp (compose_injective H2 H3). am. uhg. nin H. sh (Image.create x x0). ee. rw iso_trans_ex_rw. sh x0. apply trans_sub_bijective with x y. am. ap sub_refl. uhg; ir. rwi Image.inc_rw H0. nin H0. ee. wr H1. uh H. ee. uh H. ap H. am. Qed. Lemma sub_iso_sub: forall a b, sub a b-> iso_sub a b. Proof. ir. uhg. sh a. ee. ap are_isomorphic_refl. am. Qed. (*** sow = smallest ordinal with the property in question **) Definition cardinality x := sow (are_isomorphic x). Definition card_isomap x := isomap x (cardinality x). Definition card_isotrans x := isotrans x (cardinality x). Lemma card_isomorphic : forall x, are_isomorphic x (cardinality x). Proof. ir. uf cardinality. ap sow_property. cp (every_set_can_be_well_ordered x). nin H. ee. sh (wo_ordinal x0). ee. ap wo_ordinal_is_ordinal. am. apply trans_bij_isomorphic with (wo_avatar x0). wr H0. ap wo_avatar_bijective. am. Qed. Lemma card_isomap_bij : forall x, Map.bijective x (cardinality x) (card_isomap x). Proof. ir. uf card_isomap. ap isomap_bij. ap card_isomorphic. Qed. Lemma card_isotrans_bij : forall x, Transformation.bijective x (cardinality x) (card_isotrans x). Proof. ir. uf card_isotrans. ap isotrans_bij. ap card_isomorphic. Qed. Lemma cardinality_ordinal : forall x, is_ordinal (cardinality x). Proof. ir. uf cardinality. ap sow_ordinal. Qed. Lemma cardinality_smallest : forall x o, is_ordinal o -> are_isomorphic x o -> ordinal_leq (cardinality x) o. Proof. ir. uf cardinality. ap sow_smallest. am. am. Qed. Lemma cardinality_invariant : forall x y, are_isomorphic x y -> cardinality x = cardinality y. Proof. ir. ap ordinal_leq_leq_eq. ap cardinality_smallest. ap cardinality_ordinal. ap are_isomorphic_trans. sh y. ee; try am. ap card_isomorphic. ap cardinality_smallest. ap cardinality_ordinal. ap are_isomorphic_trans. sh x. ee; try am. ap are_isomorphic_symm. am. ap card_isomorphic. Qed. Lemma wo_ordinal_isomorphic : forall a, is_well_ordered a -> are_isomorphic (U a) (wo_ordinal a). Proof. ir. rw iso_trans_ex_rw. sh (wo_avatar a). ap wo_avatar_bijective. am. Qed. Lemma wo_ordinal_cardinal_leq : forall a, is_well_ordered a -> ordinal_leq (cardinality (U a)) (wo_ordinal a). Proof. ir. ap cardinality_smallest. ap wo_ordinal_is_ordinal. am. ap wo_ordinal_isomorphic; am. Qed. Lemma ordinal_leq_subset_wo_ordinal : forall a u, is_well_ordered a -> sub u (U a) -> ordinal_leq (cardinality u) (wo_ordinal a). Proof. ir. ap ordinal_leq_trans. pose (b:=suborder u a). sh (wo_ordinal b). assert (u = (U b)). uf b; rw underlying_suborder. tv. ee. rw H1. uf b. ap wo_ordinal_cardinal_leq. ap suborder_well_ordered. am. am. uf b. ap suborder_wo_ordinal_decreasing. am. am. Qed. Lemma subset_ordinal_cardinal_leq : forall u o, is_ordinal o -> sub u o -> ordinal_leq (cardinality u) o. Proof. ir. cp (wo_ordinal_obi_rw H). wr H1. ap ordinal_leq_subset_wo_ordinal. cp (ordinal_obi_next_compatible H). lu. rw obi_U. am. Qed. Lemma isomorphic_iso_sub : forall a b, are_isomorphic a b -> iso_sub a b. Proof. ir. rwi iso_trans_ex_rw H. nin H. rw iso_sub_trans_rw. sh f; lu. Qed. Lemma iso_sub_trans : forall a c, (exists b, iso_sub a b & iso_sub b c) -> iso_sub a c. Proof. ir. nin H. ee. rwi iso_sub_trans_rw H0. nin H0. rwi iso_sub_trans_rw H. nin H. rw iso_sub_trans_rw. sh (fun y => (x0 (x1 y))). apply compose_injective with x. am. am. Qed. Lemma iso_sub_ordinal_leq : forall u o, is_ordinal o -> iso_sub u o -> ordinal_leq (cardinality u) o. Proof. ir. uh H0. nin H0. ee. cp (cardinality_invariant H0). rw H2. ap subset_ordinal_cardinal_leq. am. am. Qed. Lemma iso_sub_cardinal_leq : forall x y, iso_sub x y -> (ordinal_leq (cardinality x) (cardinality y)). Proof. ir. assert (iso_sub x (cardinality y)). cp (card_isomorphic y). cp (isomorphic_iso_sub H0). ap iso_sub_trans. sh y; ee; am. ap iso_sub_ordinal_leq. ap cardinality_ordinal. am. Qed. Lemma sub_cardinal_leq : forall x y, sub x y -> (ordinal_leq (cardinality x) (cardinality y)). Proof. ir. ap iso_sub_cardinal_leq. ap sub_iso_sub; am. Qed. Lemma bernstein_cantor_schroeder : forall x y, iso_sub x y -> iso_sub y x -> are_isomorphic x y. Proof. ir. cp (iso_sub_cardinal_leq H). cp (iso_sub_cardinal_leq H0). cp (ordinal_leq_leq_eq H1 H2). cp (card_isomorphic x). cp (card_isomorphic y). ap are_isomorphic_trans. sh (cardinality x). ee; try am. rw H3. ap are_isomorphic_symm. am. Qed. Definition is_finite x := forall f, Transformation.injective x x f -> Transformation.bijective x x f. Definition is_infinite x := ~(is_finite x). Lemma finite_invariant : forall y, (exists x, are_isomorphic x y & is_finite x) -> is_finite y. Proof. ir. nin H. ee. rwi iso_trans_ex_rw H. nin H. uhg. ir. pose (g:= fun z => (inverse x x0 (f (x0 z)))). cp (Transformation.bijective_inverse H). assert (are_inverse y x (inverse x x0) x0). uhg; ee; lu. cp (Transformation.inverse_bijective H3). uh H0. util (H0 g). uhg. ee. uf g. uhg; ir. uh H4; ee. uh H4. ap H4. uh H1; ee; uh H1. ap H1. uh H; ee; uh H; ap H. am. uf g; uhg; ir. uh H; ee. uh H9; ee. ap H10. am. am. uh H1; ee. ap H11. ap H. am. ap H. am. uh H4; ee. uh H13; ee. ap H14. ap H1. ap H; am. ap H1; ap H; am. am. uhg; ee; try lu. uhg. ee; try lu. uhg. ir. uh H5; ee. uh H7; ee. util (H9 (inverse x x0 x1)). uh H4; ee. ap H4. am. nin H10; ee. sh (x0 x2). ee. uh H; ee; ap H. am. uh H4; ee. uh H13; ee. ap H14. uh H1; ee; ap H1. uh H; ee; ap H. am. am. am. Qed. Lemma finite_tack_on_case : forall x y f, is_finite x -> Transformation.injective (tack_on x y) (tack_on x y) f -> f y = y -> Transformation.bijective (tack_on x y) (tack_on x y) f. Proof. ir. uhg; ee; try lu. apply by_cases with (inc y x); ir. assert (tack_on x y = x). ap extensionality; uhg; ir. rwi tack_on_inc H3; nin H3. am. rw H3; am. rw tack_on_inc. ap or_introl; am. rw H3. rwi H3 H0. cp (H f H0). lu. util (H f). uhg; ee. uhg; ir. uh H0; ee. util (H0 x0). rw tack_on_inc; ap or_introl; am. rwi tack_on_inc H5; nin H5. am. assert (x0 = y). ap H4. rw tack_on_inc. ap or_introl; am. rw tack_on_inc; ap or_intror; tv. rw H5; sy; am. assert False. ap H2. wr H6; am. elim H7. uh H0; ee. uhg; ir. ap H3. rw tack_on_inc; ap or_introl; am. rw tack_on_inc; ap or_introl; am. am. uhg; ee; try lu. uhg; ir. rwi tack_on_inc H4; nin H4. uh H3; ee. uh H5; ee. cp (H7 _ H4). nin H8. ee. sh x1. ee; try am. rw tack_on_inc; ap or_introl; am. sh y; ee. rw tack_on_inc; ap or_intror; tv. rw H4. am. Qed. Lemma finite_tack_on : forall x y, is_finite x -> is_finite (tack_on x y). Proof. ir. uhg; ir. pose (g:= fun z => Transposition.create y (f y) (f z)). util (finite_tack_on_case (x:=x) (y:=y) (f:=g)). am. uhg; ee. uhg; ir. uh H0; ee. cp (H0 x0 H1). apply by_cases with (f x0 = f y); ir. uf g. rw H4. rw Transposition.i_j_j. rw tack_on_inc; ap or_intror; tv. apply by_cases with (f x0 = y); ir. uf g. rw H5. rw Transposition.i_j_i. util (H0 y). rw tack_on_inc; ap or_intror; tv. am. uf g. rw Transposition.not_i_not_j; try am. uhg; ir. uh H0; ee. ap H4; try am. apply Transposition.inj with y (f y). am. uf g. rw Transposition.i_j_j. tv. uhg; ee; try lu. uhg; ee; try lu. uhg; ir. assert (inc (Transposition.create y (f y) x0) (tack_on x y)). apply by_cases with (x0 = y); ir. rw H3; rw Transposition.i_j_i. uh H0; ee; ap H0. rw tack_on_inc; ap or_intror; tv. apply by_cases with (x0 = f y); ir. rw H4; rw Transposition.i_j_j. rw tack_on_inc; ap or_intror; tv. rw Transposition.not_i_not_j; try am. uh H1; ee. uh H4; ee. cp (H6 _ H3). nin H7. sh x1; ee; try am. apply Transposition.inj with y (f y). am. Qed. Lemma finite_emptyset : is_finite emptyset. Proof. ir. uhg. ir. uhg. dj. uhg. ir. nin H0. nin x0. uhg. ee; try am. uhg. ir. nin H1. nin x0. uhg. ee; try am. uhg. ir. nin H2. nin x0. Qed. Lemma finite_tack : forall x y, is_finite x -> is_finite (tack y x). Proof. ir. uf tack. app finite_tack_on. Qed. (****** the next things to prove ********** Lemma finite_induction: forall (p:EP) x, (p emptyset) -> (forall y z, p y -> p (tack_on y z)) -> is_finite x -> p x. Proof. Qed. Lemma subset_finite : forall x, (exists y, (sub x y & is_finite y)) -> is_finite x. Proof. Qed. Lemma image_finite : forall x f, is_finite x -> is_finite (Image.create x f). Proof. Qed. ****************************************) End Cardinal. Module Naturals. (** We give some further properties relating the inductive type [nat] with the realization of its elements as ordinals *) Export Ordinal. Import Peano. Lemma inc_R_S : forall (i:nat), inc (R i) (R (S i)). Proof. ir. rw nat_realization_S. ap or_intror; tv. Qed. Lemma sub_R_S : forall (i:nat), sub (R i) (R (S i)). Proof. ir. uhg; ir. rw nat_realization_S. app or_introl. Qed. Lemma le_implies_sub : forall (i j:nat), le i j -> sub (R i) (R j). Proof. ir. nin H. uhg; ir; am. uhg; ir. rw nat_realization_S. ap or_introl. ap IHle. am. Qed. Lemma R_S_tack_on : forall (i:nat), R (S i) = tack_on (R i) (R i). Proof. ir. ap extensionality; uhg; ir. rw tack_on_inc. rwi nat_realization_S H. am. rw nat_realization_S. rwi tack_on_inc H. am. Qed. Lemma nat_ordinal : forall (i:nat), is_ordinal (R i). Proof. ir. nin i. rw nat_zero_emptyset. ap emptyset_ordinal. rw R_S_tack_on. ap ordinal_tack_on. am. Qed. Lemma nat_R_dichotomy : forall (i j : nat), (inc (R i) (R j) \/ inc (R j) (R i) \/ i = j). Proof. ir. util (ordinal_lt_lt_eq_or (a:= (R i)) (o:= (R j))). ap nat_ordinal. ap nat_ordinal. nin H. ap or_introl. rwi ordinal_lt_rw H. ee. am. nin H. ap or_intror. ap or_introl. rwi ordinal_lt_rw H. ee; am. ap or_intror. ap or_intror. app R_inj. Qed. Lemma nat_not_inc_itself : forall (i:nat), ~(inc (R i) (R i)). Proof. ir. assert (is_ordinal (R i)). ap nat_ordinal. cp (ordinal_not_inc_itself H). am. Qed. Lemma lt_implies_inc : forall (i j:nat), lt i j -> inc (R i) (R j). Proof. ir. cp (nat_R_dichotomy i j). nin H0. am. nin H0. assert (le i j). auto with arith. cp (le_implies_sub H1). assert (inc (R j) (R j)). ap H2. am. elim (nat_not_inc_itself H3). wri H0 H. cp (lt_irrefl i). elim (H1 H). Qed. (** Natural numbers' [lt] is the same as inclusion of the realized sets; and [le] is the same as subset. *) Lemma inc_lt : forall (i j:nat), inc (R i) (R j) = lt i j. Proof. ir. ap iff_eq; ir. cp (le_or_lt j i). nin H0. cp (le_implies_sub H0). assert (inc (R i) (R i)). app H1. elim (nat_not_inc_itself H2). am. app lt_implies_inc. Qed. Lemma sub_le : forall (i j : nat), sub (R i) (R j) = le i j. Proof. ir. ap iff_eq; ir. cp (le_or_lt i j). nin H0. am. cp (lt_implies_inc H0). cp (H _ H1). elim (nat_not_inc_itself H2). app le_implies_sub. Qed. Lemma inc_nat1 : forall (i:nat) x, inc x (R i) -> (exists j:nat, (lt j i) & R j = x). Proof. intro i. nin i. ir. rwi nat_zero_emptyset H. nin H. nin x0. ir. rwi nat_realization_S H. nin H. cp (IHi x H). nin H0. ee. sh x0. ee. auto with arith. am. sh i. ee. auto with arith. sy; am. Qed. Lemma inc_nat : forall (i:nat) x, inc x (R i) = (exists j:nat, (lt j i) & R j = x). Proof. ir. ap iff_eq; ir. ap inc_nat1. am. nin H. ee. wr H0. rw inc_lt. am. Qed. Lemma sub_R_nat : forall (i:nat), sub (R i) nat. Proof. ir. uhg; ir. rwi inc_nat H. nin H. ee. wr H0. ap R_inc. Qed. Lemma inc_nat_from_inc_R : forall x, (exists i:nat, inc x (R i)) -> inc x nat. Proof. ir. nin H. cp (sub_R_nat (i:=x0)). ap H0. am. Qed. Lemma le_le_minus : forall m n p, m <= n -> m - p <= n - p. Proof. ir. om. Qed. Lemma zero_emptyset : R 0 = emptyset. Proof. rww nat_zero_emptyset. Qed. Lemma nat_succ_tack_on : forall (i:nat), R (S i) = tack_on (R i) (R i). Proof. ir. ap extensionality; uhg; ir. rwi nat_realization_S H. rw tack_on_inc. am. rw nat_realization_S. rwi tack_on_inc H. am. Qed. (*** later should say that nats are ordinals; we probably want to reorganize this ********************************) Lemma inc_one : forall x, inc x (R 1) = (x = R 0). Proof. ir. rw nat_succ_tack_on. ap iff_eq; ir. rwi tack_on_inc H. nin H. rwi zero_emptyset H. nin H. elim x0. am. rw tack_on_inc. ap or_intror; am. Qed. Lemma two_tack_on : R 2 = tack_on (R 1) (R 1). Proof. ap nat_succ_tack_on. Qed. Lemma inc_two : forall x, inc x (R 2) = ((x = R 0) \/ (x = R 1)). Proof. ir. rw two_tack_on. ap iff_eq; ir. rwi tack_on_inc H. nin H. rwi inc_one H. ap or_introl; am. ap or_intror; am. rw tack_on_inc. nin H. ap or_introl. rw inc_one. am. ap or_intror; am. Qed. Lemma sub_zero_any : forall x, sub (R 0) x. Proof. ir. uhg; ir. rwi zero_emptyset H. nin H. elim x1. Qed. Lemma inc_zero_one : inc (R 0) (R 1). Proof. rw inc_one. tv. Qed. Lemma inc_zero_two : inc (R 0) (R 2). Proof. rw inc_two. ap or_introl; tv. Qed. Lemma inc_one_two : inc (R 1) (R 2). Proof. rw inc_two. ap or_intror; tv. Qed. Lemma sub_one_two : sub (R 1) (R 2). Proof. uhg; ir. rwi inc_one H. rw inc_two. ap or_introl; am. Qed. End Naturals. Module Iterate. Definition iterate (n:nat) (f:nat -> E -> E) (s:E) : E. intro n. induction n. ir. exact s. ir. exact (f n (IHn f s)). Defined. Lemma iterate_0 : forall f s, iterate 0 f s = s. Proof. ir. tv. Qed. Lemma iterate_Sn : forall n f s, iterate (S n) f s = f n (iterate n f s). Proof. ir. tv. Qed. Lemma iterate_nplus1 : forall n f s, iterate (n+1) f s = f n (iterate n f s). Proof. ir. assert (n+1 = S n). om. rw H. tv. Qed. Lemma iterate_1 :forall f s, iterate 1 f s = f 0 s. Proof. ir. tv. Qed. Lemma iterate_plus : forall m n f s, iterate (n + m) f s = iterate m (fun i => f (n + i)) (iterate n f s). Proof. intro m. nin m. ir. assert (n+0 = n). om. rw H. rw iterate_0. tv. ir. assert (n+ S m = S (n+m)). om. rw H. rw iterate_Sn. rw iterate_Sn. ap uneq. ap IHm. Qed. Lemma iterate_same : forall m n f g s t (P : E -> Prop), m = n -> s = t -> P s -> (forall i x, P x -> i < m -> P (f i x)) -> (forall i x, P x -> i f i x = g i x) -> iterate m f s = iterate n g t. Proof. ir. wr H. clear H. wr H0. assert (iterate m f s = iterate m g s & (forall i, i<= m -> P (iterate i f s))). generalize H2 H3. nin m. ir. ee. rw iterate_0. rww iterate_0. ir. assert (i=0). om. rw H6. rw iterate_0. am. ir. ee. rw iterate_Sn. rw iterate_Sn. util IHm. ir. ap H2. am. om. ir. ap H3. am. om. ir. ap H4. am. om. ir. ap H5. am. om. ee. rw H. ap H5. wr H. ap H6. om. om. util IHm. ir. ap H2. am. om. ir. ap H3. am. om. ir. ap H4. am. om. ir. ap H5. am. om. ee. ir. assert (i <= m \/ i = S m). om. nin H8. ap H6. am. rw H8. rw iterate_Sn. ap H2. ap H6. om. om. ee. am. Qed. End Iterate. (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) Module ProductMap. Export Map. Export Function. Export Relation. Definition product_map f g := L (Cartesian.product (domain f) (domain g)) (fun y => pair (V (pr1 y) f) (V (pr2 y) g)). Lemma product_map_axioms : forall a b c d f g, Map.axioms a b f -> Map.axioms c d g -> Map.axioms (Cartesian.product a c) (Cartesian.product b d) (product_map f g). Proof. ir. uhg. ee. uf product_map. ap Function.create_axioms. uf product_map. rw create_domain. uh H; uh H0; ee. rw H3; rww H1. uf product_map. rw create_range. uhg; ir. rwi Image.inc_rw H1. nin H1. ee. cp (product_pr H1). ee. assert (inc (V (pr1 x0) f) (range f)). rw range_inc_rw. sh (pr1 x0). ee. am. tv. uh H; ee; am. assert (inc (V (pr2 x0) g) (range g)). rw range_inc_rw. sh (pr2 x0). ee. am. tv. uh H0; ee; am. ap product_inc. wr H2. ap pair_is_pair. wr H2. rw pr1_pair. uh H; ee. app H9. wr H2. rw pr2_pair. uh H0; ee. app H9. Qed. Lemma product_map_injective : forall a b c d f g, Map.injective a b f -> Map.injective c d g -> Map.injective (Cartesian.product a c) (Cartesian.product b d) (product_map f g). Proof. ir. uhg. ee. ap product_map_axioms. uh H; ee; am. uh H0; ee; am. uhg. ir. ufi product_map H3. rwi create_V_rewrite H3. rwi create_V_rewrite H3. cp (product_pr H1). cp (product_pr H2). ee. assert (V (pr1 x) f = V (pr1 y) f). transitivity (pr1 (pair (V (pr1 x) f) (V (pr2 x) g))). rww pr1_pair. rw H3. rww pr1_pair. assert (V (pr2 x) g = V (pr2 y) g). transitivity (pr2 (pair (V (pr1 x) f) (V (pr2 x) g))). rww pr2_pair. rw H3. rww pr2_pair. apply pair_extensionality. am. am. uh H; ee. uh H12; ee. ap H12. am. am. am. uh H0; ee. uh H12; ee. ap H12. am. am. am. uh H; uh H0; ee. uh H; uh H0; ee. rw H8; rww H6. uh H; uh H0; ee. uh H; uh H0; ee. rw H8; rww H6. Qed. Lemma product_map_surjective : forall a b c d f g, Map.surjective a b f -> Map.surjective c d g -> Map.surjective (Cartesian.product a c) (Cartesian.product b d) (product_map f g). Proof. ir. uhg; ee. ap product_map_axioms. uh H; ee; am. uh H0; ee; am. uhg. ir. uh H; uh H0; ee. uh H3; uh H2. cp (product_pr H1). ee. cp (H3 _ H5). cp (H2 _ H6). nin H7; nin H8; ee. sh (pair x0 x1). ee. ap product_pair_inc. am. am. uf product_map. rw create_V_rewrite. rw pr1_pair. rw pr2_pair. rw H10. rw H9. rwi is_pair_rw H4. sy; am. ap product_pair_inc. uh H; ee. rww H11. uh H0; ee. rww H11. Qed. Lemma cartesian_product_isomorphic : forall a b c d, are_isomorphic a b -> are_isomorphic c d -> are_isomorphic (Cartesian.product a c) (Cartesian.product b d). Proof. ir. uh H; uh H0; nin H; nin H0. uh H; uh H0; ee. uhg. sh (product_map x x0). uhg; ee. app product_map_axioms. app product_map_surjective. app product_map_injective. Qed. Lemma inc_product : forall x y z, inc x (product y z) = (is_pair x & inc (pr1 x) y & inc (pr2 x) z). Proof. ir. ap iff_eq; ir. cp (product_pr H). am. ap product_inc; ee; am. Qed. Lemma product_tack_on : forall a b x, product a (tack_on b x) = union2 (product a b) (product a (singleton x)). Proof. ir. ap extensionality; uhg; ir. rw inc_union2_rw. rwi inc_product H. ee. rwi tack_on_inc H1. nin H1. ap or_introl. rw inc_product. ee; try am. ap or_intror. rw inc_product. ee; try am. rw H1. ap singleton_inc. rwi inc_union2_rw H. nin H. rwi inc_product H; ee. rw inc_product; ee; try am. rw tack_on_inc. app or_introl. rwi inc_product H; ee. rw inc_product; ee; try am. rw tack_on_inc. ap or_intror. cp (singleton_eq H1). am. Qed. End ProductMap. Module Infinite. Export ProductMap. Export Cardinal. Export Naturals. Export Iterate. (** First we go back to the next things we wanted to prove in cardinal. **) Lemma is_infinite_rw1 : forall x, is_infinite x = (exists f, Transformation.injective x x f & ~(Transformation.surjective x x f)). Proof. ir. ap iff_eq; ir. uh H; ee. ap excluded_middle. uhg; ir. ap H. uhg. ir. ap excluded_middle. uhg; ir. ap H0. sh f. ee. am. uhg; ir. ap H2. uhg; ee. uh H1; ee; am. am. am. nin H. ee. uhg. uhg; ir. uh H1; ee. cp (H1 x0 H). ap H0. uh H2; ee; am. Qed. Lemma is_infinite_rw : forall x, is_infinite x = (exists f, exists u, (inc u x & Transformation.injective x x f & (forall v, inc v x -> ~ (f v = u)))). Proof. ir. ap iff_eq; ir. rwi is_infinite_rw1 H. nin H; ee. sh x0. ap excluded_middle. uhg; ir. ap H0. uhg; ee. uh H; ee; am. uhg. ir. ap excluded_middle. uhg; ir. ap H1. sh x1; ee. am. am. ir. uhg; ir. ap H3. sh v; ee. am. am. rw is_infinite_rw1. nin H. nin H. sh x0. ee. am. uhg; ir. uh H1; ee. uh H2; ee. uh H3. cp (H3 x1 H). nin H4. ee. apply H1 with x2. am. am. Qed. Lemma infinite_sub_infinite : forall x, (exists y, (is_infinite y & sub y x)) -> is_infinite x. Proof. ir. nin H. ee. rwi is_infinite_rw H. nin H. nin H. ee. set (g:= fun (y:E) => Y (inc y x0) (x1 y) y). assert (forall y, inc y x0 -> g y = x1 y). ir. uf g. rw Y_if_rw. tv. am. assert (forall y, ~inc y x0 -> g y = y). ir. uf g. rw Y_if_not_rw. tv. am. assert (forall y, inc y x -> inc (g y) x). ir. apply by_cases with (inc y x0); ir. rw H3. ap H0. uh H1; ee. uh H1. app H1. am. rw H4. am. am. assert (Transformation.injective x x g). uhg; ee. uhg. am. uhg. ir. apply by_cases with (inc x3 x0); ir. apply by_cases with (inc y x0); ir. rwi H3 H8. rwi H3 H8. uh H1; ee. uh H11. ap H11. am. am. am. am. am. rwi H3 H8. rwi H4 H8. assert False. ap H10. wr H8. uh H1; ee. uh H1. ap H1. am. elim H11. am. am. apply by_cases with (inc y x0); ir. assert False. ap H9. rwi H4 H8. rwi H3 H8. rw H8. uh H1; ee. uh H1; ap H1. am. am. am. elim H11. rwi H4 H8. rwi H4 H8. am. am. am. assert (forall v, inc v x -> g v <> x2). ir. apply by_cases with (inc v x0); ir. rw H3. app H2. am. rw H4. uhg; ir. ap H8. rww H9. am. rw is_infinite_rw. sh g. sh x2. ee. app H0. am. am. Qed. Lemma is_finite_natural : forall x, inc x nat -> is_finite x. Proof. ir. set (i:= B H). cp (B_eq H). fold i in H0. wr H0. clear H0. nin i. rw nat_zero_emptyset. ap finite_emptyset. rw nat_succ_tack_on. ap finite_tack_on. am. Qed. Lemma is_infinite_nat : is_infinite nat. Proof. rw is_infinite_rw. sh (fun x => tack_on x x). sh emptyset. ee. wr nat_zero_emptyset. ap R_inc. uhg; ee. uhg. ir. cp (B_eq H). wr H0. wr nat_succ_tack_on. ap R_inc. uhg; ir. cp (B_eq H). cp (B_eq H0). set (i:= B H). fold i in H2. set (j:= B H0). fold j in H3. wri H2 H1. wri H3 H1. wr H2; wr H3. wri nat_succ_tack_on H1. wri nat_succ_tack_on H1. assert (S i = S j). ap R_inj. am. assert (i = j). om. rww H5. ir. cp (B_eq H). set (i:= B H). fold i in H0. wr H0. wr nat_succ_tack_on. uhg; ir. wri nat_zero_emptyset H1. assert (S i = 0). app R_inj. discriminate. Qed. Lemma is_finite_cardinality : forall x, is_finite (cardinality x) = is_finite x. Proof. ir. ap iff_eq; ir. ap finite_invariant. sh (cardinality x). ee. ap are_isomorphic_symm. ap card_isomorphic. am. ap finite_invariant. sh x. ee. ap card_isomorphic. am. Qed. Lemma is_infinite_cardinality : forall x, is_infinite (cardinality x) = is_infinite x. Proof. ir. uf is_infinite. rw is_finite_cardinality. tv. Qed. (** We have to do the following to manipulate nat as an element of E because actually it is of type Set; whenever it appears in one of our formulae it gets pushed up into E but if it stands alone we should write natE e.g. in the assertion [natE = union nat]. **) Definition natE : E. exact nat. Defined. Lemma is_ordinal_nat : is_ordinal nat. Proof. change (is_ordinal natE). assert (natE = union nat). ap extensionality; uhg; ir. cp (B_eq H). set (i:= B H). fold i in H0. apply union_inc with (tack_on x x). rw tack_on_inc. ap or_intror; tv. wr H0. wr nat_succ_tack_on. ap R_inc. cp (union_exists H). nin H0. ee. assert (sub x0 nat). cp (B_eq H1). wr H2. ap Naturals.sub_R_nat. ap H2. am. rw H. ap ordinal_union. ir. cp (B_eq H0). wr H1. ap Naturals.nat_ordinal. Qed. Lemma inc_cardinality_nat_or_sub_nat_cardinality : forall x, (inc (cardinality x) nat) \/ (sub nat (cardinality x)). Proof. ir. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (is_ordinal_nat). cp (ordinal_lt_lt_eq_or H H0). nin H1. rwi ordinal_lt_rw H1. ee. ap or_introl; am. nin H1. ap or_intror. assert (ordinal_leq nat (cardinality x)). rw ordinal_leq_inc_tack_on. rw tack_on_inc. ap or_introl. rwi ordinal_lt_rw H1. ee. am. am. uh H2; ee. am. ap or_intror. rw H1. uhg; ir. am. Qed. Lemma is_finite_inc_cardinality_nat : forall x, is_finite x = inc (cardinality x) nat. Proof. ir. wr is_finite_cardinality. ap iff_eq; ir. cp (inc_cardinality_nat_or_sub_nat_cardinality x). nin H0. am. assert (is_infinite (cardinality x)). ap infinite_sub_infinite. sh natE. ee. ap is_infinite_nat. am. uh H1. assert False. app H1. elim H2. app is_finite_natural. Qed. Lemma is_infinite_sub_nat_cardinality : forall x, is_infinite x = sub nat (cardinality x). Proof. ir. uf is_infinite. rw is_finite_inc_cardinality_nat. ap iff_eq; ir. cp (inc_cardinality_nat_or_sub_nat_cardinality x). nin H0. assert False. app H. elim H1. am. uhg; ir. assert (inc (cardinality x) (cardinality x)). ap H. am. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (ordinal_not_inc_itself H2). app H3. Qed. Definition plus_one x := tack_on x x. Lemma is_ordinal_plus_one : forall x, is_ordinal x -> is_ordinal (plus_one x). Proof. ir. uf plus_one. ap ordinal_tack_on. am. Qed. Lemma plus_one_R : forall (i:nat), plus_one (R i) = R (i+1). Proof. ir. uf plus_one. wr nat_succ_tack_on. assert (S i = i+1). om. rww H. Qed. Lemma inc_plus_one_nat : forall x, inc x nat -> inc (plus_one x) nat. Proof. ir. cp (B_eq H). wr H0. rw plus_one_R. ap R_inc. Qed. Lemma function_V_tack_on_old : forall f x y z, Function.axioms f -> ~inc x (domain f) -> inc z (domain f) -> V z (tack_on f (pair x y)) = V z f. Proof. ir. sy. ap function_sub_V. ap function_tack_on_axioms. am. am. uhg. ee. am. am. uhg; ir. rw tack_on_inc. app or_introl. Qed. Lemma function_V_tack_on_new : forall f x y z, Function.axioms f -> ~inc x (domain f) -> z = x -> V z (tack_on f (pair x y)) = y. Proof. ir. util (pr2_V (f:=tack_on f (pair x y)) (x:=pair x y)). app function_tack_on_axioms. rw tack_on_inc. app or_intror. rwi pr1_pair H2. rwi pr2_pair H2. sy; rww H1. Qed. Lemma are_isomorphic_tack_on : forall x y u v, ~inc y x -> ~inc v u -> are_isomorphic x u -> are_isomorphic (tack_on x y) (tack_on u v). Proof. ir. uh H1. nin H1. uhg. sh (tack_on x0 (pair y v)). uh H1; ee. uh H1. uh H2. uh H3. ee. uh H5. uh H4. uhg. dj. uhg; ee. ap function_tack_on_axioms. am. rww H6. rw domain_tack_on. rww H6. rw range_tack_on. uhg; ir. rwi tack_on_inc H8. nin H8. rw tack_on_inc. ap or_introl. app H7. rw H8. rw tack_on_inc; app or_intror. uhg. ee. am. uhg. ir. rwi tack_on_inc H9. nin H9. cp (H5 x1 H9). nin H10. ee. sh x2. ee. rw tack_on_inc. app or_introl. rw function_V_tack_on_old. am. am. rww H6. rww H6. sh y. ee. rw tack_on_inc. app or_intror. rw function_V_tack_on_new. sy; am. am. rww H6. tv. uhg; ee. am. uhg. ir. rwi tack_on_inc H10; rwi tack_on_inc H11. nin H10; nin H11. ap H4. am. am. rwi function_V_tack_on_old H12. rwi function_V_tack_on_old H12. am. am. rww H6. rww H6. am. rww H6. rww H6. rwi function_V_tack_on_old H12. rwi function_V_tack_on_new H12. assert False. ap H0. ap H7. wr H12. ap range_inc. am. sh x1. ee. rww H6. tv. elim H13. am. rww H6. am. am. rww H6. rww H6. rwi function_V_tack_on_new H12. rwi function_V_tack_on_old H12. assert False. ap H0. ap H7. rw H12. ap range_inc. am. sh y0. ee. rww H6. tv. elim H13. am. rww H6. rww H6. am. rww H6. am. rww H11. Qed. Lemma nat_are_isomorphic_eq : forall x y, inc x nat -> inc y nat -> are_isomorphic x y -> x = y. Proof. assert (forall (i j:nat), i < j -> ~(are_isomorphic (R i) (R j))). ir. uhg; ir. assert (are_isomorphic (R j) (R i)). app are_isomorphic_symm. set (g:= isotrans (R j) (R i)). assert (is_infinite (R j)). rw is_infinite_rw. sh g. sh (R (j-1)). ee. ap Naturals.lt_implies_inc. om. uf g. assert (Transformation.bijective (R j) (R i) (isotrans (R j) (R i))). ap isotrans_bij. am. uhg; ee. uhg. ir. uh H2; ee. uh H2. assert (inc (isotrans (R j) (R i) x) (R i)). ap H2. am. assert (sub (R i) (R j)). ap Naturals.le_implies_sub. om. app H7. uhg. ir. uh H2; ee. uh H7; ee. uh H8; ee. ap H8. am. am. am. ir. assert (inc (g v) (R i)). assert (Transformation.bijective (R j) (R i) (isotrans (R j) (R i))). ap isotrans_bij. am. uf g. uh H3; ee. uh H3; ee. ap H3. am. uhg; ir. rwi H4 H3. rwi Naturals.inc_lt H3. om. uh H2. ap H2. ap is_finite_natural. ap R_inc. ir. cp (B_eq H0); cp (B_eq H1). set (i:= B H0); set (j:= B H1). fold i in H3; fold j in H4. wr H3; wr H4. assert (~ i < j). uhg; ir. cp (H _ _ H5). ap H6. rw H3; rww H4. assert (~ j < i). uhg; ir. cp (H _ _ H6). ap H7. ap are_isomorphic_symm. rw H3; rww H4. assert (i = j). om. rww H7. Qed. Lemma nat_cardinality_refl : forall x, inc x nat -> cardinality x = x. Proof. ir. ap nat_are_isomorphic_eq. wr is_finite_inc_cardinality_nat. ap is_finite_natural. am. am. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma cardinality_tack_on : forall x y, is_finite x -> ~inc y x -> cardinality (tack_on x y) = plus_one (cardinality x). Proof. ir. uf plus_one. ap nat_are_isomorphic_eq. wr is_finite_inc_cardinality_nat. ap finite_tack_on. am. assert (inc (cardinality x) nat). wr is_finite_inc_cardinality_nat. am. cp (B_eq H1). wr H2. wr nat_succ_tack_on. ap R_inc. ap are_isomorphic_trans. sh (tack_on x y). ee. ap are_isomorphic_symm. ap card_isomorphic. ap are_isomorphic_tack_on. am. ap ordinal_not_inc_itself. ap cardinality_ordinal. ap card_isomorphic. Qed. Definition number x := Bnat (cardinality x). Lemma R_number : forall x, is_finite x -> R (number x) = cardinality x. Proof. ir. rwi is_finite_inc_cardinality_nat H. uf number. rw R_Bnat. tv. am. Qed. Lemma cardinality_emptyset : cardinality emptyset = emptyset. Proof. ap extensionality; uhg; ir. assert (are_isomorphic emptyset (cardinality emptyset)). ap card_isomorphic. uh H0; ee. nin H0. uh H0; ee. uh H1; ee. uh H3. cp (H3 x H). nin H4. ee. nin H4. elim x2. nin H. elim x0. Qed. Lemma number_emptyset : forall x, x = emptyset -> number x = 0. Proof. ir. ap R_inj. rw nat_zero_emptyset. rw R_number. rw H. rww cardinality_emptyset. rw H. ap finite_emptyset. Qed. Lemma number_tack_on : forall x y, is_finite x -> ~inc y x -> number (tack_on x y) = (number x) + 1. Proof. ir. uf number. transitivity (S (Bnat (cardinality x))). rw cardinality_tack_on. ap R_inj. rw R_Bnat. rw nat_succ_tack_on. rw R_Bnat. tv. wr is_finite_inc_cardinality_nat. am. ap inc_plus_one_nat. wrr is_finite_inc_cardinality_nat. am. am. om. Qed. Definition take_out x y := complement x (singleton y). Lemma inc_take_out : forall x y z, inc z (take_out x y) = (inc z x & ~z=y). Proof. ir. uf take_out. rw inc_complement. ap iff_eq; ir. ee. am. uhg; ir. ap H0. rw H1. ap singleton_inc. ee. am. uhg; ir. ap H0. ap singleton_eq. am. Qed. Lemma tack_on_take_out : forall x y, inc y x -> tack_on (take_out x y) y = x. Proof. ir. ap extensionality; uhg; ir. rwi tack_on_inc H0. nin H0. rwi inc_take_out H0. ee. am. rww H0. rw tack_on_inc. apply by_cases with (x0 = y). ir. app or_intror. ir. ap or_introl. rww inc_take_out. ee; am. Qed. Lemma not_inc_take_out : forall x y, ~inc y (take_out x y). Proof. ir. uhg; ir. rwi inc_take_out H. ee. ap H0. tv. Qed. Lemma subset_finite : forall x, (exists y, (sub x y & is_finite y)) -> is_finite x. Proof. ir. nin H. ee. apply excluded_middle. uhg; ir. assert (is_infinite x0). apply infinite_sub_infinite. sh x. ee. am. am. uh H2; au. Qed. Lemma is_finite_take_out : forall x y, is_finite x -> is_finite (take_out x y). Proof. ir. ap subset_finite. sh x. ee. uhg; ir. rwi inc_take_out H0; ee. am. am. Qed. Lemma number_take_out : forall x y, is_finite x -> inc y x -> number (take_out x y) = (number x) -1. Proof. ir. cp (tack_on_take_out H0). transitivity (number (tack_on (take_out x y) y) - 1). rw number_tack_on. om. ap is_finite_take_out. am. ap not_inc_take_out. rww H1. Qed. Lemma number_zero_emptyset : forall x, is_finite x -> number x = 0 -> x = emptyset. Proof. ir. ap extensionality; uhg; ir. cp (tack_on_take_out H1). wri H2 H0. rwi number_tack_on H0. assert False. om. elim H3. app is_finite_take_out. ap not_inc_take_out. nin H1. nin x1. Qed. Lemma number_gt_zero_nonempty : forall x, is_finite x -> number x > 0 -> (exists y, inc y x). Proof. ir. ap excluded_middle; uhg; ir. assert (x = emptyset). ap extensionality; uhg; ir. assert False. ap H1. sh x0. am. elim H3. nin H2. nin x1. rwi H2 H0. rwi number_emptyset H0. om. tv. Qed. Lemma finite_induction: forall (p:EP) x, (p emptyset) -> (forall y z, p y -> p (tack_on y z)) -> is_finite x -> p x. Proof. ir. assert (forall n, (forall y, is_finite y -> number y = n -> p y)). intro n. nin n; ir. cp (number_zero_emptyset H2 H3). rww H4. assert (number y > 0). om. cp (number_gt_zero_nonempty H2 H4). nin H5. cp (tack_on_take_out H5). wr H6. ap H0. ap IHn. ap is_finite_take_out. am. rw number_take_out. rw H3. om. am. am. apply H2 with (number x). am. tv. Qed. Lemma image_create_tack_on : forall x y f, Image.create (tack_on x y) f = tack_on (Image.create x f) (f y). Proof. ir. ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. rwi tack_on_inc H. rw tack_on_inc. nin H. ap or_introl. rw Image.inc_rw. sh x1. ee; try am. ap or_intror. wrr H. sy; am. rwi tack_on_inc H. rw Image.inc_rw. nin H. rwi Image.inc_rw H. nin H. ee. sh x1. ee. rw tack_on_inc. app or_introl. am. sh y. ee. rw tack_on_inc. app or_intror. sy; am. Qed. Lemma image_create_emptyset : forall f, Image.create emptyset f = emptyset. Proof. ir. ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. nin H. nin x1. nin H. nin x0. Qed. Lemma image_finite : forall x f, is_finite x -> is_finite (Image.create x f). Proof. ir. apply finite_induction with (p:= fun y=> is_finite (Image.create y f)). rw image_create_emptyset. ap finite_emptyset. ir. rw image_create_tack_on. ap finite_tack_on. am. am. Qed. (** We do some additional things about infinite cardinals. These eventually should be put back into Cardinal when we do a backward-revamp. **) (** We would like to show that if [a] is an infinite cardinal then the disjoint union of [a] with itself, and the product of [a] with itself, have the same cardinality as [a]. The idea of the proof is to look at [op_triangle a] which is the set of pairs (x,y) of elements of [a] with [ordinal_leq y x]. Up to a [union2] this is basically the same as [product a a]. The [op_triangle a] is well-ordered by [op_lex] the lexicographic ordering on ordinal pairs (i.e. pairs of ordinals). If [a] is a cardinal then all downward subsets of [op_triangle a] have cardinality strictly smaller than that of [a], using the induction hypothesis; this allows us to conclude that [op_triangle a] has cardinality less than or equal to that of [a]. Along the way we use this fact to obtain the statement that [union2] doesn't increase cardinality; then we can use that to go from [op_triangle a] to [product a a] obtaining the induction step. **) Definition is_ordinal_pair x := is_pair x & is_ordinal (pr1 x) & is_ordinal (pr2 x). Definition op_lex_lt x y := is_ordinal_pair x & is_ordinal_pair y & (ordinal_lt (pr1 x) (pr1 y) \/ (pr1 x = pr1 y & ordinal_lt (pr2 x) (pr2 y))). Definition op_lex_leq x y := is_ordinal_pair x & is_ordinal_pair y & (ordinal_lt (pr1 x) (pr1 y) \/ (pr1 x = pr1 y & ordinal_leq (pr2 x) (pr2 y))). Lemma ordinal_leq_refl : forall x, is_ordinal x -> ordinal_leq x x. Proof. ir. uhg; ee. am. am. uhg; ir; am. Qed. Lemma ordinal_lt_leq : forall x y, ordinal_lt x y -> ordinal_leq x y. Proof. ir. uh H; ee; am. Qed. Lemma ordinal_leq_rw : forall x y, ordinal_leq x y = (ordinal_lt x y \/ (x = y & is_ordinal x)). Proof. ir. ap iff_eq; ir. cp (ordinal_if_leq_or H). nin H0. app or_introl. ap or_intror. ee. am. uh H; ee. am. nin H. uh H; ee. am. ee. wr H. ap ordinal_leq_refl. am. Qed. Lemma op_lex_lt_leq : forall x y, op_lex_lt x y -> op_lex_leq x y. Proof. ir. uh H; ee. uhg; ee. am. am. nin H1. app or_introl. ap or_intror. ee. am. ap ordinal_lt_leq. am. Qed. Lemma op_lex_leq_refl : forall x, is_ordinal_pair x -> op_lex_leq x x. Proof. ir. uhg; ee; try am. ap or_intror. ee. tv. ap ordinal_leq_refl. uh H; ee. am. Qed. Lemma op_lex_leq_rw : forall x y, op_lex_leq x y = (op_lex_lt x y \/ (x = y & is_ordinal_pair x)). Proof. ir. ap iff_eq; ir. uh H; ee. nin H1. ap or_introl. uhg; ee; try am. ap or_introl. am. ee. rwi ordinal_leq_rw H2. nin H2. ap or_introl. uhg; ee. am. am. ap or_intror. ee. am. am. ap or_intror. ee. uh H. uh H0. ap pair_extensionality. ee; am. ee; am. am. am. am. nin H. ap op_lex_lt_leq. am. ee. wr H. ap op_lex_leq_refl. am. Qed. Lemma not_ordinal_lt_refl : forall x, ~(ordinal_lt x x). Proof. ir. uhg; ir. uh H; ee. ap H0. tv. Qed. Lemma not_op_lex_lt_refl : forall x, ~ (op_lex_lt x x). Proof. ir. uhg; ir. uh H; ee. nin H1. ap (not_ordinal_lt_refl H1). ee. ap (not_ordinal_lt_refl H2). Qed. Lemma ordinal_lt_trans : forall x z, (exists y, (ordinal_lt x y & ordinal_lt y z)) -> ordinal_lt x z. Proof. ir. nin H. ee. uh H; uh H0; uhg. ee. ap ordinal_leq_trans. sh x0; ee; am. uhg; ir. wri H3 H0. cp (ordinal_leq_leq_eq H H0). ap H2. am. Qed. Lemma op_lex_lt_trans : forall x z, (exists y, (op_lex_lt x y & op_lex_lt y z)) -> op_lex_lt x z. Proof. ir. nin H. ee. uh H; uh H0; uhg; ee; try am. nin H4. nin H2. ap or_introl. ap ordinal_lt_trans. sh (pr1 x0). ee; am. ee. ap or_introl. wrr H2. nin H2. ap or_introl. ee. rww H4. ap or_intror; ee. wrr H2. ap ordinal_lt_trans. sh (pr2 x0); ee; am. Qed. Lemma op_lex_leq_trans : forall x z, (exists y, (op_lex_leq x y & op_lex_leq y z)) -> op_lex_leq x z. Proof. ir. nin H. ee. rwi op_lex_leq_rw H. rwi op_lex_leq_rw H0. nin H. nin H0. ap op_lex_lt_leq. ap op_lex_lt_trans. sh x0; ee; am. ee. wr H0. ap op_lex_lt_leq. am. nin H0. ee. rww H. app op_lex_lt_leq. ee. rw op_lex_leq_rw. ap or_intror. ee. rww H. am. Qed. Lemma not_ordinal_lt_lt : forall x y, ordinal_lt x y -> ordinal_lt y x -> False. Proof. ir. uh H; uh H0; ee. cp (ordinal_leq_leq_eq H H0). au. Qed. Lemma not_op_lex_lt_lt : forall x y, op_lex_lt x y -> op_lex_lt y x -> False. Proof. ir. uh H; uh H0; ee. nin H4; nin H2. apply not_ordinal_lt_lt with (pr1 x) (pr1 y). am. am. ee. rwi H2 H4. cp (not_ordinal_lt_refl H4). am. ee. rwi H4 H2. cp (not_ordinal_lt_refl H2). am. ee. apply not_ordinal_lt_lt with (pr2 x) (pr2 y). am. am. Qed. Lemma op_lex_leq_leq_eq : forall x y, op_lex_leq x y -> op_lex_leq y x -> x = y. Proof. ir. rwi op_lex_leq_rw H. rwi op_lex_leq_rw H0. nin H; nin H0. cp (not_op_lex_lt_lt H H0). elim H1. ee. sy; am. ee. am. ee. am. Qed. Lemma op_lex_dichotomy : forall x y, is_ordinal_pair x -> is_ordinal_pair y -> (op_lex_lt x y \/ op_lex_lt y x \/ x = y). Proof. ir. cp H; cp H0. uh H1; uh H2; ee. cp (ordinal_lt_lt_eq_or H5 H3). nin H7. ap or_introl. uhg; ee. am. am. app or_introl. nin H7. ap or_intror. ap or_introl. uhg; ee; try am. app or_introl. cp (ordinal_lt_lt_eq_or H6 H4). nin H8. ap or_introl. uhg; ee; try am. ap or_intror; ee. am. am. nin H8. ap or_intror. ap or_introl. uhg; ee; try am. ap or_intror; ee; try am. sy; am. ap or_intror. ap or_intror. app pair_extensionality. Qed. Definition least_ordinal z := sow (fun x => inc x z). Lemma is_ordinal_least_ordinal: forall z, is_ordinal (least_ordinal z). Proof. ir. uf least_ordinal. ap sow_ordinal. Qed. Lemma inc_least_ordinal_ex : forall z, (exists y, (inc y z & is_ordinal y)) -> inc (least_ordinal z) z. Proof. ir. uf least_ordinal. ap sow_property. nin H. ee. sh x; ee; am. Qed. Definition set_of_ordinals z := (forall y, inc y z -> is_ordinal y). Lemma inc_least_ordinal : forall z, set_of_ordinals z -> nonempty z -> inc (least_ordinal z) z. Proof. ir. ap inc_least_ordinal_ex. nin H0. sh y. ee. am. uh H; au. Qed. Lemma ordinal_leq_least_ordinal : forall y z, inc y z -> is_ordinal y -> ordinal_leq (least_ordinal z) y. Proof. ir. uf least_ordinal. ap sow_smallest. am. am. Qed. Definition set_of_ordinal_pairs z := (forall y, inc y z -> is_ordinal_pair y). Lemma set_of_ordinal_pairs_relation : forall z, set_of_ordinal_pairs z -> is_relation z. Proof. ir. uhg; ee. ir. uh H; ee. cp (H _ H0). uh H1; ee; am. Qed. Lemma set_of_ordinals_domain : forall z, set_of_ordinal_pairs z -> set_of_ordinals (domain z). Proof. ir. uhg; ee. ir. ufi domain H0. rwi Image.inc_rw H0. nin H0. ee. uh H. cp (H _ H0). uh H2. ee. wrr H1. Qed. Definition column z x:= range (Z z (fun y => pr1 y = x)). Lemma inc_column : forall z x y, is_relation z -> inc y (column z x) = inc (pair x y) z. Proof. ir. uf column. uf range. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. Ztac. uh H; ee. cp (H _ H2). rwi is_pair_rw H4. rwi H1 H4. rwi H3 H4. wrr H4. sh (pair x y). ee. Ztac. rww pr1_pair. rww pr2_pair. Qed. Lemma set_of_ordinals_column : forall z x, set_of_ordinal_pairs z -> set_of_ordinals (column z x). Proof. ir. uhg. ir. rwi inc_column H0. uh H; ee. cp (H _ H0). uh H1; ee. rwi pr2_pair H3. am. ap set_of_ordinal_pairs_relation. am. Qed. Lemma nonempty_domain : forall z, nonempty z -> nonempty (domain z). Proof. ir. nin H. sh (pr1 y). uf domain. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma nonempty_column : forall z x, is_relation z -> inc x (domain z) -> nonempty (column z x). Proof. ir. ufi domain H0. rwi Image.inc_rw H0. nin H0. ee. sh (pr2 x0). uf column. uf range. rw Image.inc_rw. sh x0. ee. Ztac. tv. Qed. Definition op_lex_least z := pair (least_ordinal (domain z)) (least_ordinal (column z (least_ordinal (domain z)))). Lemma is_ordinal_pair_op_lex_least : forall z, is_ordinal_pair (op_lex_least z). Proof. ir. uhg; ee. uf op_lex_least. ap pair_is_pair. uf op_lex_least. rw pr1_pair. ap is_ordinal_least_ordinal. uf op_lex_least. rw pr2_pair. ap is_ordinal_least_ordinal. Qed. Lemma inc_op_lex_least : forall z, set_of_ordinal_pairs z -> nonempty z -> inc (op_lex_least z) z. Proof. ir. uf op_lex_least. set (k:= least_ordinal (domain z)). assert (is_relation z). app set_of_ordinal_pairs_relation. assert (inc k (domain z)). uf k. ap inc_least_ordinal. app set_of_ordinals_domain. app nonempty_domain. wr inc_column. ap inc_least_ordinal. app set_of_ordinals_column. app nonempty_column. am. Qed. Lemma pr1_op_lex_least : forall z, pr1 (op_lex_least z) = least_ordinal (domain z). Proof. ir. uf op_lex_least. rww pr1_pair. Qed. Lemma pr2_op_lex_least : forall z, pr2 (op_lex_least z) = least_ordinal (column z (least_ordinal (domain z))). Proof. ir. uf op_lex_least. rww pr2_pair. Qed. Lemma op_lex_leq_op_lex_least : forall z y, set_of_ordinal_pairs z -> inc y z -> op_lex_leq (op_lex_least z) y. Proof. ir. assert (nonempty z). sh y. am. assert (is_ordinal_pair (op_lex_least z)). ap is_ordinal_pair_op_lex_least. assert (is_ordinal_pair y). uh H; au. uhg; ee; try am. assert (inc (pr1 y) (domain z)). uf domain. rw Image.inc_rw. sh y. ee; try am; try tv. assert (ordinal_leq (least_ordinal (domain z)) (pr1 y)). ap ordinal_leq_least_ordinal. am. assert (set_of_ordinals (domain z)). app set_of_ordinals_domain. uh H5; au. apply by_cases with (pr1 y = least_ordinal (domain z)); ir. ap or_intror. ee. sy. rww pr1_op_lex_least. assert (inc (pr2 y) (column z (least_ordinal (domain z)))). wr H6. rw inc_column. uh H3; ee. rwi is_pair_rw H3. wr H3. am. app set_of_ordinal_pairs_relation. rw pr2_op_lex_least. ap ordinal_leq_least_ordinal. am. uh H3; ee; am. ap or_introl. uhg; ee. rww pr1_op_lex_least. rw pr1_op_lex_least. uhg; ir. ap H6. sy; am. Qed. (** With the above lemma we have basically finished showing that any set of ordinal pairs is well-ordered by the relation op_lex_leq. However we need to put this into the notation of well-ordered sets. **) Definition op_lex z := Order_notation.create z op_lex_leq. Lemma U_op_lex : forall z, U (op_lex z) = z. Proof. ir. uf op_lex. rw underlying_create; tv. Qed. Lemma leq_op_lex : forall z u v:E, leq (op_lex z) u v = (inc u z & inc v z & op_lex_leq u v). Proof. ir. uf op_lex; rw leq_create_all. tv. Qed. Lemma op_lex_axioms : forall z:E, set_of_ordinal_pairs z -> Order.Definitions.axioms (op_lex z). Proof. ir. uf op_lex. ap Order.Definitions.create_axioms. uf property; dj. ap op_lex_leq_refl. uh H; ee; au. ap op_lex_leq_leq_eq. am. am. ap op_lex_leq_trans. sh y. ee. am. am. Qed. Lemma is_linear_op_lex : forall z:E, set_of_ordinal_pairs z -> is_linear (op_lex z). Proof. ir. uhg; ee. app op_lex_axioms. ir. rwi U_op_lex H0. rwi U_op_lex H1. uh H; ee. cp (H _ H0). cp (H _ H1). cp (op_lex_dichotomy H2 H3). nin H4. ap or_introl. rw leq_op_lex. ee; try am. app op_lex_lt_leq. nin H4. ap or_intror. rw leq_op_lex. ee; try am. app op_lex_lt_leq. ap or_introl. wr H4. rw leq_op_lex. ee; try am. app op_lex_leq_refl. Qed. Lemma is_well_ordered_op_lex : forall z, set_of_ordinal_pairs z -> is_well_ordered (op_lex z). Proof. ir. uhg; ee. app is_linear_op_lex. ir. rwi U_op_lex H0. assert (set_of_ordinal_pairs b). uhg; ir. uh H; ap H. app H0. sh (op_lex_least b). uhg; ee. uhg; ee. app op_lex_axioms. rww U_op_lex. rw U_op_lex. ap H0. ap inc_op_lex_least. am. am. ir. rw leq_op_lex. ee. ap H0. app inc_op_lex_least. app H0. app op_lex_leq_op_lex_least. app inc_op_lex_least. Qed. Definition prod_reflexive z := are_isomorphic z (Cartesian.product z z). Lemma prod_reflexive_invariant : forall y z, are_isomorphic y z -> prod_reflexive y -> prod_reflexive z. Proof. ir. uh H0. uhg. assert (are_isomorphic (product y y) (product z z)). app cartesian_product_isomorphic. ap are_isomorphic_trans. sh (product y y). ee. ap are_isomorphic_trans. sh y. ee. app are_isomorphic_symm. am. am. Qed. Definition sub_prod_reflexive z := forall y, sub y z -> is_infinite y -> prod_reflexive y. Lemma sub_prod_reflexive_rw : forall z, sub_prod_reflexive z = (forall y, iso_sub y z -> is_infinite y -> prod_reflexive y). Proof. ir. ap iff_eq; ir. uh H0. nin H0. ee. apply prod_reflexive_invariant with x. app are_isomorphic_symm. uh H. ap H. am. uhg. uhg; ir. uh H1. ap H1. ap finite_invariant. sh x. ee; try am. app are_isomorphic_symm. uhg. ir. ap H. uhg. sh y. ee. ap are_isomorphic_refl. am. am. Qed. Lemma sub_prod_reflexive_invariant : forall y z, iso_sub y z -> sub_prod_reflexive z -> sub_prod_reflexive y. Proof. ir. uh H0. uhg. ir. assert (iso_sub y0 z). uh H. nin H. ee. uhg. cp (isotrans_bij H). sh (Image.create y0 (isotrans y x)). ee. rw iso_trans_ex_rw. sh (isotrans y x). uhg; dj. uhg. ir. rw Image.inc_rw. sh x0; ee; try am. tv. uhg; ee; try am. uhg; ir. rwi Image.inc_rw H6. nin H6. ee. sh x1; ee. am. am. uhg; ee; try am. uhg; ir. uh H4; ee. uh H11; ee. uh H12. ap H12. ap H1. am. app H1. am. uhg; ir. rwi Image.inc_rw H5. nin H5; ee. wr H6. uh H4; ee. uh H4. assert (inc x1 y). app H1. cp (H4 _ H9). app H3. assert (sub_prod_reflexive z). am. rwi sub_prod_reflexive_rw H4. ap H4. am. am. Qed. Lemma sub_prod_reflexive_prod_reflexive : forall z, is_infinite z -> sub_prod_reflexive z -> prod_reflexive z. Proof. ir. uh H0; ee. ap H0. uhg; ir; am. am. Qed. Lemma finite_sub_prod_reflexive : forall z, is_finite z -> sub_prod_reflexive z. Proof. ir. uhg; ir. assert False. uh H1; ap H1. ap subset_finite. sh z. ee; am. elim H2. Qed. Definition op_triangle z := Z (Cartesian.product z z) (fun y => (ordinal_leq (pr2 y) (pr1 y))). Lemma inc_op_triangle : forall y z, is_ordinal z -> inc y (op_triangle z) = (is_ordinal_pair y & ordinal_lt (pr1 y) z & ordinal_leq (pr2 y) (pr1 y)). Proof. ir. ap iff_eq; ir. ufi op_triangle H0. Ztac. uhg; ee. cp (product_pr H1); ee. am. cp (product_pr H1); ee. apply ordinal_inc_ordinal with z. am. am. cp (product_pr H1); ee. apply ordinal_inc_ordinal with z. am. am. rw ordinal_lt_rw. ee. am. cp (product_pr H1); ee; am. ee. uf op_triangle. Ztac. ap product_inc. uh H0; ee. am. rwi ordinal_lt_rw H1. ee. am. assert (ordinal_lt (pr2 y) z). cp (ordinal_if_leq_or H2). nin H3. ap ordinal_lt_trans. sh (pr1 y). ee; am. rww H3. rwi ordinal_lt_rw H3. ee; am. Qed. Lemma set_of_ordinal_pairs_op_triangle : forall z, is_ordinal z -> set_of_ordinal_pairs (op_triangle z). Proof. ir. uhg. ir. rwi inc_op_triangle H0. ee. am. am. Qed. Lemma iso_sub_op_triangle : forall z, is_ordinal z -> iso_sub z (op_triangle z). Proof. ir. rw iso_sub_trans_rw. sh (fun x => pair x emptyset). uhg; ee. uhg; ir. rw inc_op_triangle. ee. uhg; ee. ap pair_is_pair. rw pr1_pair. apply ordinal_inc_ordinal with z. am. am. rw pr2_pair. ap emptyset_ordinal. rw pr1_pair. rw ordinal_lt_rw. ee; am. rw pr2_pair. rw pr1_pair. uhg; ee. ap emptyset_ordinal. apply ordinal_inc_ordinal with z. am. am. uhg; ir. nin H1. nin x1. am. uhg; ir. transitivity (pr1 (pair x emptyset)). rww pr1_pair. rw H2. rww pr1_pair. Qed. Lemma sub_op_triangle_product : forall z, sub (op_triangle z) (product z z). Proof. ir. uhg; ir. ufi op_triangle H. Ztac. Qed. Lemma same_cardinality_op_triangle : forall z, is_infinite z -> is_ordinal z -> sub_prod_reflexive z -> cardinality (op_triangle z) = cardinality z. Proof. ir. assert (prod_reflexive z). app sub_prod_reflexive_prod_reflexive. uh H2. ap cardinality_invariant. ap bernstein_cantor_schroeder. ap iso_sub_trans. sh (product z z). ee. ap sub_iso_sub. ap sub_op_triangle_product. ap isomorphic_iso_sub. app are_isomorphic_symm. app iso_sub_op_triangle. Qed. Lemma op_triangle_sub : forall y z, sub y z -> sub (op_triangle y) (op_triangle z). Proof. ir. uf op_triangle. uhg; ir. Ztac. assert (inc x (product z z)). rwi inc_product H1; rw inc_product; ee; try am. app H. app H. app Z_inc. Qed. Definition op_triangle_lex z := op_lex (op_triangle z). Lemma U_op_triangle_lex : forall z, U (op_triangle_lex z) = op_triangle z. Proof. ir. uf op_triangle_lex. rww U_op_lex. Qed. Lemma leq_op_triangle_lex : forall z u v, leq (op_triangle_lex z) u v = (inc u (op_triangle z) & inc v (op_triangle z) & op_lex_leq u v). Proof. ir. uf op_triangle_lex. rww leq_op_lex. Qed. Lemma is_well_ordered_op_triangle_lex : forall z, is_ordinal z -> is_well_ordered (op_triangle_lex z). Proof. ir. uf op_triangle_lex. ap is_well_ordered_op_lex. app set_of_ordinal_pairs_op_triangle. Qed. Definition is_cardinal z := cardinality z = z. Lemma is_cardinal_rw : forall z, is_cardinal z = (is_ordinal z & (forall y, ordinal_lt y z -> ordinal_lt (cardinality y) (cardinality z))). Proof. ir. ap iff_eq; ir. ee. uh H. wr H. ap cardinality_ordinal. ir. uh H; ee. ufi cardinality H. assert (ordinal_leq (cardinality y) (cardinality z)). ap sub_cardinal_leq. assert (ordinal_leq y z). rw ordinal_leq_rw. app or_introl. uh H1; ee; am. rwi ordinal_leq_rw H1. nin H1. am. ee. assert (are_isomorphic y z). cp (card_isomorphic y). cp (card_isomorphic z). ap are_isomorphic_trans. sh (cardinality y). ee. am. rw H1. app are_isomorphic_symm. assert (ordinal_leq z y). wr H. ap sow_smallest. rwi ordinal_lt_rw H0. ee. apply ordinal_inc_ordinal with z. am. am. app are_isomorphic_symm. assert (y = z). ap ordinal_leq_leq_eq. ap ordinal_lt_leq. am. am. uh H0. ee. elim (H6 H5). ee. uhg. ap ordinal_leq_leq_eq. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. assert (is_ordinal (cardinality z)). ap cardinality_ordinal. cp (ordinal_leq_leq_or H H1). nin H2. am. rwi ordinal_leq_rw H2. nin H2. cp (H0 _ H2). assert (cardinality (cardinality z) = cardinality z). ap cardinality_invariant. ap are_isomorphic_symm. ap card_isomorphic. rwi H4 H3. uh H3; ee. assert False. app H5. elim H6. ee. rw H2. uhg; ee. am. am. uhg; ir; am. Qed. Lemma is_cardinal_rw2 : forall z, is_cardinal z = (is_ordinal z & (forall y, is_ordinal y -> iso_sub z y -> ordinal_leq z y)). Proof. ir. ap iff_eq; ir. rwi is_cardinal_rw H. ee. am. ir. cp (ordinal_lt_lt_eq_or H H1). nin H3. app ordinal_lt_leq. nin H3. cp (H0 _ H3). assert (cardinality y = cardinality z). ap ordinal_leq_leq_eq. ap ordinal_lt_leq. am. app iso_sub_cardinal_leq. rwi H5 H4. uh H4; ee. assert False. app H6. elim H7. rw H3. uhg; ee. am. am. uhg; ir; am. ee. uhg. ap ordinal_leq_leq_eq. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. ap H0. ap cardinality_ordinal. uhg. sh (cardinality z). ee. ap card_isomorphic. uhg; ir; am. Qed. Lemma is_cardinal_cardinality : forall z, is_cardinal (cardinality z). Proof. ir. rw is_cardinal_rw2. ee. ap cardinality_ordinal. ir. ap ordinal_leq_trans. sh (cardinality y). ee. ap iso_sub_cardinal_leq. ap iso_sub_trans. sh (cardinality z). ee. ap isomorphic_iso_sub. ap card_isomorphic. am. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. Qed. Lemma infinite_cardinality_tack_on : forall x y, is_infinite x -> cardinality (tack_on x y) = cardinality x. Proof. ir. apply by_cases with (inc y x); ir. assert (tack_on x y = x). ap extensionality; uhg; ir. rwi tack_on_inc H1. nin H1. am. rww H1. rw tack_on_inc. ap or_introl. am. rww H1. ap ordinal_leq_leq_eq. ap iso_sub_cardinal_leq. rwi is_infinite_rw H. nin H. nin H. ee. rw iso_sub_trans_rw. sh (fun z => Y (z = y) x1 (x0 z)). uhg; ee. uhg; ir. rwi tack_on_inc H3. nin H3. rw Y_if_not_rw. uh H1; ee. uh H1. ap H1. am. uhg; ir. ap H0. wrr H4. rw Y_if_rw. am. am. uhg; ir. rwi tack_on_inc H3; rwi tack_on_inc H4; nin H3; nin H4. uh H1; ee. uh H6; ap H6. am. am. rwi Y_if_not_rw H5. rwi Y_if_not_rw H5. am. uhg; ir. ap H0. wrr H7. uhg; ir. ap H0. wrr H7. rwi Y_if_not_rw H5. rwi Y_if_rw H5. assert False. cp (H2 _ H3). ap H6. am. elim H6. am. uhg; ir. ap H0. wrr H6. rwi Y_if_rw H5. rwi Y_if_not_rw H5. unfold not in H2. assert False. apply H2 with y0. am. sy; am. elim H6. uhg; ir. ap H0. wrr H6. am. rww H4. ap sub_cardinal_leq. uhg; ir. rw tack_on_inc. app or_introl. Qed. Lemma cardinality_lt_ordinal_lt : forall y z, is_ordinal y -> is_ordinal z -> ordinal_lt (cardinality y) (cardinality z) -> ordinal_lt y z. Proof. ir. cp (ordinal_lt_lt_eq_or H H0). nin H2. am. nin H2. assert (cardinality y = cardinality z). ap cardinality_invariant. ap bernstein_cantor_schroeder. assert (sub (cardinality y) (cardinality z)). cp (ordinal_lt_leq H1). uh H3; ee; am. ap iso_sub_trans. sh (cardinality y). ee. uhg. sh (cardinality y). ee. ap card_isomorphic. uhg; ir; am. ap iso_sub_trans. sh (cardinality z). ee. app sub_iso_sub. uhg; sh z; ee. ap are_isomorphic_symm. ap card_isomorphic. ap sub_refl. ap sub_iso_sub. cp (ordinal_lt_leq H2). uh H3; ee; am. uh H1; ee. assert False. app H4. elim H5. uh H1; ee. assert False. ap H3. rww H2. elim H4. Qed. Lemma ord_card_leq_criterion : forall y z, is_ordinal y -> is_cardinal z -> (forall x, inc x y -> ordinal_lt x z) -> ordinal_leq y z. Proof. ir. uhg; ee. am. rwi is_cardinal_rw H0. ee; am. uhg; ir. cp (H1 _ H2). rwi ordinal_lt_rw H3. ee; am. Qed. Lemma inc_punctured_downward_subset : forall a x y, Order.Definitions.axioms a -> inc x (U a) -> inc y (punctured_downward_subset a x) = lt a y x. Proof. ir. ap iff_eq; ir. ufi punctured_downward_subset H1. Ztac. uf punctured_downward_subset. Ztac. uh H1; ee. uh H1; ee; am. Qed. Lemma punctured_downward_subset_wo_avatar : forall a x, is_well_ordered a -> inc x (U a) -> Transformation.bijective (punctured_downward_subset a x) (wo_avatar a x) (wo_avatar a). Proof. ir. wrr wo_punctured_downward. cp (wo_avatar_bijective H). set (k:= punctured_downward_subset a x). assert (sub k (U a)). uf k. uhg; ir. rwi inc_punctured_downward_subset H2. uh H2; ee. uh H2; ee. am. lu. am. uhg; dj. uhg; ir. rw Image.inc_rw. sh x0; ee; try am. tv. uhg; ee; try am. uhg; ir. rwi Image.inc_rw H4. nin H4. ee. sh x1; ee; am. uhg; ee; try am. uhg; ir. uh H1; ee. uh H9; ee. uh H10. ap H10. app H2. app H2. am. Qed. Lemma cardinality_punctured_downward_subset : forall a x, is_well_ordered a -> inc x (U a) -> (cardinality (punctured_downward_subset a x) = cardinality (wo_avatar a x)). Proof. ir. ap cardinality_invariant. apply trans_bij_isomorphic with (wo_avatar a). app punctured_downward_subset_wo_avatar. Qed. Lemma card_leq_criterion : forall a z, is_well_ordered a -> is_cardinal z -> (forall x, inc x (U a) -> ordinal_lt (cardinality (punctured_downward_subset a x)) z) -> ordinal_leq (cardinality (U a)) z. Proof. ir. ap ord_card_leq_criterion. ap cardinality_ordinal. am. ir. assert (ordinal_leq (cardinality (U a)) (wo_ordinal a)). app wo_ordinal_cardinal_leq. assert (inc x (wo_ordinal a)). uh H3; ee. app H5. ufi wo_ordinal H4. rwi Image.inc_rw H4. nin H4. ee. cp (H1 _ H4). rwi cardinality_punctured_downward_subset H6. ap cardinality_lt_ordinal_lt. wr H5. ap wo_avatar_is_ordinal. am. am. rwi is_cardinal_rw H0; ee; am. uh H0. rw H0. wrr H5. am. am. Qed. Lemma sub_punctured_downward_cone_op_triangle : forall y z, is_ordinal z -> inc y (op_triangle z) -> sub (punctured_downward_subset (op_triangle_lex z) y) (op_triangle (tack_on (pr1 y) (pr1 y))). Proof. ir. uhg; ir. rwi inc_punctured_downward_subset H1. uh H1. ee. rwi leq_op_triangle_lex H1. ee. assert (is_ordinal_pair x). rwi inc_op_triangle H1. ee; am. am. assert (is_ordinal_pair y). rwi inc_op_triangle H3. ee; am. am. rw inc_op_triangle. ee. am. rw ordinal_lt_rw. ee. ap ordinal_tack_on. uh H6; ee; am. uh H4; ee. nin H8. rw tack_on_inc. ap or_introl. rwi ordinal_lt_rw H8. ee; am. ee. rw H8. rw tack_on_inc. ap or_intror; tv. rwi inc_op_triangle H1. ee. am. am. ap ordinal_tack_on. uh H6; ee; am. assert (is_well_ordered (op_triangle_lex z)). app is_well_ordered_op_triangle_lex. lu. rw U_op_triangle_lex. am. Qed. Definition sub_prod_reflexive_below z := is_cardinal z & is_infinite z & (forall y, ordinal_lt y z -> sub_prod_reflexive y). Lemma ordinal_leq_lt_trans : forall x y, (exists z, (ordinal_leq x z & ordinal_lt z y)) -> ordinal_lt x y. Proof. ir. nin H. ee. uhg; ee. ap ordinal_leq_trans. sh x0. ee. am. app ordinal_lt_leq. uhg; ir. uh H0; ee. ap H2. ap ordinal_leq_leq_eq. am. wrr H1. Qed. Lemma is_finite_union2 : forall a b, is_finite a -> is_finite b -> is_finite (union2 a b). Proof. ir. cp (finite_induction (p:=fun x => (is_finite (union2 a x)))). cp (H1 b). ap H2. assert (union2 a emptyset = a). ap extensionality; uhg; ir. rwi inc_union2_rw H3. nin H3. am. nin H3. nin x0. rw inc_union2_rw. app or_introl. rw H3. am. ir. assert (union2 a (tack_on y z) = tack_on (union2 a y) z). ap extensionality; uhg; ir. rwi inc_union2_rw H4. rw tack_on_inc. rw inc_union2_rw. rwi tack_on_inc H4. intuition. rwi tack_on_inc H4. rwi inc_union2_rw H4. rw inc_union2_rw. rw tack_on_inc. intuition. rw H4. ap finite_tack_on. am. am. Qed. Lemma product_singleton_isomorphic : forall a x, are_isomorphic a (product a (singleton x)). Proof. ir. apply trans_bij_isomorphic with (fun y => pair y x). uhg; dj. uhg; ir. rw inc_product. ee. ap pair_is_pair. rww pr1_pair. rw pr2_pair. ap singleton_inc. uhg; ee; try am. uhg; ir. rwi inc_product H0. ee. cp (singleton_eq H2). sh (pr1 x0). ee. am. rwi is_pair_rw H0. sy. wrr H3. uhg; ee; try am. uhg; ir. transitivity (pr1 (pair x0 x)). rww pr1_pair. rw H3. rww pr1_pair. Qed. Lemma is_finite_product : forall a b, is_finite a -> is_finite b -> is_finite (product a b). Proof. ir. set (p := fun x => is_finite (product a x)). change (p b). apply finite_induction. uf p. assert (product a emptyset = emptyset). ap extensionality; uhg; ir. rwi inc_product H1. ee. nin H3. nin x0. nin H1. nin x0. rw H1. ap finite_emptyset. ir. uh H1. uhg. rw product_tack_on. ap is_finite_union2. am. ap finite_invariant. sh a. ee. ap product_singleton_isomorphic. am. am. Qed. Lemma infinite_tack_on_isomorphic: forall z x, is_infinite z -> are_isomorphic z (tack_on z x). Proof. ir. ap are_isomorphic_trans. sh (cardinality z). ee. ap card_isomorphic. ap are_isomorphic_trans. sh (cardinality (tack_on z x)). ee. rw infinite_cardinality_tack_on. ap are_isomorphic_refl. am. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma sprb_op_triangle_leq : forall z, sub_prod_reflexive_below z -> ordinal_leq (cardinality (op_triangle z)) z. Proof. ir. assert (op_triangle z = U (op_triangle_lex z)). rww U_op_triangle_lex. rw H0. ap card_leq_criterion. ap is_well_ordered_op_triangle_lex. uh H; ee. rwi is_cardinal_rw H. ee; am. uh H; ee; am. ir. rwi U_op_triangle_lex H1. ap ordinal_leq_lt_trans. sh (cardinality (op_triangle (tack_on (pr1 x) (pr1 x)))). ee. ap sub_cardinal_leq. ap sub_punctured_downward_cone_op_triangle. uh H; ee. rwi is_cardinal_rw H; ee; am. am. set (k:= tack_on (pr1 x) (pr1 x)). ap ordinal_leq_lt_trans. sh (cardinality (product k k)). ee. ap sub_cardinal_leq. ap sub_op_triangle_product. apply by_cases with (is_finite k); ir. assert (is_finite (product k k)). ap is_finite_product. am. am. cp H3. rwi is_finite_inc_cardinality_nat H4. uh H; ee. rwi is_infinite_sub_nat_cardinality H5. cp H. uh H7. rwi H7 H5. rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. ap H5. am. assert (is_infinite k). am. uh H; ee. assert (sub_prod_reflexive (pr1 x)). ap H5. rwi inc_op_triangle H1. ee. am. rwi is_cardinal_rw H; ee; am. assert (sub_prod_reflexive k). apply sub_prod_reflexive_invariant with (pr1 x). uf k. uhg. sh (pr1 x). ee. ap are_isomorphic_symm. ap infinite_tack_on_isomorphic. uhg; uhg; ir. ap H2. uf k. ap finite_tack_on. am. uhg; ir; am. am. assert (prod_reflexive k). ap sub_prod_reflexive_prod_reflexive. am. am. uh H8; ee. assert (cardinality (product k k) = cardinality k). ap cardinality_invariant. app are_isomorphic_symm. rw H9. uf k. rw infinite_cardinality_tack_on. apply ordinal_leq_lt_trans. sh (pr1 x). ee. ap iso_sub_ordinal_leq. rwi inc_op_triangle H1. ee. uh H1; ee; am. rwi is_cardinal_rw H; ee; am. ap sub_iso_sub. uhg; ir; am. rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. rwi inc_op_triangle H1. ee. rwi ordinal_lt_rw H10. ee; am. rwi is_cardinal_rw H; ee; am. uhg; uhg; ir. ap H2. uf k. ap finite_tack_on. am. Qed. Lemma inc_tack_on_infinite_cardinal : forall z x, is_cardinal z -> is_infinite z -> inc x z -> inc (tack_on x x) z. Proof. ir. cp H. rwi is_cardinal_rw H2; ee. assert (ordinal_lt x z). rw ordinal_lt_rw. ee; am. assert (ordinal_lt (tack_on x x) z). apply cardinality_lt_ordinal_lt. ap ordinal_tack_on. uh H4; ee. uh H4; ee. am. am. apply by_cases with (is_finite x); ir. assert (is_finite (tack_on x x)). ap finite_tack_on. am. rwi is_finite_inc_cardinality_nat H6. rwi is_infinite_sub_nat_cardinality H0. rw ordinal_lt_rw. ee. ap cardinality_ordinal. ap H0. am. assert (is_infinite x). am. ap ordinal_leq_lt_trans. sh (cardinality x). ee. rw infinite_cardinality_tack_on. ap ordinal_leq_refl. ap cardinality_ordinal. am. au. rwi ordinal_lt_rw H5; ee; am. Qed. Lemma tack_on_injective : forall a b, is_ordinal a -> is_ordinal b -> tack_on a a = tack_on b b -> a = b. Proof. ir. assert (forall z, is_ordinal z -> union (tack_on z z) = z). ir. ap extensionality; uhg; ir. cp (union_exists H3). nin H4; ee. rwi tack_on_inc H5. nin H5. assert (ordinal_lt x0 z). rw ordinal_lt_rw. ee. am. am. uh H6; ee. uh H6; ee. ap H9. am. wrr H5. apply union_inc with z. am. rw tack_on_inc. app or_intror. cp (H2 _ H). cp (H2 _ H0). wr H3; wr H4. rww H1. Qed. Lemma iso_sub_double_op_triangle : forall z, is_cardinal z -> is_infinite z -> iso_sub (product z (R 2)) (op_triangle z). Proof. ir. rw iso_sub_trans_rw. sh (fun x => pair (tack_on (pr1 x) (pr1 x)) (pr2 x)). uhg; ee. uhg; ir. rwi inc_product H1. ee. assert (is_ordinal (pr1 x)). assert (ordinal_lt (pr1 x) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H4; ee. uh H4; ee; am. assert (is_ordinal (pr2 x)). assert (ordinal_lt (pr2 x) (R 2)). rw ordinal_lt_rw. ee. ap Naturals.nat_ordinal. am. uh H5; ee. uh H5; ee; am. rw inc_op_triangle. rw pr1_pair. rw pr2_pair. ee. uhg; ee. ap pair_is_pair. rw pr1_pair. ap ordinal_tack_on. am. rw pr2_pair. am. ap cardinality_lt_ordinal_lt. ap ordinal_tack_on. am. rwi is_cardinal_rw H; ee; am. apply by_cases with (is_finite (pr1 x)); ir. assert (is_finite (tack_on (pr1 x) (pr1 x))). ap finite_tack_on. am. rwi is_finite_inc_cardinality_nat H7. rwi is_infinite_sub_nat_cardinality H0. rw ordinal_lt_rw. ee. ap cardinality_ordinal. app H0. rw infinite_cardinality_tack_on. rwi is_cardinal_rw H. ee. ap H7. rw ordinal_lt_rw. ee. am. am. am. uhg; ee. am. ap ordinal_tack_on. am. uhg; ir. rwi inc_two H3. nin H3. rwi zero_emptyset H3. rwi H3 H6. nin H6. nin x1. rwi H3 H6. rwi inc_one H6. rw H6. assert (is_ordinal (R 0)). ap Naturals.nat_ordinal. cp (ordinal_lt_lt_eq_or H4 H7). nin H8. rwi ordinal_lt_rw H8. ee. rwi zero_emptyset H9. nin H9. nin x1. nin H8. rwi ordinal_lt_rw H8. ee. rw tack_on_inc; app or_introl. rw tack_on_inc. ap or_intror; sy; am. rwi is_cardinal_rw H; ee; am. uhg; ir. apply pair_extensionality. rwi inc_product H1; ee; am. rwi inc_product H2; ee; am. ap tack_on_injective. rwi inc_product H1. ee. assert (ordinal_lt (pr1 x) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H6; ee. uh H6; ee; am. rwi inc_product H2. ee. assert (ordinal_lt (pr1 y) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H6; ee. uh H6; ee; am. transitivity (pr1 (pair (tack_on (pr1 x) (pr1 x)) (pr2 x))). rww pr1_pair. rw H3. rww pr1_pair. transitivity (pr2 (pair (tack_on (pr1 x) (pr1 x)) (pr2 x))). rww pr2_pair. rw H3. rww pr2_pair. Qed. Lemma finite_ordinal_cardinal : forall x, is_ordinal x -> is_finite x -> is_cardinal x. Proof. ir. uhg. ap ordinal_leq_leq_eq. ap cardinality_smallest. am. ap are_isomorphic_refl. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (ordinal_lt_lt_eq_or H H1). nin H2. rw ordinal_leq_rw. app or_introl. nin H2. uh H2. ee. uh H2; ee. assert (iso_sub x (cardinality x)). uhg. sh (cardinality x). ee. ap card_isomorphic. uhg; ir; am. rwi iso_sub_trans_rw H6. nin H6. assert (Transformation.injective x x x0). uhg; ee. uhg; ir. uh H6; ee. uh H6. ap H5. au. uh H6; ee. am. uh H0. cp (H0 _ H7). assert (cardinality x = x). ap extensionality; uhg; ir. app H5. uh H8; ee. uh H10; ee. uh H12. cp (H12 _ H9). nin H13. ee. wr H14. uh H6; ee. uh H6. au. rw H9. ap ordinal_leq_refl. am. wr H2. app ordinal_leq_refl. Qed. Lemma ordinal_lt_finite_infinite : forall x y, is_ordinal x -> is_ordinal y -> is_finite x -> is_infinite y -> ordinal_lt x y. Proof. ir. assert (is_cardinal x). app finite_ordinal_cardinal. rwi is_finite_inc_cardinality_nat H1. rwi is_infinite_sub_nat_cardinality H2. assert (sub nat y). apply sub_trans with (cardinality y). am. assert (ordinal_leq (cardinality y) y). ap cardinality_smallest. am. ap are_isomorphic_refl. uh H4; ee; am. rw ordinal_lt_rw. ee. am. uh H3; ee. wr H3. app H4. Qed. Lemma dumb_sub_product : forall z, is_ordinal z -> is_infinite z -> sub (product z (R 2)) (product z z). Proof. ir. uhg; ir. rwi inc_product H1. ee. assert (is_finite (R 2)). assert (R 2 = tack_on (R 1) (R 1)). wr nat_succ_tack_on. trivial. rw H4. ap finite_tack_on. assert (R 1 = tack_on (R 0) (R 0)). wrr nat_succ_tack_on. rw H5. ap finite_tack_on. rw zero_emptyset. ap finite_emptyset. assert (ordinal_leq (R 2) z). assert (ordinal_lt (R 2) z). ap ordinal_lt_finite_infinite. ap Naturals.nat_ordinal. am. am. am. uh H5; ee; am. uh H5; ee. rw inc_product. ee. am. am. app H7. Qed. Definition lim_sprb z := sub_prod_reflexive_below (cardinality z) \/ sub_prod_reflexive z . Lemma cardinality_double : forall z, is_ordinal z -> is_infinite z -> lim_sprb z -> cardinality (product z (R 2)) = cardinality z. Proof. ir. uf lim_sprb. ap ordinal_leq_leq_eq. nin H1. cp (sprb_op_triangle_leq H1). ap ordinal_leq_trans. sh (cardinality (op_triangle (cardinality z))). ee. ap ordinal_leq_trans. sh (cardinality (product (cardinality z) (R 2))). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. ap card_isomorphic. ap are_isomorphic_refl. ap iso_sub_cardinal_leq. ap iso_sub_double_op_triangle. ap is_cardinal_cardinality. rww is_infinite_cardinality. am. assert (prod_reflexive z). app sub_prod_reflexive_prod_reflexive. uh H2. ap iso_sub_cardinal_leq. ap iso_sub_trans. sh (product z z). ee. ap sub_iso_sub. app dumb_sub_product. uhg. sh z. ee. app are_isomorphic_symm. uhg; ir; am. ap iso_sub_cardinal_leq. uhg. sh (product z (R 1)). ee. rw R_one_singleton_emptyset. app product_singleton_isomorphic. uhg; ir. rwi inc_product H2. rw inc_product; ee. am. am. rw Naturals.R_S_tack_on. rw tack_on_inc. app or_introl. Qed. Lemma cardinal_leq_image : forall z f, ordinal_leq (cardinality (Image.create z f)) (cardinality z). Proof. ir. ap iso_sub_cardinal_leq. rw iso_sub_trans_rw. sh (fun x => choose (fun y => (inc y z & f y = x))). uhg; ee. uhg; ir. set (p:= fun y : E => inc y z & f y = x). assert (p (choose p)). ap choose_pr. rwi Image.inc_rw H. am. uh H0. ee. am. uhg. intros x y H H0. set (px:= fun y0 : E => inc y0 z & f y0 = x). set (py:= fun y0 : E => inc y0 z & f y0 = y). assert (px (choose px)). rwi Image.inc_rw H. app choose_pr. assert (py (choose py)). rwi Image.inc_rw H0. app choose_pr. uh H1; uh H2; ee. ir. wr H4; wr H3. rww H5. Qed. Lemma cardinal_leq_iso_sub : forall a b, ordinal_leq (cardinality a) (cardinality b) -> iso_sub a b. Proof. ir. ap iso_sub_trans. sh (cardinality a). ee. ap isomorphic_iso_sub. ap card_isomorphic. ap iso_sub_trans. sh (cardinality b). ee. ap sub_iso_sub. uh H; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma ordinal_leq_cardinality_union2_double : forall a b z, ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality (product z (R 2))). Proof. ir. assert (iso_sub a z). app cardinal_leq_iso_sub. assert (iso_sub b z). app cardinal_leq_iso_sub. uh H1; uh H2; nin H1; nin H2; ee. set (y:= Z (product z (R 2)) (fun u => (inc (pr1 u) x & pr2 u = R 0) \/ (inc (pr1 u) x0 & pr2 u = R 1))). assert (yinc : forall v, inc v y = (is_pair v & ((inc (pr1 v) x & pr2 v = R 0) \/ (inc (pr1 v) x0 & pr2 v = R 1)))). ir. ap iff_eq; ir. ufi y H5. Ztac. rwi inc_product H6. ee; am. ee. uf y. ap Z_inc. rw inc_product. ee; try am. nin H6; ee. app H4. app H3. nin H6; ee. rw H7. rw Naturals.R_S_tack_on. rw tack_on_inc. ap or_introl. rw Naturals.R_S_tack_on. rw tack_on_inc. app or_intror. rw H7. assert (R 2 = tack_on (R 1) (R 1)). ap Naturals.R_S_tack_on. rw H8. rw tack_on_inc. app or_intror. am. assert (are_isomorphic x a). app are_isomorphic_symm. assert (are_isomorphic x0 b). app are_isomorphic_symm. rwi iso_trans_ex_rw H5. rwi iso_trans_ex_rw H6. nin H5; nin H6. set (f:= fun d => Y (pr2 d = R 0) (x1 (pr1 d)) (x2 (pr1 d))). assert (sub (union2 a b) (Image.create y f)). uhg; ir. rwi inc_union2_rw H7. nin H7. uh H5; ee. uh H8; ee. uh H10. cp (H10 _ H7). nin H11. ee. rw Image.inc_rw. sh (pair x4 (R 0)). ee. rw yinc. ee. ap pair_is_pair. ap or_introl. ee. rw pr1_pair. am. rww pr2_pair. uf f. rw Y_if_rw. rww pr1_pair. rww pr2_pair. uh H6; ee. uh H8; ee. uh H10; ee. cp (H10 _ H7). nin H11. ee. rw Image.inc_rw. sh (pair x4 (R 1)). ee. rw yinc. ee. ap pair_is_pair. ap or_intror. ee. rw pr1_pair. am. rww pr2_pair. uf f. rw Y_if_not_rw. rww pr1_pair. rw pr2_pair. uhg; ir. assert (1 = 0). app R_inj. discriminate H14. ap ordinal_leq_trans. sh (cardinality (Image.create y f)). ee. ap iso_sub_cardinal_leq. app sub_iso_sub. ap ordinal_leq_trans. sh (cardinality y). ee. ap cardinal_leq_image. ap iso_sub_cardinal_leq. ap sub_iso_sub. uhg; ir. ufi y H8. Ztac. Qed. Lemma lim_sprb_cardinal_union2 : forall a b z, lim_sprb z -> is_infinite z -> ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality z). Proof. ir. ap ordinal_leq_trans. sh (cardinality (product z (R 2))). ee. app ordinal_leq_cardinality_union2_double. ap ordinal_leq_trans. sh (cardinality (product (cardinality z) (R 2))). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. ap card_isomorphic. ap are_isomorphic_refl. set (k:= cardinality z). assert (is_cardinal k). uf k. ap is_cardinal_cardinality. assert (is_infinite k). uf k. rww is_infinite_cardinality. ap ordinal_leq_trans; sh (cardinality k). ee. ap ordinal_leq_trans; sh (cardinality (op_triangle k)); ee. ap iso_sub_cardinal_leq. ap iso_sub_double_op_triangle. am. am. cp H3. uh H5. rw H5. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H6; ee. uh H6; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. uf k. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap are_isomorphic_symm. ap card_isomorphic. Qed. Definition reflect_pair x := pair (pr2 x) (pr1 x). Definition reflected_op_triangle z := Image.create (op_triangle z) reflect_pair. Lemma cardinal_leq_reflected_op_triangle : forall z, ordinal_leq (cardinality (reflected_op_triangle z)) (cardinality (op_triangle z)). Proof. ir. uf reflected_op_triangle. ap cardinal_leq_image. Qed. Lemma inc_ordinal_prod_itself_or : forall z x, is_ordinal z -> inc x (product z z) = (inc x (op_triangle z) \/ inc x (reflected_op_triangle z)). Proof. ir. ap iff_eq; ir. rwi inc_product H0. ee. assert (is_ordinal (pr1 x)). apply ordinal_inc_ordinal with z. am. am. assert (is_ordinal (pr2 x)). apply ordinal_inc_ordinal with z. am. am. cp (ordinal_lt_lt_eq_or H3 H4). nin H5. ap or_intror. uf reflected_op_triangle. rw Image.inc_rw. sh (pair (pr2 x) (pr1 x)). ee. rw inc_op_triangle. ee. uhg; ee. ap pair_is_pair. rww pr1_pair. rww pr2_pair. rw pr1_pair. rw ordinal_lt_rw. ee; am. rw pr2_pair. rw pr1_pair. uh H5; ee; am. am. uf reflect_pair. rw pr2_pair. rw pr1_pair. rwi is_pair_rw H0. sy; am. nin H5. ap or_introl. rw inc_op_triangle. ee. uhg; ee. am. am. am. rw ordinal_lt_rw; ee; am. uh H5; ee; am. am. ap or_introl. rw inc_op_triangle. ee. uhg; ee. am. am. am. rw ordinal_lt_rw; ee; am. rw ordinal_leq_rw. ap or_intror; ee; try am. sy; am. am. nin H0. rwi inc_op_triangle H0. ee. assert (ordinal_lt (pr2 x) z). ap ordinal_leq_lt_trans. sh (pr1 x). ee; am. rw inc_product. ee. uh H0; ee; am. rwi ordinal_lt_rw H1; ee; am. rwi ordinal_lt_rw H3; ee; am. am. ufi reflected_op_triangle H0. rwi Image.inc_rw H0. nin H0. ee. assert (is_pair x). wr H1. uf reflect_pair. ap pair_is_pair. assert (pr1 x = pr2 x0). wr H1. uf reflect_pair. rww pr1_pair. assert (pr2 x = pr1 x0). wr H1. uf reflect_pair. rww pr2_pair. rwi inc_op_triangle H0. ee. assert (ordinal_lt (pr2 x0) z). ap ordinal_leq_lt_trans. sh (pr1 x0). ee. am. am. rw inc_product. ee. am. rw H3. rwi ordinal_lt_rw H7; ee; am. rw H4. rwi ordinal_lt_rw H5; ee; am. am. Qed. Lemma ordinal_prod_itself_decomposition : forall z, is_ordinal z -> product z z = union2 (op_triangle z) (reflected_op_triangle z). Proof. ir. ap extensionality; uhg; ir. rwi inc_ordinal_prod_itself_or H0. rw inc_union2_rw. intuition. am. rwi inc_union2_rw H0. rw inc_ordinal_prod_itself_or. intuition. am. Qed. Lemma lim_sprb_cardinal_product : forall z, lim_sprb z -> is_infinite z -> ordinal_leq (cardinality (product z z)) (cardinality z). Proof. ir. set (k:= cardinality z). assert (is_cardinal k). uf k. ap is_cardinal_cardinality. ap ordinal_leq_trans. sh (cardinality (product k k)). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. uf k. ap card_isomorphic. uf k. ap card_isomorphic. assert (is_infinite k). uf k. rww is_infinite_cardinality. rw ordinal_prod_itself_decomposition. ap ordinal_leq_trans. sh (cardinality z). ee. ap lim_sprb_cardinal_union2. am. am. assert (cardinality z = k). tv. rw H3. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H4; ee. uh H4; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. ap ordinal_leq_trans. sh (cardinality (op_triangle k)). ee. ap cardinal_leq_reflected_op_triangle. assert (cardinality z = k). tv. rw H3. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H4; ee. uh H4; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. uf k. ap ordinal_leq_refl. ap cardinality_ordinal. rwi is_cardinal_rw H1. ee; am. Qed. Lemma lim_sprb_sub_prod_reflexive : forall z, lim_sprb z -> sub_prod_reflexive z. Proof. ir. uh H; nin H; try am. uh H; ee. cp H0. rwi is_infinite_cardinality H2. uhg; ir. assert (ordinal_leq (cardinality y) (cardinality z)). app sub_cardinal_leq. rwi ordinal_leq_rw H5. nin H5. cp (H1 _ H5). assert (prod_reflexive (cardinality y)). ap sub_prod_reflexive_prod_reflexive. rww is_infinite_cardinality. am. uh H7; uhg. ap are_isomorphic_trans. sh (cardinality y). ee. ap card_isomorphic. ap are_isomorphic_trans. sh (product (cardinality y) (cardinality y)). ee. am. ap cartesian_product_isomorphic. ap are_isomorphic_symm. ap card_isomorphic. ap are_isomorphic_symm. ap card_isomorphic. ee. assert (lim_sprb y). uhg. ap or_introl. rw H5. uhg; ee; am. cp (lim_sprb_cardinal_product H7 H4). assert (cardinality (product y y) = cardinality y). ap ordinal_leq_leq_eq. am. ap iso_sub_cardinal_leq. assert (nonempty y). ap excluded_middle. uhg; ir. uh H4. ap H4. assert (y = emptyset). ap extensionality; uhg; ir. assert False. ap H9. sh x. am. elim H11. nin H10. nin x0. rw H10. ap finite_emptyset. nin H9. uhg. sh (product y (singleton y0)). ee. ap product_singleton_isomorphic. uhg; ir. rwi inc_product H10; rw inc_product; ee; try am. cp (singleton_eq H12). rw H13. am. uhg. ap are_isomorphic_trans. sh (cardinality y); ee; try (ap card_isomorphic). wr H9. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma ordinal_lt_leq_trans : forall x z, (exists y, ordinal_lt x y & ordinal_leq y z) -> ordinal_lt x z. Proof. ir. nin H. ee. rw ordinal_lt_rw. ee. uh H0; ee. am. uh H0; ee. ap H2. rwi ordinal_lt_rw H. ee; am. Qed. Lemma all_ordinals_sub_prod_reflexive : forall z, is_ordinal z -> sub_prod_reflexive z. Proof. ap excluded_middle. uhg; ir. assert (exists z, is_ordinal z & ~(sub_prod_reflexive z)). ap excluded_middle. uhg; ir. ap H. ir. ap excluded_middle. uhg; ir. ap H0. sh z; ee; am. nin H0. ee. set (p:= fun y => ~(sub_prod_reflexive y)). set (u:= sow p). assert (p u). uf u. ap sow_property. sh x; ee; am. ufi p H2. assert (lim_sprb u). uhg. ap or_introl. uhg. ee. ap is_cardinal_cardinality. uhg; uhg; ir. ap H2. uhg. ir. assert False. uh H5; ap H5. assert (is_finite u). ap finite_invariant. sh (cardinality u); ee. ap are_isomorphic_symm. ap card_isomorphic. am. ap subset_finite. sh u. ee. am. am. elim H6. ir. assert (ordinal_leq (cardinality u) u). ap iso_sub_ordinal_leq. uf u. ap sow_ordinal. ap sub_iso_sub. uhg; ir; am. assert (ordinal_lt y u). ap ordinal_lt_leq_trans. sh (cardinality u). ee; am. ap excluded_middle. uhg; ir. assert (ordinal_leq u y). uf u. ap sow_smallest. uh H5; ee; uh H5; ee; am. am. rwi ordinal_leq_rw H7. nin H7. exact (not_ordinal_lt_lt H5 H7). ee. rwi H7 H5. exact (not_ordinal_lt_refl H5). (** now we have finished showing [lim_sprb u] **) ap H2. ap lim_sprb_sub_prod_reflexive. am. Qed. Lemma all_sub_prod_reflexive : forall z, sub_prod_reflexive z. Proof. ir. apply sub_prod_reflexive_invariant with (cardinality z). ap isomorphic_iso_sub. ap card_isomorphic. ap all_ordinals_sub_prod_reflexive. ap cardinality_ordinal. Qed. Lemma are_isomorphic_product : forall z, is_infinite z -> are_isomorphic z (product z z). Proof. ir. change (prod_reflexive z). assert (sub_prod_reflexive z). ap all_sub_prod_reflexive. uh H0. ap H0. uhg; ir; am. am. Qed. Lemma cardinality_product_infinite : forall z, is_infinite z -> cardinality (product z z) = cardinality z. Proof. ir. ap cardinality_invariant. ap are_isomorphic_symm. ap are_isomorphic_product. am. Qed. Lemma cardinality_union2_infinite : forall a b z, is_infinite z -> ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality z). Proof. ir. app lim_sprb_cardinal_union2. uhg. ap or_intror. ap all_sub_prod_reflexive. Qed. Lemma iso_sub_union2 : forall a b z, is_infinite z -> iso_sub a z ->iso_sub b z -> iso_sub (union2 a b) z. Proof. ir. ap cardinal_leq_iso_sub. ap cardinality_union2_infinite. am. app iso_sub_cardinal_leq. app iso_sub_cardinal_leq. Qed. (** This finishes the properties of cardinal arithemetic for unions and products of infinite cardinals. We use Russell's paradox to show that powerset is strictly bigger. ***) Lemma russell : forall z, ~(iso_sub (powerset z) z). Proof. ir. uhg; ir. rwi iso_sub_trans_rw H. nin H. set (rp:= fun y => (exists s, sub s z & x s = y & ~(inc y s))). set (t:= Z z rp). set (v:= x t). assert (sub t z). uf t. uhg; ir; Ztac. assert (inc v z). uh H; ee. uh H. uf v. ap H. rww powerset_inc_rw. apply by_cases with (inc v t); ir. (** the case [inc v t] **) cp H2. ufi t H3. Ztac. uh H5. nin H5. ee. assert (x0 = t). uh H; ee. uh H8. ap H8. rww powerset_inc_rw. rww powerset_inc_rw. am. ap H7. rww H8. (** the case [~(inc v t)] **) ap H2. uf t. Ztac. uhg. sh t. ee. am. tv. am. Qed. Lemma cardinal_lt_powerset : forall z, ordinal_lt (cardinality z) (cardinality (powerset z)). Proof. ir. assert (is_ordinal (cardinality z)). ap cardinality_ordinal. assert (is_ordinal (cardinality (powerset z))). ap cardinality_ordinal. cp (ordinal_lt_lt_eq_or H H0). nin H1. am. assert (ordinal_leq (cardinality (powerset z)) (cardinality z)). rw ordinal_leq_rw. intuition. assert False. cp (russell (z:=z)). ap H3. ap cardinal_leq_iso_sub. am. elim H3. Qed. (** for ord.v ***) Definition ordinal_outside x := sow (fun z => ~inc z x). Lemma ordinal_outside_exists : forall x, ex (fun z => is_ordinal z & ~inc z x). Proof. ir. apply excluded_middle. uhg; ir. assert (forall q, is_ordinal q -> inc q x). ir. apply excluded_middle. uhg; ir. ap H. sh q. ee; am. assert (sub (cardinality (powerset x)) x). uhg; ir. assert (is_ordinal (cardinality (powerset x))). ap cardinality_ordinal. ap H0. apply ordinal_inc_ordinal with (cardinality (powerset x)). am. am. assert (ordinal_leq (cardinality (powerset x)) (cardinality x)). ap iso_sub_cardinal_leq. ap iso_sub_trans. sh (cardinality (powerset x)). ee. ap isomorphic_iso_sub. ap card_isomorphic. ap sub_iso_sub. am. assert (iso_sub (powerset x) x). app Infinite.cardinal_leq_iso_sub. exact (Infinite.russell H3). Qed. Lemma ordinal_outside_outside : forall x , inc (ordinal_outside x) x -> False. Proof. ir. util (sow_property (p:= (fun z => ~inc z x))). app ordinal_outside_exists. exact (H0 H). Qed. Lemma ordinal_outside_ordinal : forall x, is_ordinal (ordinal_outside x). Proof. ir. uf ordinal_outside. app sow_ordinal. Qed. Lemma ordinal_outside_smallest : forall x o, is_ordinal o -> ~ inc o x -> ordinal_leq (ordinal_outside x) o. Proof. ir. uf ordinal_outside. ap sow_smallest. am. am. Qed. Lemma ordinal_not_leq_lt : forall x y, ordinal_leq x y -> ordinal_lt y x -> False. Proof. ir. ufi ordinal_lt H0. ee. ap H1. app ordinal_leq_leq_eq. Qed. Lemma ordinal_outside_refl_criterion : forall o, (forall x, inc x o -> is_ordinal x) -> (forall x y, inc x o -> ordinal_lt y x -> inc y o) -> ordinal_outside o = o. Proof. ir. assert (is_ordinal (ordinal_outside o)). ap ordinal_outside_ordinal. apply extensionality; uhg; ir. apply excluded_middle. uhg; ir. assert (ordinal_leq (ordinal_outside o) x). ap ordinal_outside_smallest. apply ordinal_inc_ordinal with (ordinal_outside o). am. am. am. assert (ordinal_lt x (ordinal_outside o)). rww ordinal_lt_rw. ee. am. am. exact (ordinal_not_leq_lt H4 H5). assert (is_ordinal x). au. cp (ordinal_lt_lt_eq_or H1 H3). nin H4. cp (H0 _ _ H2 H4). cp (ordinal_outside_outside H5). elim H6. nin H4. rwi ordinal_lt_rw H4. ee; am. wri H4 H2. cp (ordinal_outside_outside H2). elim H5. Qed. Lemma ordinal_criterion : forall o, (forall x, inc x o -> is_ordinal x) -> (forall x y, inc x o -> ordinal_lt y x -> inc y o) -> is_ordinal o. Proof. ir. cp (ordinal_outside_refl_criterion H H0). wr H1. ap ordinal_outside_ordinal. Qed. Lemma ordinal_outside_refl : forall o, is_ordinal o -> ordinal_outside o = o. Proof. ir. ap ordinal_outside_refl_criterion. ir. apply ordinal_inc_ordinal with o. am. am. ir. assert (ordinal_lt x o). rw ordinal_lt_rw. ee; am. assert (ordinal_lt y o). ap Infinite.ordinal_lt_trans. sh x. ee; am. rwi ordinal_lt_rw H3; ee; am. Qed. Lemma cardinality_zero_empty : forall x, cardinality x = R 0 -> x = emptyset. Proof. ir. assert (is_finite x). rw Infinite.is_finite_inc_cardinality_nat. rw H. ap R_inc. ap Infinite.number_zero_emptyset. am. uf Infinite.number. rw H. rww Bnat_R. Qed. Lemma cardinality_R : forall (i:nat), cardinality (R i) = (R i). Proof. ir. ap Infinite.nat_cardinality_refl. ap R_inc. Qed. Lemma is_finite_R : forall (i:nat), is_finite (R i). Proof. ir. rw Infinite.is_finite_inc_cardinality_nat. rww cardinality_R. ap R_inc. Qed. End Infinite. (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************) (*****************************************************************************************)