From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 9 Sep 2008 17:13:55 +0000 (+0000)
Subject: Reordering of lemmas in proper places.
X-Git-Tag: make_still_working~4795
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd7f52dfd7f80b80368661fce5b58b644c102d7b;hp=52f4a3c6a3e47f1cb6a5912aeff3bcbdb76bc17f;p=helm.git

Reordering of lemmas in proper places.
---

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 63aedcd61..f19e39d2a 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -132,4 +132,43 @@ definition BP: category1.
     change with (a\sub\c ∘ (id_relation_pair o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
     apply ((id_neutral_right1 ????)‡#);
   ]
-qed.
\ No newline at end of file
+qed.
+
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+ λo.extS ?? (rel o).
+
+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; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (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; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (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]]
+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 _)).
diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 462eefd00..d95072cb9 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -14,79 +14,6 @@
 
 include "formal_topology/basic_pairs.ma".
 
-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.
-qed.
-
-interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
-
-definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
-  [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros;
-     [ apply (. #‡(#‡H)); assumption
-     | apply (. #‡(#‡H\sup -1)); assumption]]
-qed.
-
-definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
-
-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;
-  [ intro F; constructor 1; constructor 1;
-    [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
-    | intros; split; intro; cases f (H1 H2); clear f; split;
-       [ apply (. (H‡#)); assumption
-       |3: apply (. (H\sup -1‡#)); assumption
-       |2,4: cases H2 (w H3); exists; [1,3: apply w]
-         [ apply (. (#‡(H‡#))); assumption
-         | apply (. (#‡(H \sup -1‡#))); assumption]]]
-  | intros; split; simplify; intros; cases f; cases H1; split;
-     [1,3: assumption
-     |2,4: exists; [1,3: apply w]
-      [ apply (. (#‡H)‡#); assumption
-      | apply (. (#‡H\sup -1)‡#); assumption]]]
-qed.
-
-definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
- λo.extS ?? (rel o).
-
-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; split; simplify; intros;
-     [ apply (. #‡((†H)‡(†H1))); assumption
-     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersects" 'fintersects U V = (fun1 ___ (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; split; simplify; intros;
-     [ apply (. #‡((†H)‡(†H1))); assumption
-     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (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]]
-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 _)).
-
 record concrete_space : Type ≝
  { bp:> BP;
    converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
@@ -129,53 +56,6 @@ definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1
 
 coercion rp''.
 
-lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
- intros;
- unfold extS; simplify;
- split; simplify;
-  [ intros 2; change with (a ∈ X);
-    cases f; clear f;
-    cases H; clear H;
-    cases x; clear x;
-    change in f2 with (eq1 ? a w);
-    apply (. (f2\sup -1‡#));
-    assumption
-  | intros 2; change in f with (a ∈ X);
-    split;
-     [ whd; exact I 
-     | exists; [ apply a ]
-       split;
-        [ assumption
-        | change with (a = a); apply refl]]]
-qed.
-
-lemma extS_id: ∀o:BP.∀X.extS (concr o) (concr o) (id1 ? o) \sub \c X = X.
- intros;
- unfold extS; simplify;
- split; simplify; intros;
-  [ change with (a ∈ X);
-    cases f; cases H; cases x; change in f3 with (eq1 ? a w);
-    apply (. (f3\sup -1‡#));
-    assumption
-  | change in f with (a ∈ X);
-    split;
-     [ apply I
-     | exists; [apply a]
-       split; [ assumption | change with (a = a); apply refl]]]
-qed.
-
-lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
- intros; unfold extS; simplify; split; intros; simplify; intros;
-  [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
-    cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
-    exists; [apply w1] split [2: assumption] constructor 1; [assumption]
-    exists; [apply w] split; assumption
-  | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
-    cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
-    cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
-    assumption]
-qed.
-
 definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
   binary_morphism1
@@ -222,7 +102,7 @@ definition CSPA: category1.
        apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
                     (equalset_extS_id_X_X ??)\sup -1)));
        apply refl1;
-     | apply (.= (extS_id ??));
+     | apply (.= (equalset_extS_id_X_X ??));
        apply refl1]
   | apply convergent_relation_space_composition
   | intros; simplify;
@@ -237,4 +117,4 @@ definition CSPA: category1.
     change with (a ∘ id1 ? o2 = a);
     apply (.= id_neutral_right1 ????);
     apply refl1]
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index e9989d4f7..72e12aa9d 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -98,4 +98,71 @@ coercion full_subset.
 
 definition setoid1_of_REL: REL → setoid ≝ λS. S.
 
-coercion setoid1_of_REL.
\ No newline at end of file
+coercion 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.
+qed.
+
+interpretation "subset comprehension" 'comprehension s p =
+ (comprehension s (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
+ apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (H‡#)); apply refl1
+  | intros; simplify; split; intros; simplify; intros;
+     [ apply (. #‡(#‡H)); assumption
+     | apply (. #‡(#‡H\sup -1)); 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;
+  [ intro F; constructor 1; constructor 1;
+    [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
+    | intros; split; intro; cases f (H1 H2); clear f; split;
+       [ apply (. (H‡#)); assumption
+       |3: apply (. (H\sup -1‡#)); assumption
+       |2,4: cases H2 (w H3); exists; [1,3: apply w]
+         [ apply (. (#‡(H‡#))); assumption
+         | apply (. (#‡(H \sup -1‡#))); assumption]]]
+  | intros; split; simplify; intros; cases f; cases H1; split;
+     [1,3: assumption
+     |2,4: exists; [1,3: apply w]
+      [ apply (. (#‡H)‡#); assumption
+      | apply (. (#‡H\sup -1)‡#); assumption]]]
+qed.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
+ intros;
+ unfold extS; simplify;
+ split; simplify;
+  [ intros 2; change with (a ∈ X);
+    cases f; clear f;
+    cases H; clear H;
+    cases x; clear x;
+    change in f2 with (eq1 ? a w);
+    apply (. (f2\sup -1‡#));
+    assumption
+  | intros 2; change in f with (a ∈ X);
+    split;
+     [ whd; exact I 
+     | exists; [ apply a ]
+       split;
+        [ assumption
+        | change with (a = a); apply refl]]]
+qed.
+
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+ intros; unfold extS; simplify; split; intros; simplify; intros;
+  [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
+    exists; [apply w1] split [2: assumption] constructor 1; [assumption]
+    exists; [apply w] split; assumption
+  | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+    cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
+    cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
+    assumption]
+qed.
+