From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Sep 2010 16:01:20 +0000 (+0000)
Subject: th 16.2 proved in the setoids setting
X-Git-Tag: make_still_working~2835
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b15a4df27469ee4b64d1b3b8fc996cd15e8a61f0;p=helm.git

th 16.2 proved in the setoids setting
---

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 14d52373e..ab2d13458 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -31,6 +31,7 @@ match l1 with
 ndefinition LIST : setoid → setoid.
 #S; @(list S); @(eq_list S); ncases admit; nqed.  
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint 0 ≔ S : setoid;
   P1 ≟ refl ? (eq0 (LIST S)),
   P2 ≟ sym ? (eq0 (LIST S)),
@@ -168,7 +169,7 @@ unification hint 0 ≔ A : Alpha;
      carr X ≡ (re T).
 
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
-notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
 interpretation "or" 'plus a b = (o ? a b).
            
@@ -297,6 +298,21 @@ unification hint 0 ≔ S,a,b;
    L ≟ (list S)
 (* -------------------------------------------- *) ⊢
    eq_list S a b ≡ eq_rel L (eq0 R) a b.
+   
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.   
+   
+alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
+unification hint 0 ≔ S : setoid, x,y;
+  SS ≟ LIST S,
+  TT ≟ setoid1_of_setoid SS
+(*-----------------------------------------*) ⊢ 
+  eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
+  
+unification hint 0 ≔ SS : setoid;
+  S ≟ carr SS,
+  TT ≟ setoid1_of_setoid (LIST SS)
+(*-----------------------------------------------------------------*) ⊢ 
+  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}.
@@ -306,30 +322,11 @@ notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B
 interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
 interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
 
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
 
-nlemma exists_is_morph: (* BUG *) ∀S,T:setoid.∀P: S ⇒_1 (T ⇒_1 (CProp[0]:?)).
-  ∀y,z:S.y =_0 z → (Ex T (P y)) = (Ex T (P z)).
-#S T P y z E; @;
-##[ *; #x Px; @x; alias symbol "refl" (instance 4) = "refl".
-    alias symbol "prop2" (instance 2) = "prop21".
-    napply (. E^-1‡#); napply Px;
-##| *; #x Px; @x; napply (. E‡#); napply Px;##]
-nqed.
-
-ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? P); ##| #P1 P2 E; @; 
-*; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
-nqed.
- 
 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.
 
-(* desiderata : Σ(λx.H‡#)
-   ottenute   : Σ H (λx,H.H‡#) -- quindi monoriscrittura. H toplevel permette inferenza di y e z in Sig
-*)
-
 notation "∑" non associative with precedence 90 for @{Sig ?????}.
 
 nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
@@ -343,7 +340,7 @@ nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
  ∀x,y:setoid1_of_setoid S.x =_1 y → 
    (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
 #S m x y E;
-napply (.=_1 #‡(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
+napply (.=_1 #╪_1(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
 napply #.
 nqed.
 
@@ -387,11 +384,15 @@ ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
       ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
         @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
       napply ((X‡#)‡#); ##]
-    napply #;
-##] nqed.
-    
-    FINQUI
+    napply #;##] 
+nqed.
 
+unification hint 0 ≔ S : Alpha,e : pitem S; 
+  SS ≟ (list S),
+  X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e)))
+(*-----------------------------------------------------------------*)⊢ 
+  ext_carr SS X ≡ 𝐋\p e.
+  
 ndefinition epsilon ≝ 
   λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].
 
@@ -403,9 +404,9 @@ ndefinition L_pr ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
   
 interpretation "L_pr" 'L_pi E = (L_pr ? E).
 
-nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. w1 @ w2 = [ ] → w1 = [ ].
+nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. [ ] = w1 @ w2 → w1 = [ ].
 #S w1; ncases w1; //. nqed.
-
+  
 (* lemma 12 *)
 nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = true).
 #S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
@@ -414,19 +415,26 @@ nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = tru
 ##| #r1 r2 H G; *; ##[##2: nassumption; ##]
 ##| #r1 r2 H1 H2; *; /2/ by {}]
 *; #w1; *; #w2; *; *; 
-##[ #defw1 H1 foo; napply H; napply (. #‡#); (append_eq_nil … defw1)^-1‡#);
-
- nrewrite > (append_eq_nil ? … w1 w2 …); /3/ by {};//;
+##[ #defw1 H1 foo; napply H;
+    napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+    nassumption; 
+##| #defw1 H1 foo; napply H;
+    napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+    nassumption; 
+##]
 nqed.
 
-nlemma not_epsilon_lp : ∀S.∀e:pitem S. ¬ (𝐋\p e [ ]).
-#S e; nelim e; nnormalize; /2/ by nmk;
-##[ #; @; #; ndestruct;
-##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
-    nrewrite > (append_eq_nil …H…); /2/;
-##| #r1 r2 n1 n2; @; *; /2/;
-##| #r n; @; *; #w1; *; #w2; *; *; #H;     
-    nrewrite > (append_eq_nil …H…); /2/;##]
+nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ([ ] ∈ (𝐋\p e)).
+#S e; nelim e; ##[##1,2,3,4: nnormalize;/2/]
+##[ #p1 p2 np1 np2; *; ##[##2: napply np2] *; #w1; *; #w2; *; *; #abs;
+    nlapply (append_eq_nil ??? abs); # defw1; #; napply np1;
+    napply (. defw1^-1╪_1#);
+    nassumption;
+##| #p1 p2 np1 np2; *; nchange with (¬?); //;
+##| #r n; *; #w1; *; #w2; *; *; #abs; #; napply n;
+    nlapply (append_eq_nil ??? abs); # defw1; #;
+    napply (. defw1^-1╪_1#);
+    nassumption;##]
 nqed.
 
 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
@@ -451,12 +459,12 @@ ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
 
 notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
 interpretation "lk" 'lk op a = (lk ? op a).
-notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
+notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}.
 
 notation > "•" non associative with precedence 60 for @{eclose ?}.
 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
  match E with
-  [ pz ⇒ 〈 ∅, false 〉
+  [ pz ⇒ 〈 0, false 〉
   | pe ⇒ 〈 ϵ,  true 〉
   | ps x ⇒ 〈 `.x, false 〉
   | pp x ⇒ 〈 `.x, false 〉
@@ -470,48 +478,123 @@ 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).
 
-ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
+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.
 
-naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
+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; napply extP; #w; nnormalize; @; /2/; *; //; *;
+#S b1 b2; ncases b1; ncases b2; 
+nchange in match (true || true) with true;
+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; ##]
+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.
+
+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 cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; 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.
 
-nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
-#S a b; napply extP; #w; @; *; nnormalize; /2/; 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));
-nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …);
-nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …);
-nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //;
+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…));
+//;
 nqed.
 
