Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export functions. Module Notation_gen. Module preregions. Definition add_translates (phi : E1) (x : E) := union2 x (IM (fun a : x => phi (R a))). Lemma add_translates_sub : forall (phi : E1) (x : E), sub x (add_translates phi x). ir; uf add_translates; uf sub; ir. ap union2_first; am. Qed. Lemma add_translates_new : forall (phi : E1) (x y : E), inc y x -> inc (phi y) (add_translates phi x). ir; uf add_translates; ir. ap union2_second. ap IM_inc. sh (B H). rw B_eq. tv. Qed. Definition im_pr (x : E) := union2 (add_translates P x) (add_translates Q x). Lemma im_pr_sub : forall x : E, sub x (im_pr x). ir. uf sub; ir. uf im_pr. ap union2_first. ap add_translates_sub. am. Qed. Lemma im_pr_pr1 : forall x a : E, inc a x -> inc (pr1 a) (im_pr x). ir. uf im_pr. ap union2_first. ap add_translates_new. am. Qed. Lemma im_pr_pr2 : forall x a : E, inc a x -> inc (pr2 a) (im_pr x). ir. uf im_pr. ap union2_second. ap add_translates_new. am. Qed. Definition add_pairs (x : E) := union2 (im_pr x) (product x x). Lemma add_pairs_sub : forall x : E, sub x (add_pairs x). ir; uf add_pairs. uf sub. ir. ap union2_first. ap im_pr_sub. am. Qed. Lemma add_pairs_pairs : forall x a b : E, inc a x -> inc b x -> inc (pair a b) (add_pairs x). ir. uf add_pairs. ap union2_second. ap product_pair_inc; am. Qed. Lemma add_pairs_pr : forall x a : E, inc a x -> (inc (pr1 a) (add_pairs x) & inc (pr2 a) (add_pairs x)). ir. dj. uf add_pairs. ap union2_first. ap im_pr_pr1. am. uf add_pairs. ap union2_first. ap im_pr_pr2. am. Qed. Definition add_elements (x : E) := union2 x (union x). Lemma add_elements_sub : forall x : E, sub x (add_elements x). ir; uf add_elements; uf sub; ir. ap union2_first; am. Qed. Lemma add_elements_elts : forall x y z : E, inc y x -> inc z y -> inc z (add_elements x). ir; uf add_elements; ap union2_second. apply union_inc with y; am. Qed. Definition add_values := add_translates (fun x : E => V (pr1 x) (pr2 x)). Lemma add_values_sub : forall x : E, sub x (add_values x). ir; uf add_values; ap add_translates_sub. Qed. Lemma add_values_values : forall x y : E, inc y x -> inc (V (pr1 y) (pr2 y)) (add_values x). ir. exact (add_translates_new (fun z : E => V (pr1 z) (pr2 z)) H). Qed. Definition add_all (phi : E1) (x : E) := add_values (add_elements (add_translates phi (add_pairs x))). Lemma add_all_sub : forall (phi : E1) (x : E), sub x (add_all phi x). uf add_all; uf sub; ir. ap add_values_sub. ap add_elements_sub. ap add_translates_sub. ap add_pairs_sub. am. Qed. Lemma add_all_pair : forall (phi : E1) (x a b : E), inc a x -> inc b x -> inc (pair a b) (add_all phi x). ir; uf add_all. ap add_values_sub. ap add_elements_sub. ap add_translates_sub. ap add_pairs_pairs; am. Qed. Lemma add_all_pr : forall (phi : E1) (x a : E), inc a x -> (inc (pr1 a) (add_all phi x) & inc (pr2 a) (add_all phi x)). ir. dj. uf add_all. ap add_values_sub. ap add_elements_sub. ap add_translates_sub. cp (add_pairs_pr H). xd. cp (add_pairs_pr H). uf add_all. ap add_values_sub. ap add_elements_sub. ap add_translates_sub. xd. Qed. Lemma add_all_translate : forall (phi : E1) (x a : E), inc a x -> inc (phi a) (add_all phi x). ir; uf add_all; ap add_values_sub; ap add_elements_sub. ap add_translates_new. ap add_pairs_sub; am. Qed. Lemma add_all_elt : forall (phi : E1) (x y z : E), inc y x -> inc z y -> inc z (add_all phi x). ir; uf add_all. ap add_values_sub. apply add_elements_elts with y. ap add_translates_sub; ap add_pairs_sub; am. am. Qed. Lemma add_all_values : forall (phi : E1) (x y : E), inc y x -> inc (V (pr1 y) (pr2 y)) (add_all phi x). ir. uf add_all. ap add_values_values. ap add_elements_sub. ap add_translates_sub. ap add_pairs_sub. am. Qed. Definition add_all_rec : forall (n : nat) (phi : E1), E1. intro n; nin n. ir; am. ir. exact (add_all phi (IHn phi X0)). Defined. Definition pool (phi : E1) (x : E) := IM (fun n : nat => add_all_rec n phi x). Lemma aar_in_pool : forall (n : nat) (phi : E1) (x : E), inc (add_all_rec n phi x) (pool phi x). ir. uf pool; ap IM_inc. sh n. tv. Qed. Lemma pool_from_aar : forall (phi : E1) (x y : E), inc y (pool phi x) -> exists n : nat, y = add_all_rec n phi x. ir. ufi pool H. pose (IM_exists H). nin e. sh x0. sy; am. Qed. Lemma pool_add_all : forall (phi : E1) (x y z : E), inc y (pool phi x) -> inc z (add_all phi y) -> ex (fun w : E => (inc w (pool phi x) & inc z w)). ir. pose (pool_from_aar H). nin e. sh (add_all_rec (S x0) phi x). ee. ap aar_in_pool. change (inc z (add_all phi (add_all_rec x0 phi x))) in |- *. wr H1. am. Qed. Lemma nat_family_sub : forall (f : nat -> E) (hyp : forall n : nat, sub (f n) (f (S n))) (n m : nat), n < m -> sub (f n) (f m). ir. nin H. ap hyp. apply sub_trans with (f m); au. Qed. Lemma aar_S_sub : forall (n : nat) (phi : E1) (x : E), sub (add_all_rec n phi x) (add_all_rec (S n) phi x). ir. set (K := add_all_rec n phi x) in *. change (sub K (add_all phi K)) in |- *. ap add_all_sub. Qed. Lemma aar_lt_sub : forall (n m : nat) (phi : E1) (x : E), n < m -> sub (add_all_rec n phi x) (add_all_rec m phi x). ir. pose (nat_family_sub (f:=fun i : nat => add_all_rec i phi x)). pose (s (fun n : nat => aar_S_sub (n:=n) (phi:=phi) (x:=x))). ap s0; ir; am. Qed. Lemma strub_exists : forall m n : nat, exists p : nat, (m < p & n < p). ir. pose (lt_eq_lt_dec m n). nin s. nin a. sh (S n). xd. sh (S n). xd. rw b; au. sh (S m); xd. Qed. Definition zoom (phi : E1) (x : E) := union (pool phi x). Lemma zoom_pr : forall (phi : E1) (x a b : E), inc a (zoom phi x) -> inc b (zoom phi x) -> ex (fun z : E => (inc a z & inc b z & sub (add_all phi z) (zoom phi x))). ir. ufi zoom H; ufi zoom H0. pose (union_exists H); pose (union_exists H0). nin e; nin e0. ee. nin (pool_from_aar H4). nin (pool_from_aar H3). nin (strub_exists x2 x3). ee. pose (aar_lt_sub (phi:=phi) (x:=x) H7). pose (aar_lt_sub (phi:=phi) (x:=x) H8). sh (add_all_rec x4 phi x). xd. ap s; wr H5; am. ap s0; wr H6; am. uf sub; ir; uf zoom. apply union_inc with (add_all_rec (S x4) phi x). exact H9. ap aar_in_pool. Qed. Lemma zoom_sub : forall (phi : E1) (x : E), sub x (zoom phi x). uf sub; ir. uf zoom. apply union_inc with (add_all_rec 0 phi x). exact H. ap aar_in_pool. Qed. Lemma zoom_translate : forall (phi : E1) (x y : E), inc y (zoom phi x) -> inc (phi y) (zoom phi x). ir. nin (zoom_pr H H); ee. ap H2. ap add_all_translate. am. Qed. Lemma zoom_pair : forall (phi : E1) (x a b : E), inc a (zoom phi x) -> inc b (zoom phi x) -> inc (pair a b) (zoom phi x). ir. nin (zoom_pr H H0). ee. ap H3. ap add_all_pair; am. Qed. Lemma zoom_projections : forall (phi : E1) (x a : E), inc a (zoom phi x) -> (inc (pr1 a) (zoom phi x) & inc (pr2 a) (zoom phi x)). ir. pose (zoom_pr H H). nin e. ee; pose (add_all_pr phi H0); xd. Qed. Lemma zoom_elt : forall (phi : E1) (x y z : E), inc y (zoom phi x) -> inc z y -> inc z (zoom phi x). ir. nin (zoom_pr H H); ee. ap H3. apply add_all_elt with y; am. Qed. Lemma zoom_values : forall (phi : E1) (x y : E), inc y (zoom phi x) -> inc (V (pr1 y) (pr2 y)) (zoom phi x). ir. nin (zoom_pr H H); ee. ap H2. ap add_all_values. am. Qed. End preregions. Definition arity_type : nat -> Type. ir. nin H. exact E. exact (E -> IHnat). Defined. Fixpoint arex (n : nat) : E1 -> arity_type n := match n return (E1 -> arity_type n) with | O => fun u : E1 => u emptyset | S m => fun (u : E1) (x : E) => arex m (fun y : E => u (pair x y)) end. Lemma arex_S_rw : forall (n : nat) (u : E1), arex (S n) u = (fun x : E => arex n (fun y : E => u (pair x y))). ir; tv. Qed. Fixpoint arsimilar (reg : E) (n : nat) {struct n} : arity_type n -> arity_type n -> Prop := match n return (arity_type n -> arity_type n -> Prop) with | O => fun x y : E => x = y | S m => fun u v : E -> arity_type m => forall x : E, inc x reg -> arsimilar reg (u x) (v x) end. Lemma arsimilar_O : forall (reg : E) (f g : arity_type 0), arsimilar reg (n:=0) f g -> f = g. ir; am. Qed. Lemma arsimilar_S : forall (reg : E) (n : nat) (f g : arity_type (S n)), arsimilar reg (n:=S n) f g -> forall x : E, inc x reg -> arsimilar reg (n:=n) (f x) (g x). intros reg n f g H. am. Qed. Lemma arsimilarS : forall (reg : E) (n : nat) (f g : arity_type (S n)), (forall x : E, inc x reg -> arsimilar reg (n:=n) (f x) (g x)) -> arsimilar reg (n:=S n) f g. intros reg n f g H. am. Qed. Lemma E1_nonempty : nonemptyT E1. apply nonemptyT_intro. ir; am. Qed. Fixpoint arex_inv (n : nat) : arity_type n -> E1 := match n return (arity_type n -> E1) with | O => fun a b : E => a | S m => fun (f : arity_type (S m)) (x : E) => arex_inv (n:=m) (f (pr1 x)) (pr2 x) end. Lemma arex_inv_pr : forall (n : nat) (f : arity_type n), arex n (arex_inv f) = f. intro n; nin n; ir. tv. change ((fun x : E => arex n (fun y : E => arex_inv f (pair x y))) = f) in |- *. apply arrow_extensionality. ir. assert ((fun y : E => arex_inv f (pair a y)) = arex_inv (f a)). apply arrow_extensionality. ir. transitivity (arex_inv (n:=n) (f (pr1 (pair a a0))) (pr2 (pair a a0))); tv. rw pr1_pair. rw pr2_pair. tv. rw H. rw IHn. tv. Qed. Definition approximates (reg : E) (f : E1) (u : E) := forall y : E, inc y reg -> V y u = f y. Lemma L_approx : forall (reg : E) (f : E1), approximates reg f (Function.create reg f). ir. uf approximates; ir. apply Function.create_V_rewrite. am. Qed. Lemma arsimilar_arex : forall (reg : E) (n : nat) (u v : E1), inc emptyset reg -> (forall a b : E, inc a reg -> inc b reg -> inc (pair a b) reg) -> arsimilar reg (n:=1) u v -> arsimilar reg (n:=n) (arex n u) (arex n v). intros reg n; nin n; ir. change (u emptyset = v emptyset) in |- *. cp (arsimilar_S H1). ap H2. am. ap arsimilarS. ir. rw arex_S_rw. rw arex_S_rw. ap IHn; au. ap arsimilarS. ir. change (u (pair x x0) = v (pair x x0)) in |- *. ap H1. ap H0; am. Qed. Lemma arsimilar_f_arex : forall (reg : E) (n : nat) (f : arity_type n) (u : E1), inc emptyset reg -> (forall a b : E, inc a reg -> inc b reg -> inc (pair a b) reg) -> (forall x : E, inc x reg -> arex_inv f x = u x) -> arsimilar reg (n:=n) f (arex n u). ir. assert (f = arex n (arex_inv f)). sy. ap arex_inv_pr. rw H2. ap arsimilar_arex. am. am. am. Qed. Definition object (t : E) (k : t -> nat) := forall a : t, arity_type (k a). Definition obex (* : (t:E; k:t->nat)(E->E) -> (object k) *) (t : E) (k : t -> nat) (f : E1) (a : t) := arex (k a) (fun x : E => f (pair (R a) x)). Definition obex_inv (* :(t:E; k:t->nat)(object k) -> E -> E *) (t : E) (k : t -> nat) (o : object k) (x : E) := choose (fun y : E => forall hyp : inc (pr1 x) t, y = arex_inv (o (B hyp)) (pr2 x)). Definition obex_pr (t : E) (k : t -> nat) (o : object k) (x y : E) := forall hyp : inc (pr1 x) t, y = arex_inv (o (B hyp)) (pr2 x). Lemma obex_pr_rw : forall (t : E) (k : t -> nat) (o : object k) (x : E), obex_inv o x = choose (obex_pr o x). ir; tv. Qed. Lemma obex_inv_rw : forall (t : E) (k : t -> nat) (o : object k) (a : t) (x : E), obex_inv o (pair (R a) x) = arex_inv (o a) x. ir. uf obex_inv. assert (ex (fun y : E => forall hyp : inc (pr1 (pair (R a) x)) t, y = arex_inv (o (B hyp)) (pr2 (pair (R a) x)))). apply ex_intro with (arex_inv (o a) x). ir. assert (B hyp = a). ap R_inj; rw B_eq; tv. ap pr1_pair. rw H. rw pr2_pair. tv. pose (choose_pr H). assert (inc (pr1 (pair (R a) x)) t). rw pr1_pair. ap R_inc. pose (e H0). rw e0. assert (B H0 = a). ap R_inj; rw B_eq; tv. ap pr1_pair. rw H1. rw pr2_pair; tv. Qed. Lemma obex_inv_pr : forall (t : E) (k : t -> nat) (o : object k), obex k (obex_inv o) = o. ir. uf obex. assert (forall a : t, arex (k a) (fun x : E => obex_inv o (pair (R a) x)) = o a). ir. assert ((fun x : E => obex_inv o (pair (R a) x)) = arex_inv (o a)). ap arrow_extensionality. ir. ap obex_inv_rw. rw H. ap arex_inv_pr. exact (prod_extensionality (x:=t) (y:=fun a : t => arity_type (k a)) (u:=fun a : t => arex (k a) (fun x : E => obex_inv o (pair (R a) x))) (v:=o) H). Qed. Definition preregion (t : E) (k : t -> nat) (o : object k) := preregions.zoom (obex_inv o) (union2 t (singleton emptyset)). Fixpoint preserves (reg : E) (n : nat) {struct n} : arity_type n -> Prop := match n return (arity_type n -> Prop) with | O => fun f : E => inc f reg | S m => fun f : E -> arity_type m => forall x : E, inc x reg -> preserves reg (n:=m) (f x) end. Lemma preserves_S : forall (reg : E) (n : nat) (f : arity_type (S n)), preserves reg f = (forall x : E, inc x reg -> preserves reg (n:=n) (f x)). ir. ap iff_eq. intro H; am. intro H; am. Qed. Lemma preserves_criterion : forall (reg : E) (n : nat) (f : arity_type n), (forall a b : E, inc a reg -> inc b reg -> inc (pair a b) reg) -> (forall a : E, inc a reg -> inc (arex_inv f a) reg) -> nonempty reg -> preserves reg f. intros reg n; nin n. ir. change (inc f reg) in |- *. nin H1. exact (H0 y H1). ir. change (forall x : E, inc x reg -> preserves reg (n:=n) (f x)) in |- *. ir. ap IHn. am. ir. assert (arex_inv (n:=n) (f x) a = arex_inv (n:=S n) f (pair x a)). transitivity (arex_inv (n:=n) (f (pr1 (pair x a))) (pr2 (pair x a))). rw pr1_pair; rw pr2_pair; tv. tv. rw H4. ap H0. ap H; am. am. Qed. Lemma preregion_stability : forall (t : E) (k : t -> nat) (o : object k), (sub t (preregion o) & (forall a b : E, inc a (preregion o) -> inc b (preregion o) -> inc (pair a b) (preregion o)) & (forall x y : E, inc x (preregion o) -> inc y x -> inc y (preregion o)) & (forall a : t, preserves (preregion o) (o a)) & inc emptyset (preregion o) & (forall x : E, inc x (preregion o) -> (inc (pr1 x) (preregion o) & inc (pr2 x) (preregion o))) & (forall x y : E, inc x (preregion o) -> inc y (preregion o) -> inc (V x y) (preregion o))). ir. dj. uf preregion. apply sub_trans with (union2 t (singleton emptyset)). uf sub; ir. ap union2_first. am. ap preregions.zoom_sub. uf preregion; ap preregions.zoom_pair; am. uf preregion; apply preregions.zoom_elt with x; am. ap preserves_criterion. am. uf preregion. ir. assert (arex_inv (n:=k a) (o a) a0 = obex_inv o (pair (R a) a0)). sy. ap obex_inv_rw. rw H3. ap preregions.zoom_translate. ap preregions.zoom_pair. ap H. ap R_inc. am. apply nonempty_intro with (R a). ap H. ap R_inc. assert (sub (union2 t (singleton emptyset)) (preregion o)). uf preregion. ap preregions.zoom_sub. ap H3. ap union2_second. ap singleton_inc. ufi preregion H4. pose (preregions.zoom_projections H4). xd. ufi preregion H4. pose (preregions.zoom_projections H4). xd. assert (inc (pair x y) (preregion o)). ap H0; am. set (z := pair x y) in *. assert (V x y = V (pr1 z) (pr2 z)). uf z. rw pr1_pair. rw pr2_pair. tv. rw H8. cp (preregions.zoom_values H7). exact H9. Qed. Definition stability_condition (t : E) (k : t -> nat) (o : object k) (reg : E) := sub t reg & (forall a b : E, inc a reg -> inc b reg -> inc (pair a b) reg) & (forall x y : E, inc x reg -> inc y x -> inc y reg) & (forall a : t, preserves reg (o a)) & inc emptyset reg & (forall x : E, inc x reg -> A (inc (pr1 x) reg) (inc (pr2 x) reg)) & (forall x y : E, inc x reg -> inc y reg -> inc (V x y) reg). Lemma preregion_cond : forall (t : E) (k : t -> nat) (o : object k), stability_condition o (preregion o). ir. exact (preregion_stability o). Qed. Lemma preserves_intersection : forall (n : nat) (f : arity_type n) (regint : E), (forall r : E, inc r regint -> preserves r f) -> nonempty regint -> preserves (intersection regint) f. intro n; nin n; ir. change (inc f (intersection regint)) in |- *. ap intersection_inc; am. change (forall x : E, inc x (intersection regint) -> preserves (intersection regint) (n:=n) (f x)) in |- *. ir. ap IHn. ir. cp (H r H2). assert (inc x r). apply intersection_forall with regint; am. apply (H3 x H4). am. Qed. Lemma stability_condition_intersection : forall (t : E) (k : t -> nat) (o : object k) (regint : E), (forall r : E, inc r regint -> stability_condition o r) -> nonempty regint -> stability_condition o (intersection regint). ir. uf stability_condition; xd. uf sub; ir. ap intersection_inc. am. ir. cp (H y H2). ufi stability_condition H3. xd. ir. cp (intersection_use_inc H1). cp (intersection_use_inc H2). ap intersection_inc. am. ir. assert (inc a y). apply H3; am. assert (inc b y). ap H4; am. cp (H y H5). ufi stability_condition H8. xd. ir. cp (intersection_use_inc H1). ap intersection_inc. am. ir. cp (H y0 H4). ufi stability_condition H5. xd. apply H7 with x. ap H3; am. am. ir. ap preserves_intersection. ir. ufi stability_condition H; cp (H r H1); xd. am. ap intersection_inc. am. ir. cp (H y H1). ufi stability_condition H2; xd. ir. xd. ap intersection_inc. am. ir. cp (H y H2). ufi stability_condition H3; xd. cp (intersection_use_inc H1). cp (H10 y H2). cp (H8 x H11). xd. ap intersection_inc. am. ir. cp (H y H2). ufi stability_condition H3; xd. cp (intersection_use_inc H1). cp (H10 y H2). cp (H8 x H11). xd. ir. ap intersection_inc. am. ir. cp (H _ H3). uh H4; ee. ap H10. ap (intersection_use_inc H1). am. ap (intersection_use_inc H2). am. Qed. Lemma stability_condition_intersection2 : forall (t : E) (k : t -> nat) (o : object k) (r1 r2 : E), stability_condition o r1 -> stability_condition o r2 -> stability_condition o (intersection2 r1 r2). ir. uf intersection2. ap stability_condition_intersection. ir. cp (doubleton_or H1). nin H2. rw H2; am. rw H2; am. sh r1. ap doubleton_first. Qed. Definition region_intersecters (t : E) (k : t -> nat) (o : object k) := Z (powerset (preregion o)) (fun r : E => stability_condition o r). Definition region (t : E) (k : t -> nat) (o : object k) := intersection (region_intersecters o). Lemma region_stability : forall (t : E) (k : t -> nat) (o : object k), stability_condition o (region o). ir. uf region. ap stability_condition_intersection. ir. ufi region_intersecters H. Ztac. sh (preregion o). uf region_intersecters. Ztac. ap powerset_inc; uf sub; ir; am. ap preregion_cond. Qed. Lemma region_smallest : forall (t : E) (k : t -> nat) (o : object k) (r : E), stability_condition o r -> sub (region o) r. ir. set (s := preregion o). assert (stability_condition o s). uf s; ap preregion_cond. set (u := intersection2 r s). assert (stability_condition o u). uf u; ap stability_condition_intersection2; am. uf region. assert (inc u (region_intersecters o)). uf region_intersecters; Ztac. ap powerset_inc. change (sub u s) in |- *. uf u. uf sub; ir. apply intersection2_second with r. am. apply sub_trans with u. apply intersection_sub. am. uf u; uf sub; ir. apply intersection2_first with s. am. Qed. Definition similar (reg t : E) (k : t -> nat) (o p : object k) := forall a : t, arsimilar reg (o a) (p a). Lemma arsimilar_symm : forall (n : nat) (f g : arity_type n) (r : E), arsimilar r f g -> arsimilar r g f. intro n; nin n; ir. change (g = f) in |- *. sy. am. ap arsimilarS. ir. ap IHn. ap H. am. Qed. Lemma arsimilar_sub : forall (n : nat) (f g : arity_type n) (r1 r2 : E), sub r1 r2 -> arsimilar r2 f g -> arsimilar r1 f g. intro n; nin n; ir. am. ap arsimilarS. cp (arsimilar_S H0). ir. apply IHn with r2. am. ap H1. ap H; am. Qed. Lemma similar_symm : forall (t : E) (k : t -> nat) (o p : object k) (r : E), similar r o p -> similar r p o. uf similar; ir. ap arsimilar_symm; ap H. Qed. Lemma similar_sub : forall (t : E) (k : t -> nat) (o p : object k) (r1 r2 : E), sub r1 r2 -> similar r2 o p -> similar r1 o p. uf similar; ir. apply arsimilar_sub with r2. am. ap H0. Qed. Lemma arsimilar_preserves : forall (n : nat) (f g : arity_type n) (r : E), preserves r f -> arsimilar r f g -> preserves r g. intro n; nin n; ir. change (inc g r) in |- *. cp (arsimilar_O H0). wr H1; am. rw preserves_S. ir. rwi preserves_S H. cp (arsimilar_S H0). apply IHn with (f x). ap H; am. ap H2; am. Qed. Lemma similar_stab : forall (t : E) (k : t -> nat) (o p : object k) (r : E), stability_condition o r -> similar r o p -> stability_condition p r. uf stability_condition; ir; xd. ufi similar H0. ir. apply arsimilar_preserves with (o a). ap H3. ap H0. Qed. Lemma similar_same_region1 : forall (t : E) (k : t -> nat) (o p : object k) (r : E), stability_condition o r -> similar r o p -> region o = region p. ir. ap extensionality. ap region_smallest. apply similar_stab with p. ap region_stability. apply similar_sub with r. ap region_smallest. apply similar_stab with o; am. ap similar_symm. am. ap region_smallest. apply similar_stab with o. ap region_stability. apply similar_sub with r. ap region_smallest. am. am. Qed. Lemma similar_same_region : forall (t : E) (k : t -> nat) (o p : object k), similar (region o) o p -> region o = region p. ir. apply similar_same_region1 with (region o). ap region_stability. am. Qed. Definition createN (t : E) (k : t -> nat) (o : object k) := Function.create (region o) (obex_inv o). Definition extract (t : E) (k : t -> nat) (u : E) := obex k (fun x : E => V x u). Lemma extract_create_similar : forall (t : E) (k : t -> nat) (o : object k), similar (region o) o (extract k (createN o)). ir. uf similar; ir. uf extract. uf obex. assert (stability_condition o (region o)). ap region_stability. ap arsimilar_f_arex. ufi stability_condition H; xd. ir. ufi stability_condition H. xd. ir. uf createN. rw Function.create_V_rewrite. rw obex_inv_rw. tv. ufi stability_condition H. xd. ap H1. ap H. ap R_inc. am. Qed. Lemma stability_pr1 : forall (t : E) (k : t -> nat) (o : object k) (r x : E), stability_condition o r -> inc x r -> inc (pr1 x) r. ir. ufi stability_condition H. xd. pose (H5 x H0). xd. Qed. Lemma stability_pr2 : forall (t : E) (k : t -> nat) (o : object k) (r x : E), stability_condition o r -> inc x r -> inc (pr2 x) r. ir. ufi stability_condition H. xd. pose (H5 x H0). xd. Qed. Lemma arsimilar_arex_inv : forall (reg : E) (n : nat) (f g : arity_type n) (x : E), inc x reg -> (forall x : E, inc x reg -> (inc (pr1 x) reg & inc (pr2 x) reg)) -> arsimilar reg f g -> arex_inv f x = arex_inv g x. intros reg n; nin n; ir. change (f = g) in |- *. am. change (arex_inv (f (pr1 x)) (pr2 x) = arex_inv (g (pr1 x)) (pr2 x)) in |- *. cp (H0 x H); ee. ap IHn. am. am. cp (arsimilar_S H1). ap H4; am. Qed. Lemma similar_obex_imp : forall (t : E) (k : t -> nat) (o p : object k) (r x y : E), similar r o p -> stability_condition o r -> inc x r -> obex_pr o x y -> obex_pr p x y. ir. ufi stability_condition H0; xd. cp (H7 x H1). xd. uf obex_pr. ir. ufi obex_pr H2. cp (H2 hyp). ufi similar H. cp (H (B hyp)). rw H11. apply arsimilar_arex_inv with r; am. Qed. Lemma similar_obex_inv : forall (t : E) (k : t -> nat) (o p : object k) (r : E), similar r o p -> stability_condition o r -> stability_condition p r -> forall x : E, inc x r -> obex_inv o x = obex_inv p x. ir. rw obex_pr_rw. rw obex_pr_rw. assert (obex_pr o x = obex_pr p x). ap arrow_extensionality. ir. ap iff_eq. ir. apply similar_obex_imp with o r; am. ir. apply similar_obex_imp with p r. ap similar_symm; am. am. am. am. rw H3. tv. Qed. Lemma similar_create_eq1 : forall (t : E) (k : t -> nat) (o p : object k) (r : E), similar r o p -> stability_condition o r -> stability_condition p r -> createN o = createN p. ir. uf createN. ap Function.create_extensionality. apply similar_same_region1 with r; am. ir. assert (similar (region o) o p). apply similar_sub with r. ap region_smallest; am. am. apply similar_obex_inv with (region o). am. ap region_stability. assert (region o = region p). apply similar_same_region. am. rw H5. ap region_stability. am. Qed. Lemma similar_create_eq : forall (t : E) (k : t -> nat) (o p : object k), similar (region o) o p -> createN o = createN p. ir. apply similar_create_eq1 with (region o). am. ap region_stability. assert (region o = region p). ap similar_same_region; am. rw H0. ap region_stability. Qed. Lemma create_extract_create : forall (t : E) (k : t -> nat) (o p : object k), createN (extract k (createN o)) = createN o. ir. sy. ap similar_create_eq. ap extract_create_similar. Qed. Lemma region_preserves : forall (t : E) (k : t -> nat) (o : object k) (a : t), preserves (region o) (o a). ir. cp (region_stability o). ufi stability_condition H. xd. Qed. Lemma region_preserves_sub : forall (t : E) (k : t -> nat) (o : object k) (x : E), inc x (region o) -> sub x (region o). ir. assert (stability_condition o (region o)). ap region_stability. uf sub; ir. ufi stability_condition H0; xd. apply H3 with x; am. Qed. Lemma region_value : forall (t : E) (k : t -> nat) (o : object k) (x : E) (a : t), inc x (region o) -> inc (V (pair (R a) emptyset) x) (region o). ir. assert (stability_condition o (region o)). ap region_stability. uh H0. ee. ap H6. ap H1. ap H0. ap R_inc. ap H4. am. Qed. Definition default_arity : forall n : nat, arity_type n. intro n; nin n. exact emptyset. exact (fun x : E => IHn). Defined. Definition related (t : E) (k : t -> nat) (o : object k) (a : E) := inc a (region o). Ltac sub_relate a := match goal with | |- (related ?X1 _) => uf related; ap (region_preserves_sub (region_preserves X1 a)) end. Lemma related_value : forall (t : E) (k : t -> nat) (o : object k) (x : E) (a : t), related o x -> related o (V (pair (R a) emptyset) x). ir. uf related. ap region_value. am. Qed. Lemma arsimilar_arity0 : forall (t : E) (k : t -> nat) (o : object k) (f g : E), arsimilar (region o) (n:=0) f g -> f = g. ir. exact H. Qed. Lemma arsimilar_arity1 : forall (t : E) (k : t -> nat) (o : object k) (f g : E1), arsimilar (region o) (n:=1) f g -> forall a : E, related o a -> f a = g a. ir. cp (arsimilar_S H H0). exact H1. Qed. Lemma arsimilar_arity2 : forall (t : E) (k : t -> nat) (o : object k) (f g : E2), arsimilar (region o) (n:=2) f g -> forall a b : E, related o a -> related o b -> f a b = g a b. ir. set (K1 := arsimilar_S H H0). exact (arsimilar_S K1 H1). Qed. Lemma arsimilar_arity3 : forall (t : E) (k : t -> nat) (o : object k) (f g : E3), arsimilar (region o) (n:=3) f g -> forall a b c : E, related o a -> related o b -> related o c -> f a b c = g a b c. ir. set (K1 := arsimilar_S H H0). set (K2 := arsimilar_S K1 H1). exact (arsimilar_S K2 H2). Qed. Lemma arsimilar_arity4 : forall (t : E) (k : t -> nat) (o : object k) (f g : E4), arsimilar (region o) (n:=4) f g -> forall a b c d : E, related o a -> related o b -> related o c -> related o d -> f a b c d = g a b c d. ir. set (K1 := arsimilar_S H H0). set (K2 := arsimilar_S K1 H1). set (K3 := arsimilar_S K2 H2). exact (arsimilar_S K3 H3). Qed. Lemma arsimilar_arity5 : forall (t : E) (k : t -> nat) (o : object k) (f g : E5), arsimilar (region o) (n:=5) f g -> forall a b c d e : E, related o a -> related o b -> related o c -> related o d -> related o e -> f a b c d e = g a b c d e. ir. set (K1 := arsimilar_S H H0). set (K2 := arsimilar_S K1 H1). set (K3 := arsimilar_S K2 H2). set (K4 := arsimilar_S K3 H3). exact (arsimilar_S K4 H4). Qed. Ltac notatac1 := match goal with | |- (extract ?X1 (createN ?X2) ?X3 = _) => transitivity (X2 X3); [ sy; apply (arsimilar_arity0 (extract_create_similar X2 X3)) | tv ] | |- (extract ?X1 (createN ?X2) ?X3 ?X4 = _ ?X4) => transitivity (X2 X3 X4); [ sy; apply (arsimilar_arity1 (extract_create_similar X2 X3)) | tv ] | |- (extract ?X1 (createN ?X2) ?X3 ?X4 ?X5 = _ ?X4 ?X5) => transitivity (X2 X3 X4 X5); [ sy; apply (arsimilar_arity2 (extract_create_similar X2 X3)) | tv ] | |- (extract ?X1 (createN ?X2) ?X3 ?X4 ?X5 ?X6 = _ ?X4 ?X5 ?X6) => transitivity (X2 X3 X4 X5 X6); [ sy; apply (arsimilar_arity3 (extract_create_similar X2 X3)) | tv ] | |- (extract ?X1 (createN ?X2) ?X3 ?X4 ?X5 ?X6 ?X7 = _ ?X4 ?X5 ?X6 ?X7) => transitivity (X2 X3 X4 X5 X6 X7); [ sy; apply (arsimilar_arity4 (extract_create_similar X2 X3)) | tv ] | |- (extract ?X1 (createN ?X2) ?X3 ?X4 ?X5 ?X6 ?X7 ?X8 = _ ?X4 ?X5 ?X6 ?X7 ?X8) => transitivity (X2 X3 X4 X5 X6 X7 X8); [ sy; apply (arsimilar_arity5 (extract_create_similar X2 X3)) | tv ] | _ => fail end. End Notation_gen. Module Notation. Export Notation_gen. (**** the following definition allows us to literally SPELL OUT elements of nota; the DOT i notation at the end lets us specify the arity *********************************) Inductive nota : E := DOT :nat-> nota | a_:nota->nota | b_:nota->nota | c_:nota->nota | d_:nota->nota | e_:nota->nota | f_:nota->nota | g_:nota->nota | h_:nota->nota | i_:nota->nota | j_:nota->nota | k_:nota->nota | l_:nota->nota | m_:nota->nota | n_:nota->nota | o_:nota->nota | p_:nota->nota | q_:nota->nota | r_:nota->nota | s_:nota->nota | t_:nota->nota | u_:nota->nota | v_:nota->nota | w_:nota->nota | x_:nota->nota | y_:nota->nota | z_:nota->nota . Fixpoint arity (k : nota) : nat := match k return nat with (DOT m) => m | (a_ n) => (arity n) | (b_ n) => (arity n) | (c_ n) => (arity n) | (d_ n) => (arity n) | (e_ n) => (arity n) | (f_ n) => (arity n) | (g_ n) => (arity n) | (h_ n) => (arity n) | (i_ n) => (arity n) | (j_ n) => (arity n) | (k_ n) => (arity n) | (l_ n) => (arity n) | (m_ n) => (arity n) | (n_ n) => (arity n) | (o_ n) => (arity n) | (p_ n) => (arity n) | (q_ n) => (arity n) | (r_ n) => (arity n) | (s_ n) => (arity n) | (t_ n) => (arity n) | (u_ n) => (arity n) | (v_ n) => (arity n) | (w_ n) => (arity n) | (x_ n) => (arity n) | (y_ n) => (arity n) | (z_ n) => (arity n) end. Definition da (op : nota) := default_arity (arity op). Notation obj := (object arity). Notation extra := (extract arity). Definition mask (*: Prop -> E -> E *) (P : Prop) (x : E) := Y P x emptyset. Lemma mask_in : forall (P : Prop) (x : E), P -> mask P x = x. ir. uf mask. ap Y_if. am. tv. Qed. Lemma mask_out : forall (P : Prop) (x : E), ~ P -> mask P x = emptyset. ir. uf mask. ap Y_if_not. am. tv. Qed. Definition atof op := arity_type (arity op). Definition notn := forall (x:nota), atof x. (*** our first example is the basic notational element corresponding to the underlying set of most common mathematical objects; having everybody share the same notation for underlying set allows us to fix the general notion of Umorphism as a morphism between objects which acts as a function on the underlying set (see the module Umorphism below) ****) Definition Underlying := (u_(n_(d_(r_(DOT 0))))). Definition U (x : E) := extra x Underlying. Definition caseUnderlying a (b : notn) op:= match op return (atof op) with (u_(n_(d_(r_(DOT 0))))) => a | z => (b z) end. Lemma U_formula : forall x : E, U x = V (pair (R Underlying) emptyset) x. ir. tv. Qed. Lemma related_U : forall (o : obj) (x : E), related o x -> related o (U x). ir. uhg. rw U_formula. ap region_value. am. Qed. End Notation. Module Arrow. Export Function. Export Notation. Definition Source := (s_(o_(u_(r_(c_(DOT 0)))))). Definition Target := (t_(a_(r_(g_(t_(DOT 0)))))). Definition Arrow := (a_(r_(r_(o_(w_(DOT 0)))))). Definition caseSource a (b : notn) op := match op return (atof op) with (s_(o_(u_(r_(c_(DOT 0)))))) => a | z => (b z) end. Definition caseTarget a (b : notn) op := match op return (atof op) with (t_(a_(r_(g_(t_(DOT 0)))))) => a | z => (b z) end. Definition caseArrow a (b : notn) op := match op return (atof op) with (a_(r_(r_(o_(w_(DOT 0)))))) => a | z => (b z) end. Definition source (x : E) := extra x Source. Definition target (x : E) := extra x Target. Definition arrow (x : E) := extra x Arrow. Definition create_obj (x y a: E) (op : nota) := caseUnderlying (U x) ( caseSource x ( caseTarget y ( caseArrow a ( da)))) op. Section Construction. Variables x y a:E. Definition create := createN (create_obj x y a). Lemma source_create : source create = x. ir; uf source; uf create; uf create_obj. notatac1; am. Qed. Lemma target_create : target create = y. ir; uf target; uf create; uf create_obj. notatac1; am. Qed. Lemma arrow_create : arrow create = a. ir; uf arrow; uf create; uf create_obj. notatac1; am. Qed. End Construction. Definition like a := a = create (source a) (target a) (arrow a). Lemma create_like : forall s t a :E, like (create s t a). Proof. ir. uf like. rw source_create. rw target_create. rw arrow_create. tv. Qed. Definition flip a := Y (like a) (create (target a) (source a) (arrow a)) a. Lemma source_flip : forall a, like a -> source (flip a) = target a. Proof. ir. uf flip. rw Y_if_rw. rw source_create. tv. am. Qed. Lemma target_flip : forall a, like a -> target (flip a) = source a. Proof. ir. uf flip. rw Y_if_rw. rw target_create. tv. am. Qed. Lemma flip_not_like : forall a, ~(like a) -> flip a = a. Proof. ir. uf flip. rw Y_if_not_rw. tv. am. Qed. Lemma arrow_flip : forall a, arrow (flip a) = arrow a. Proof. ir. apply by_cases with (like a); ir. uf flip. rw Y_if_rw. rw arrow_create. tv. am. rw flip_not_like. tv. am. Qed. Lemma flip_like : forall a, like a -> flip a = create (target a) (source a) (arrow a). Proof. ir. uf flip. rw Y_if_rw. tv. am. Qed. Lemma like_flip : forall a, like a = like (flip a). Proof. ir. ap iff_eq; ir. uf flip. rw Y_if_rw. ap create_like. am. apply by_cases with (like a); ir. am. rwi flip_not_like H. am. am. Qed. Lemma flip_flip : forall a, flip (flip a) = a. Proof. ir. apply by_cases with (like a); ir. rw flip_like. rw target_flip. rw source_flip. rw arrow_flip. uh H. sy; am. am. am. wr like_flip. am. rw flip_not_like. rw flip_not_like. tv. am. uhg; ir. ap H. rw like_flip. am. Qed. Definition ev u x := V x (arrow u). End Arrow. Module Umorphism. Export Arrow. Section Construction. Variables (x y : E) (f : E1). Definition create := Arrow.create x y (L (U x) f). Lemma source_create : source create = x. Proof. uf create. rw Arrow.source_create. tv. Qed. Lemma target_create : target create = y. Proof. uf create. rw Arrow.target_create. tv. Qed. Lemma ev_create : forall a : E, inc a (U x) -> ev create a = f a. Proof. ir. uf ev. uf create. rw Arrow.arrow_create. rw create_V_rewrite. tv. am. Qed. Lemma arrow_create : arrow create = L (U (source create)) (ev create). Proof. uf create. rw Arrow.arrow_create. rw Arrow.source_create. uf ev. ap Function.create_extensionality. tv. ir. rw Arrow.arrow_create. rw Function.create_V_rewrite. tv. am. Qed. End Construction. Lemma create_extens : forall (x x' y y' : E) (f g : E1), x = x' -> y = y' -> (forall a : E, inc a (U x) -> f a = g a) -> create x y f = create x' y' g. ir. wr H; wr H0. uf create. ap uneq. ap create_extensionality. tv. ir. au. Qed. Definition realizes (x y : E) (f : E1) (a : E) := source a = x & target a = y & (forall z : E, inc z (U x) -> ev a z = f z). Definition property (x y : E) (f : E1) := Transformation.axioms (U x) (U y) f. Definition like (a : E) := create (source a) (target a) (ev a) = a. Lemma create_like : forall (x y : E) (f : E1), like (create x y f). ir. uf like. ap create_extens. ap source_create. ap target_create. ir. ap ev_create. rwi source_create H. am. Qed. Lemma like_arrow_like : forall u, like u -> Arrow.like u. Proof. ir. uh H. uhg. ufi create H. set (f:=Function.create (U (source u)) (ev u)) in H. assert (arrow u = f). wr H. rw Arrow.arrow_create. tv. rw H0. sy; am. Qed. Lemma create_realizes : forall (x y : E) (f : E1), realizes x y f (create x y f). ir. pose source_create. pose target_create. pose ev_create. unfold realizes in |- *; xe. Qed. Lemma realizes_like_eq : forall (x y : E) (f : E1) (a : E), like a -> realizes x y f a -> create x y f = a. ir. ufi like H. wr H. ap create_extens; ufi realizes H0; xd. ir; sy; ap H2; am. Qed. Definition axioms (a : E) := property (source a) (target a) (ev a). Definition strong_axioms (a : E) := (axioms a & like a). Lemma axioms_from_strong : forall a : E, strong_axioms a -> axioms a. ir. unfold strong_axioms in H; xe. Qed. Lemma create_strong_axioms : forall (x y : E) (f : E1), property x y f -> strong_axioms (create x y f). ir. unfold strong_axioms in |- *. ee. unfold axioms in |- *. rw source_create. rw target_create. uf property. uf Transformation.axioms. ir. rw ev_create. ufi property H. ufi Transformation.axioms H. ap H. am. am. ap create_like. Qed. Lemma create_axioms : forall (x y : E) (f : E1), property x y f -> axioms (create x y f). ir. ap axioms_from_strong. ap create_strong_axioms; au. Qed. Definition identity (x : E) := create x x (fun y : E => y). Definition compose (a b : E) := create (source b) (target a) (fun y : E => ev a (ev b y)). Lemma identity_strong_axioms : forall x : E, strong_axioms (identity x). ir. uf identity. ap create_strong_axioms. uf property. ap Transformation.identity_axioms. Qed. Lemma identity_axioms : forall x : E, axioms (identity x). ir. cp (identity_strong_axioms x). ufi strong_axioms H; xe. Qed. Lemma left_identity : forall a : E, strong_axioms a -> compose (identity (target a)) a = a. ir. unfold compose in |- *. ap realizes_like_eq. unfold strong_axioms in H; xe. unfold realizes in |- *. xe. unfold identity in |- *; rewrite target_create. tv. ir. unfold identity in |- *. rewrite ev_create. tv. unfold strong_axioms in H. xd. Qed. Lemma right_identity : forall a : E, strong_axioms a -> compose a (identity (source a)) = a. ir. unfold compose in |- *. ap realizes_like_eq. unfold strong_axioms in H; xe. unfold realizes in |- *. xe. unfold identity in |- *; rewrite source_create. tv. ir. unfold identity in |- *; rewrite ev_create. tv. unfold identity in H0; rewrite source_create in H0. am. Qed. Lemma source_identity : forall x : E, source (identity x) = x. ir. unfold identity in |- *; rewrite source_create. tv. Qed. Lemma target_identity : forall x : E, target (identity x) = x. ir. unfold identity in |- *; rewrite target_create. tv. Qed. Lemma ev_identity : forall x y : E, inc y (U x) -> ev (identity x) y = y. ir. unfold identity in |- *; rewrite ev_create; au. Qed. Lemma source_compose : forall a b : E, source (compose a b) = source b. ir. unfold compose in |- *; rewrite source_create; tv. Qed. Lemma target_compose : forall a b : E, target (compose a b) = target a. ir. unfold compose in |- *; rewrite target_create; tv. Qed. Lemma ev_compose : forall a b y : E, inc y (U (source b)) -> ev (compose a b) y = ev a (ev b y). ir. unfold compose in |- *; rewrite ev_create; au. Qed. Definition composable (a b : E) := (axioms a & axioms b & source a = target b). Lemma compose_strong_axioms : forall a b : E, composable a b -> strong_axioms (compose a b). ir. unfold strong_axioms in |- *. xe. unfold axioms in |- *. rewrite source_compose. rewrite target_compose. unfold property in |- *. unfold Transformation.axioms in |- *. ir. rewrite ev_compose. unfold composable in H. xe. unfold axioms in H. unfold property in H. unfold Transformation.axioms in H. ap H. unfold axioms in H1. unfold property in H1. unfold Transformation.axioms in H1. rewrite H2. ap H1. am. am. unfold compose in |- *. ap create_like. Qed. Lemma compose_axioms : forall a b : E, composable a b -> axioms (compose a b). ir. set (K := compose_strong_axioms H). unfold strong_axioms in (type of K); xe. Qed. Lemma extens : forall a b : E, strong_axioms a -> strong_axioms b -> source a = source b -> target a = target b -> (forall x : E, inc x (U (source a)) -> inc x (U (source b)) -> ev a x = ev b x) -> a = b. ir. unfold strong_axioms in H, H0. xe. unfold like in H5, H4. rewrite <- H5. ap realizes_like_eq; au. unfold realizes in |- *. xe. ir. sy; ap H3. am. rewrite <- H1. am. Qed. Lemma associativity : forall a b c : E, composable a b -> composable b c -> compose (compose a b) c = compose a (compose b c). ir. ap extens. ap compose_strong_axioms. unfold composable in |- *. xe. ap compose_axioms; au. unfold composable in H0; xe. rewrite source_compose. unfold composable in H0; xe. ap compose_strong_axioms. unfold composable in |- *; xe. unfold composable in H; xe. ap compose_axioms. am. rewrite target_compose. unfold composable in H; xe. repeat rewrite source_compose. tv. repeat rewrite target_compose; tv. ir. repeat rewrite ev_compose. tv. repeat rewrite source_compose in H1. am. rewrite source_compose in H2. am. repeat rewrite source_compose in H1. unfold composable in H0. xe. rewrite H4. ap H3. am. repeat rewrite source_compose in H1. am. Qed. Definition inclusion (a b : E) := create a b (fun y : E => y). Lemma inclusion_strong_axioms : forall a b : E, sub (U a) (U b) -> strong_axioms (inclusion a b). ir. unfold inclusion in |- *. ap create_strong_axioms. unfold property in |- *. unfold Transformation.axioms in |- *. ir. ap H; au. Qed. Lemma inclusion_axioms : forall a b : E, sub (U a) (U b) -> axioms (inclusion a b). ir. ap axioms_from_strong. ap inclusion_strong_axioms; au. Qed. Definition injective (u : E) := axioms u & Transformation.injective (U (source u)) (U (target u)) (ev u). Lemma injective_rewrite : forall u : E, axioms u -> injective u = (forall x y : E, inc x (U (source u)) -> inc y (U (source u)) -> ev u x = ev u y -> x = y). ir. ap iff_eq; ir. unfold injective in H0. xe. unfold Transformation.injective in H4. xe. au. unfold injective in |- *; xe. unfold Transformation.injective in |- *; xe. Qed. Lemma injective_compose_with : forall u v w : E, strong_axioms u -> strong_axioms v -> injective w -> composable w u -> composable w v -> compose w u = compose w v -> u = v. ir. ap extens; au. transitivity (source (compose w u)). rewrite source_compose; au. rewrite H4. rewrite source_compose; au. unfold composable in H2, H3. xe. transitivity (source w); au. ir. unfold injective in H1. xe. unfold Transformation.injective in H7. xe. ap H8. unfold strong_axioms in H. xe. unfold axioms in H. unfold property in H. unfold composable in H2. xe. rewrite H11. ap H. am. unfold composable in H3; xe. rewrite H10. unfold strong_axioms in v; xe. au. transitivity (ev (compose w u) x). rewrite ev_compose; au. rewrite H4. rewrite ev_compose; au. Qed. Definition surjective (u : E) := axioms u & Transformation.surjective (U (source u)) (U (target u)) (ev u). Lemma surjective_rewrite : forall u : E, axioms u -> surjective u = (forall x : E, inc x (U (target u)) -> ex (fun y : E => (inc y (U (source u)) & ev u y = x))). ir. ap iff_eq; ir. unfold surjective in H0; xe. unfold Transformation.surjective in H2; xe. au. unfold surjective in |- *; xe. unfold Transformation.surjective in |- *; xe. Qed. Definition inverse (u : E) := create (target u) (source u) (Transformation.inverse (U (source u)) (ev u)). Lemma surjective_inverse_axioms : forall u : E, surjective u -> strong_axioms (inverse u). ir. unfold strong_axioms in |- *; xe. unfold inverse in |- *. ap create_axioms. unfold property in |- *. ap Transformation.surjective_inverse_axioms. unfold surjective in H; xe. unfold inverse in |- *. ap create_like. Qed. Lemma surjective_composable_left : forall u : E, surjective u -> composable (inverse u) u. ir. unfold composable in |- *. xe. ap axioms_from_strong. ap surjective_inverse_axioms; au. unfold surjective in H; xe. unfold inverse in |- *. rewrite source_create; tv. Qed. Lemma surjective_composable_right : forall u : E, surjective u -> composable u (inverse u). ir. unfold composable in |- *; xe. unfold surjective in H; xe. ap axioms_from_strong. ap surjective_inverse_axioms; au. unfold inverse in |- *; rewrite target_create; tv. Qed. Lemma surjective_inverse_right : forall u : E, surjective u -> compose u (inverse u) = identity (target u). ir. assert (axioms u). unfold surjective in H; xe. ap extens. ap compose_strong_axioms. ap surjective_composable_right. am. ap identity_strong_axioms. rewrite source_compose. rewrite source_identity. unfold inverse in |- *; rewrite source_create. tv. rewrite target_compose. rewrite target_identity; tv. ir. rewrite ev_compose. rewrite ev_identity. unfold inverse in |- *. rewrite ev_create. unfold surjective in H. xe. rewrite source_identity in H2. pose (Transformation.surjective_inverse_right H3 H2). ap e. rewrite source_identity in H2; am. rewrite source_identity in H2; am. rewrite source_compose in H1; am. Qed. Definition bijective (u : E) := (injective u & surjective u). Lemma bijective_transformation_bijective : forall u : E, bijective u -> Transformation.bijective (U (source u)) (U (target u)) (ev u). ir. unfold bijective in H; xe. unfold injective in H. unfold surjective in H0. xe. unfold axioms in H. unfold property in H. unfold Transformation.bijective in |- *; xe. Qed. Lemma transformation_bijective_bijective : forall u : E, axioms u -> Transformation.bijective (U (source u)) (U (target u)) (ev u) -> bijective u. ir. unfold Transformation.bijective in H0. unfold bijective in |- *. xe. unfold injective in |- *; xe. unfold surjective in |- *; xe. Qed. Definition are_inverse (u v : E) := composable u v & composable v u & compose u v = identity (source v) & compose v u = identity (source u). Lemma inverse_symm : forall u v : E, are_inverse u v -> are_inverse v u. ir. unfold are_inverse in |- *. unfold are_inverse in H. xe. Qed. Lemma inverse_unique : forall u v w : E, strong_axioms v -> strong_axioms w -> are_inverse u v -> are_inverse u w -> v = w. ir. transitivity (compose v (identity (source v))). sy. ap right_identity. am. unfold are_inverse in H1, H2; ee. assert (source v = target u). unfold composable in H6; xe. assert (source v = source w). rewrite H9. unfold composable in H3; xe. rewrite H10. rewrite <- H4. rewrite <- associativity. rewrite H8. assert (source u = target w). unfold composable in H2; xe. rewrite H11. ap left_identity. am. am. am. Qed. Definition has_inverse (u : E) := ex (fun v : E => are_inverse u v). Lemma are_inverse_transfo_inverse : forall u v : E, are_inverse u v -> Transformation.are_inverse (U (source u)) (U (target u)) ( ev u) (ev v). ir. unfold Transformation.are_inverse in |- *. unfold are_inverse in H. xe. unfold composable in H; xe. unfold composable in H, H0; xe. rewrite <- H4. rewrite H6. am. ir. transitivity (ev (compose v u) x). sy; ap ev_compose. am. rewrite H2. ap ev_identity. am. ir. assert (inc y (U (source v))). unfold composable in H0; xe. rewrite H5; am. transitivity (ev (compose u v) y). rewrite ev_compose. tv. am. rewrite H1. rewrite ev_identity. tv. am. Qed. Lemma inverse_bijective : forall u v : E, are_inverse u v -> bijective u. ir. ap transformation_bijective_bijective. unfold are_inverse in H; xe. unfold composable in H; xe. apply Transformation.inverse_bijective with (ev v). ap are_inverse_transfo_inverse. am. Qed. Lemma bijective_inverse : forall u : E, bijective u -> are_inverse u (inverse u). ir. unfold bijective in H; xe. pose (surjective_composable_left H0). pose (surjective_composable_right H0). pose (surjective_inverse_right H0). unfold are_inverse in |- *; ee. am. am. unfold composable in (type of c); ee. rewrite H3. ap e. apply injective_compose_with with u. ap compose_strong_axioms; au. ap identity_strong_axioms. am. unfold composable in |- *. ee. unfold injective in H; xe. ap compose_axioms; au. rewrite target_compose. unfold composable in (type of c0); xe. unfold composable in |- *; ee. unfold injective in H; xe. ap identity_axioms. rewrite target_identity; tv. rewrite <- associativity. rewrite e. ap extens. ap compose_strong_axioms. unfold composable in |- *; ee. ap identity_axioms. unfold injective in H; xe. rewrite source_identity. tv. ap compose_strong_axioms. unfold composable in |- *; ee. unfold injective in H; xe. ap identity_axioms. rewrite target_identity; tv. rewrite source_compose. rewrite source_compose. rewrite source_identity; tv. repeat rewrite target_compose. rewrite target_identity. tv. ir. repeat rewrite ev_compose. repeat rewrite ev_identity. tv. rewrite source_compose in H2. rewrite source_identity in H2; am. unfold injective in H; ee. unfold axioms in H. unfold property in H; xe. ap H. rewrite source_compose in H2. rewrite source_identity in H2. am. rewrite source_compose in H2; am. rewrite source_compose in H2. rewrite source_identity in H2. am. am. am. Qed. Lemma bijective_has_inverse : forall u : E, bijective u -> has_inverse u. ir. unfold has_inverse in |- *. apply ex_intro with (inverse u). ap bijective_inverse; au. Qed. Lemma bijective_eq_has_inverse : forall u : E, bijective u = has_inverse u. ir. ap iff_eq; ir. unfold has_inverse in |- *. apply ex_intro with (inverse u). ap bijective_inverse; au. unfold has_inverse in H. nin H. apply inverse_bijective with x; au. Qed. Lemma bijective_eq_inverse : forall u : E, bijective u = are_inverse u (inverse u). ir. ap iff_eq; ir. ap bijective_inverse. am. apply inverse_bijective with (inverse u); am. Qed. Lemma has_inverse_eq_inverse : forall u : E, has_inverse u = are_inverse u (inverse u). ir. rewrite <- bijective_eq_inverse. rewrite bijective_eq_has_inverse. tv. Qed. Definition Uempty_obj (i : nota) := match i with | u => da u end. Definition Uempty := createN Uempty_obj. Definition Uempty_initial (a : E) := inclusion Uempty a. Lemma underlying_Uempty : U Uempty = emptyset. uf Uempty. uf U. notatac1. Qed. Lemma Uempty_initial_strong_axioms : forall a : E, strong_axioms (Uempty_initial a). ir. uf Uempty_initial. ap inclusion_strong_axioms. rw underlying_Uempty. uf sub; ir. nin H. elim x0. Qed. Lemma use_axioms : forall u x y a : E, axioms u -> source u = x -> target u = y -> inc a (U x) -> inc (ev u a) (U y). ir. cx. wr H1. ap H. rw H0. am. Qed. Ltac clst := match goal with | id1:?X1 |- _ => first [ rewrite source_create in id1; clst | rewrite target_create in id1; clst | rewrite source_identity in id1; clst | rewrite target_identity in id1; clst | rewrite source_compose in id1; clst | rewrite target_compose in id1; clst ] | |- _ => first [ rewrite source_create; clst | rewrite target_create; clst | rewrite source_identity; clst | rewrite target_identity; clst | rewrite source_compose; clst | rewrite target_compose; clst ] | _ => idtac end. End Umorphism.