From: Enrico Tassi Date: Mon, 22 Dec 2008 14:25:53 +0000 (+0000) Subject: some work X-Git-Tag: make_still_working~4336 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fc511bf7be55ad8f545f5b08b0833f80ecca07b;p=helm.git some work --- 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 9cadd514c..78372e72f 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -22,23 +22,23 @@ constructor 1; [apply bool] constructor 1; [ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]); | whd; simplify; intros; cases x; apply I; | whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption; -| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; try assumption; apply I] +| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; + try assumption; apply I] qed. -definition hint: objs1 SET → setoid. - intros; apply o; -qed. +definition setoid_OF_SET: objs1 SET → setoid. + intros; apply o; qed. -coercion hint. +coercion setoid_OF_SET. lemma IF_THEN_ELSE_p : ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → (λm.match m with [ true ⇒ a | false ⇒ b ]) x = (λm.match m with [ true ⇒ a | false ⇒ b ]) y. +whd in ⊢ (?→?→?→%→?); intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H; qed. - interpretation "unary morphism comprehension with no proof" 'comprehension T P = (mk_unary_morphism T _ P _). @@ -50,7 +50,6 @@ for @{ 'comprehension_by $s (λ${ident i}:$_. $p) $by}. interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p = (mk_unary_morphism s _ f p). - record OAlgebra : Type := { oa_P :> SET; oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *) @@ -70,8 +69,7 @@ record OAlgebra : Type := { oa_overlap_preservers_meet: ∀p,q.oa_overlap p q → oa_overlap p (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q }); - (*(oa_meet BOOL (if_then_else oa_P p q));*) - oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *) + oa_join_split: ∀I:SET.∀p.∀q:arrows1 SET I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i); (*oa_base : setoid; oa_enum : ums oa_base oa_P; @@ -122,33 +120,25 @@ interpretation "o-algebra join with explicit function" 'oa_join_mk f = (fun_1 __ (oa_join __) (mk_unary_morphism _ _ f _)). record ORelation (P,Q : OAlgebra) : Type ≝ { - or_f :> arrows1 SET P Q; - or_f_minus_star : arrows1 SET P Q; - or_f_star : arrows1 SET Q P; - or_f_minus : arrows1 SET Q P; - or_prop1 : ∀p,q. (or_f p ≤ q) = (p ≤ or_f_star q); - or_prop2 : ∀p,q. (or_f_minus p ≤ q) = (p ≤ or_f_minus_star q); - or_prop3 : ∀p,q. (or_f p >< q) = (p >< or_f_minus q) + or_f_ : arrows1 SET P Q; + or_f_minus_star_ : arrows1 SET P Q; + or_f_star_ : arrows1 SET Q P; + or_f_minus_ : arrows1 SET Q P; + or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q); + or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q); + or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q) }. -notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}. -notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}. -interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r). - -notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}. -notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}. -interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r). - -notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. -notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. -interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r). definition ORelation_setoid : OAlgebra → OAlgebra → setoid1. intros (P Q); constructor 1; [ apply (ORelation P Q); | constructor 1; - [ apply (λp,q. And4 (eq1 ? p⎻* q⎻* ) (eq1 ? p⎻ q⎻) (eq1 ? p q) (eq1 ? p* q* )); + [ apply (λp,q. And4 (eq1 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) + (eq1 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) + (eq1 ? (or_f_ ?? p) (or_f_ ?? q)) + (eq1 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); | whd; simplify; intros; repeat split; intros; apply refl1; | whd; simplify; intros; cases H; clear H; split; intro a; apply sym; generalize in match a;assumption; @@ -159,43 +149,87 @@ constructor 1; | apply (.= (H5 a)); apply H9;]]] qed. -lemma hint1 : ∀P,Q. ORelation_setoid P Q → arrows1 SET P Q. intros; apply (or_f ?? c);qed. -coercion hint1. - -lemma hint3 : ∀P,Q. arrows1 SET P Q → P ⇒ Q. intros; apply c;qed. -coercion hint3. - -lemma hint2: OAlgebra → setoid. intros; apply (oa_P o). qed. -coercion hint2. - -definition or_f_minus_star2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. +definition or_f_minus_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. intros; constructor 1; - [ apply or_f_minus_star; + [ apply or_f_minus_star_; | intros; cases H; assumption] qed. -definition or_f2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. +definition or_f: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. intros; constructor 1; - [ apply or_f; + [ apply or_f_; | intros; cases H; assumption] qed. -definition or_f_minus2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. +coercion or_f. + +definition or_f_minus: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. intros; constructor 1; - [ apply or_f_minus; + [ apply or_f_minus_; | intros; cases H; assumption] qed. -definition or_f_star2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. +definition or_f_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. intros; constructor 1; - [ apply or_f_star; + [ apply or_f_star_; | intros; cases H; assumption] qed. -interpretation "o-relation f⎻* 2" 'OR_f_minus_star r = (fun_1 __ (or_f_minus_star2 _ _) r). -interpretation "o-relation f⎻ 2" 'OR_f_minus r = (fun_1 __ (or_f_minus2 _ _) r). -interpretation "o-relation f* 2" 'OR_f_star r = (fun_1 __ (or_f_star2 _ _) r). -coercion or_f2. +lemma arrows1_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → arrows1 SET P Q. +intros; apply (or_f ?? c); +qed. + +coercion arrows1_OF_ORelation_setoid nocomposites. + +lemma umorphism_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. +intros; apply (or_f ?? c); +qed. + +coercion umorphism_OF_ORelation_setoid. + + +lemma uncurry_arrows : ∀B,C. arrows1 SET B C → B → C. +intros; apply ((fun_1 ?? c) t); +qed. + +coercion uncurry_arrows 1. + +lemma hint3 : ∀P,Q. arrows1 SET P Q → P ⇒ Q. intros; apply c;qed. +coercion hint3 nocomposites. + +(* +lemma hint2: OAlgebra → setoid. intros; apply (oa_P o). qed. +coercion hint2 nocomposites. +*) + + +notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}. +notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}. + +notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}. +notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}. + +notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. +notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. + +interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun_1 __ (or_f_minus_star _ _) r). +interpretation "o-relation f⎻" 'OR_f_minus r = (fun_1 __ (or_f_minus _ _) r). +interpretation "o-relation f*" 'OR_f_star r = (fun_1 __ (or_f_star _ _) r). + +definition or_prop1 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q. + (F p ≤ q) = (p ≤ F* q). +intros; apply (or_prop1_ ?? F p q); +qed. + +definition or_prop2 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q. + (F⎻ p ≤ q) = (p ≤ F⎻* q). +intros; apply (or_prop2_ ?? F p q); +qed. + +definition or_prop3 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q. + (F p >< q) = (p >< F⎻ q). +intros; apply (or_prop3_ ?? F p q); +qed. definition ORelation_composition : ∀P,Q,R. binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R). @@ -203,29 +237,26 @@ intros; constructor 1; [ intros (F G); constructor 1; - [ apply (or_f2 ?? G ∘ or_f2 ?? F); - | alias symbol "compose" = "category1 composition". - apply (G⎻* ∘ F⎻* ); + [ lapply (G ∘ F); + apply (G ∘ F); + | apply (G⎻* ∘ F⎻* ); | apply (F* ∘ G* ); | apply (F⎻ ∘ G⎻); - | intros; - alias symbol "eq" = "setoid1 eq". + | intros; change with ((G (F p) ≤ q) = (p ≤ (F* (G* q)))); - apply (.= or_prop1 ??? (F p) ?); - apply (.= or_prop1 ??? p ?); - apply refl1 - | intros; alias symbol "eq" = "setoid1 eq". + apply (.= (or_prop1 :?)); + apply (or_prop1 :?); + | intros; change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q)))); - alias symbol "trans" = "trans1". - apply (.= or_prop2 ?? F ??); - apply (.= or_prop2 ?? G ??); - apply refl1; + apply (.= (or_prop2 :?)); + apply or_prop2 ; | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q)))); - apply (.= or_prop3 ??? (F p) ?); - apply (.= or_prop3 ??? p ?); - apply refl1 + apply (.= (or_prop3 :?)); + apply or_prop3; ] -| intros; split; simplify; [1,3: apply ((†H)‡(†H1)); | 2,4: apply ((†H1)‡(†H));]] +| intros; split; simplify; + [1,3: unfold arrows1_OF_ORelation_setoid; apply ((†H)‡(†H1)); + |2,4: apply ((†H1)‡(†H));]] qed. definition OA : category1. @@ -236,12 +267,12 @@ split; [1,2,3,4: apply id1; |5,6,7:intros; apply refl1;] | apply ORelation_composition; -| intros; split; - [ apply (comp_assoc1 ????? (a12⎻* ) (a23⎻* ) (a34⎻* )); - | alias symbol "invert" = "setoid1 symmetry". - apply ((comp_assoc1 ????? (a34⎻) (a23⎻) (a12⎻)) \sup -1); - | apply (comp_assoc1 ????? a12 a23 a34); - | apply ((comp_assoc1 ????? (a34* ) (a23* ) (a12* )) \sup -1);] +| intros (P Q R S F G H); split; + [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* )); + apply (comp_assoc1 ????? (F⎻* ) (G⎻* ) (H⎻* )); + | apply ((comp_assoc1 ????? (H⎻) (G⎻) (F⎻))^-1); + | apply ((comp_assoc1 ????? F G H)^-1); + | apply ((comp_assoc1 ????? H* G* F* ));] | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1; | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;] qed. \ 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 cbdf68fdd..633f0b89e 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 @@ -17,34 +17,37 @@ include "o-saturations.ma". notation "□ \sub b" non associative with precedence 90 for @{'box $b}. notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}. -interpretation "Universal image ⊩⎻*" 'box x = (or_f_minus_star _ _ (rel x)). +interpretation "Universal image ⊩⎻*" 'box x = (fun_1 _ _ (or_f_minus_star _ _) (rel x)). notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}. notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}. -interpretation "Existential image ⊩" 'diamond x = (or_f _ _ (rel x)). +interpretation "Existential image ⊩" 'diamond x = (fun_1 _ _ (or_f _ _) (rel x)). notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}. notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}. -interpretation "Universal pre-image ⊩*" 'rest x = (or_f_star _ _ (rel x)). +interpretation "Universal pre-image ⊩*" 'rest x = (fun_1 _ _ (or_f_star _ _) (rel x)). 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 = (or_f_minus _ _ (rel x)). +interpretation "Existential pre-image ⊩⎻" 'ext x = (fun_1 _ _ (or_f_minus _ _) (rel x)). + +lemma hint : ∀p,q.arrows1 OA p q → ORelation_setoid p q. +intros; assumption; +qed. + +coercion hint nocomposites. definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)). intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); - | do 2 unfold FunClass_1_OF_carr1; intros; apply (†(†H));] + | do 2 unfold uncurry_arrows; intros; apply (†(†H));] qed. lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed. -coercion xxx. +coercion xxx nocomposites. -definition d_p_i : - ∀S,I:SET.∀d:unary_morphism S S.∀p:arrows1 SET I S.arrows1 SET I S. -intros; constructor 1; - [ apply (λi:I. u (c i)); - | unfold FunClass_1_OF_carr1; intros; apply (†(†H));]. +lemma down_p : ∀S,I:SET.∀u:S⇒S.∀c:arrows1 SET I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a'). +intros; unfold uncurry_arrows; apply (†(†H)); qed. alias symbol "eq" = "setoid eq". @@ -58,12 +61,13 @@ record concrete_space : Type ≝ (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2))); all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp); il2: ∀I:SET.∀p:arrows1 SET I (oa_P (form bp)). - downarrow (oa_join ? I (d_p_i ?? downarrow p)) = - oa_join ? I (d_p_i ?? downarrow p); + downarrow (∨ { x ∈ I | downarrow (p x) | down_p ???? }) = + ∨ { x ∈ I | downarrow (p x) | down_p ???? }; il1: ∀q.downarrow (A ? q) = A ? q }. -interpretation "o-concrete space downarrow" 'downarrow x = (fun_1 __ (downarrow _) x). +interpretation "o-concrete space downarrow" 'downarrow x = + (fun_1 __ (downarrow _) x). definition bp': concrete_space → basic_pair ≝ λc.bp c. coercion bp'.