From 05cfeb82d2624860e66941421a937f308d66cf33 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Jul 2010 10:42:33 +0000 Subject: [PATCH] some notation for map_arrows2 --- .../overlap/basic_pairs_to_o-basic_pairs.ma | 12 ++++++------ .../formal_topology/overlap/basic_topologies.ma | 6 +++--- .../formal_topology/overlap/categories.ma | 4 ++++ .../formal_topology/overlap/o-algebra.ma | 4 ++++ .../formal_topology/overlap/o-basic_pairs.ma | 6 +----- .../overlap/relations_to_o-algebra.ma | 16 +++++----------- 6 files changed, 23 insertions(+), 25 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma index 65709f465..b72e4a5fa 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma @@ -19,9 +19,9 @@ include "relations_to_o-algebra.ma". definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair. intro b; constructor 1; - [ apply (map_objs2 ?? POW (concr b)); - | apply (map_objs2 ?? POW (form b)); - | apply (map_arrows2 ?? POW (concr b) (form b) (rel b)); ] + [ apply (POW (concr b)); + | apply (POW (form b)); + | apply (POW⎽⇒ ?); apply (rel b); ] qed. definition o_relation_pair_of_relation_pair: @@ -29,7 +29,7 @@ definition o_relation_pair_of_relation_pair: Orelation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). intros; constructor 1; - [ apply (map_arrows2 ?? POW (concr BP1) (concr BP2) (r \sub \c)); + [ unfold o_basic_pair_of_basic_pair; simplify; apply (POW⎽⇒ ?); apply (r\sub \c); | apply (map_arrows2 ?? POW (form BP1) (form BP2) (r \sub \f)); | apply (.= (respects_comp2 ?? POW (concr BP1) (concr BP2) (form BP2) r\sub\c (⊩\sub BP2) )^-1); cut ( ⊩ \sub BP2 ∘ r \sub \c =_12 r\sub\f ∘ ⊩ \sub BP1) as H; @@ -115,7 +115,7 @@ qed. theorem BP_to_OBP_faithful: ∀S,T.∀f,g:arrows2 (category2_of_category1 BP) S T. - map_arrows2 ?? BP_to_OBP ?? f = map_arrows2 ?? BP_to_OBP ?? g → f=g. + BP_to_OBP⎽⇒ f = BP_to_OBP⎽⇒ g → f=g. intros; change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c); apply (POW_faithful); apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T)); @@ -126,7 +126,7 @@ theorem BP_to_OBP_faithful: qed. theorem BP_to_OBP_full: - ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f). + ∀S,T.∀f. exT22 ? (λg:arrows2 ? S T. BP_to_OBP⎽⇒ g = f). intros; cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc); cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf); diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma index b24a730cb..5cb82832a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma @@ -145,9 +145,9 @@ definition BTop: category1. = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X)))); [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);] clear K H' H1'; - alias symbol "compose" (instance 2) = "category1 composition". -cut (∀X:Ω \sup o1. - minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X)); +alias symbol "compose" (instance 1) = "category1 composition". +cut (∀X:Ω^o1. + minus_star_image ?? (b ∘ a) (A o1 X) =_1 minus_star_image ?? (b'∘a') (A o1 X)); [2: intro; apply (.= (minus_star_image_comp ??????)); apply (.= #‡(saturated ?????)); diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 72af642c3..65320ae53 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -355,6 +355,10 @@ record functor2 (C1: category2) (C2: category2) : Type3 ≝ ∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3. map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}. +notation > "F⎽⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}. +notation "F\sub⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}. +interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x). + definition functor2_setoid: category2 → category2 → setoid3. intros (C1 C2); constructor 1; diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index 915afc26d..a86d286bc 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -324,6 +324,10 @@ coercion ORelation_setoid_of_arrows2_OA. prefer coercion Type_OF_objs2. +notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}. +notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}. +interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B). + (* qui la notazione non va *) lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q). intros; diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 6f16b0d3f..f0e0b712c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -23,10 +23,6 @@ record Obasic_pair: Type2 ≝ { interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y). interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c). -notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}. -notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}. -interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B). - record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ { Oconcr_rel: (Oconcr BP1) ⇒_\o2 (Oconcr BP2); Oform_rel: (Oform BP1) ⇒_\o2 (Oform BP2); Ocommute: ⊩ ∘ Oconcr_rel =_2 Oform_rel ∘ ⊩ @@ -248,4 +244,4 @@ interpretation "Universal pre-image ⊩*" 'rest x = (fun12 ? ? (or_f_star ? ?) ( notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}. notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}. -interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)). \ No newline at end of file +interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)). diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma index 9bcd51c7c..8bf57da98 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma @@ -51,7 +51,7 @@ qed. definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x. coercion powerset_of_POW'. -definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (POW' o1) (POW' o2). +definition orelation_of_relation: ∀o1,o2:REL. o1 ⇒_\r1 o2 → (POW' o1) ⇒_\o2 (POW' o2). intros; constructor 1; [ constructor 1; @@ -90,7 +90,7 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA ( qed. lemma orelation_of_relation_preserves_equality: - ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. + ∀o1,o2:REL.∀t,t': o1 ⇒_\r1 o2. t = t' → orelation_of_relation ?? t =_2 orelation_of_relation ?? t'. intros; split; unfold orelation_of_relation; simplify; intro; split; intro; simplify; whd in o1 o2; @@ -140,7 +140,7 @@ qed. alias symbol "eq" = "setoid2 eq". alias symbol "compose" = "category1 composition". lemma orelation_of_relation_preserves_composition: - ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3. + ∀o1,o2,o3:REL.∀F: o1 ⇒_\r1 o2.∀G: o2 ⇒_\r1 o3. orelation_of_relation ?? (G ∘ F) = comp2 OA ??? (orelation_of_relation ?? F) (orelation_of_relation ?? G). intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros; @@ -172,7 +172,7 @@ qed. theorem POW_faithful: ∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T. - map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f = g. + POW⎽⇒ f =_2 POW⎽⇒ g → f =_2 g. intros; unfold POW in e; simplify in e; cases e; unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4; intros 2; cases (e3 {(x)}); @@ -186,13 +186,7 @@ lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C). intros; constructor 1; [ apply (b c); | intros; apply (#‡e);] qed. -(* -interpretation "lifting singl" 'singl x = - (fun11 ? (objs2 (POW ?)) (singleton ?) x). -*) - - -theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f). +theorem POW_full: ∀S,T.∀f: (POW S) ⇒_\o2 (POW T) . exT22 ? (λg. POW⎽⇒ g = f). intros; exists; [ constructor 1; constructor 1; [ apply (λx:carr S.λy:carr T. y ∈ f {(x)}); -- 2.39.2