From 7db606e36d5c17681a62cf5186bafde65cbfa3db Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Jan 2009 18:47:38 +0000
Subject: [PATCH] The new coercion from SET to Type0 with higher priority
 really helps a lot: almost all explicit occurrences of carr have been
 removed.

---
 .../formal_topology/overlap/basic_pairs.ma    |  2 +-
 .../formal_topology/overlap/categories.ma     |  3 ++
 .../formal_topology/overlap/o-algebra.ma      | 16 +----------
 .../formal_topology/overlap/relations.ma      | 14 ++++------
 .../overlap/relations_to_o-algebra.ma         | 28 +++++++------------
 .../formal_topology/overlap/subsets.ma        |  2 +-
 6 files changed, 22 insertions(+), 43 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 9d2818727..2635d51ce 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -178,7 +178,7 @@ 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:carr (form o).y ∈ S ∧ x ⊩ y);
+  [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩ y);
   | intros; split; intros; cases e2; exists [1,3: apply w]
      [ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
      | apply (. (#‡e1)‡(e‡#)); assumption]]
diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index d83fd0319..84cde74dd 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -320,6 +320,9 @@ definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1
 qed.
 coercion Type_OF_setoid1_of_carr.
 
+definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
+coercion carr'. (* we prefer the lower carrier projection *)
+
 interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
 
 lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.
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 6f58f53b2..838876f93 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -48,16 +48,12 @@ interpretation "unary morphism comprehension with proof" 'comprehension_by s \et
 interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p = 
   (mk_unary_morphism1 s _ f p).
 
-definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
-coercion carr'. (* we prefer the lower carrier projection *)
-
 (* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
    lattices, Definizione 0.9 *)
 (* USARE L'ESISTENZIALE DEBOLE *)
-(*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*)
 record OAlgebra : Type2 := {
   oa_P :> SET1;
-  oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *)
+  oa_leq : binary_morphism1 oa_P oa_P CPROP;
   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
   oa_meet: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P;
   oa_join: ∀I:SET.unary_morphism2 (I ⇒ oa_P) oa_P;
@@ -67,7 +63,6 @@ record OAlgebra : Type2 := {
   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
-  (* Errore: = in oa_meet_inf e oa_join_sup *)
   oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
   oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = ∀i:I.oa_leq (p_i i) p;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
@@ -75,7 +70,6 @@ record OAlgebra : Type2 := {
   oa_overlap_preserves_meet_: 
       ∀p,q:oa_P.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 });
-  (* ⇔ deve essere =, l'esiste debole *)
   oa_join_split:
       ∀I:SET.∀p.∀q:I ⇒ oa_P.
        oa_overlap p (oa_join I q) = ∃i:I.oa_overlap p (q i);
@@ -100,16 +94,8 @@ non associative with precedence 50 for @{ 'oa_meet $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
 
-(*
-notation < "hovbox(a ∧ b)" left associative with precedence 35
-for @{ 'oa_meet_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-*)
 notation > "hovbox(∧ f)" non associative with precedence 60
 for @{ 'oa_meet $f }.
-(*
-notation > "hovbox(a ∧ b)" left associative with precedence 50
-for @{ 'oa_meet (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
-*)
 interpretation "o-algebra meet" 'oa_meet f = 
   (fun12 __ (oa_meet __) f).
 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index ec7db6df4..5678b6a89 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -44,9 +44,7 @@ definition composition:
   [ intros (R12 R23);
     constructor 1;
     constructor 1;
-     [ alias symbol "and" = "and_morphism".
-       (* carr to avoid universe inconsistency *)  
-       apply (λs1:carr A.λs3:carr C.∃s2:carr B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+     [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
      | intros;
        split; intro; cases e2 (w H3); clear e2; exists; [1,3: apply w ]
         [ apply (. (e^-1‡#)‡(#‡e1^-1)); assumption
@@ -107,7 +105,7 @@ definition setoid1_of_REL: REL → setoid ≝ λS. S.
 coercion setoid1_of_REL.
 
 lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*).
- [ apply (setoid1_of_SET o1);
+ [ apply rule o1;
  | intros; apply t;]
 qed.
 coercion Type_OF_setoid1_of_REL.
@@ -187,7 +185,7 @@ qed.
 (* the same as ⋄ for a basic pair *)
 definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:carr U. x ♮r y ∧ x ∈ S });
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S });
     intros; simplify; split; intro; cases e1; exists [1,3: apply w]
      [ apply (. (#‡e^-1)‡#); assumption
      | apply (. (#‡e)‡#); assumption]
@@ -201,7 +199,7 @@ qed.
 (* the same as □ for a basic pair *)
 definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:carr U. x ♮r y → x ∈ S});
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
     intros; simplify; split; intros; apply f;
      [ apply (. #‡e); assumption
      | apply (. #‡e ^ -1); assumption]
@@ -212,7 +210,7 @@ qed.
 (* the same as Rest for a basic pair *)
 definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S});
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S});
     intros; simplify; split; intros; apply f;
      [ apply (. e ‡#); assumption
      | apply (. e^ -1‡#); assumption]
@@ -224,7 +222,7 @@ qed.
 definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
  intros; constructor 1;
   [ 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) });
+      exT ? (λy:V.x ♮r y ∧ y ∈ S) });
     intros; simplify; split; intro; cases e1; exists [1,3: apply w]
      [ apply (. (e ^ -1‡#)‡#); assumption
      | apply (. (e‡#)‡#); assumption]
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 781514e07..e661fbfd0 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
@@ -30,26 +30,18 @@ definition SUBSETS: objs1 SET → OAlgebra.
   | intros; whd; split; assumption
   | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption]
   | intros; cases f; exists [apply w] assumption
-  | intros; intros 2; apply (f ? f1 i);
-  | intros; intros 2; apply f;
-    (* senza questa change, universe inconsistency *)
-    whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
-    exists; [apply i] assumption;
+  | intros; split; [ intros 4; apply (f ? f1 i); | intros 3; intro; apply (f i ? f1); ]
+  | intros; split;
+     [ intros 4; apply f; exists; [apply i] assumption;
+     | intros 3; intros; cases f1; apply (f w a x); ]
   | intros 3; cases f;
   | intros 3; constructor 1;
   | intros; cases f; exists; [apply w]
      [ assumption
      | whd; intros; cases i; simplify; assumption]
   | intros; split; intro;
-     [ cases f; cases x1;
-       (* senza questa change, universe inconsistency *)
-       change in ⊢ (? ? (λ_:%.?)) with (carr I);
-       exists [apply w1] exists [apply w] assumption;
-     | cases e; cases x; exists; [apply w1]
-        [ assumption
-        | (* senza questa change, universe inconsistency *)
-          whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
-          exists; [apply w] assumption]]
+     [ cases f; cases x1; exists [apply w1] exists [apply w] assumption;
+     | cases e; cases x; exists; [apply w1] [ assumption | 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‡#));
@@ -129,15 +121,15 @@ lemma orelation_of_relation_preserves_identity:
   | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
     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);
+    change with ((∃y: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‡#); apply f1;
-  | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
+  | change with (a1 ∈ a → ∃y: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);
+  | change with ((∃x: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^-1‡#); apply f1;
-  | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
+  | change with (a1 ∈ a → ∃x: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;
diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index c15ef844e..eaa6954a4 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -157,7 +157,7 @@ definition big_union:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
  intros; constructor 1;
   [ intro; whd; whd in A; whd in I;
-    apply ({x | ∃i:carr I. x ∈ t i });
+    apply ({x | ∃i:I. x ∈ t i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
     apply x;
-- 
2.39.2