X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fre%2Fre-setoids.ma;h=a340fadf7479936938446351098237b2d3388d34;hb=e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc;hp=ab2d13458928808becfd8616589c91bd2a5bce26;hpb=b15a4df27469ee4b64d1b3b8fc996cd15e8a61f0;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index ab2d13458..a340fadf7 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -41,6 +41,12 @@ unification hint 0 ≔ S : setoid;
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
+unification hint 0 ≔ S,a,b;
+   R ≟ LIST S,
+   L ≟ (list S)
+(* -------------------------------------------- *) ⊢
+   eq_list S a b ≡ eq_rel L (eq0 R) a b.
+
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
   for @{'cons $hd $tl}.
@@ -68,33 +74,9 @@ ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l.
 
 ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z. 
 
-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force ≝ 
-  λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
-    match lock return λ_.Type[2] with [ unit ⇒ T].
-
-nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝ 
- match lock return λlock.force S s T t lock with [ unit ⇒ t ].
-
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-unification hint 0 ≔ R : setoid; 
-   TR ≟ setoid, MR ≟ (carr R), lock ≟ unit 
-(* ---------------------------------------- *) ⊢ 
-   setoid ≡ force ?(*Type[0]*) MR TR R lock.
-
-unification hint 0 ≔ R : setoid1; 
-   TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit 
-(* ---------------------------------------- *) ⊢ 
-   setoid1 ≡ force ? MR TR R lock.
 
 ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
 
 interpretation "iff" 'iff a b = (iff a b).  
 
@@ -136,6 +118,12 @@ unification hint 0 ≔ ;
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ bool.
 
+unification hint 0 ≔ a,b;
+   R ≟ BOOL,
+   L ≟ bool
+(* -------------------------------------------- *) ⊢
+   eq bool a b ≡ eq_rel L (eq0 R) a b.
+
 nrecord Alpha : Type[1] ≝ { 
    acarr :> setoid;
    eqb: acarr → acarr → bool; 
@@ -168,6 +156,12 @@ unification hint 0 ≔ A : Alpha;
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ (re T).
 
+unification hint 0 ≔ A,a,b;
+   R ≟ RE A,
+   L ≟ re A
+(* -------------------------------------------- *) ⊢
+   eq_re A a b ≡ eq_rel L (eq0 R) a b.
+
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
 notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
@@ -186,8 +180,8 @@ interpretation "atom" 'ps a = (s ? a).
 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
 interpretation "epsilon" 'epsilon = (e ?).
 
-notation "0" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+notation "0" non associative with precedence 90 for @{ 'empty_r }.
+interpretation "empty" 'empty_r = (z ?).
 
 notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
 notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
@@ -198,16 +192,6 @@ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
 match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
 
-
-ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }.
-notation "∅" non associative with precedence 90 for @{'emptyset}.
-interpretation "empty set" 'emptyset = (empty_set ?).
-
-(*
-notation "{}" non associative with precedence 90 for @{'empty_lang}.
-interpretation "empty lang" 'empty_lang = (empty_lang ?).
-*)
-
 ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
 interpretation "sing lang" 'singl x = (sing_lang ? x).
 
@@ -264,7 +248,7 @@ interpretation "ppatom" 'pp a = (pp ? a).
 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?.
 interpretation "patom" 'ps a = (ps ? a).
 interpretation "pepsilon" 'epsilon = (pe ?).
-interpretation "pempty" 'empty = (pz ?).
+interpretation "pempty" 'empty_r = (pz ?).
 
 notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
@@ -293,12 +277,7 @@ notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E}
 notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
 interpretation "in_pl" 'L_pi E = (L_pi ? E).
 
-unification hint 0 ≔ S,a,b;
-   R ≟ LIST S,
-   L ≟ (list S)
-(* -------------------------------------------- *) ⊢
-   eq_list S a b ≡ eq_rel L (eq0 R) a b.
-   
+(* The caml, as some patches for it *)
 ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.   
    
 alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
@@ -314,15 +293,7 @@ unification hint 0 ≔ SS : setoid;
 (*-----------------------------------------------------------------*) ⊢ 
   list S ≡ carr1 TT.
 
-notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
-notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
-
-interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
-interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
-
-
+(* Ex setoid support *)
 nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
   ∀y,z:T.y = z → (∀x.y=z → P x y = P x z)  → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
 #S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
@@ -359,6 +330,7 @@ nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
 napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
 napply #.
 nqed.
+(* Ex setoid support end *)
 
 ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
 #S r; @(𝐋\p r); #w1 w2 E; nelim r; 
@@ -478,15 +450,6 @@ notation > "• x" non associative with precedence 60 for @{'eclose $x}.
 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 interpretation "reclose" 'eclose x = (reclose ? x).
 
-nlemma cup0 :∀S.∀p:lang S.p ∪ ∅ = p.
-#S p; @; #w; ##[*; //| #; @1; //] *; nqed.
-
-nlemma cupC : ∀S. ∀a,b:lang S.a ∪ b = b ∪ a.
-#S a b; @; #w; *; nnormalize; /2/; nqed.
-
-nlemma cupID : ∀S. ∀a:lang S.a ∪ a = a.
-#S a; @; #w; ##[*; //] /2/; nqed.
-
 nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
 #S b1 b2; ncases b1; ncases b2; 
 nchange in match (true || true) with true;
@@ -494,88 +457,28 @@ nchange in match (true || false) with true;
 nchange in match (ϵ true) with {[]};
 nchange in match (ϵ false) with ∅;
 ##[##1,4: napply ((cupID…)^-1);
-##| napply ((cup0 S {[]})^-1);
-##| napply (.= (cup0 S {[]})^-1); napply cupC; ##]
+##| napply ((cup0 ? {[]})^-1);
+##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##]
 nqed.
 
-nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; @; #w; *; /3/; *; /3/; nqed.
-
-nlemma setP : ∀S.∀A,B:Ω^S.∀x:S. A = B → (x ∈ A) = (x ∈ B).
-#S A B x; *; #H1 H2; @; ##[ napply H1 | napply H2] nqed.
-
-nlemma pset_ext : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B.
-#S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed.
-
+(* XXX move somewere else *)
 ndefinition if': ∀A,B:CPROP. A = B → A → B.
 #A B; *; /2/. nqed.
 
 ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?.
 
-(* move in sets.ma? *)
-nlemma union_morphism : ∀A.Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
-#X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
-#A1 A2 B1 B2 EA EB; napply pset_ext; #x;
-nchange in match (x ∈ (A1 ∪ B1)) with (?∨?);
-napply (.= (setP ??? x EA)‡#);
-napply (.= #‡(setP ??? x EB)); //;
-nqed.
-
-nlemma union_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
- #S A B; @ (A ∪ B); #x y Exy; @; *; #H1; 
-##[##1,3: @; ##|##*: @2 ]
-##[##1,3: napply (. (Exy^-1)╪_1#) 
-##|##2,4: napply (. Exy╪_1#)]
-nassumption;
-nqed.
-
-alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
-  A : setoid, B,C :  𝛀^A;
-  R ≟ (mk_ext_powerclass ? (B ∪ C) (ext_prop ? (union_is_ext ? B C)))
-  (* ----------------------------------------------------------------*)  ⊢
-    ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
-
-unification hint 0 ≔ S:Type[0], A,B:Ω^S;
-  MM ≟ mk_unary_morphism1 ??
-        (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_morphism S A)))
-        (prop11 ?? (union_morphism S))
- (*-----------------------------------------------------*) ⊢
-   fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B.
-   
-nlemma union_is_ext_morph:∀A:setoid.𝛀^A ⇒_1 (𝛀^A ⇒_1 𝛀^A).
-#A; napply (mk_binary_morphism1 …  (union_is_ext …));
-#x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_morphism A)); nassumption.
-nqed.
-            
-unification hint 1 ≔
-      AA : setoid, B,C : 𝛀^AA;
-      A ≟ carr AA,
-      R ≟ (mk_unary_morphism1 ??
-              (λS:(*ext_powerclass_setoid AA*)𝛀^AA.
-               mk_unary_morphism1 ??
-                (λS':(*ext_powerclass_setoid AA*)𝛀^AA.
-                  mk_ext_powerclass AA (S ∪ S') (ext_prop AA (union_is_ext ? S S')))
-                (prop11 ?? (union_is_ext_morph AA S)))
-              (prop11 ?? (union_is_ext_morph AA))) ,
-       BB ≟ (ext_carr ? B),
-       CC ≟ (ext_carr ? C)
-   (* ------------------------------------------------------*) ⊢
-            ext_carr AA (R B C) ≡ union A BB CC.
-
-   
 (* theorem 16: 2 *)
 nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
 #S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
 nwhd in ⊢ (???(??%)?);
 nchange in ⊢(???%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
 nchange in ⊢(???(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
-napply (.= #╪_1 (epsilon_or ???));
-napply (.= (cupA…)^-1);
-napply (.= (cupA…)╪_1#);
-napply (.= (#╪_1(cupC…))╪_1#);
-napply (.= (cupA…)^-1╪_1#);
-napply (.= (cupA…));
+napply (.=_1 #╪_1 (epsilon_or ???));
+napply (.=_1 (cupA…)^-1);
+napply (.=_1 (cupA…)╪_1#);
+napply (.=_1 (#╪_1(cupC…))╪_1#);
+napply (.=_1 (cupA…)^-1╪_1#);
+napply (.=_1 (cupA…));
 //;
 nqed.