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 alias symbol "eq" = "setoid eq".
  21 alias symbol "eq" = "setoid1 eq".
  22 alias symbol "eq" = "setoid eq".
  23 alias symbol "eq" = "setoid1 eq".
  24 alias symbol "eq" = "setoid eq".
  25 alias symbol "eq" = "setoid1 eq".
  26 alias symbol "eq" = "setoid eq".
  27 alias symbol "eq" = "setoid1 eq".
  28 alias symbol "eq" = "setoid eq".
  29 alias symbol "eq" = "setoid1 eq".
  30 alias symbol "eq" = "setoid eq".
  31 nrecord partition (A: setoid) : Type[1] ≝
  32  { support: setoid;
  33    indexes: qpowerclass support;
  34    class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
  35    inhabited: ∀i. i ∈ indexes → class i ≬ class i;
  36    disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i=j;
  37    covers: big_union support ? ? (λx.class x) = full_set A
  38  }. napply indexes; nqed.
  39
  40 naxiom daemon: False.
  41
  42 nlet rec partition_splits_card_map
  43  A (P:partition A) n s (f:isomorphism ?? (Nat_ n) (indexes ? P))
  44  (fi: ∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) m index
  45  on index : A ≝
  46  match ltb m (s index) with
  47   [ true ⇒ iso_f ???? (fi index) m
  48   | false ⇒
  49      match index with
  50       [ O ⇒ (* dummy value: it could be an elim False: *) iso_f ???? (fi O) O
  51       | S index' ⇒
  52          partition_splits_card_map A P n s f fi (minus m (s index)) index']].
  53
  54 naxiom big_union_preserves_iso:
  55  ∀A,A',B,T,T',f.
  56   ∀g: isomorphism A' A T' T.
  57    big_union A B T f = big_union A' B T' (λx.f (iso_f ???? g x)).
  58
  59 naxiom le_to_lt_or_eq: ∀n,m. n ≤ m → n < m ∨ n = m.
  60 alias symbol "eq" = "leibnitz's equality".
  61 naxiom minus_canc: ∀n. O = minus n n.
  62 naxiom lt_to_ltb_t: ∀n,m. ∀P: bool → CProp[0]. P true → n < m → P (ltb n m).
  63 naxiom lt_to_ltb_f: ∀n,m. ∀P: bool → CProp[0]. P false → ¬ (n < m) → P (ltb n m).
  64 naxiom lt_to_minus: ∀n,m. n < m →  S (minus (minus m n) (S O)) = minus m n.
  65 naxiom not_lt_O: ∀n. ¬ (n < O).
  66 naxiom minus_S: ∀n,m. m ≤ n → minus (S n) m = S (minus n m).
  67 naxiom minus_lt_to_lt: ∀n,m,p. n < p → minus n m < p.
  68 naxiom minus_O_n: ∀n. O = minus O n.
  69 naxiom le_O_to_eq: ∀n. n ≤ O → n=O.
  70 naxiom lt_to_minus_to_S: ∀n,m. m < n → ∃k. minus n m = S k.
  71 naxiom ltb_t: ∀n,m. n < m → ltb n m = true.
  72 naxiom ltb_f: ∀n,m. ¬ (n < m) → ltb n m = false.
  73 naxiom plus_n_O: ∀n. plus n O = n.
  74 naxiom not_lt_plus: ∀n,m. ¬ (plus n m < n).
  75 naxiom lt_to_lt_plus: ∀n,m,l. n < m → n < m + l.
  76 naxiom S_plus: ∀n,m. S (n + m) = n + S m.
  77 naxiom big_plus_ext: ∀n,f,f'. (∀i,p. f i p = f' i p) → big_plus n f = big_plus n f'.
  78 naxiom ad_hoc1: ∀n,m,l. n + (m + l) = l + (n + m).
  79 naxiom assoc: ∀n,m,l. n + m + l = n + (m + l).
  80 naxiom lt_canc: ∀n,m,p. n < m → p + n < p + m.
  81 naxiom ad_hoc2: ∀a,b. a < b → b - a - (b - S a) = S O.
  82 naxiom ad_hoc3: ∀a,b. b < a → S (O + (a - S b) + b) = a.
  83 naxiom ad_hoc4: ∀a,b. a - S b ≤ a - b.
  84
  85 naxiom split_big_plus:
  86   ∀n,m,f. m ≤ n →
  87    big_plus n f = big_plus m (λi,p.f i ?) + big_plus (n - m) (λi.λp.f (i + m) ?).
  88  nelim daemon.
  89 nqed.
  90
  91 nlemma partition_splits_card:
  92  ∀A. ∀P:partition A. ∀n,s.
  93   ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
  94    (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
  95     (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
  96  #A; #P; #Sn; ncases Sn
  97   [ #s; #f; #fi;
  98     ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
  99     ngeneralize in match
 100      (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f) in ⊢ ?;
 101      *; #K; #_; nwhd in K: (? → ? → %);
 102     nelim daemon (* impossibile *)
 103   | #n; #s; #f; #fi; napply mk_isomorphism
 104   [ napply mk_unary_morphism
 105      [ napply (λm.partition_splits_card_map A P (S n) s f fi m n)
 106      | #a; #a'; #H; nrewrite < H; napply refl ]
 107 ##| #y; #_;
 108     ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc;
 109     ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
 110     ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
 111     ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
 112      [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
 113     *; #nindex2; *; #Hni21; #Hni22;
 114     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
 115     napply (ex_intro … xxx); napply conj
 116      [ nwhd in Hni1; nwhd; nwhd in ⊢ (?(? %)%);
 117        nchange with (? < plus (s n) (big_plus n ?));
 118        nelim (le_to_lt_or_eq … (le_S_S_to_le … Hni1))
 119         [##2: #E; nrewrite < E; nrewrite < (minus_canc nindex);
 120           nwhd in ⊢ (?%?); nrewrite < E; napply lt_to_lt_plus; nassumption
 121         | #L; nrewrite > (split_big_plus n (S nindex) (λm.λ_.s m) L);
 122           nrewrite > (split_big_plus (n - nindex) (n - S nindex) (λi.λ_.s (S (i+nindex))) ?)
 123            [ ngeneralize in match (big_plus_ext (n - S nindex)
 124               (λi,p.s (S (i+nindex))) (λi,p.s (i + S nindex)) ?) in ⊢ ?
 125                [ #E;
 126                  napply (eq_rect_CProp0_r ??
 127                   (λx:nat.λ_. x + big_plus (n - nindex - (n - S nindex))
 128                    (λi,p.s (S (i + (n - S nindex)+nindex))) + nindex2 <
 129                    s n + (big_plus (S nindex) (λi,p.s i) +
 130                     big_plus (n - S nindex) (λi,p. s (i + S nindex)))) ? ? E);
 131                  nrewrite > (ad_hoc1 (s n) (big_plus (S nindex) (λi,p.s i))
 132                   (big_plus (n - S nindex) (λi,p. s (i + S nindex))));
 133                  napply (eq_rect_CProp0_r
 134                   ?? (λx.λ_.x < ?) ?? (assoc
 135                   (big_plus (n - S nindex) (λi,p.s (i + S nindex)))
 136                   (big_plus (n - nindex - (n - S nindex))
 137                    (λi,p.s (S (i + (n - S nindex)+nindex))))
 138                   nindex2));
 139                  napply lt_canc;
 140                  nrewrite > (ad_hoc2 … L); nwhd in ⊢ (?(?%?)?);
 141                  nrewrite > (ad_hoc3 … L);
 142                  napply (eq_rect_CProp0_r ?? (λx.λ_.x < ?) ?? (assoc …));
 143                  napply lt_canc; nnormalize in ⊢ (?%?); nwhd in ⊢ (??%);
 144                  napply lt_to_lt_plus; nassumption
 145              ##|##2: #i; #_; nrewrite > (S_plus i nindex); napply refl]
 146          ##| napply ad_hoc4]##]
 147    ##| nwhd in ⊢ (???%?);
 148        nchange in Hni1 with (nindex < S n);
 149        ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?;
 150        nwhd in ⊢ (? → ???(???????%?)?);
 151        napply (nat_rect_CProp0
 152         (λx. nindex ≤ x →
 153           eq_rel (carr A) (eq A)
 154           (partition_splits_card_map A P (S n) s f fi
 155            (plus
 156              (big_plus (minus x nindex) (λi.λ_:i < minus x nindex.s (S (plus i nindex))))
 157              nindex2) x) y) ?? n)
 158         [ #K; nrewrite < (minus_O_n nindex); nwhd in ⊢ (???(???????%?)?);
 159           nwhd in ⊢ (???%?); nchange in Hni21 with (nindex2 < s nindex);
 160           ngeneralize in match (le_O_to_eq … K) in ⊢ ?; #K';
 161           ngeneralize in match Hni21 in ⊢ ?;
 162           ngeneralize in match Hni22 in ⊢ ?;
 163           nrewrite > K' in ⊢ (% → % → ?); #K1; #K2;
 164           nrewrite > (ltb_t … K2);
 165           nwhd in ⊢ (???%?); nassumption
 166         | #n'; #Hrec; #HH; nelim (le_to_lt_or_eq … HH)
 167            [##2: #K; nrewrite < K; nrewrite < (minus_canc nindex);
 168             nwhd in ⊢ (???(???????%?)?);
 169             nrewrite > K;
 170             nwhd in ⊢ (???%?); nrewrite < K; nrewrite > (ltb_t … Hni21);
 171             nwhd in ⊢ (???%?); nassumption
 172          ##| #K; ngeneralize in match (le_S_S_to_le … K) in ⊢ ?; #K';
 173              nwhd in ⊢ (???%?);
 174
 175
 176              XXX;
 177              nrewrite > (minus_S n' nindex ?) [##2: napply le_S_S_to_le; nassumption]
 178              ngeneralize in match (? :
 179               ltb (plus (big_plus (S (minus n' nindex)) (λi.λ_.s (S (plus i nindex)))) nindex2)
 180                (s (S n')) = false) in ⊢ ?
 181                [ #Hc; nrewrite > Hc; nwhd in ⊢ (???%?);
 182                  nelim (le_to_lt_or_eq … (le_S_S_to_le … K))
 183                   [
 184                 ##| #E; ngeneralize in match Hc in ⊢ ?;
 185                     nrewrite < E; nrewrite < (minus_canc nindex);
 186                     nnormalize in ⊢ (??(?%?)? → ?);
 187                     nrewrite > (plus_n_O (s (S nindex)));
 188                     nrewrite > (ltb_f (plus (s (S nindex)) nindex2) (s (S nindex)) ?);
 189
 190                     XXX;
 191
 192
 193                 ngeneralize in match (? :
 194                  minus (plus (big_plus (minus n' nindex) (λi.λ_.s (S (plus i nindex)))) nindex2)
 195                   (s (S n'))
 196                  =
 197                   plus
 198                    match minus n' nindex with
 199                     [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] nindex2)
 200                  in ⊢ ?
 201                   [ #F; nrewrite > F; napply Hrec; napply le_S_S_to_le; nassumption
 202                   | nelim (le_to_lt_or_eq … (le_S_S_to_le … K))
 203                      [
 204                    ##| #E; nrewrite < E; nrewrite < (minus_canc nindex); nnormalize;
 205
 206                        nwhd in ⊢ (???%);
 207                      ]
 208
 209
 210               nrewrite > He;
 211
 212
 213               nnormalize in ⊢ (???%?);
 214
 215
 216
 217        nelim (le_to_lt_or_eq … K)
 218         [##2: #K'; nrewrite > K'; nrewrite < (minus_canc n); nnormalize;
 219          napply (eq_rect_CProp0 nat nindex (λx:nat.λ_.partition_splits_card_map A P (S n) s f fi nindex2 x = y) ? n K');
 220          nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?;
 221          ngeneralize in match Hni22 in ⊢ ?;
 222          nelim nindex
 223           [ #X1; #X2; nwhd in ⊢ (??? % ?);
 224             napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption
 225           | #n0; #_; #X1; #X2; nwhd in ⊢ (??? % ?);
 226             napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption]
 227       ##| #K'; ngeneralize in match (lt_to_minus … K') in ⊢ ?; #K2;
 228           napply (eq_rect_CProp0 ?? (λx.λ_.?) ? ? K2); (* uffa, ancora??? *)
 229           nwhd in ⊢ (??? (???????(?%?)?) ?);
 230           ngeneralize in match K' in ⊢ ?;
 231           napply (nat_rect_CProp0
 232            (λx. nindex < x →
 233              partition_splits_card_map A P (S n) s f fi
 234               (plus (big_op plus_magma_type (minus (minus x nindex) (S O))
 235                 (λi.λ_.s (S (plus i nindex))) O) nindex2) x = y) ?? n)
 236            [ #A; nelim (not_lt_O … A)
 237            | #n'; #Hrec; #X; nwhd in ⊢ (???%?);
 238              ngeneralize in match
 239               (? : ¬ ((plus (big_op plus_magma_type (minus (minus (S n') nindex) (S O))
 240                 (λi.λ_.s (S (plus i nindex))) O) nindex2) < s (S n'))) in ⊢ ?
 241               [ #B1; napply (lt_to_ltb_f ???? B1); #B1'; nwhd in ⊢ (???%?);
 242                 nrewrite > (minus_S n' nindex …) [##2: napply le_S_S_to_le; nassumption]
 243                 ngeneralize in match (le_S_S_to_le … X) in ⊢ ?; #X';
 244                 nelim (le_to_lt_or_eq … X')
 245                  [##2: #X'';
 246                   nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?;
 247                   nrewrite > X''; nrewrite < (minus_canc n');
 248                   nrewrite < (minus_canc (S O)); nnormalize in ⊢ (? → %);
 249                   nelim n'
 250                    [ #Y; nwhd in ⊢ (??? % ?);
 251                      ngeneralize in match (minus_lt_to_lt ? (s (S O)) ? Y) in ⊢ ?; #Y';
 252                      napply (lt_to_ltb_t … Y'); #H; nwhd in ⊢ (???%?);
 253
 254                 nrewrite > (minus_S (minus n' nindex) (S O) …) [##2:
 255
 256               XXX;
 257
 258           nelim n in f K' ⊢ ?
 259            [ #A; nelim daemon;
 260
 261        (* BEL POSTO DOVE FARE UN LEMMA *)
 262        (* invariante: Hni1; altre premesse: Hni1, Hni22 *)
 263        nelim n in ⊢ (% → ??? (????????%) ?)
 264         [ #A (* decompose *)
 265         | #index'; #Hrec; #K; nwhd in ⊢ (???%?);
 266           nelim (ltb xxx (s (S index')));
 267           #K1; nwhd in ⊢ (???%?)
 268            [
 269
 270            nindex < S index' + 1
 271            +^{nindex} (s i) w < s (S index')
 272            S index' == nindex
 273
 274            |
 275            ]
 276         ]
 277      ]
 278   | #x; #x'; nnormalize in ⊢ (? → ? → %);
 279     nelim daemon
 280   ]
 281 nqed.
 282
 283 (************** equivalence relations vs partitions **********************)
 284
 285 ndefinition partition_of_compatible_equivalence_relation:
 286  ∀A:setoid. compatible_equivalence_relation A → partition A.
 287  #A; #R; napply mk_partition
 288   [ napply (quotient ? R)
 289   | napply Full_set
 290   | #a; napply mk_qpowerclass
 291      [ napply {x | R x a}
 292      | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
 293 ##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl
 294   | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2);
 295     napply sym; nassumption
 296   | nnormalize; napply conj
 297      [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##]
 298 nqed.