snapshot for CSC

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

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index c5771028d59d7386d37991bc46e9fa689c6a036d..3b17099a371474318101168301daff9fe23a31ef 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -18,14 +18,7 @@ include "nat/compare.ma".
 include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
+
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
@@ -101,25 +94,15 @@ ntheorem iso_nat_nat_union_char:
         [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
         [##2: nassumption
         |napply conj
-         [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ??
-           (split_big_plus
-            (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
-            (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
-            (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?))
-           [##2: napply ad_hoc11]
-          napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?)
-           ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?))
-            [##2: nassumption]
-          nwhd in ⊢ (???(?(??%)?));
-          nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)
-           [##2: nassumption]
+         [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
+          nrewrite > (ad_hoc12 …); ##[##2: nassumption]
+          nwhd in ⊢ (????(?(??%)?));
+          nrewrite > (ad_hoc13 …);##[##2: nassumption]
           napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
           nwhd in ⊢ (???(?(??%)?));
-          napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ??
-           (plus_n_O (big_plus (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
-            (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n')))))));
-          nassumption
-        | napply le_S; nassumption ]##]##]##]
+          nrewrite > (plus_n_O …);
+          nassumption;
+        ##| napply le_S; nassumption ]##]##]##]
 nqed.
 
 ntheorem iso_nat_nat_union_pre:
@@ -130,7 +113,11 @@ ntheorem iso_nat_nat_union_pre:
  nrewrite > (split_big_plus (S n) (S i1) (λi.λ_.s i) ?)
   [##2: napply le_to_le_S_S; nassumption]
  napply ad_hoc15
-  [ nrewrite > (minus_S_S n i1 …); napply big_plus_preserves_ext; #i; #_;
+  [ nwhd in ⊢ (???(?%?));
+  
+    napply (eq_rect_CProp0_r nat (n - i1) (λx.λy.?) ?? (minus_S_S …)); STOP
+  
+    nrewrite > (minus_S_S n i1); napply big_plus_preserves_ext; #i; #_;
     nrewrite > (plus_n_S i i1); napply refl
   | nrewrite > (split_big_plus (S i1) i1 (λi.λ_.s i) ?) [##2: napply le_S; napply le_n]
     napply ad_hoc16; nrewrite > (minus_S i1); nnormalize; nrewrite > (plus_n_O (s i1) …);
@@ -151,7 +138,7 @@ nlemma partition_splits_card:
   ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
    (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
     (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
- #A; #P; #Sn; ncases Sn
+ STOP #A; #P; #Sn; ncases Sn
   [ #s; #f; #fi;
     ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
     (*