From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 14 Aug 2009 17:51:48 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3541
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d3d0248bf4770c63361f7805d2099b2a607f44d;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/nat/order.ma b/helm/software/matita/nlibrary/nat/order.ma
index dd8c544ae..4587e8435 100644
--- a/helm/software/matita/nlibrary/nat/order.ma
+++ b/helm/software/matita/nlibrary/nat/order.ma
@@ -28,6 +28,8 @@ nqed.
 naxiom le_S_S: ∀n,m. le n m → le (S n) (S m).
 naxiom le_S_S_to_le: ∀n,m. le (S n) (S m) → le n m.
 naxiom lt_Sn_m: ∀n,m. lt (S n) m → lt n m.
+naxiom lt_to_le: ∀n,m. lt n m → le n m.
+naxiom lt_le_trans: ∀n,m,p. lt n m → le m p → lt n p.
 
 nlemma lt_O_Sn: ∀n. lt O (S n).
  #n; napply le_S_S; napply le_O_n.
diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 43940e1f9..0ef3fa8c4 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -39,27 +39,37 @@ nlemma subset_of_finite:
 nqed.
 *)
 
+naxiom daemon: False.
+
 nlet rec partition_splits_card_map
  A (P: finite_partition A) (s: ∀i. lt i (card ? P) → nat)
   (H:∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p))
-  m (H1: lt m (big_plus ? s)) index (p: lt index (card ? P)) on index : A ≝
- match index return λx. lt x (card ? P) → ? with
-  [ O ⇒ λp'.f ??? (H O p') m ?
-  | S index' ⇒ λp'.
-     match ltb m (s index p) with
-      [ or_introl K ⇒ f ??? (H index p) m K 
-      | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s index p)) ? index' ? ]] p.
-##[##2: napply lt_minus; nassumption
-  |##3: napply lt_Sn_m; nassumption
-  |
+  m index on index:
+  le (S index) (card ? P) → lt m (big_plus (S index) (λi,p. s i ?)) → lt index (card ? P) → A ≝
+ match index return λx. le (S x) (card ? P) → lt m (big_plus (S x) ?) → lt x (card ? P) → ? with
+  [ O ⇒ λL,H1,p.f ??? (H O p) m ?
+  | S index' ⇒ λL,H1,p.
+     match ltb m (s (S index') p) with
+      [ or_introl K ⇒ f ??? (H (S index') p) m K 
+      | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s (S index') p)) index' ??? ]].
+##[##3: napply lt_minus; nelim daemon (*nassumption*)
+  |##4: napply lt_Sn_m; nassumption
+  |##5: napply (lt_le_trans … p); nassumption
+##|##2: napply lt_to_le; nassumption
+##|##1: nnormalize in H1; nelim daemon ]
 nqed.
-
+(*
 nlemma partition_splits_card:
  ∀A. ∀P: finite_partition A. ∀s: ∀i. lt i (card ? P) → nat.
   (∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p)) →
    has_card A (full_set A) (big_plus (card ? P) s).
- #A; #P; #s; #H; napply mk_has_card
+ #A; #P; #s; #H; ncases (card A P)
+  [ nnormalize; napply mk_has_card
+     [ #m; #H; nelim daemon
+     | #m; #H; nelim daemon ]
+##| #c; napply mk_has_card
   [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P))
   |
   ]
-nqed.
\ No newline at end of file
+nqed.
+*)
\ No newline at end of file