hints polished and fixed to allow recursive inference of ext_carr

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 0038ad4f652bcea45dcc2e2866fd191d6fe2bc77..c8f303a6b407920f101126160a4b6d6333d9acfc 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -119,20 +119,18 @@ nlemma mem_ext_powerclass_setoid_is_morph:
 [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 nqed.
 
-unification hint 0 ≔  AA, x, S;  
+unification hint 0 ≔  AA : setoid, S : 𝛀^AA, x : carr AA;  
      A ≟ carr AA,
      SS ≟ (ext_carr ? S),
      TT ≟ (mk_unary_morphism1 ?? 
-             (λx:setoid1_of_setoid ?.
+             (λx:carr1 (setoid1_of_setoid ?).
                mk_unary_morphism1 ??
-                 (λS:ext_powerclass_setoid ?. x ∈ S)
-                 (prop11 ?? (mem_ext_powerclass_setoid_is_morph AA x)))
+                 (λS:carr1 (ext_powerclass_setoid ?). x ∈ (ext_carr ? S))
+                 (prop11 ?? (fun11 ?? (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 AA)
-       (unary_morphism1_setoid1 XX CPROP) TT x S 
-    ≡ mem A SS x.
+     T2 ≟ (ext_powerclass_setoid AA)
+(*---------------------------------------------------------------------------*) ⊢ 
+    fun11 T2 CPROP (fun11 (setoid1_of_setoid AA) (unary_morphism1_setoid1 T2 CPROP) TT x) S ≡ mem A SS x.
 
 nlemma set_ext : ∀S.∀A,B:Ω^S.A =_1 B → ∀x:S.(x ∈ A) =_1 (x ∈ B).
 #S A B; *; #H1 H2 x; @; ##[ napply H1 | napply H2] nqed.
@@ -153,11 +151,15 @@ nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ 
-  A : setoid, B,C : ext_powerclass A;
-  R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C))) 
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+  AA ≟ carr A,
+  BB ≟ ext_carr ? B,
+  CC ≟ ext_carr ? C,
+  R ≟ (mk_ext_powerclass ? 
+        (ext_carr ? B ∩ ext_carr ? C) 
+        (ext_prop ? (intersect_is_ext ? B C))) 
   (* ------------------------------------------*)  ⊢ 
-    ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
+    ext_carr A R ≡ intersect AA BB CC.
     
 nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A.
 #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
@@ -168,7 +170,8 @@ alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ A : Type[0], B,C : Ω^A;
   T ≟ powerclass_setoid A,
   R ≟ mk_unary_morphism1 ??
-       (λS. mk_unary_morphism1 ?? (λS'.S ∩ S') (prop11 ?? (intersect_is_morph A S))) 
+       (λX. mk_unary_morphism1 ?? 
+         (λY.X ∩ Y) (prop11 ?? (fun11 ?? (intersect_is_morph A) X))) 
        (prop11 ?? (intersect_is_morph A))
 (*------------------------------------------------------------------------*) ⊢ 
     fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C  ≡ intersect A B C.
@@ -186,12 +189,12 @@ 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 ??
-                (λS':𝛀^AA.
-                  mk_ext_powerclass AA (S∩S') (ext_prop AA (intersect_is_ext ? S S')))
-                (prop11 ?? (intersect_is_ext_morph AA S))) 
+      R ≟ (mk_unary_morphism1 ?? (λX:𝛀^AA.
+               mk_unary_morphism1 ?? (λY:𝛀^AA.
+                  mk_ext_powerclass AA 
+                    (ext_carr ? X ∩ ext_carr ? Y) 
+                    (ext_prop AA (intersect_is_ext ? X Y)))
+                (prop11 ?? (fun11 ?? (intersect_is_ext_morph AA) X))) 
               (prop11 ?? (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
@@ -217,16 +220,20 @@ 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)))
+unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
+   AA ≟ carr A,
+   BB ≟ ext_carr ? B,
+   CC ≟ ext_carr ? C,
+   R ≟ mk_ext_powerclass ? 
+         (ext_carr ? B ∪ ext_carr ? C) (ext_prop ? (union_is_ext ? B C))
 (*-------------------------------------------------------------------------*)  ⊢
