eq -> eq0 renaming

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 58fe2184456dc39dddfa35854563ac686c960b82..c159be66a6633198187c9ee9cd5ae79ed888b131 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -16,25 +16,15 @@ include "logic/connectives.ma".
 include "properties/relations.ma".
 include "hints_declaration.ma".
 
-(*
-notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
-for @{ 'eqID $a $b }.
-
-notation > "hvbox(a break =_\ID b)" non associative with precedence 45
-for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
-
-interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
-*)
-
 nrecord setoid : Type[1] ≝
  { carr:> Type[0];
-   eq: equivalence_relation carr
+   eq0: equivalence_relation carr
  }.
 
-interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
-for @{ eq_rel ? (eq ?) $a $b }.
+for @{ eq_rel ? (eq0 ?) $a $b }.
 
 interpretation "setoid symmetry" 'invert r = (sym ???? r).
 notation ".= r" with precedence 50 for @{'trans $r}.
@@ -42,7 +32,7 @@ interpretation "trans" 'trans r = (trans ????? r).
 
 nrecord unary_morphism (A,B: setoid) : Type[0] ≝
  { fun1:1> A → B;
-   prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
+   prop1: ∀a,a'. a = a' → fun1 a = fun1 a'
  }.
 
 notation "† c" with precedence 90 for @{'prop1 $c }.
@@ -59,13 +49,16 @@ ndefinition unary_morph_setoid : setoid → setoid → setoid.
 ##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; napply (trans … (H1 …) (H2 …)); //; ##]
 nqed.
 
-unification hint 0
- (∀o1,o2. (λx,y:Type[0].True) (carr (unary_morph_setoid o1 o2)) (unary_morphism o1 o2)).
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ o1,o2 ; 
+     X ≟ unary_morph_setoid o1 o2
+  (* ------------------------------ *) ⊢ 
+     carr X ≡ unary_morphism o1 o2.
 
 interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
 
 nlemma unary_morph_eq: ∀A,B.∀f,g: unary_morphism A B. (∀x. f x = g x) → f=g.
-/3/. nqed.
+#A B f g H x1 x2 E; napply (.= †E); napply H; nqed.
 
 nlemma mk_binary_morphism:
  ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
@@ -88,8 +81,8 @@ ndefinition comp_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o1 o2;
-   R ≟ (mk_unary_morphism ?? (composition … f g)
-        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g)))
+   R ≟ mk_unary_morphism ?? (composition … f g)
+        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
                               fun1 ?? R ≡ (composition … f g).
 
@@ -100,4 +93,4 @@ ndefinition comp_binary_morphisms:
 #o1; #o2; #o3; napply mk_binary_morphism
  [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
  | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
-nqed.
\ No newline at end of file
+nqed.

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 69e0958744de4f83c3257f88ad3b8e4ac78ef8fa..4aac43e448e107e9559a528938d113a2a8c96443 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -25,7 +25,7 @@ ndefinition setoid1_of_setoid: setoid → setoid1.
  #s; napply mk_setoid1
   [ napply (carr s)
   | napply (mk_equivalence_relation1 s)
-    [ napply eq
+    [ napply eq0
     | napply refl
     | napply sym
     | napply trans]##]
@@ -36,12 +36,12 @@ nqed.
 (*prefer coercion Type_OF_setoid.*)
 
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
-interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
 notation > "hvbox(a break =_12 b)" non associative with precedence 45
 for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
-for @{ eq_rel ? (eq ?) $a $b }.
+for @{ eq_rel ? (eq0 ?) $a $b }.
 notation > "hvbox(a break =_1 b)" non associative with precedence 45
 for @{ eq_rel1 ? (eq1 ?) $a $b }.
 
@@ -111,4 +111,4 @@ ndefinition comp1_binary_morphisms:
 #o1; #o2; #o3; napply mk_binary_morphism1
  [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
  | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
-nqed.
\ No newline at end of file
+nqed.

diff --git a/helm/software/matita/nlibrary/sets/setoids2.ma b/helm/software/matita/nlibrary/sets/setoids2.ma
index 578503f6ced96fd59baab50cee6065432b028446..34036a48b37becddc01b1538ab9d4e46e3d831e9 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids2.ma
+++ b/helm/software/matita/nlibrary/sets/setoids2.ma
@@ -40,7 +40,7 @@ notation > "hvbox(a break =_12 b)" non associative with precedence 45
 for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
 *)
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
-for @{ eq_rel ? (eq ?) $a $b }.
+for @{ eq_rel ? (eq0 ?) $a $b }.
 notation > "hvbox(a break =_1 b)" non associative with precedence 45
 for @{ eq_rel1 ? (eq1 ?) $a $b }.
 notation > "hvbox(a break =_2 b)" non associative with precedence 45

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index d4a13507c79bf6790b4d8dce4da16266dc8fb9cc..9fd5b7eeb77c78d77de0fb5b220f42e93f84779d 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -84,7 +84,7 @@ nrecord ext_powerclass (A: setoid) : Type[1] ≝
 notation > "𝛀 ^ term 90 A" non associative with precedence 70 
 for @{ 'ext_powerclass $A }.
 
-notation "Ω term 90 A \atop ≈" non associative with precedence 70 
+notation < "Ω term 90 A \atop ≈" non associative with precedence 90 
 for @{ 'ext_powerclass $A }.
 
 interpretation "extensional powerclass" 'ext_powerclass a = (ext_powerclass a).
@@ -140,12 +140,12 @@ unification hint 0 ≔  A:setoid, x, S;
 nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
  #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
- #a; #a'; #b; #b'; *; #H1; #H2; *; /5/.
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
 nqed.
 
 unification hint 0 ≔ A,a,a'
  (*-----------------------------------------------------------------*) ⊢
-  eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
+  eq_rel ? (eq0 A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
 
 nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
  #A; #S; #S'; @ (S ∩ S');
@@ -262,7 +262,7 @@ nqed.
 
 ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
  λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
-  {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq B) (f x) y}.
+  {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq0 B) (f x) y}.
 
 ndefinition counter_image: ∀A,B. (carr A → carr B) → Ω^B → Ω^A ≝
  λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.