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 naxiom daemon: False.
  43
  44 nlet rec partition_splits_card_map
  45  A (P: finite_partition A) (s: ∀i. lt i (card ? P) → nat)
  46   (H:∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p))
  47   m index on index:
  48   le (S index) (card ? P) → lt m (big_plus (S index) (λi,p. s i ?)) → lt index (card ? P) → A ≝
  49  match index return λx. le (S x) (card ? P) → lt m (big_plus (S x) ?) → lt x (card ? P) → ? with
  50   [ O ⇒ λL,H1,p.f ??? (H O p) m ?
  51   | S index' ⇒ λL,H1,p.
  52      match ltb m (s (S index') p) with
  53       [ or_introl K ⇒ f ??? (H (S index') p) m K
  54       | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s (S index') p)) index' ??? ]].
  55 ##[##3: napply lt_minus; nelim daemon (*nassumption*)
  56   |##4: napply lt_Sn_m; nassumption
  57   |##5: napply (lt_le_trans … p); nassumption
  58 ##|##2: napply lt_to_le; nassumption
  59 ##|##1: nnormalize in H1; nelim daemon ]
  60 nqed.
  61 (*
  62 nlemma partition_splits_card:
  63  ∀A. ∀P: finite_partition A. ∀s: ∀i. lt i (card ? P) → nat.
  64   (∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p)) →
  65    has_card A (full_set A) (big_plus (card ? P) s).
  66  #A; #P; #s; #H; ncases (card A P)
  67   [ nnormalize; napply mk_has_card
  68      [ #m; #H; nelim daemon
  69      | #m; #H; nelim daemon ]
  70 ##| #c; napply mk_has_card
  71   [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P))
  72   |
  73   ]
  74 nqed.
  75 *)