]> matita.cs.unibo.it Git - helm.git/commitdiff
Some work on concrete spaces.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 17:28:59 +0000 (17:28 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 17:28:59 +0000 (17:28 +0000)
helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/overlap/depends
helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/overlap/relations.ma

index 97e386c1545e1b3b8af6122a94843f7ed2e418ef..d0e4ffd4a67607650efe5cbc7127fc1dbc333b2d 100644 (file)
@@ -139,49 +139,50 @@ definition BP: category1.
     apply ((id_neutral_left1 ????)‡#);]
 qed.
 
-(*
 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
  intros; constructor 1;
   [ apply (ext ? ? (rel o));
   | intros;
-    apply (.= #‡H);
+    apply (.= #‡e);
     apply refl1]
 qed.
 
-definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
- λo.extS ?? (rel o).
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+  [ apply (minus_image ?? (rel o));
+  | intros; apply (#‡e); ]
+qed.
 
 definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
  intros (o); constructor 1;
   [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
-    intros; simplify; apply (.= (†H)‡#); apply refl1
+    intros; simplify; apply (.= (†e)‡#); apply refl1
   | intros; split; simplify; intros;
-     [ apply (. #‡((†H)‡(†H1))); assumption
-     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+     [ apply (. #‡((†e)‡(†e1))); assumption
+     | apply (. #‡((†e\sup -1)‡(†e1\sup -1))); assumption]]
 qed.
 
-interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
+interpretation "fintersects" 'fintersects U V = (fun21 ___ (fintersects _) U V).
 
 definition fintersectsS:
  ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
  intros (o); constructor 1;
   [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
-    intros; simplify; apply (.= (†H)‡#); apply refl1
+    intros; simplify; apply (.= (†e)‡#); apply refl1
   | intros; split; simplify; intros;
-     [ apply (. #‡((†H)‡(†H1))); assumption
-     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+     [ apply (. #‡((†e)‡(†e1))); assumption
+     | apply (. #‡((†e\sup -1)‡(†e1\sup -1))); assumption]]
 qed.
 
-interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
+interpretation "fintersectsS" 'fintersects U V = (fun21 ___ (fintersectsS _) U V).
 
 definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
  intros (o); constructor 1;
-  [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
-  | intros; split; intros; cases H2; exists [1,3: apply w]
-     [ apply (. (#‡H1)‡(H‡#)); assumption
-     | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+  [ apply (λx:concr o.λS: Ω \sup (form o).∃y:carr (form o).y ∈ S ∧ x ⊩ y);
+  | intros; split; intros; cases e2; exists [1,3: apply w]
+     [ apply (. (#‡e1)‡(e‡#)); assumption
+     | apply (. (#‡e1 \sup -1)‡(e \sup -1‡#)); assumption]]
 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 _)).
-*)
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun21 (concr _) __ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun21 ___ (relS _)).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
new file mode 100644 (file)
index 0000000..ff6774b
--- /dev/null
@@ -0,0 +1,124 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_pairs.ma".
+
+(* full_subset e' una coercion che non mette piu' *)
+record concrete_space : Type1 ≝
+ { bp:> BP;
+   converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+   all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
+ }.
+
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+coercion bp'.
+
+definition bp'': concrete_space → objs1 BP ≝ λc.bp c.
+coercion bp''.
+
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> arrows1 ? CS1 CS2;
+   respects_converges:
+    ∀b,c.
+     minus_image ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+     BPextS CS1 ((minus_image ?? rp \sub\f b) ↓ (minus_image ?? rp \sub\f c));
+   respects_all_covered:
+    minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1))
+ }.
+(*
+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.
+ 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]]
+qed.
+
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
+ λCS1,CS2,c.rp ?? c.
+
+coercion rp''.
+
+definition convergent_relation_space_composition:
+ ∀o1,o2,o3: concrete_space.
+  binary_morphism1
+   (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 ⊢ %;
+       constructor 1;
+        [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+        | intros;
+          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+            with (c1 \sub \f ∘ c \sub \f);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+            with (c1 \sub \f ∘ c \sub \f);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_converges ?????)));
+          apply (.= (respects_converges ?????));
+          apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
+          apply refl1;
+        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_all_covered ???)));
+          apply (.= respects_all_covered ???);
+          apply refl1]
+     | 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));
+       apply refl1]
+qed.
+
+definition CSPA: category1.
+ constructor 1;
+  [ apply concrete_space
+  | apply convergent_relation_space_setoid
+  | intro; constructor 1;
+     [ apply id1
+     | intros;
+       unfold id; simplify;
+       apply (.= (equalset_extS_id_X_X ??));
+       apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
+                    (equalset_extS_id_X_X ??)\sup -1)));
+       apply refl1;
+     | apply (.= (equalset_extS_id_X_X ??));
+       apply refl1]
+  | apply convergent_relation_space_composition
+  | intros; simplify;
+    change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
+    apply (.= ASSOC1);
+    apply refl1
+  | intros; simplify;
+    change with (a ∘ id1 ? o1 = a);
+    apply (.= id_neutral_right1 ????);
+    apply refl1
+  | intros; simplify;
+    change with (id1 ? o2 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
+    apply refl1]
+qed.
+*)
\ No newline at end of file
index 1295f994d34cc3332977ceedb78e31031fdb5559..50152aeabd0e4bc02cc423a48c93688e1d049df9 100644 (file)
@@ -6,9 +6,11 @@ saturations.ma relations.ma
 o-algebra.ma categories.ma
 o-formal_topologies.ma o-basic_topologies.ma
 categories.ma cprop_connectives.ma
+formal_topologies.ma basic_topologies.ma
 saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
 subsets.ma categories.ma
 basic_topologies.ma relations.ma saturations.ma
+concrete_spaces.ma basic_pairs.ma
 relations.ma subsets.ma
 o-basic_topologies.ma o-algebra.ma o-saturations.ma
 basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
new file mode 100644 (file)
index 0000000..eb2b0b1
--- /dev/null
@@ -0,0 +1,121 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_topologies.ma".
+
+definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
+
+coercion btop_carr.
+
+definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
+
+coercion btop_carr'.
+
+definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
+    intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
+    split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
+  | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
+    try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
+qed.
+
+interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+
+definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λU,V. ↓U ∩ ↓V);
+  | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+
+record formal_topology: Type ≝
+ { bt:> BTop;
+   converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
+ }.
+
+definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
+
+coercion bt'.
+
+definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
+  | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+
+record formal_map (S,T: formal_topology) : Type ≝
+ { cr:> continuous_relation_setoid S T;
+   C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
+   C2: extS ?? cr T = S
+ }.
+
+definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
+ λFT1,FT2,c. cr FT1 FT2 c.
+
+coercion cr'.
+
+definition formal_map_setoid: formal_topology → formal_topology → setoid1.
+ intros (S T); constructor 1;
+  [ apply (formal_map S T);
+  | constructor 1;
+     [ apply (λf,f1: formal_map S T.f=f1);
+     | simplify; intros 1; apply refl1
+     | simplify; intros 2; apply sym1
+     | simplify; intros 3; apply trans1]]
+qed.
+
+definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
+ λFT1,FT2,c.cr ?? c.
+
+coercion cr''.
+
+definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
+ λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
+
+coercion cr'''.
+
+axiom C1':
+ ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
+  extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
+
+definition formal_map_composition:
+ ∀o1,o2,o3: formal_topology.
+  binary_morphism1
+   (formal_map_setoid o1 o2)
+   (formal_map_setoid o2 o3)
+   (formal_map_setoid o1 o3).
+ intros; constructor 1;
+  [ intros; whd in c c1; constructor 1;
+     [ apply (comp1 BTop ??? c c1);
+     | intros;
+       apply (.= (extS_com ??? c c1 ?));
+       apply (.= †(C1 ?????));
+       apply (.= (C1' ?????));
+       apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
+       apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
+       apply (.= (extS_singleton ????)‡(extS_singleton ????));
+       apply refl1;
+     | apply (.= (extS_com ??? c c1 ?));
+       apply (.= (†(C2 ???)));
+       apply (.= (C2 ???));
+       apply refl1;]
+  | intros; simplify;
+    change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
+    apply prop1; assumption]
+qed.
+
index dc3c091bbfe49d75ba005997b44ef38b386db4d6..c4502f3d080b61874360cfb4e650bde1f3b99694 100644 (file)
@@ -96,14 +96,12 @@ definition REL: category1.
           first [apply refl | assumption]]]
 qed.
 
-(*
 definition full_subset: ∀s:REL. Ω \sup s.
  apply (λs.{x | True});
  intros; simplify; split; intro; assumption.
 qed.
 
 coercion full_subset.
-*)
 
 definition setoid1_of_REL: REL → setoid ≝ λS. S.
 coercion setoid1_of_REL.
@@ -114,23 +112,27 @@ lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 →
 qed.
 coercion Type_OF_setoid1_of_REL.
 
-(*
-definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
- intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+ intros; simplify;
+ alias symbol "trans" = "trans1".
+ alias symbol "prop1" = "prop11".
+ apply (.= †e); apply refl1.
 qed.
 
 interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
+ (comprehension s (mk_unary_morphism1 __ p _)).
 
 definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
- apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
-  [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
-     [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
-     | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (e‡#)); apply refl1
+  | intros; simplify; split; intros; simplify;
+     [ change with (∀x. x ♮a b → x ♮a' b'); intros;
+       apply (. (#‡e1)); whd in e; apply (if ?? (e ??)); assumption
+     | change with (∀x. x ♮a' b' → x ♮a b); intros;
+       apply (. (#‡e1\sup -1)); whd in e; apply (fi ?? (e ??));assumption]]
 qed.
-
+(*
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
  intros (X S r); constructor 1;