From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Sep 2010 11:35:23 +0000 (+0000)
Subject: nicer hints, 16.1->3 done
X-Git-Tag: make_still_working~2821
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f2f5039ef719f60ebcf24d7ee17c83eac6cc635;p=helm.git

nicer hints, 16.1->3 done
---

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 20942ecc8..9b352d4a4 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -81,6 +81,7 @@ unification hint 0 ≔ A,B:CProp[0];
 (*-------------------------------------------------------------*) ⊢
   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
   
+(* XXX always applied, generates hard unif problems  
 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
  #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
@@ -88,12 +89,16 @@ ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CP
  //.
 nqed.
 
-unification hint 0 ≔ A,B ⊢
- mk_unary_morphism1 …
-  (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
-  (prop11 … if_morphism)
-  A B ≡ A → B.
-  
+unification hint 0 ≔ A,B:CProp[0];
+  T ≟ CPROP,
+  R ≟ mk_unary_morphism1 …
+       (λX:CProp[0].mk_unary_morphism1 … 
+         (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
+         (prop11 … if_morphism)
+(*----------------------------------------------------------------------*) ⊢
+  fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R A) B ≡ A → B.
+*)
+
 (* not as morphism *)
 nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
 @(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 3d8682365..cfbd7cb31 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -242,12 +242,11 @@ unification hint 0 ≔ A : setoid, B,C :  Elang A;
     
 unification hint 0 ≔ S:setoid, A,B:lang S;
     T ≟ powerclass_setoid (list S),
-    TT ≟ unary_morphism1_setoid1 T T,
-    MM ≟ mk_unary_morphism1 T TT  
+    MM ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
           (λA:lang S.
              mk_unary_morphism1 T T 
-               (λB:lang S.A · B) (prop11 T T (cat_is_morph S A)))
-          (prop11 T TT (cat_is_morph S))
+               (λB:lang S.cat S A B) (prop11 T T (cat_is_morph S A)))
+          (prop11 T (unary_morphism1_setoid1 T T) (cat_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ cat S A B.
    
@@ -259,19 +258,18 @@ nqed.
 unification hint 1 ≔ AA : setoid, B,C : Elang AA;
   AAS ≟ LIST AA,
   T ≟ ext_powerclass_setoid (list AA),
-  TT ≟ unary_morphism1_setoid1 T T,
-  R ≟ mk_unary_morphism1 ??
+  R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
           (λS:Elang AA.
-           mk_unary_morphism1 ??
+           mk_unary_morphism1 T T
             (λS':Elang AA.
-              mk_ext_powerclass (list AA) (ext_carr ? S · ext_carr ? S') 
+              mk_ext_powerclass (list AA) (cat AA (ext_carr ? S) (ext_carr ? S')) 
                 (ext_prop (list AA) (cat_is_ext AA S S')))
-            (prop11 ?? (cat_is_ext_morph AA S)))
-          (prop11 ?? (cat_is_ext_morph AA)),
+            (prop11 T T (cat_is_ext_morph AA S)))
+          (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
    BB ≟ ext_carr ? B,
    CC ≟ ext_carr ? C
 (*------------------------------------------------------*) ⊢
-   ext_carr AAS (fun11 T T (fun11 T TT R B) C) ≡ cat AA BB CC.
+   ext_carr AAS (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ cat AA BB CC.
 
 (* end hints for cat *)
 
@@ -340,13 +338,11 @@ unification hint 0 ≔ A:Alpha, a:re A;
    fun11 T T2 MM a ≡  𝐋 a.
    
 nlemma L_re_is_ext_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 𝛀^(list A).
-#A; @; ##[ #a; napply (L_re_is_ext ? a); ##] #a b E; @; #x H;
-##[ nchange with (x ∈ 𝐋 b); napply (. #╪_1?); 
-    ##[ nchange with (𝐋 b = ?); napply (.= ┼_1 E^-1); napply #| ##skip]
-    nassumption;
-##| nchange with (x ∈ 𝐋 a); napply (. #╪_1?); 
-    ##[ nchange with (𝐋 a = ?); napply (.= ┼_1 E); napply #| ##skip]
-    nassumption; ##]
+#A; @; ##[ #a; napply (L_re_is_ext ? a); ##] #a b E;
+ncut (𝐋 b =  𝐋 a); ##[ napply (.=_1 (┼_1 E^-1)); // ] #EL;
+@; #x H; nchange in H ⊢ % with (x ∈ 𝐋 ?); 
+##[ napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply EL;
+##| napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply (EL^-1)]
 nqed.
             
 unification hint 1 ≔  AA : Alpha, a: re AA;
@@ -711,14 +707,15 @@ nlemma odot_dot_aux : ∀S:Alpha.∀e1,e2: pre S.
     nlapply (erase_bull S e2'); #XX;
     napply (.=_1 (((# ╪_1 (┼_1 ?) )╪_1 #)╪_1 #)); ##[##2: napply XX; ##| ##skip]
     //;   
-##| ncases e2; #e2' b2'; nchange in match (〈e1',false〉⊙?) with 〈?,?〉;
-    nchange in match (𝐋\p ?) with (?∪?);
-    nchange in match (𝐋\p (e1'·?)) with (?∪?);
-    nchange in match (𝐋\p 〈e1',?〉) with (?∪?);
-    nrewrite > (cup0…); 
-    nrewrite > (cupA…); //;##]
+##| ncases e2; #e2' b2'; nchange in match (𝐋\p ?) with (?∪?∪?);
+    napply (.=_1 (cupA…));
+    napply (?^-1); nchange in match (𝐋\p 〈?,false〉) with (?∪?);
+    napply (.=_1 ((cup0…)╪_1#)╪_1#);
+    //]
 nqed.
 
+STOP
+
 nlemma sub_dot_star : 
   ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
 #S X b; napply extP; #w; @;
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 0516982cd..a7a5e74b0 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -106,7 +106,7 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
    R ≟ mk_unary_morphism ?? (composition ??? f g)
         (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun1 ?? R ≡ (composition ??? f g).
+     fun1 o1 o3 R ≡ (composition o1 o2 o3 f g).
 
 ndefinition comp_binary_morphisms: 
   ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 068334183..889fb0545 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -91,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).
@@ -123,7 +123,7 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
    R ≟ (mk_unary_morphism1 ?? (composition1 ??? f g)
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun11 ?? R ≡ (composition1 ??? f g).
+       fun11 o1 o3 R ≡ (composition1 o1 o2 o3 f g).
                               
 ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index d547fbbbf..0038ad4f6 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -185,6 +185,7 @@ nqed.
 unification hint 1 ≔ 
       AA : setoid, B,C : 𝛀^AA;
       A ≟ carr AA,
+      T ≟ ext_powerclass_setoid AA,
       R ≟ (mk_unary_morphism1 ??
               (λS:𝛀^AA.
                mk_unary_morphism1 ??
@@ -194,11 +195,11 @@ unification hint 1 ≔
               (prop11 ?? (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
-   (* ------------------------------------------------------*) ⊢ 
-            ext_carr AA (R B C) ≡ intersect A BB CC.
+   (* ---------------------------------------------------------------------------------------*) ⊢ 
+      ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ intersect A BB CC.
 
 
-(* hints for ∩ *)
+(* hints for ∪ *)
 nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
 #X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
 #A1 A2 B1 B2 EA EB; napply ext_set; #x;
@@ -238,6 +239,7 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
+  T ≟ ext_powerclass_setoid AA,  
   R ≟ (mk_unary_morphism1 ??
           (λS:𝛀^AA.
            mk_unary_morphism1 ??
@@ -248,7 +250,7 @@ unification hint 1 ≔
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R B C) ≡ union A BB CC.
+   ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ union A BB CC.
 
 
 (* hints for - *)
@@ -288,6 +290,7 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
+  T ≟ ext_powerclass_setoid AA,    
   R ≟ (mk_unary_morphism1 ??
           (λS:𝛀^AA.
            mk_unary_morphism1 ??
@@ -298,7 +301,7 @@ unification hint 1 ≔
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R B C) ≡ substract A BB CC.
+   ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ substract A BB CC.
 
 (* hints for {x} *)
 nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
@@ -316,22 +319,24 @@ unification hint 0 ≔ A : setoid, a:A;
 
 unification hint 0 ≔ A:setoid, a:A;
   T ≟ setoid1_of_setoid A,
+  AA ≟ carr A,
   MM ≟ mk_unary_morphism1 ?? 
          (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 T (powerclass_setoid A) MM a ≡ {(a)}.
+   fun11 T (powerclass_setoid AA) MM a ≡ {(a)}.
    
 nlemma single_is_ext_morph:∀A:setoid.(setoid1_of_setoid A) ⇒_1 𝛀^A.
 #A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.
             
 unification hint 1 ≔
   AA : setoid, a: AA;
+  T ≟ ext_powerclass_setoid AA,
   R ≟ mk_unary_morphism1 ??
        (λa:setoid1_of_setoid AA.
          mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
             (prop11 ?? (single_is_ext_morph AA))
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R a) ≡ singleton AA a.
+   ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.