+FINQUI
+
+manca setoide per pair (e pre)
+
 nlemma odotEt : 
-  ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
+  ∀S:Alpha.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = ?.〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
 #S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
 
 nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) =  𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed.
 
-nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r). 
+nlemma cup_dotD : ∀S.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r). 
 #S p q r; napply extP; #w; nnormalize; @; 
 ##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
 ##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
 nqed.
 
-nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
-#S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
 
 nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| =  𝐋 .|e1| · 𝐋 .|e2|.
 #S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 9fd5b7eeb..5600b9a16 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -123,17 +123,18 @@ nlemma mem_ext_powerclass_setoid_is_morph:
   [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 nqed.
 
-unification hint 0 ≔  A:setoid, x, S;  
+unification hint 0 ≔  AA, x, S;  
+     A ≟ carr AA,
      SS ≟ (ext_carr ? S),
      TT ≟ (mk_unary_morphism1 … 
              (λx:setoid1_of_setoid ?.
                mk_unary_morphism1 …
                  (λS:ext_powerclass_setoid ?. x ∈ S)
-                 (prop11 … (mem_ext_powerclass_setoid_is_morph A x)))
-             (prop11 … (mem_ext_powerclass_setoid_is_morph A))),
-     XX ≟ (ext_powerclass_setoid A)
+                 (prop11 … (mem_ext_powerclass_setoid_is_morph AA x)))
+             (prop11 … (mem_ext_powerclass_setoid_is_morph AA))),
+     XX ≟ (ext_powerclass_setoid AA)
   (*-------------------------------------*) ⊢ 
-      fun11 (setoid1_of_setoid A)
+      fun11 (setoid1_of_setoid AA)
        (unary_morphism1_setoid1 XX CPROP) TT x S 
     ≡ mem A SS x.
 
@@ -143,6 +144,7 @@ nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
 nqed.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
 unification hint 0 ≔ A,a,a'
  (*-----------------------------------------------------------------*) ⊢
   eq_rel ? (eq0 A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
@@ -189,18 +191,19 @@ nlemma intersect_is_ext_morph:
 nqed.
 
 unification hint 1 ≔ 
-      A:setoid, B,C : 𝛀^A;
+      AA : setoid, B,C : 𝛀^AA;
+      A ≟ carr AA,
       R ≟ (mk_unary_morphism1 …
-              (λS:ext_powerclass_setoid A.
+              (λS:ext_powerclass_setoid AA.
                mk_unary_morphism1 ??
-                (λS':ext_powerclass_setoid A.
-                  mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S')))
-                (prop11 … (intersect_is_ext_morph A S))) 
-              (prop11 … (intersect_is_ext_morph A))) ,
+                (λS':ext_powerclass_setoid AA.
+                  mk_ext_powerclass AA (S∩S') (ext_prop AA (intersect_is_ext ? S S')))
+                (prop11 … (intersect_is_ext_morph AA S))) 
+              (prop11 … (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
    (* ------------------------------------------------------*) ⊢ 
-            ext_carr A (R B C) ≡ intersect (carr A) BB CC.
+            ext_carr AA (R B C) ≡ intersect A BB CC.
 
 (*
 alias symbol "hint_decl" = "hint_decl_Type2".