From a799c56fa883a1318cb42e185c0d0929b368a961 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Jan 2009 11:57:57 +0000
Subject: [PATCH] unary_morphism_N : seoidN -> setoidN -> setoidN (was ... ->
 setoidN+1) notation for . is now bound to fi instead of if (i.e. rewrites ->
 )

---
 .../formal_topology/overlap/categories.ma     | 14 +++----
 .../overlap/cprop_connectives.ma              |  8 +---
 .../contribs/formal_topology/overlap/depends  |  9 +++--
 .../formal_topology/overlap/relations.ma      | 40 +++++++++----------
 .../overlap/relations_to_o-algebra.ma         | 26 ++++++------
 .../formal_topology/overlap/subsets.ma        | 28 ++++++-------
 6 files changed, 60 insertions(+), 65 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 75ca005c6..2582167dc 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -85,7 +85,7 @@ definition setoid2_of_setoid1: setoid1 → setoid2.
     | apply (trans1 s)]]
 qed.
 
-(*coercion setoid2_of_setoid1.*)
+coercion setoid2_of_setoid1.
 
 (*
 definition Leibniz: Type → setoid.
@@ -171,12 +171,12 @@ definition CPROP: setoid1.
 qed.
 
 alias symbol "eq" = "setoid1 eq".
-definition if': ∀A,B:CPROP. A = B → A → B.
- intros; apply (if ?? e); assumption.
+definition fi': ∀A,B:CPROP. A = B → B → A.
+ intros; apply (fi ?? e); assumption.
 qed.
 
-notation ". r" with precedence 50 for @{'if $r}.
-interpretation "if" 'if r = (if' __ r).
+notation ". r" with precedence 50 for @{'fi $r}.
+interpretation "fi" 'fi r = (fi' __ r).
 
 definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
@@ -269,7 +269,7 @@ interpretation "category assoc" 'assoc = (comp_assoc ________).
 
 (* bug grande come una casa?
    Ma come fa a passare la quantificazione larga??? *)
-definition unary_morphism_setoid: setoid → setoid → setoid1.
+definition unary_morphism_setoid: setoid → setoid → setoid.
  intros;
  constructor 1;
   [ apply (unary_morphism s s1);
@@ -318,7 +318,7 @@ notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Impl
 interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
 interpretation "SET eq" 'eq x y = (eq_rel _ (eq' _) x y).
 
-definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2.
+definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
  intros;
  constructor 1;
   [ apply (unary_morphism1 s s1);
diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
index 4855bf658..aff6849b3 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
@@ -86,18 +86,12 @@ record Iff1 (A,B:CProp1) : CProp1 ≝
    fi1: B → A
  }.
  
