From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Aug 2009 16:54:16 +0000 (+0000)
Subject: One half done.
X-Git-Tag: make_still_working~3532
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8272528f48b942a80024aeb9b625d99cfe3f0f44;p=helm.git

One half done.
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 93172d617..f24b11a13 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -21,6 +21,8 @@ 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".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -49,6 +51,12 @@ naxiom big_union_preserves_iso:
   ∀g: isomorphism A' A T' T.
    big_union A B T f = big_union A' B T' (λx.f (iso_f ???? g x)).
 
+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:
+ ∀n,m. ∀P: n < m ∨ ¬ (n < m) → CProp[0].
+  (∀H: n < m. P (or_introl ?? H)) → n < m → P (ltb n m). 
+
 nlemma partition_splits_card:
  ∀A. ∀P:partition A. ∀n,s.
   ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
@@ -72,13 +80,27 @@ nlemma partition_splits_card:
     ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
      [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
-    nletin xxx ≝ (plus match nindex return λ_.nat with [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s i)] nindex2);
+    nletin xxx ≝ (plus match minus n nindex return λ_.nat with [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] nindex2);
     napply (ex_intro … xxx); napply conj
-     [ nwhd in Hni1; nelim daemon
+     [ nwhd in Hni1; nwhd; nelim daemon
      | nwhd in ⊢ (???%?);
+       nchange in Hni1 with (nindex < S n);
+       ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?; #K;
+       nwhd in ⊢ (???(???????%?)?);
+       nelim (le_to_lt_or_eq … K)
+        [##2: #K'; nrewrite > K'; nrewrite < (minus_canc n); nnormalize;
+         napply (eq_rect_CProp0 nat nindex (λx:nat.λ_.partition_splits_card_map A P (S n) s f fi nindex2 x = y) ? n K');
+         nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?;
+         ngeneralize in match Hni22 in ⊢ ?;
+         nelim nindex
+          [ #X1; #X2; nwhd in ⊢ (??? % ?);
+            napply (lt_to_ltb ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption
+          | #n0; #_; #X1; #X2; nwhd in ⊢ (??? % ?);
+            napply (lt_to_ltb ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption]
+        
+         
        (* BEL POSTO DOVE FARE UN LEMMA *)
        (* invariante: Hni1; altre premesse: Hni1, Hni22 *)
-       nchange in Hni1 with (nindex < S n); ngeneralize in match Hni1 in ⊢ ?;
        nelim n in ⊢ (% → ??? (????????%) ?)
         [ #A (* decompose *)
         | #index'; #Hrec; #K; nwhd in ⊢ (???%?);