X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=6d6b68743195a8acd2f86b6b4b134165d10e35dd;hb=b2d91e46900424ce5eb5a058c33841e72cc4b229;hp=0571b6dfa8e5e2c890657ff682fc14f5341e5592;hpb=1dd64d6c49db7dc0dc0ee39c30da4c7a043b8bde;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 0571b6dfa..6d6b68743 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -12,165 +12,68 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "properties/relations1.ma".
 include "sets/setoids.ma".
+include "hints_declaration.ma".
 
-(*
-definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
-definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
-definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
-
-record setoid1 : Type ≝
- { carr1:> Type;
-   eq1: carr1 → carr1 → CProp;
-   refl1: reflexive1 ? eq1;
-   sym1: symmetric1 ? eq1;
-   trans1: transitive1 ? eq1
+nrecord setoid1: Type[2] ≝
+ { carr1:> Type[1];
+   eq1: equivalence_relation1 carr1
  }.
 
-definition proofs1: CProp → setoid1.
- intro;
- constructor 1;
-  [ apply A
-  | intros;
-    apply True
-  | intro;
-    constructor 1
-  | intros 3;
-    constructor 1
-  | intros 5;
-    constructor 1]
-qed.
-
-ndefinition CCProp: setoid1.
- constructor 1;
-  [ apply CProp
-  | apply iff
-  | intro;
-    split;
-    intro;
-    assumption
-  | intros 3;
-    cases H; clear H;
-    split;
-    assumption
-  | intros 5;
-    cases H; cases H1; clear H H1;
-    split;
-    intros;
-    [ apply (H4 (H2 H))
-    | apply (H3 (H5 H))]]
-qed.
-
-record function_space1 (A: setoid1) (B: setoid1): Type ≝
- { f1:1> A → B;
-   f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
+ndefinition setoid1_of_setoid: setoid → setoid1.
+ #s; napply mk_setoid1
+  [ napply (carr s)
+  | napply (mk_equivalence_relation1 s)
+    [ napply eq
+    | napply refl
+    | napply sym
+    | napply trans]##]
+nqed.
+
+(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.*)
+(*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).
+
+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 }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+
+interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans1" 'trans r = (trans1 ????? r).
+interpretation "trans" 'trans r = (trans ????? r).
+
+nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
+ { fun11:1> A → B;
+   prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
  }.
 
-definition function_space_setoid1: setoid1 → setoid1 → setoid1.
- intros (A B);
- constructor 1;
-  [ apply (function_space1 A B);
-  | intros;
-    apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
-  |*: cases daemon] (* simplify;
-    intros;
-    apply (f1_ok ? ? x);
-    unfold proofs; simplify;
-    apply (refl1 A)
-  | simplify;
-    intros;
-    unfold proofs; simplify;
-    apply (sym1 B);
-    apply (f a)
-  | simplify;
-    intros;
-    unfold carr; unfold proofs; simplify;
-    apply (trans1 B ? (y a));
-    [ apply (f a)
-    | apply (f1 a)]] *)
-qed.
-
-interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
-
-definition setoids: setoid1.
- constructor 1;
-  [ apply setoid;
-  | apply isomorphism;
-  | intro;
-    split;
-     [1,2: constructor 1;
-        [1,3: intro; assumption;
-        |*: intros; assumption]
-     |3,4:
-       intros;
-       simplify;
-       unfold proofs; simplify;
-       apply refl;]
-  |*: cases daemon]
-qed.
-
-definition setoid1_of_setoid: setoid → setoid1.
- intro;
- constructor 1;
-  [ apply (carr s)
-  | apply (eq s)
-  | apply (refl s)
-  | apply (sym s)
-  | apply (trans s)]
-qed.
-
-coercion setoid1_of_setoid.
-
-record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
- { fo:> ∀a:A.proofs (B a) }.
-
-record subset (A: setoid) : CProp ≝
- { mem: A ⇒ CCProp }.
-
-definition ssubset: setoid → setoid1.
- intro;
- constructor 1;
-  [ apply (subset s);
-  | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
-  | simplify;
-    intros;
-    split;
-    intro;
-    assumption
-  | simplify;
-    cases daemon
-  | cases daemon]
-qed.
-
-definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
- intros;
- constructor 1;
-  [ apply mem; 
-  | unfold function_space_setoid1; simplify;
-    intros (b b');
-    change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
-    unfold proofs1; simplify; intros;
-    unfold proofs1 in c; simplify in c;
-    unfold ssubset in c; simplify in c;
-    cases (c a); clear c;
-    split;
-    assumption]
-qed.
-
-definition sand: CCProp ⇒ CCProp.
-
-definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
- intro;
- constructor 1;
-  [ intro;
-    constructor 1;
-     [ intro;
-       constructor 1;
-       constructor 1;
-       intro;
-       apply (mem ? c c2 ∧ mem ? c1 c2);
-     |
-  |
-  |
+nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
+ { fun21:2> A → B → C;
+   prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
+ }.
 
-*)
+interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
+interpretation "refl1" 'refl = (refl1 ???).
+
+ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
+ #s; #s1; @ (unary_morphism1 s s1); @
+     [ #f; #g; napply (∀a:s. f a = g a)
+     | #x; #a; napply refl1
+     | #x; #y; #H; #a; napply sym1; nauto
+     | #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##]
+nqed.
+
+unification hint 0 ≔ S, T ;
+ R ≟ (unary_morphism1_setoid1 S T)
+(* --------------------------------- *) ⊢
+   carr1 R ≡ unary_morphism1 S T.
\ No newline at end of file