update in groud_2 and models

[helm.git] / helm / software / matita / nlibrary / sets / setoids1.ma

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 622c9401d08aec0ce1e66b3010c8c781c1b25322..90be6bc94be18f5758c7ce8b8fb5ee8c2d63c5a4 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -21,10 +21,34 @@ nrecord setoid1: Type[2] ≝ {
   eq1: equivalence_relation1 carr1 
 }.
 
+unification hint 0 ≔ R : setoid1; 
+   MR ≟ (carr1 R), 
+   lock ≟ mk_lock2 Type[1] MR setoid1 R 
+(* ---------------------------------------- *) ⊢ 
+   setoid1 ≡ force2 ? MR lock.
+
+notation < "[\setoid1\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid1 $x}.
+interpretation "mk_setoid1" 'mk_setoid1 x = (mk_setoid1 x ?).
+
+(* da capire se mettere come coercion *)
 ndefinition setoid1_of_setoid: setoid → setoid1.
  #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
 nqed.
 
+alias symbol "hint_decl" = "hint_decl_CProp2".
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
+unification hint 0 ≔ A,x,y;
+   T  ≟ carr A, 
+   R  ≟ setoid1_of_setoid A,
+   T1 ≟ carr1 R
+(*-----------------------------------------------*) ⊢
+   eq_rel T (eq0 A) x y ≡ eq_rel1 T1 (eq1 R) x y.
+
+unification hint 0 ≔ A;
+   R  ≟ setoid1_of_setoid A
+(*-----------------------------------------------*) ⊢
+   carr A ≡ carr1 R.
+
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
@@ -67,7 +91,7 @@ nqed.
 unification hint 0 ≔ S, T ;
    R ≟ (unary_morphism1_setoid1 S T)
 (* --------------------------------- *) ⊢
-   carr1 R ≡ S ⇒_1 T.
+   carr1 R ≡ unary_morphism1 S T.
    
 notation "l ╪_1 r" with precedence 89 for @{'prop2_x1 $l $r }.
 interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
@@ -96,16 +120,14 @@ ndefinition comp1_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
-   R ≟ (mk_unary_morphism1 ?? (composition1 … f g)
+   R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g))
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun11 ?? R ≡ (composition1 … f g).
+       fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
                               
 ndefinition comp1_binary_morphisms:
- ∀o1,o2,o3.
-   (unary_morphism1_setoid1 o2 o3) ⇒_1
-     (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+ ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
 #o1; #o2; #o3; napply mk_binary_morphism1
- [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
+ [ #f; #g; napply (comp1_unary_morphisms … f g) 
  | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
 nqed.