From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 20 Aug 2009 11:07:14 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3530
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=97090ce8f20a9446fbb064bf254c96b76b93a1b2;hp=bc9fca01f135aecc2940e7318f77fea34fd6ef30;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index f24b11a13..23fd3ecea 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -53,9 +53,16 @@ naxiom big_union_preserves_iso:
 
 naxiom le_to_lt_or_eq: ∀n,m. n ≤ m → n < m ∨ n = m.
 naxiom minus_canc: ∀n. O = minus n n.
-naxiom lt_to_ltb:
+naxiom lt_to_ltb_t:
  ∀n,m. ∀P: n < m ∨ ¬ (n < m) → CProp[0].
-  (∀H: n < m. P (or_introl ?? H)) → n < m → P (ltb n m). 
+  (∀H: n < m. P (or_introl ?? H)) → n < m → P (ltb n m).
+naxiom lt_to_ltb_f:
+ ∀n,m. ∀P: n < m ∨ ¬ (n < m) → CProp[0].
+  (∀H: ¬ (n < m). P (or_intror ?? H)) → ¬ (n < m) → P (ltb n m).
+naxiom lt_to_minus: ∀n,m. n < m →  S (minus (minus m n) (S O)) = minus m n.
+naxiom not_lt_O: ∀n. ¬ (n < O).
+naxiom minus_S: ∀n,m. m ≤ n → minus (S n) m = S (minus n m).
+naxiom minus_lt_to_lt: ∀n,m,p. n < p → minus n m < p. 
 
 nlemma partition_splits_card:
  ∀A. ∀P:partition A. ∀n,s.
@@ -94,10 +101,42 @@ nlemma partition_splits_card:
          ngeneralize in match Hni22 in ⊢ ?;
          nelim nindex
           [ #X1; #X2; nwhd in ⊢ (??? % ?);
-            napply (lt_to_ltb ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption
+            napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption
           | #n0; #_; #X1; #X2; nwhd in ⊢ (??? % ?);
-            napply (lt_to_ltb ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption]
-        
+            napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption]
+      ##| #K'; ngeneralize in match (lt_to_minus … K') in ⊢ ?; #K2;
+          napply (eq_rect_CProp0 ?? (λx.λ_.?) ? ? K2); (* uffa, ancora??? *)
+          nwhd in ⊢ (??? (???????(?%?)?) ?);
+          ngeneralize in match K' in ⊢ ?;
+          napply (nat_rect_CProp0
+           (λx. nindex < x →
+             partition_splits_card_map A P (S n) s f fi
+              (plus (big_op plus_magma_type (minus (minus x nindex) (S O))
+                (λi.λ_.s (S (plus i nindex))) O) nindex2) x = y) ?? n)
+           [ #A; nelim (not_lt_O … A)
+           | #n'; #Hrec; #X; nwhd in ⊢ (???%?);
+             ngeneralize in match
+              (? : ¬ ((plus (big_op plus_magma_type (minus (minus (S n') nindex) (S O))
+                (λi.λ_.s (S (plus i nindex))) O) nindex2) < s (S n'))) in ⊢ ?
+              [ #B1; napply (lt_to_ltb_f ???? B1); #B1'; nwhd in ⊢ (???%?);
+                nrewrite > (minus_S n' nindex …) [##2: napply le_S_S_to_le; nassumption]
+                ngeneralize in match (le_S_S_to_le … X) in ⊢ ?; #X';
+                nelim (le_to_lt_or_eq … X')
+                 [##2: #X'';
+                  nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?;
+                  nrewrite > X''; nrewrite < (minus_canc n');
+                  nrewrite < (minus_canc (S O)); nnormalize in ⊢ (? → %);
+                  nelim n'
+                   [ #Y; nwhd in ⊢ (??? % ?);
+                     ngeneralize in match (minus_lt_to_lt ? (s (S O)) ? Y) in ⊢ ?; #Y';
+                     napply (lt_to_ltb_t … Y'); #H; nwhd in ⊢ (???%?);  
+                 
+                nrewrite > (minus_S (minus n' nindex) (S O) …) [##2: 
+              
+              XXX;
+          
+          nelim n in f K' ⊢ ?
+           [ #A; nelim daemon;
          
        (* BEL POSTO DOVE FARE UN LEMMA *)
        (* invariante: Hni1; altre premesse: Hni1, Hni22 *)