Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export 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. ***) 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). 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. 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.