update in groud_2 and models

[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 d547fbbbfcbd37efadd825e130a9575b3e6d892a..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.
 
 [ 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 ?? 
      A ≟ carr AA,
      SS ≟ (ext_carr ? S),
      TT ≟ (mk_unary_morphism1 ?? 

-             (λx:setoid1_of_setoid ?.
+             (λx:carr1 (setoid1_of_setoid ?).

                mk_unary_morphism1 ??
                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))),
              (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.
 
 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".
 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'));
     
 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 ??
 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.
        (prop11 ?? (intersect_is_morph A))
 (*------------------------------------------------------------------------*) ⊢ 
     fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C  ≡ intersect A B C.


@@ -185,20 +188,21 @@ nqed.
 unification hint 1 ≔ 
       AA : setoid, B,C : 𝛀^AA;
       A ≟ carr AA,
 unification hint 1 ≔ 
       AA : setoid, B,C : 𝛀^AA;
       A ≟ carr 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))) 
+      T ≟ ext_powerclass_setoid 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 (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)
               (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 â\88© *)
+(* hints for â\88ª *)

 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;
 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;


@@ -216,16 +220,20 @@ nassumption;
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
 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 ??
 
 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.
         (prop11 ?? (union_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.


@@ -238,17 +246,17 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr 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))) ,
+  T ≟ ext_powerclass_setoid 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)
 (*------------------------------------------------------*) ⊢
    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 - *)
 
 
 (* hints for - *)


@@ -266,16 +274,21 @@ nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
 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 ??
 
 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.
         (prop11 ?? (substract_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.


@@ -288,17 +301,18 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr 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))) ,
+  T ≟ ext_powerclass_setoid 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)
 (*------------------------------------------------------*) ⊢
    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.
 
 (* hints for {x} *)
 nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.


@@ -309,33 +323,30 @@ 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".
 #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.
 
    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,
   T ≟ setoid1_of_setoid A,

+  AA ≟ carr A,

   MM ≟ mk_unary_morphism1 ?? 
   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 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.
             
    
 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 ??
   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))
 (*------------------------------------------------------*) ⊢
          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.

 
 
 (*
 
 
 (*