-interpretation "logical iff" 'iff x y = (Iff x y).
-
 notation "hvbox(a break ⇔ b)" right associative with precedence 25 for @{'iff1 $a $b}.
+interpretation "logical iff" 'iff x y = (Iff x y).
 interpretation "logical iff type1" 'iff1 x y = (Iff1 x y).
 
 inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
   ex_introT: ∀w:A. P w → exT A P.
-  
-notation "\ll term 19 a, break term 19 b \gg" 
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b = 
-  (ex_introT _ _ a b).
 
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends
index ef49925f3..63392b5b3 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/depends
+++ b/helm/software/matita/contribs/formal_topology/overlap/depends
@@ -1,21 +1,22 @@
 o-basic_pairs.ma o-algebra.ma
 o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
 o-saturations.ma o-algebra.ma
-basic_pairs.ma relations.ma
 saturations.ma relations.ma
+basic_pairs.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
+categories.ma cprop_connectives.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
+subsets.ma categories.ma
 concrete_spaces.ma basic_pairs.ma
 relations.ma subsets.ma
 concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.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
 basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
+basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
 cprop_connectives.ma logic/connectives.ma
 relations_to_o-algebra.ma o-algebra.ma relations.ma
+o-basic_pairs_to_o-basic_topologies.ma concrete_spaces.ma o-basic_pairs.ma o-basic_topologies.ma
 logic/connectives.ma 
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index c4502f3d0..ec7db6df4 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -49,8 +49,8 @@ definition composition:
        apply (λs1:carr A.λs3:carr C.∃s2:carr B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
      | intros;
        split; intro; cases e2 (w H3); clear e2; exists; [1,3: apply w ]
-        [ apply (. (e‡#)‡(#‡e1)); assumption
-        | apply (. ((e \sup -1)‡#)‡(#‡(e1 \sup -1))); assumption]]
+        [ apply (. (e^-1‡#)‡(#‡e1^-1)); assumption
+        | apply (. (e‡#)‡(#‡e1)); assumption]]
   | intros 8; split; intro H2; simplify in H2 ⊢ %;
     cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
     [ lapply (if ?? (e x w) H2) | lapply (fi ?? (e x w) H2) ]
@@ -88,8 +88,8 @@ definition REL: category1.
   |6,7: intros 5; unfold composition; simplify; split; intro;
         unfold setoid1_of_setoid in x y; simplify in x y;
         [1,3: cases e (w H1); clear e; cases H1; clear H1; unfold;
-          [ apply (. (e ^ -1 : eq1 ? w x)‡#); assumption
-          | apply (. #‡(e : eq1 ? w y)); assumption]
+          [ apply (. (e : eq1 ? x w)‡#); assumption
+          | apply (. #‡(e : eq1 ? w y)^-1); assumption]
         |2,4: exists; try assumption; split;
           (* change required to avoid universe inconsistency *)
           change in x with (carr o1); change in y with (carr o2);
@@ -128,9 +128,9 @@ definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
   [ 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
+       apply (. (#‡e1^-1)); 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]]
+       apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
 qed.
 (*
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
@@ -189,12 +189,12 @@ definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:carr U. x ♮r y ∧ x ∈ S });
     intros; simplify; split; intro; cases e1; exists [1,3: apply w]
-     [ apply (. (#‡e)‡#); assumption
-     | apply (. (#‡e ^ -1)‡#); assumption]
+     [ apply (. (#‡e^-1)‡#); assumption
+     | apply (. (#‡e)‡#); assumption]
   | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
-     [ apply (. #‡(#‡e1)); cases x; split; try assumption;
+     [ apply (. #‡(#‡e1^-1)); cases x; split; try assumption;
        apply (if ?? (e ??)); assumption
-     | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
+     | apply (. #‡(#‡e1)); cases x; split; try assumption;
        apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
@@ -203,9 +203,9 @@ definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \s
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:carr U. x ♮r y → x ∈ S});
     intros; simplify; split; intros; apply f;
-     [ apply (. #‡e ^ -1); assumption
-     | apply (. #‡e); assumption]
-  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+     [ apply (. #‡e); assumption
+     | apply (. #‡e ^ -1); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1^ -1); | apply (. #‡e1 )]
     apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
 qed.
 
@@ -214,9 +214,9 @@ definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V)
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S});
     intros; simplify; split; intros; apply f;
-     [ apply (. e ^ -1‡#); assumption
-     | apply (. e‡#); assumption]
-  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+     [ apply (. e ‡#); assumption
+     | apply (. e^ -1‡#); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1 ^ -1); | apply (. #‡e1)]
     apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
 qed.
 
@@ -226,12 +226,12 @@ definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V)
   [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
       exT ? (λy:carr V.x ♮r y ∧ y ∈ S) });
     intros; simplify; split; intro; cases e1; exists [1,3: apply w]
-     [ apply (. (e‡#)‡#); assumption
-     | apply (. (e ^ -1‡#)‡#); assumption]
+     [ apply (. (e ^ -1‡#)‡#); assumption
+     | apply (. (e‡#)‡#); assumption]
   | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
-     [ apply (. #‡(#‡e1)); cases x; split; try assumption;
+     [ apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
        apply (if ?? (e ??)); assumption
-     | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
+     | apply (. #‡(#‡e1)); cases x; split; try assumption;
        apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
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 40db8183f..781514e07 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
@@ -52,7 +52,7 @@ definition SUBSETS: objs1 SET → OAlgebra.
           exists; [apply w] assumption]]
   | intros; intros 2; cases (f (singleton ? a) ?);
      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]
-     | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#));
+     | change in x1 with (a = w); change with (mem A a q); apply (. (x1‡#));
        assumption]]
 qed.
 
@@ -99,21 +99,21 @@ lemma orelation_of_relation_preserves_equality:
  intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
  simplify; whd in o1 o2;
   [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
-    apply (. #‡(e‡#));
+    apply (. #‡(e^-1‡#));
   | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a);
-    apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
     apply (. #‡(e‡#));
-  | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
+  | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
     apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
+  | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
     apply (. #‡(e‡#));
-  | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
+  | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
     apply (. #‡(e ^ -1‡#));
-  | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
+  | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
     apply (. #‡(e‡#));
+  | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
+    apply (. #‡(e ^ -1‡#));
   | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a);
-    apply (. #‡(e ^ -1‡#)); ]
+    apply (. #‡(e‡#)); ]
 qed.
 
 lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
@@ -127,22 +127,22 @@ lemma orelation_of_relation_preserves_identity:
   [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;
   | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
-    change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f;
+    change in f1 with (x = a1); apply (. f1‡#); apply f;
   | alias symbol "and" = "and_morphism".
     change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
-    apply (. f^-1‡#); apply f1;
+    apply (. f‡#); apply f1;
   | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
   | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
-    apply (. f‡#); apply f1;
+    apply (. f^-1‡#); apply f1;
   | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
   | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;
   | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
-    change in f1 with (a1 = y); apply (. f1‡#); apply f;]
+    change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;]
 qed.
 
 lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 3aaf2d3d6..c15ef844e 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -90,10 +90,10 @@ definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
   [ apply (λA:objs1 SET.λU,V:Ω \sup A.(exT2 ? (λx:A.?(*x*) ∈ U) (λx:A.?(*x*) ∈ V) : CProp0))
   | intros;
     constructor 1; intro; cases e2; exists; [1,4: apply w]
-     [ apply (. #‡e); assumption
-     | apply (. #‡e1); assumption
-     | apply (. #‡(e \sup -1)); assumption;
-     | apply (. #‡(e1 \sup -1)); assumption]]
+     [ apply (. #‡e^-1); assumption
+     | apply (. #‡e1^-1); assumption
+     | apply (. #‡e); assumption;
+     | apply (. #‡e1); assumption]]
 qed.
 
 interpretation "overlaps" 'overlaps U V = (fun21 ___ (overlaps _) U V).
@@ -106,8 +106,8 @@ definition intersects:
     intros; simplify; apply (.= (e‡#)‡(e‡#)); apply refl1;
   | intros;
     split; intros 2; simplify in f ⊢ %;
-    [ apply (. (#‡e)‡(#‡e1)); assumption
-    | apply (. (#‡(e \sup -1))‡(#‡(e1 \sup -1))); assumption]]
+    [ apply (. (#‡e^-1)‡(#‡e1^-1)); assumption
+    | apply (. (#‡e)‡(#‡e1)); assumption]]
 qed.
 
 interpretation "intersects" 'intersects U V = (fun21 ___ (intersects _) U V).
@@ -120,8 +120,8 @@ definition union:
     intros; simplify; apply (.= (e‡#)‡(e‡#)); apply refl1
   | intros;
     split; intros 2; simplify in f ⊢ %;
-    [ apply (. (#‡e)‡(#‡e1)); assumption
-    | apply (. (#‡(e \sup -1))‡(#‡(e1 \sup -1))); assumption]]
+    [ apply (. (#‡e^-1)‡(#‡e1^-1)); assumption
+    | apply (. (#‡e)‡(#‡e1)); assumption]]
 qed.
 
 interpretation "union" 'union U V = (fun21 ___ (union _) U V).
@@ -146,11 +146,11 @@ definition big_intersects:
  intros; constructor 1;
   [ intro; whd; whd in I;
     apply ({x | ∀i:I. x ∈ t i});
-    simplify; intros; split; intros; [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
+    simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ]
     apply f;
   | intros; split; intros 2; simplify in f ⊢ %; intro;
-     [ apply (. (#‡(e i))); apply f;
-     | apply (. (#‡(e i)\sup -1)); apply f]]
+     [ apply (. (#‡(e i)^-1)); apply f;
+     | apply (. (#‡e i)); apply f]]
 qed.
 
 definition big_union:
@@ -159,9 +159,9 @@ definition big_union:
   [ intro; whd; whd in A; whd in I;
     apply ({x | ∃i:carr I. x ∈ t i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
-    [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
+    [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
     apply x;
   | intros; split; intros 2; simplify in f ⊢ %; cases f; clear f; exists; [1,3:apply w]
-     [ apply (. (#‡(e w))); apply x;
-     | apply (. (#‡(e w)\sup -1)); apply x]]
+     [ apply (. (#‡(e w)^-1)); apply x;
+     | apply (. (#‡e w)); apply x]]
 qed.
-- 
2.39.2