-    ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
+    ext_carr A R ≡ union AA BB CC.
 
 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
   T ≟ powerclass_setoid S,
   MM ≟ mk_unary_morphism1 ??
-        (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_is_morph S A)))
+        (λA.mk_unary_morphism1 ?? 
+          (λB.A ∪ B) (prop11 ?? (fun11 ?? (union_is_morph S) A)))
         (prop11 ?? (union_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.
@@ -240,13 +247,12 @@ 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 ??
-            (λS':𝛀^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))) ,
+  R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+           mk_unary_morphism1 ?? (λY:𝛀^AA.
+              mk_ext_powerclass AA 
+               (ext_carr ? X ∪ ext_carr ? Y) (ext_prop AA (union_is_ext ? X Y)))
+            (prop11 ?? (fun11 ?? (union_is_ext_morph AA) X)))
+          (prop11 ?? (union_is_ext_morph AA)),
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
@@ -268,16 +274,21 @@ nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
-   A : setoid, B,C :  𝛀^A;
-   R ≟ (mk_ext_powerclass ? (B - C) (ext_prop ? (substract_is_ext ? B C)))
-(*-------------------------------------------------------------------------*)  ⊢
-    ext_carr A R ≡ substract ? (ext_carr ? B) (ext_carr ? C).
+unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
+   AA ≟ carr A,
+   BB ≟ ext_carr ? B,
+   CC ≟ ext_carr ? C,
+   R ≟ mk_ext_powerclass ? 
+         (ext_carr ? B - ext_carr ? C) 
+         (ext_prop ? (substract_is_ext ? B C))
+(*---------------------------------------------------*)  ⊢
+    ext_carr A R ≡ substract AA BB CC.
 
 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
   T ≟ powerclass_setoid S,  
   MM ≟ mk_unary_morphism1 ??
-        (λA.mk_unary_morphism1 ?? (λB.A - B) (prop11 ?? (substract_is_morph S A)))
+        (λA.mk_unary_morphism1 ?? 
+          (λB.A - B) (prop11 ?? (fun11 ?? (substract_is_morph S) A)))
         (prop11 ?? (substract_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.
@@ -291,13 +302,13 @@ 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 ??
-            (λS':𝛀^AA.
-              mk_ext_powerclass AA (S - S') (ext_prop AA (substract_is_ext ? S S')))
-            (prop11 ?? (substract_is_ext_morph AA S)))
-          (prop11 ?? (substract_is_ext_morph AA))) ,
+  R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+           mk_unary_morphism1 ?? (λY:𝛀^AA.
+              mk_ext_powerclass AA 
+                (ext_carr ? X - ext_carr ? Y) 
+                (ext_prop AA (substract_is_ext ? X Y)))
+            (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+          (prop11 ?? (substract_is_ext_morph AA)),
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
@@ -312,37 +323,32 @@ nlemma single_is_ext: ∀A:setoid. A → 𝛀^A.
 #X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed. 
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ A : setoid, a:A;
+unification hint 0 ≔ A : setoid, a : carr A;
    R ≟ (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
 (*-------------------------------------------------------------------------*)  ⊢
     ext_carr A R ≡ singleton A a.
 
-unification hint 0 ≔ A:setoid, a:A;
+unification hint 0 ≔ A:setoid, a : carr A;
   T ≟ setoid1_of_setoid A,
   AA ≟ carr A,
   MM ≟ mk_unary_morphism1 ?? 
-         (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+         (λa:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph 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;
+unification hint 1 ≔ AA : setoid, a: carr AA;
   T ≟ ext_powerclass_setoid AA,
   R ≟ mk_unary_morphism1 ??
-       (λa:setoid1_of_setoid AA.
+       (λa:carr1 (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 (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.
 
 
-
-
-
-
 (*
 alias symbol "hint_decl" = "hint_decl_Type2".
 unification hint 0 ≔