X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids.ma;h=9d31b09439dc29f0b12eb9550140f9918f41ac3a;hb=f5e6cad85ff6f10b63622a0348ad65492578022e;hp=87546cae917e94addf8a25dbdf142ad05a9e808f;hpb=347c7d213fd1d106f22acd6fff82a83af14c1bbd;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 87546cae9..9d31b0943 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -1,21 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
 include "logic/connectives.ma".
 include "properties/relations.ma".
 
-nrecord iff (A,B: CProp) : CProp ≝
- { if: A → B;
-   fi: B → A
- }.
-
-notation > "hvbox(a break \liff b)"
-  left associative with precedence 25
-for @{ 'iff $a $b }.
-
-notation "hvbox(a break \leftrightarrow b)"
-  left associative with precedence 25
-for @{ 'iff $a $b }.
-
-interpretation "logical iff" 'iff x y = (iff x y).
-
 nrecord setoid : Type[1] ≝
  { carr:> Type;
    eq: carr → carr → CProp;
@@ -32,83 +31,20 @@ ndefinition proofs: CProp → setoid.
 ##]
 nqed.
 
-(*
-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
- }.
-
-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.
-
-*)
-
-(************************CSC
-nrecord function_space (A,B: setoid): Type[1] ≝
- { f:1> carr A → carr B}.;
+nrecord function_space (A,B: setoid): Type ≝
+ { f:1> A → B;
    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  }.
- 
 
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 
-(*
-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'))
- }.
-*)
-
-definition function_space_setoid: setoid → setoid → setoid.
- intros (A B);
- constructor 1;
-  [ apply (function_space A B);
-  | intros;
-    apply (∀a:A. proofs (eq ? (f a) (f1 a)));
-  | simplify;
-    intros;
-    apply (f_ok ? ? x);
-    unfold carr; unfold proofs; simplify;
+ndefinition function_space_setoid: setoid → setoid → setoid.
+ #A; #B; napply (mk_setoid ?????);
+##[ napply (function_space A B);
+##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a)));
+##| nwhd; #x; #a;
+    napply (f_ok ? ? x ? ? ?); (* QUI!! *)
+(*    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;
     intros;
@@ -123,33 +59,7 @@ definition function_space_setoid: setoid → setoid → setoid.
     | apply (f1 a)]]
 qed.
 
-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).
-
-record isomorphism (A,B: setoid): Type ≝
+nrecord isomorphism (A,B: setoid): Type ≝
  { map1:> function_space_setoid A B;
    map2:> function_space_setoid B A;
    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
@@ -158,92 +68,10 @@ record isomorphism (A,B: setoid): Type ≝
 
 interpretation "isomorphism" 'iff x y = (isomorphism x y).
 
-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 dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
  { dp:> ∀a:A.carr (B a);
    dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
  }.*)
-
-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);
-     |
-  |
-  |
-*)
-*******************)
+ 
+ *)
\ No newline at end of file