Set Implicit Arguments. Unset Strict Implicit. Require Export Arith. Require Export Omega. Require Export cardinal. Require Export cat_examples. Require Export fiprod. Ltac om := omega. Module Back. (** Defines [Bdefault] as a version of [B] where a default value is given and thus no hypothesis of inclusion is required; applies this to get [Bnat] sending a set back to a natural with default value [0]. *) Definition RBdefault x z (d:z) := Y (inc x z) x (R d). Lemma RBdefault_in : forall x z (d:z), inc x z -> RBdefault x d = x. Proof. ir. uf RBdefault. rw Y_if_rw. tv. am. Qed. Lemma RBdefault_out : forall x z (d:z), ~(inc x z) -> RBdefault x d = (R d). Proof. ir. uf RBdefault. rw Y_if_not_rw. tv. am. Qed. Lemma inc_RBdefault : forall x z (d:z), inc (RBdefault x d) z. Proof. ir. apply by_cases with (inc x z); ir. rw RBdefault_in. am. am. rw RBdefault_out. ap R_inc. am. Qed. Definition Bdefault x z (d:z) : z := B (inc_RBdefault x d). Lemma R_Bdefault_in : forall x z (d:z), inc x z -> R (Bdefault x d) = x. Proof. ir. uf Bdefault. rw B_eq. rww RBdefault_in. Qed. Lemma Bdefault_out : forall x z (d:z), ~(inc x z) -> (Bdefault x d) = d. Proof. ir. uf Bdefault. ap R_inj. rw B_eq. rww RBdefault_out. Qed. Lemma Bdefault_R : forall z (y d:z), Bdefault (R y) d = y. Proof. ir. ap R_inj. rw R_Bdefault_in. tv. ap R_inc. Qed. Definition Bnat x := Bdefault x (z:=nat) 0. Lemma R_Bnat : forall x, inc x nat -> R (Bnat x) = x. Proof. ir. uf Bnat. rww R_Bdefault_in. Qed. Lemma Bnat_out : forall x, ~(inc x nat) -> Bnat x = 0. Proof. ir. uf Bnat. rww Bdefault_out. Qed. Lemma Bnat_R : forall (i:nat), Bnat (R i) = i. Proof. ir. ap R_inj. rww R_Bnat. ap R_inc. Qed. End Back. Export Back. 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. 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 Relation. Export Quotient. Definition is_relation r := forall y, inc y r -> is_pair y. Definition substrate r := union2 (Image.create r pr1) (Image.create r pr2). Lemma inc_pr1_substrate : forall r y, inc y r -> inc (pr1 y) (substrate r). Proof. ir. uf substrate. ap union2_first. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma inc_pr2_substrate : forall r y, inc y r -> inc (pr2 y) (substrate r). Proof. ir. uf substrate. ap union2_second. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma substrate_smallest : forall r s, (forall y, inc y r -> inc (pr1 y) s) -> (forall y, inc y r -> inc (pr2 y) s) -> sub (substrate r) s. Proof. ir. uhg; ir. ufi substrate H1. cp (union2_or H1). nin H2. rwi Image.inc_rw H2. nin H2. ee. wr H3. ap H. am. rwi Image.inc_rw H2. nin H2. ee. wr H3. ap H0. am. Qed. Lemma inc_substrate : forall r x, is_relation r -> inc x (substrate r) = ((exists y, inc (pair x y) r) \/ (exists y, inc (pair y x) r)). Proof. ir. ap iff_eq; ir. ufi substrate H0. cp (union2_or H0). nin H1. ap or_introl. rwi Image.inc_rw H1. nin H1. ee. sh (pr2 x0). assert (pair x (pr2 x0) = x0). wr H2. uh H; ee. cp (H _ H1). uh H3. nin H3. nin H3. rw H3. rw pr1_pair. rw pr2_pair. tv. rww H3. ap or_intror. rwi Image.inc_rw H1. nin H1. ee. sh (pr1 x0). assert (pair (pr1 x0) x = x0). wr H2. uh H; ee. cp (H _ H1). uh H3. nin H3. nin H3. rw H3. rw pr1_pair. rw pr2_pair. tv. rww H3. nin H0. nin H0. assert (x = pr1 (pair x x0)). rww pr1_pair. rw H1. app inc_pr1_substrate. nin H0. assert (x = pr2 (pair x0 x)). rww pr2_pair. rw H1. app inc_pr2_substrate. Qed. Definition related r x y := inc (pair x y) r. Definition is_reflexive r := is_relation r & (forall y, inc y (substrate r) ->related r y y). Lemma reflexive_inc_substrate : forall r x, is_reflexive r -> inc x (substrate r) = inc (pair x x) r. Proof. ir. ap iff_eq; ir. uh H; ee. cp (H1 _ H0). am. rw inc_substrate. ap or_introl. sh x. am. lu. Qed. Lemma reflexive_ap : forall r x, is_reflexive r -> inc x (substrate r) -> related r x x. Proof. ir. uh H; ee. cp (H1 _ H0). am. Qed. Definition is_transitive r := is_relation r & (forall x y z, related r x y -> related r y z -> related r x z). Lemma transitive_ap : forall r x z, is_transitive r -> (exists y, related r x y & related r y z) -> related r x z. Proof. ir. nin H0. uh H; ee. ap (H2 x x0). am. am. Qed. Definition is_symmetric r := is_relation r & (forall x y, related r x y -> related r y x). Lemma symmetric_ap : forall r x y, is_symmetric r -> related r x y -> related r y x. Proof. ir. uh H; ee; au. Qed. Definition is_equivalence_relation r := is_relation r & is_reflexive r & is_transitive r & is_symmetric r. Lemma relation_intersection : forall z, nonempty z -> (forall r, inc r z -> is_relation r) -> is_relation (intersection z). Proof. ir. uhg; ee. ir. unfold is_relation in H0. nin H. apply H0 with y0. am. apply intersection_forall with z. am. am. Qed. Lemma related_intersection : forall z x y, nonempty z -> related (intersection z) x y = (forall r, inc r z -> related r x y). Proof. ir. ap iff_eq; ir. uh H0. uhg. apply intersection_forall with z. am. am. uhg. app intersection_inc. Qed. Lemma substrate_sub : forall r s, sub r s -> sub (substrate r) (substrate s). Proof. ir. uhg; ir. uf substrate. ufi substrate H0. cp (union2_or H0). nin H1. ap union2_first. rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. sh x0; ee. app H. am. ap union2_second. rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. sh x0; ee. app H. am. Qed. Lemma substrate_intersection_sub : forall r z, inc r z -> sub (substrate (intersection z)) (substrate r). Proof. ir. ap substrate_sub. uhg; ir. apply intersection_forall with z. am. am. Qed. Lemma reflexive_intersection : forall z, nonempty z -> (forall r, inc r z -> is_reflexive r) -> is_reflexive (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rw related_intersection. ir. cp (H0 _ H2). uh H3; ee. ap H4. assert (sub (substrate (intersection z)) (substrate r)). app substrate_sub. uhg; ir. apply intersection_forall with z. am. am. ap H5. am. am. Qed. Lemma transitive_intersection : forall z, nonempty z -> (forall r, inc r z -> is_transitive r) -> is_transitive (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rww related_intersection. ir. rwi related_intersection H1; rwi related_intersection H2. cp (H0 _ H3). uh H4; ee. apply H5 with y. au. au. am. am. am. Qed. Lemma symmetric_intersection : forall z, nonempty z -> (forall r, inc r z -> is_symmetric r) -> is_symmetric (intersection z). Proof. ir. uhg; ee. app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. ir. rww related_intersection. ir. rwi related_intersection H1. cp (H0 _ H2). uh H3; ee. ap H4. au. au. Qed. Lemma symmetric_transitive_reflexive : forall r, is_symmetric r -> is_transitive r -> is_reflexive r. Proof. ir. uhg; ee. uh H; ee; am. ir. rwi inc_substrate H1. nin H1. nin H1. app transitive_ap. sh x. ee. am. app symmetric_ap. nin H1. app transitive_ap. sh x. ee. app symmetric_ap. am. uh H; ee; am. Qed. Lemma show_equivalence_relation : forall r, is_relation r -> (forall x y, related r x y -> related r y x) -> (forall x y z, related r x y -> related r y z -> related r x z) -> is_equivalence_relation r. Proof. ir. assert (is_symmetric r). uhg; ee; am. assert (is_transitive r). uhg; ee; am. uhg; ee; try am. app symmetric_transitive_reflexive. Qed. Lemma symmetric_transitive_equivalence : forall r, is_symmetric r -> is_transitive r -> is_equivalence_relation r. Proof. ir. uhg; ee. uh H; ee; am. app symmetric_transitive_reflexive. am. am. Qed. Lemma equivalence_relation_intersection : forall z, nonempty z -> (forall r, inc r z -> is_equivalence_relation r) -> is_equivalence_relation (intersection z). Proof. ir. ap symmetric_transitive_equivalence. app symmetric_intersection. ir. cp (H0 _ H1). lu. app transitive_intersection. ir. cp (H0 _ H1). lu. Qed. Definition class r x := Image.create (Z r (fun y => pr1 y = x)) pr2. Lemma is_pair_rw : forall x, is_pair x = (x = pair (pr1 x) (pr2 x)). Proof. ir. ap iff_eq. ir. cp (pair_recov H). uh H0. sy; am. ir. rw H. ap pair_is_pair. Qed. Lemma inc_class : forall r x y, is_relation r -> inc y (class r x) = related r x y. Proof. ir. uf class. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. Ztac. assert (x0 = pair x y). uh H; ee. cp (H _ H2). rwi is_pair_rw H4. rw H4. rw H1; rww H3. uhg. wrr H4. sh (pair x y). ee. app Z_inc. rww pr1_pair. rww pr2_pair. Qed. Lemma nonempty_class_symmetric : forall r x, is_symmetric r -> nonempty (class r x) = inc x (substrate r). Proof. ir. ap iff_eq; ir. rw inc_substrate. nin H0. rwi inc_class H0. ap or_introl. sh y. am. lu. lu. rwi inc_substrate H0. nin H0. nin H0. sh x0. rw inc_class. am. lu. nin H0. sh x0. rw inc_class. app symmetric_ap. lu. lu. Qed. Lemma related_product : forall a b x y, related (product a b) x y = (inc x a & inc y b). Proof. ir. ap iff_eq; ir. uh H. cp (product_pr H). rwi pr1_pair H0; rwi pr2_pair H0; xd. uhg. ee; app product_pair_inc. Qed. Lemma full_equivalence_relation : forall b, is_equivalence_relation (Cartesian.product b b). Proof. ir. ap show_equivalence_relation. uhg. ir. cp (Cartesian.product_pr H). ee; am. ir. rwi related_product H. rw related_product; xd. ir. rwi related_product H; rwi related_product H0. rw related_product; xd. Qed. Lemma related_class_eq : forall r u v, is_equivalence_relation r -> related r u u -> related r u v = (class r u = class r v). Proof. ir. ap iff_eq; ir. ap extensionality; uhg; ir. rwi inc_class H2. rw inc_class. ap transitive_ap. lu. sh u. ee. ap symmetric_ap. lu. am. am. lu. lu. rwi inc_class H2. rw inc_class. ap transitive_ap. lu. sh v. ee; try am. lu. lu. wri inc_class H0. rwi H1 H0. rwi inc_class H0. ap symmetric_ap. lu. am. lu. lu. Qed. End Relation. Module Sundry. Export Map. Export Relation. Export Category. 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 inc_union2_rw : forall a b x, inc x (union2 a b) = (inc x a \/ inc x b). Proof. ir. ap iff_eq; ir. app union2_or. nin H. ap union2_first. am. ap union2_second. 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. Lemma subcategory_all_criterion : forall a b, is_subcategory a b -> (forall u, mor b u -> mor a u) -> a = b. Proof. ir. ap is_subcategory_extensionality. am. uhg; dj. uh H; ee; am. uh H; ee; am. uh H; ee; sy; am. ir. assert (x = source (id b x)). rww source_id. rw H5. rw ob_source. tv. ap H0. app mor_id. ap H0; am. sy. ap is_subcategory_same_comp. am. app H5. app H5. am. sy. ap is_subcategory_same_id. am. au. Qed. Lemma invertible_id : forall a b x, a = b -> ob a x -> invertible a (id b x). Proof. ir. wr H. uhg; ee. sh (id a x). uhg; dj. app mor_id. app mor_id. rww source_id. rww target_id. rww source_id. rww target_id. rww source_id. rww left_id. rww target_id. rww source_id. rww left_id. rww target_id. Qed. Lemma inverse_id : forall a b x, a = b -> ob a x -> inverse a (id b x) = id a x. Proof. ir. wr H. assert (invertible a (id a x)). app invertible_id. transitivity (comp a (inverse a (id a x)) (id a x)). rww right_id. app mor_inverse. rww source_inverse. rww target_id. rww left_inverse. rww source_id. Qed. End Sundry. Module UpdateA. Export Back. Export Naturals. Export Iterate. Export Relation. Export Sundry. End UpdateA.