1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sets/sets.ma".
16 include "nat/plus.ma".
17 include "nat/compare.ma".
18 include "nat/minus.ma".
20 (* sbaglia a fare le proiezioni *)
21 nrecord finite_partition (A: Type[0]) : Type[1] ≝
23 class: ∀n. lt n card → Ω \sup A;
24 inhabited: ∀i,p. class i p ≬ class i p(*;
25 disjoint: ∀i,j,p,p'. class i p ≬ class j p' → i=j;
26 covers: big_union ?? class = full_set A*)
29 nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : CProp[0] ≝
30 { f: ∀m:nat. lt m n → A;
31 in_S: ∀m.∀p:lt m n. f ? p ∈ S (*;
32 f_inj: injective ?? f;
33 f_sur: surjective ?? f*)
37 nlemma subset_of_finite:
38 ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m.
42 nlet rec partition_splits_card_map
43 A (P: finite_partition A) (s: ∀i. lt i (card ? P) → nat)
44 (H:∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p))
45 m (H1: lt m (big_plus ? s)) index (p: lt index (card ? P)) on index : A ≝
46 match index return λx. lt x (card ? P) → ? with
47 [ O ⇒ λp'.f ??? (H O p') m ?
49 match ltb m (s index p) with
50 [ or_introl K ⇒ f ??? (H index p) m K
51 | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s index p)) ? index' ? ]] p.
52 ##[##2: napply lt_minus; nassumption
53 |##3: napply lt_Sn_m; nassumption
57 nlemma partition_splits_card:
58 ∀A. ∀P: finite_partition A. ∀s: ∀i. lt i (card ? P) → nat.
59 (∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p)) →
60 has_card A (full_set A) (big_plus (card ? P) s).
61 #A; #P; #s; #H; napply mk_has_card
62 [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P))