100/birthday.ml

   1 (* ========================================================================= *)
   2 (* Birthday problem.                                                         *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Restricted function space.                                                *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 parse_as_infix("-->",(13,"right"));;
  12
  13 let funspace = new_definition
  14  `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\
  15                         (!x. ~(x IN s) ==> f(x) = @y. T)}`;;
  16
  17 (* ------------------------------------------------------------------------- *)
  18 (* Sizes.                                                                    *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 let FUNSPACE_EMPTY = prove
  22  (`({} --> t) = {(\x. @y. T)}`,
  23   REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN
  24   REWRITE_TAC[FUN_EQ_THM]);;
  25
  26 let HAS_SIZE_FUNSPACE = prove
  27  (`!s:A->bool t:B->bool m n.
  28         s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`,
  29   REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
  30   ONCE_REWRITE_TAC[IMP_CONJ] THEN
  31   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
  32   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
  33    [SIMP_TAC[CARD_CLAUSES; FINITE_RULES; FUNSPACE_EMPTY; NOT_IN_EMPTY] THEN
  34     REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  35     ASM_REWRITE_TAC[EXP; ARITH];
  36     ALL_TAC] THEN
  37   REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
  38   SUBGOAL_THEN
  39    `(x INSERT s) --> t =
  40         IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
  41               {y,g | y IN t /\ g IN s --> t}`
  42   SUBST1_TAC THENL
  43    [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
  44     ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
  45     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
  46     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  47     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  48     X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
  49      [STRIP_TAC THEN MAP_EVERY EXISTS_TAC
  50        [`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
  51       REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[IN_INSERT];
  52       REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  53       MAP_EVERY X_GEN_TAC [`y:B`; `g:A->B`] THEN
  54       STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
  55       ASM_MESON_TAC[IN_INSERT]];
  56     ALL_TAC] THEN
  57   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
  58    [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
  59     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
  60     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
  61     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
  62     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  63     REWRITE_TAC[FUN_EQ_THM; funspace; IN_ELIM_THM] THEN
  64     REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
  65      [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN
  66     X_GEN_TAC `u:A` THEN ASM_CASES_TAC `u:A = x` THEN ASM_MESON_TAC[];
  67     ALL_TAC] THEN
  68   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[CARD_CLAUSES; EXP] THEN
  69   MATCH_MP_TAC HAS_SIZE_PRODUCT THEN ASM_MESON_TAC[]);;
  70
  71 (* ------------------------------------------------------------------------- *)
  72 (* The restriction to injective functions.                                   *)
  73 (* ------------------------------------------------------------------------- *)
  74
  75 let FACT_DIVIDES = prove
  76  (`!m n. m <= n ==> ?d. FACT(n) = d * FACT(m)`,
  77   REWRITE_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
  78   X_GEN_TAC `m:num` THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  79   SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
  80   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT] THEN
  81   ASM_MESON_TAC[MULT_AC; MULT_CLAUSES]);;
  82
  83 let FACT_DIV_MULT = prove
  84  (`!m n. m <= n ==> FACT n = (FACT(n) DIV FACT(m)) * FACT(m)`,
  85   REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o MATCH_MP FACT_DIVIDES) THEN
  86   ASM_REWRITE_TAC[] THEN
  87   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
  88   ASM_SIMP_TAC[DIV_MULT; GSYM LT_NZ; FACT_LT]);;
  89
  90 let HAS_SIZE_FUNSPACE_INJECTIVE = prove
  91  (`!s:A->bool t:B->bool m n.
  92         s HAS_SIZE m /\ t HAS_SIZE n
  93         ==> {f | f IN (s --> t) /\
  94                  (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}
  95             HAS_SIZE (if n < m then 0 else (FACT n) DIV (FACT(n - m)))`,
  96   REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
  97   ONCE_REWRITE_TAC[IMP_CONJ] THEN
  98   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
  99   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
 100    [SIMP_TAC[CARD_CLAUSES; FINITE_RULES; FUNSPACE_EMPTY; NOT_IN_EMPTY] THEN
 101     REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 102     REWRITE_TAC[SET_RULE `{x | x IN s} = s`] THEN
 103     ASM_SIMP_TAC[FINITE_RULES; CARD_CLAUSES; FACT] THEN
 104     SIMP_TAC[NOT_IN_EMPTY; LT; SUB_0; DIV_REFL; GSYM LT_NZ; FACT_LT] THEN
 105     REWRITE_TAC[ARITH];
 106     ALL_TAC] THEN
 107   REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
 108   SUBGOAL_THEN
 109    `{f | f IN (x INSERT s) --> t /\
 110     (!u v. u IN (x INSERT s) /\ v IN (x INSERT s) /\ f u = f v ==> u = v)} =
 111         IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
 112               {y,g | y IN t /\
 113                      g IN {f | f IN (s --> (t DELETE y)) /\
 114                                !u v. u IN s /\ v IN s /\ f u = f v ==> u = v}}`
 115   SUBST1_TAC THENL
 116    [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
 117     ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
 118     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
 119     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 120     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 121     X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
 122      [REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
 123       STRIP_TAC THEN MAP_EVERY EXISTS_TAC
 124        [`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
 125       REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[];
 126       REWRITE_TAC[IN_INSERT; IN_DELETE; LEFT_IMP_EXISTS_THM] THEN
 127       MAP_EVERY X_GEN_TAC [`y:B`; `g:A->B`] THEN
 128       STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 129       ASM_MESON_TAC[]];
 130     ALL_TAC] THEN
 131   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
 132    [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
 133     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 134     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
 135     REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
 136     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 137     REWRITE_TAC[FUN_EQ_THM; funspace; IN_ELIM_THM; IN_INSERT; IN_DELETE] THEN
 138     REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
 139      [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN
 140     X_GEN_TAC `u:A` THEN ASM_CASES_TAC `u:A = x` THEN ASM_MESON_TAC[];
 141     ALL_TAC] THEN
 142   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[CARD_CLAUSES; EXP] THEN
 143   SUBGOAL_THEN
 144    `(if n < SUC (CARD s) then 0 else FACT n DIV FACT (n - SUC (CARD s))) =
 145     n * (if (n - 1) < CARD(s:A->bool) then 0
 146          else FACT(n - 1) DIV FACT (n - 1 - CARD s))`
 147   SUBST1_TAC THENL
 148    [ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; LT_0] THEN
 149     ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (n - 1 < m <=> n < SUC m)`] THEN
 150     COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
 151     REWRITE_TAC[ARITH_RULE `n - SUC(m) = n - 1 - m`] THEN
 152     UNDISCH_TAC `~(n = 0)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
 153     INDUCT_TAC THEN REWRITE_TAC[FACT; SUC_SUB1] THEN DISCH_TAC THEN
 154     MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
 155     REWRITE_TAC[ADD_CLAUSES; FACT_LT; GSYM MULT_ASSOC] THEN
 156     AP_TERM_TAC THEN MATCH_MP_TAC FACT_DIV_MULT THEN ARITH_TAC;
 157     MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN
 158     X_GEN_TAC `y:B` THEN DISCH_TAC THEN
 159     FIRST_X_ASSUM MATCH_MP_TAC THEN
 160     RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
 161     ASM_SIMP_TAC[HAS_SIZE; FINITE_DELETE; CARD_DELETE]]);;
 162
 163 (* ------------------------------------------------------------------------- *)
 164 (* So the actual birthday result.                                            *)
 165 (* ------------------------------------------------------------------------- *)
 166
 167 let HAS_SIZE_DIFF = prove
 168  (`!s t:A->bool m n.
 169         s SUBSET t /\ s HAS_SIZE m /\ t HAS_SIZE n
 170         ==> (t DIFF s) HAS_SIZE (n - m)`,
 171   SIMP_TAC[HAS_SIZE; FINITE_DIFF] THEN
 172   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 173   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 174   DISCH_THEN(SUBST_ALL_TAC o SYM) THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
 175   FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE
 176    `s SUBSET t ==> t = s UNION (t DIFF s)`)) THEN
 177   DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 178   ASM_SIMP_TAC[CARD_UNION; FINITE_DIFF; ADD_SUB2;
 179                SET_RULE `s INTER (t DIFF s) = {}`]);;
 180
 181 let BIRTHDAY_THM = prove
 182  (`!s:A->bool t:B->bool m n.
 183         s HAS_SIZE m /\ t HAS_SIZE n
 184         ==> {f | f IN (s --> t) /\
 185                  ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)}
 186             HAS_SIZE (if m <= n then (n EXP m) - (FACT n) DIV (FACT(n - m))
 187                       else n EXP m)`,
 188   REPEAT STRIP_TAC THEN
 189   REWRITE_TAC[SET_RULE
 190    `{f:A->B | f IN (s --> t) /\
 191               ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)} =
 192     (s --> t) DIFF
 193     {f | f IN (s --> t) /\
 194                  (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}`] THEN
 195   REWRITE_TAC[ARITH_RULE
 196    `(if a <= b then x - y else x) = x - (if b < a then 0 else y)`] THEN
 197   MATCH_MP_TAC HAS_SIZE_DIFF THEN
 198   ASM_SIMP_TAC[HAS_SIZE_FUNSPACE_INJECTIVE; HAS_SIZE_FUNSPACE] THEN
 199   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 200
 201 (* ------------------------------------------------------------------------- *)
 202 (* The usual explicit instantiation.                                         *)
 203 (* ------------------------------------------------------------------------- *)
 204
 205 let FACT_DIV_SIMP = prove
 206  (`!m n. m < n
 207          ==> (FACT n) DIV (FACT m) = n * FACT(n - 1) DIV FACT(m)`,
 208   GEN_TAC THEN REWRITE_TAC[LT_EXISTS; LEFT_IMP_EXISTS_THM] THEN
 209   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 210   SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
 211   REWRITE_TAC[ARITH_RULE `(m + SUC d) - 1 - m = d`] THEN
 212   REWRITE_TAC[ARITH_RULE `(m + SUC d) - 1 = m + d`; ADD_SUB2] THEN
 213   GEN_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
 214   REWRITE_TAC[FACT_LT; ARITH_RULE `x + 0 = x`] THEN REWRITE_TAC[FACT] THEN
 215   SIMP_TAC[GSYM MULT_ASSOC; GSYM FACT_DIV_MULT; LE_ADD] THEN
 216   REWRITE_TAC[ADD_CLAUSES; FACT]);;
 217
 218 let BIRTHDAY_THM_EXPLICIT = prove
 219  (`!s t. s HAS_SIZE 23 /\ t HAS_SIZE 365
 220          ==> 2 * CARD {f | f IN (s --> t) /\
 221                            ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)}
 222              >= CARD (s --> t)`,
 223   REPEAT GEN_TAC THEN DISCH_TAC THEN
 224   FIRST_ASSUM(MP_TAC o MATCH_MP BIRTHDAY_THM) THEN
 225   FIRST_ASSUM(MP_TAC o MATCH_MP HAS_SIZE_FUNSPACE) THEN
 226   CONV_TAC(ONCE_DEPTH_CONV NUM_SUB_CONV) THEN
 227   REPEAT(CHANGED_TAC
 228    (SIMP_TAC[FACT_DIV_SIMP; ARITH_LE; ARITH_LT] THEN
 229     CONV_TAC(ONCE_DEPTH_CONV NUM_SUB_CONV))) THEN
 230   SIMP_TAC[DIV_REFL; GSYM LT_NZ; FACT_LT] THEN
 231   REWRITE_TAC[HAS_SIZE] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 232   CONV_TAC NUM_REDUCE_CONV);;