From 02ce2fd650a68d04fff678441cca9086c8310005 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Jan 2009 13:01:49 +0000 Subject: [PATCH] Back to step 1: all files that used to pass now pass again. --- .../formal_topology/overlap/categories.ma | 8 +- .../formal_topology/overlap/o-basic_pairs.ma | 18 ++-- .../overlap/o-concrete_spaces.ma | 90 ++++++++++--------- 3 files changed, 59 insertions(+), 57 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 1452652fa..86bc2529c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -286,13 +286,11 @@ record category2 : Type3 ≝ }. notation "'ASSOC'" with precedence 90 for @{'assoc}. -notation "'ASSOC1'" with precedence 90 for @{'assoc1}. -notation "'ASSOC2'" with precedence 90 for @{'assoc2}. interpretation "category2 composition" 'compose x y = (fun22 ___ (comp2 ____) y x). -interpretation "category2 assoc" 'assoc1 = (comp_assoc2 ________). +interpretation "category2 assoc" 'assoc = (comp_assoc2 ________). interpretation "category1 composition" 'compose x y = (fun21 ___ (comp1 ____) y x). -interpretation "category1 assoc" 'assoc1 = (comp_assoc1 ________). +interpretation "category1 assoc" 'assoc = (comp_assoc1 ________). interpretation "category composition" 'compose x y = (fun2 ___ (comp ____) y x). interpretation "category assoc" 'assoc = (comp_assoc ________). @@ -408,4 +406,4 @@ interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y). lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T. intros; apply t; qed. -coercion unary_morphism1_of_arrows1_SET1. \ No newline at end of file +coercion unary_morphism1_of_arrows1_SET1. 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 c5f125ac6..7e0064e46 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 @@ -97,23 +97,23 @@ definition relation_pair_composition: | apply (r1 \sub\f ∘ r \sub\f) | lapply (commute ?? r) as H; lapply (commute ?? r1) as H1; - apply rule (.= ASSOC1); + apply rule (.= ASSOC); apply (.= #‡H1); - apply rule (.= ASSOC1\sup -1); + apply rule (.= ASSOC ^ -1); apply (.= H‡#); - apply rule ASSOC1] + apply rule ASSOC] | intros; change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c)); change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); - apply rule (.= ASSOC1); + apply rule (.= ASSOC); apply (.= #‡e1); apply (.= #‡(commute ?? b')); - apply rule (.= ASSOC1 \sup -1); + apply rule (.= ASSOC \sup -1); apply (.= e‡#); - apply rule (.= ASSOC1); + apply rule (.= ASSOC); apply (.= #‡(commute ?? b')\sup -1); - apply rule (ASSOC1 \sup -1)] + apply rule (ASSOC \sup -1)] qed. definition BP: category2. @@ -125,7 +125,7 @@ definition BP: category2. | intros; change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); - apply rule (ASSOC1‡#); + apply rule (ASSOC‡#); | intros; change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_right2 ????)‡#); @@ -184,4 +184,4 @@ qed. interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y). interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). -*) \ No newline at end of file +*) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index 78ea321a5..6a9d7794d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -37,11 +37,6 @@ intros; constructor 1; | do 2 unfold FunClass_1_OF_Type_OF_setoid21; intros; apply (†(†e));] qed. -(* -lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed. -coercion xxx nocomposites. -*) - lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a'). intros; apply (†(†e)); qed. @@ -61,28 +56,30 @@ record concrete_space : Type2 ≝ }. interpretation "o-concrete space downarrow" 'downarrow x = - (fun_1 __ (downarrow _) x). + (fun11 __ (downarrow _) x). definition bp': concrete_space → basic_pair ≝ λc.bp c. coercion bp'. -lemma setoid_OF_OA : OA → setoid. -intros; apply (oa_P o); +definition bp'': concrete_space → objs2 BP. + intro; apply (bp' c); qed. - -coercion setoid_OF_OA. +coercion bp''. definition binary_downarrow : ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C). intros; constructor 1; -[ intros; apply (↓ c ∧ ↓ c1); -| intros; apply ((†H)‡(†H1));] +[ intros; apply (↓ t ∧ ↓ t1); +| intros; + alias symbol "prop2" = "prop21". + alias symbol "prop1" = "prop11". + apply ((†e)‡(†e1));] qed. -interpretation "concrete_space binary ↓" 'fintersects a b = (fun1 _ _ _ (binary_downarrow _) a b). +interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (binary_downarrow _) a b). -record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ - { rp:> arrows1 ? CS1 CS2; +record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝ + { rp:> arrows2 ? CS1 CS2; respects_converges: ∀b,c. eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (rp\sub\f⎻ b ↓ rp\sub\f⎻ c)); respects_all_covered: @@ -92,69 +89,76 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝ λCS1,CS2,c. rp CS1 CS2 c. - coercion rp'. -definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. +definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2. intros; constructor 1; [ apply (convergent_relation_pair c c1) | constructor 1; [ intros; apply (relation_pair_equality c c1 c2 c3); - | intros 1; apply refl1; - | intros 2; apply sym1; - | intros 3; apply trans1]] + | intros 1; apply refl2; + | intros 2; apply sym2; + | intros 3; apply trans2]] qed. -definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝ - λCS1,CS2,c.rp ?? c. +definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ + λCS1,CS2,c.rp ?? c. coercion rp''. +definition rp''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ + λCS1,CS2,c.rp ?? c. +coercion rp'''. + +definition rp'''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝ + λCS1,CS2,c.rp ?? c. +coercion rp''''. + definition convergent_relation_space_composition: ∀o1,o2,o3: concrete_space. - binary_morphism1 + binary_morphism2 (convergent_relation_space_setoid o1 o2) (convergent_relation_space_setoid o2 o3) (convergent_relation_space_setoid o1 o3). intros; constructor 1; - [ intros; whd in c c1 ⊢ %; + [ intros; whd in t t1 ⊢ %; constructor 1; - [ apply (c1 ∘ c); + [ apply (t1 ∘ t); | intros; - change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2)))); - unfold uncurry_arrows; + change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c)))); + unfold FunClass_1_OF_Type_OF_setoid21; alias symbol "trans" = "trans1". apply (.= († (respects_converges : ?))); - apply (respects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2)); - | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (form o3))))); - unfold uncurry_arrows; + apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c)); + | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3))))); + unfold FunClass_1_OF_Type_OF_setoid21; apply (.= (†(respects_all_covered :?))); - apply rule (respects_all_covered ?? c);] + apply rule (respects_all_covered ?? t);] | intros; change with (b ∘ a = b' ∘ a'); - change in H with (rp'' ?? a = rp'' ?? a'); - change in H1 with (rp'' ?? b = rp ?? b'); - apply ( (H‡H1));] + change in e with (rp'' ?? a = rp'' ?? a'); + change in e1 with (rp'' ?? b = rp ?? b'); + apply (e‡e1);] qed. -definition CSPA: category1. +definition CSPA: category2. constructor 1; [ apply concrete_space | apply convergent_relation_space_setoid | intro; constructor 1; - [ apply id1 + [ apply id2 | intros; apply refl1; | apply refl1] | apply convergent_relation_space_composition - | intros; simplify; + | intros; simplify; whd in a12 a23 a34; change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); - apply ASSOC1; + apply rule ASSOC; | intros; simplify; - change with (a ∘ id1 ? o1 = a); - apply (id_neutral_right1 : ?); + change with (a ∘ id2 ? o1 = a); + apply (id_neutral_right2 : ?); | intros; simplify; - change with (id1 ? o2 ∘ a = a); - apply (id_neutral_left1 : ?);] -qed. + change with (id2 ? o2 ∘ a = a); + apply (id_neutral_left2 : ?);] +qed. \ No newline at end of file -- 2.39.2