]> matita.cs.unibo.it Git - helm.git/commitdiff
non ho resistito!
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 28 Sep 2009 19:27:14 +0000 (19:27 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 28 Sep 2009 19:27:14 +0000 (19:27 +0000)
helm/software/matita/nlibrary/sets/partitions.ma
helm/software/matita/nlibrary/sets/sets.ma
helm/software/matita/nlibrary/topology/igft.ma

index 93f9cd6b5d3e014121adf9ff04042816848cb5a6..c1092c497cb355e766a188c8f3c59b1862f8c961 100644 (file)
@@ -25,6 +25,7 @@ alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -165,28 +166,28 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
        nlapply
         (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
           nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????)
-        [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
-        | napply le_S_S_to_le; nassumption
+        [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
+        |##5: napply le_S_S_to_le; nassumption
         |##*: nassumption]##]
 ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
-    ngeneralize in match (? : ∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2') in ⊢ ?
-     [##2: #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
-      ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ?
+    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2');
+    ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
+       nlapply(disjoint … P (f i1) (f i1') ???)
        [##2,3: napply f_closed; nassumption
-       |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
-         [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip]
-         nwhd; napply f_closed; nassumption]##]
-      #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
-       [##2: napply (f_inj … E'); nassumption
-       | #E''; nrewrite < E''; napply conj
-          [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''')
+       |##1: @ (fi i1 i2); @;
+         ##[ napply f_closed; nassumption ##| napply (. E‡#);
+             nwhd; napply f_closed; nassumption]##]
+      #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
+      #E''; nrewrite < E''; @; 
+      ##[ @;
+      ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''')
              [ nassumption | nrewrite > E''; nassumption ]##]##]
    ##] #K;
     nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x;
     nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x';
-    ngeneralize in match (K … E) in ⊢ ?
-     [##2,3: napply le_to_le_S_S; nassumption
-     |##4,5: nassumption]
+    nlapply (K … E)  
+     [##1,2: nassumption;
+     ##|##3,4:napply le_to_le_S_S; nassumption; ##]
     *; #K1; #K2;
     napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x');
     napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x);
index c4fc89f210b0c90f5a049d80442f0cf6b7222e11..96521773738786bc15cd6eb0d2bbc4c35ce8be50 100644 (file)
@@ -102,13 +102,13 @@ ndefinition qpowerclass_setoid: setoid → setoid1.
   [ napply (qpowerclass A)
   | napply (qseteq A) ]
 nqed.
-
+              
 unification hint 0 ≔ A ⊢  
-  carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
+  carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) 
+≡ qpowerclass A.
 
-(*CSC: non va!  
-unification hint 0 ≔ A ⊢  
-  carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*)
+ncoercion pc' : ∀A.∀x:qpowerclass_setoid A. Ω^A ≝ pc 
+on _x : (carr1 (qpowerclass_setoid ?)) to (Ω^?). 
 
 nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @
@@ -120,15 +120,15 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid
   ##]
 nqed.
 
-(*CSC: bug qui se metto x o S al posto di ?
-nlemma foo: True.
-nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in
-    fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S);
-*)
 unification hint 0 ≔  A:setoid, x, S;  
-         SS ≟ (pc ? S)
+         SS ≟ (pc ? S),
+         TT ≟ (mk_binary_morphism1 ??? 
+                 (λx:setoid1_of_setoid ?.λS:qpowerclass_setoid ?. x ∈ S) 
+                 (prop21 ??? (mem_ok A)))
+           
   (*-------------------------------------*) ⊢ 
-    fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x.
+    fun21 ? ? ? TT x S 
+  ≡ mem A SS x.
 
 nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
  #A; @
@@ -144,6 +144,53 @@ unification hint 0 ≔ A,a,a'
  (*-----------------------------------------------------------------*) ⊢
   eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
 
+nlemma intersect_ok: ∀A. qpowerclass A → qpowerclass A → qpowerclass A.
+ #A; #S; #S'; @ (S ∩ S');
+ #a; #a'; #Ha; @; *; #H1; #H2; @
+  [##1,2: napply (. Ha^-1‡#); nassumption;
+##|##3,4: napply (. Ha‡#); nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 1 ≔ 
+  A : setoid, B,C : qpowerclass A ⊢ 
+    pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C))) 
+    ≡ intersect ? (pc ? B) (pc ? C).
+
+nlemma intersect_ok': ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A).
+ #A; @ (λS,S'. S ∩ S');
+ #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @
+  [ napply Ha1; nassumption
+  | napply Hb1; nassumption
+  | napply Ha2; nassumption
+  | napply Hb2; nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ 
+  A : Type[0], B,C : powerclass A ⊢ 
+    fun21 …
+     (mk_binary_morphism1 …
+       (λS,S'.S ∩ S') 
+       (prop21 … (intersect_ok' A))) B C
+    ≡ intersect ? B C.
+
+ndefinition prop21_mem : 
+  ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C.
+   ∀a,a':setoid1_of_setoid A.
+    ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'.
+#A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption;
+nqed.
+    
+interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r).
+    
+    
+nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A →
+ ∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
+ #U; #A; #B; #H; #x; #y; #K; #K2; napply (. K^-1‡H); nassumption;
+nqed. 
+
+(*
 nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
  #A; @
   [ #S; #S'; @
@@ -162,11 +209,18 @@ nqed.
 alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ 
   A : setoid, B,C : qpowerclass A ⊢ 
-    pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C).
+    pc A (fun21 …
+            (mk_binary_morphism1 …
+              (λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S'))) 
+              (prop21 … (intersect_ok A))) 
+            B
+            C) 
+    ≡ intersect ? (pc ? B) (pc ? C).
 
 nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V.
  #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
 nqed.
+*)
 
 ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
  λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
index ce02f95df55f5327341d25fa8fc4d4ffcac88bb3..d35030b3553932a3f033b5c811f8911503c7c2e6 100644 (file)
@@ -823,27 +823,25 @@ Appendix: natural deduction like tactics explanation
 -----------------------------------------------------
 
 In this appendix we try to give a description of tactics
-in terms of natural deduction rules annotated with proofs.
+in terms of sequent calculus rules annotated with proofs.
 The `:` separator has to be read as _is a proof of_, in the spirit
 of the Curry-Howard isomorphism.
 
-                  f  :  A1 → … → An → B    ?1 : A1 … ?n  :  An 
-    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                           (f ?1 … ?n )  :  B
+                  Γ ⊢  f  :  A1 → … → An → B    Γ ⊢ ?1 : A1 … ?n  :  An 
+    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                           Γ ⊢ (f ?1 … ?n )  :  B
  
 foo  
 
-                               [x : T]
-                                  ⋮  
-                               ?  :  P(x) 
+                         Γ; x : T  ⊢ ?  :  P(x) 
     #x;         ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                            λx:T.?  :  ∀x:T.P(x)
+                         Γ ⊢ λx:T.?  :  ∀x:T.P(x)
 
 baz
                        
-                 (?1 args1)  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
-    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                   match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    
+                 Γ; args… : Args… ⊢ ?i  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
+    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                 Γ ⊢ match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    
 
 bar