From 3d3d0248bf4770c63361f7805d2099b2a607f44d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Aug 2009 17:51:48 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/nat/order.ma | 2 ++ .../matita/nlibrary/sets/partitions.ma | 36 ++++++++++++------- 2 files changed, 25 insertions(+), 13 deletions(-) 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 -- 2.39.2