helm/software/matita/nlibrary/sets/partitions.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "sets/sets.ma".
  16 include "nat/plus.ma".
  17 include "nat/compare.ma".
  18 include "nat/minus.ma".
  19
  20 (* sbaglia a fare le proiezioni *)
  21 nrecord finite_partition (A: Type[0]) : Type[1] ≝
  22  { card: nat;
  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*)
  27  }.
  28
  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*)
  34  }.
  35
  36 (*
  37 nlemma subset_of_finite:
  38  ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m.
  39 nqed.
  40 *)
  41
  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 ?
  48   | S index' ⇒ λp'.
  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
  54   |
  55 nqed.
  56
  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))
  63   |
  64   ]
  65 nqed.