100/realsuncountable.ml

   1 (* ========================================================================= *)
   2 (* #22: non-denumerability of continuum (= uncountability of the reals).     *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/card.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of countability.                                               *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let countable = new_definition
  14   `countable s <=> s <=_c (UNIV:num->bool)`;;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* Set of repeating digits and its countability.                             *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 let repeating = new_definition
  21  `repeating = {s:num->bool | ?n. !m. m >= n ==> s m}`;;
  22
  23 let BINARY_BOUND = prove
  24 (`!n. nsum(0..n) (\i. if b(i) then 2 EXP i else 0) < 2 EXP (n + 1)`,
  25   INDUCT_TAC THEN REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THENL
  26    [COND_CASES_TAC THEN REWRITE_TAC[ARITH]; ALL_TAC] THEN
  27   POP_ASSUM MP_TAC THEN REWRITE_TAC[LE_0; EXP_ADD; EXP_1; EXP] THEN
  28   ARITH_TAC);;
  29
  30 let BINARY_DIV_POW2 = prove
  31  (`!n. (nsum(0..n) (\i. if b(i) then 2 EXP i else 0)) DIV (2 EXP (SUC n)) = 0`,
  32   SIMP_TAC[ADD1; DIV_LT; BINARY_BOUND]);;
  33
  34 let PLUS_MOD_REFL = prove
  35  (`!a b. ~(b = 0) ==> (a + b) MOD b = a MOD b`,
  36   REPEAT STRIP_TAC THEN MATCH_MP_TAC MOD_EQ THEN MESON_TAC[MULT_CLAUSES]);;
  37
  38 let BINARY_PLUS_DIV_POW2 = prove
  39  (`!n. (nsum(0..n) (\i. if b(i) then 2 EXP i else 0) + 2 EXP (SUC n))
  40        DIV (2 EXP (SUC n)) = 1`,
  41   GEN_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN
  42   EXISTS_TAC `nsum(0..n) (\i. if b(i) then 2 EXP i else 0)` THEN
  43   ASM_REWRITE_TAC[BINARY_BOUND; ADD1] THEN
  44   REWRITE_TAC[ADD_AC; MULT_CLAUSES]);;
  45
  46 let BINARY_UNIQUE_LEMMA = prove
  47  (`!n. nsum(0..n) (\i. if b(i) then 2 EXP i else 0) =
  48        nsum(0..n) (\i. if c(i) then 2 EXP i else 0)
  49        ==> !i. i <= n ==> (b(i) <=> c(i))`,
  50   INDUCT_TAC THEN REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THENL
  51    [SIMP_TAC[LE] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH]);
  52     REWRITE_TAC[LE_0]] THEN
  53   REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THENL
  54    [UNDISCH_THEN `i = SUC n` SUBST_ALL_TAC THEN
  55     FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x DIV (2 EXP (SUC n))`) THEN
  56     REPEAT COND_CASES_TAC THEN
  57     ASM_REWRITE_TAC[ADD_CLAUSES; BINARY_DIV_POW2; BINARY_PLUS_DIV_POW2] THEN
  58     REWRITE_TAC[ARITH_EQ];
  59     FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x MOD (2 EXP (SUC n))`) THEN
  60     REPEAT COND_CASES_TAC THEN
  61     SIMP_TAC[ADD_CLAUSES; BINARY_BOUND; MOD_LT; PLUS_MOD_REFL; EXP_EQ_0; ARITH;
  62              ADD1] THEN
  63     ASM_MESON_TAC[LE_REFL]]);;
  64
  65 let COUNTABLE_REPEATING = prove
  66  (`countable repeating`,
  67   REWRITE_TAC[countable] THEN
  68   TRANS_TAC CARD_LE_TRANS `(UNIV:num->bool) *_c (UNIV:num->bool)` THEN
  69   CONJ_TAC THENL
  70     [ALL_TAC;
  71      MATCH_MP_TAC CARD_EQ_IMP_LE THEN REWRITE_TAC[CARD_SQUARE_NUM]] THEN
  72   REWRITE_TAC[le_c] THEN EXISTS_TAC
  73    `\s:num->bool. let n = minimal n. !m. m >= n ==> s m in
  74                   n,nsum(0..n) (\i. if s(i) then 2 EXP i else 0)` THEN
  75   REWRITE_TAC[repeating; IN_ELIM_THM] THEN CONJ_TAC THENL
  76    [GEN_TAC THEN LET_TAC THEN REWRITE_TAC[mul_c; IN_ELIM_THM; IN_UNIV] THEN
  77     MESON_TAC[];
  78     ALL_TAC] THEN
  79   MAP_EVERY X_GEN_TAC [`s:num->bool`; `t:num->bool`] THEN
  80   ONCE_REWRITE_TAC[MINIMAL] THEN
  81   ABBREV_TAC `k = minimal n. !m. m >= n ==> s m` THEN
  82   ABBREV_TAC `l = minimal n. !m. m >= n ==> t m` THEN
  83   ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; PAIR_EQ] THEN
  84   REPEAT(POP_ASSUM(K ALL_TAC)) THEN
  85   ASM_CASES_TAC `l:num = k` THEN ASM_REWRITE_TAC[] THEN
  86   FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[FUN_EQ_THM; GE] THEN
  87   STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP BINARY_UNIQUE_LEMMA) THEN
  88   ASM_MESON_TAC[LE_CASES]);;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Canonical digits and their uncountability.                                *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let canonical = new_definition
  95  `canonical = {s:num->bool | !n. ?m. m >= n /\ ~(s m)}`;;
  96
  97 let UNCOUNTABLE_CANONICAL = prove
  98  (`~countable canonical`,
  99   REWRITE_TAC[countable] THEN STRIP_TAC THEN
 100   MP_TAC (INST_TYPE [`:num`,`:A`] CANTOR_THM_UNIV) THEN
 101   REWRITE_TAC[CARD_NOT_LT] THEN
 102   MP_TAC(ISPECL [`canonical`; `repeating`] CARD_DISJOINT_UNION) THEN
 103   ANTS_TAC THENL
 104    [REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM;
 105                 canonical; repeating; GE] THEN
 106     MESON_TAC[];
 107     ALL_TAC] THEN
 108   SUBGOAL_THEN `canonical UNION repeating = UNIV` SUBST1_TAC THENL
 109    [REWRITE_TAC[EXTENSION; IN_UNION; IN_ELIM_THM;
 110                 canonical; repeating; GE; IN_UNIV] THEN
 111     MESON_TAC[];
 112     ALL_TAC] THEN
 113   DISCH_TAC THEN TRANS_TAC CARD_LE_TRANS `canonical +_c repeating` THEN
 114   ASM_SIMP_TAC[CARD_EQ_IMP_LE] THEN
 115   TRANS_TAC CARD_LE_TRANS `(UNIV:num->bool) +_c (UNIV:num->bool)` THEN
 116   CONJ_TAC THENL
 117    [ASM_MESON_TAC[countable; COUNTABLE_REPEATING; CARD_LE_ADD];
 118     MATCH_MP_TAC CARD_ADD_ABSORB_LE THEN
 119     REWRITE_TAC[num_INFINITE; CARD_LE_REFL]]);;
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Injection of canonical digits into the reals.                             *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 needs "Library/analysis.ml";;
 126
 127 prioritize_real();;
 128
 129 let SUM_BINSEQUENCE_LBOUND = prove
 130  (`!m n. &0 <= sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0)`,
 131   MATCH_MP_TAC SUM_POS THEN GEN_TAC THEN REWRITE_TAC[] THEN
 132   COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL; REAL_LE_INV_EQ] THEN
 133   SIMP_TAC[REAL_POW_LE; REAL_POS]);;
 134
 135 let SUM_BINSEQUENCE_UBOUND_SHARP = prove
 136  (`!s m n. sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0)
 137              <= &2 / &2 pow m - &2 / &2 pow (m + n)`,
 138   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN
 139   REWRITE_TAC[ADD_CLAUSES; REAL_SUB_REFL; REAL_LE_REFL] THEN
 140   MATCH_MP_TAC(REAL_ARITH
 141    `&0 <= y /\ x + y <= a ==> x + (if b then y else &0) <= a`) THEN
 142   SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
 143   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 144    `x <= a ==> a + y <= b ==> x + y <= b`)) THEN
 145   REWRITE_TAC[real_pow; real_div; REAL_INV_MUL] THEN REAL_ARITH_TAC);;
 146
 147 let SUMMABLE_BINSEQUENCE = prove
 148  (`!s. summable (\i. if s(i) then inv(&2 pow i) else &0)`,
 149   GEN_TAC THEN REWRITE_TAC[summable; sums; GSYM convergent] THEN
 150   MATCH_MP_TAC SEQ_ICONV THEN REWRITE_TAC[MR1_BOUNDED] THEN CONJ_TAC THENL
 151    [MAP_EVERY EXISTS_TAC [`&2`; `0`] THEN
 152     REWRITE_TAC[GE; LE_0; LE_REFL] THEN X_GEN_TAC `n:num` THEN
 153     MP_TAC(SPECL [`s:num->bool`; `0`; `n:num`]
 154          SUM_BINSEQUENCE_UBOUND_SHARP) THEN
 155     MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ a < b ==> x <= a ==> abs x < b`) THEN
 156     REWRITE_TAC[SUM_BINSEQUENCE_LBOUND; real_pow; REAL_DIV_1; ADD_CLAUSES] THEN
 157     REWRITE_TAC[REAL_ARITH `a - x < a <=> &0 < x`] THEN
 158     SIMP_TAC[REAL_LT_DIV; REAL_POW_LT; REAL_OF_NUM_LT; ARITH];
 159     GEN_TAC THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE; LE_EXISTS] THEN
 160     DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[GSYM SUM_SPLIT] THEN
 161     MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> a + x >= a`) THEN
 162     REWRITE_TAC[SUM_BINSEQUENCE_LBOUND]]);;
 163
 164 let SUMS_BINSEQUENCE = prove
 165  (`!s. (\i. if s(i) then inv(&2 pow i) else &0) sums
 166        (suminf (\i. if s(i) then inv(&2 pow i) else &0))`,
 167   SIMP_TAC[SUMMABLE_SUM; SUMMABLE_BINSEQUENCE]);;
 168
 169 let SUM_BINSEQUENCE_UBOUND_LE = prove
 170  (`!s m n. sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0) <= &2 / &2 pow m`,
 171   MP_TAC SUM_BINSEQUENCE_UBOUND_SHARP THEN
 172   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 173   MATCH_MP_TAC(REAL_ARITH `&0 <= b ==> x <= a - b ==> x <= a`) THEN
 174   SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; REAL_POS]);;
 175
 176 (* ------------------------------------------------------------------------- *)
 177 (* The main injection and hence main theorem.                                *)
 178 (* ------------------------------------------------------------------------- *)
 179
 180 let SUMINF_INJ_LEMMA = prove
 181  (`!s t n. ~(s n) /\ t n /\
 182            (!m. m < n ==> (s(m) <=> t(m))) /\
 183            (!n. ?m. m >= n /\ ~(s m))
 184            ==> suminf(\n. if s n then inv (&2 pow n) else &0)
 185                 < suminf(\n. if t n then inv (&2 pow n) else &0)`,
 186   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
 187   EXISTS_TAC `sum(0,n+1) (\n. if t n then inv (&2 pow n) else &0)` THEN
 188   CONJ_TAC THENL
 189    [ALL_TAC;
 190     MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC
 191      [`\k:num. sum(0,n+1) (\n. if t n then inv (&2 pow n) else &0)`;
 192       `\n:num. sum(0,n) (\n. if t n then inv (&2 pow n) else &0)`] THEN
 193     REWRITE_TAC[SEQ_CONST; GSYM sums; SUMS_BINSEQUENCE] THEN
 194     EXISTS_TAC `n + 1` THEN X_GEN_TAC `m:num` THEN
 195     REWRITE_TAC[GE; LE_EXISTS] THEN DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
 196     REWRITE_TAC[GSYM ADD1] THEN
 197     REWRITE_TAC[GSYM SUM_SPLIT; REAL_LE_ADDR; SUM_BINSEQUENCE_LBOUND]] THEN
 198   ASM_REWRITE_TAC[GSYM SUM_SPLIT; SUM_1; ADD_CLAUSES] THEN
 199   UNDISCH_THEN `!n:num. ?m. m >= n /\ ~s m` (MP_TAC o SPEC `n + 1`) THEN
 200   REWRITE_TAC[GE] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 201   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC
 202     `sum(0,m) (\n. if s n then inv (&2 pow n) else &0) + inv(&2 pow m)` THEN
 203   CONJ_TAC THENL
 204    [MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC
 205      [`\n:num. sum(0,n) (\n. if s n then inv (&2 pow n) else &0)`;
 206       `\k:num. sum(0,m) (\n. if s n then inv(&2 pow n) else &0) +
 207                inv(&2 pow m)`] THEN
 208     REWRITE_TAC[SEQ_CONST; GSYM sums; SUMS_BINSEQUENCE] THEN
 209     EXISTS_TAC `m:num` THEN REWRITE_TAC[GE; LE_REFL] THEN
 210     X_GEN_TAC `r:num` THEN REWRITE_TAC[LE_EXISTS] THEN
 211     DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
 212     REWRITE_TAC[GSYM SUM_SPLIT; REAL_LE_LADD; ADD_CLAUSES] THEN
 213     DISJ_CASES_THEN SUBST_ALL_TAC (ARITH_RULE `p = 0 \/ p = 1 + PRE p`) THEN
 214     SIMP_TAC[sum; REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
 215     ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
 216     ASM_REWRITE_TAC[SUM_1; REAL_ADD_LID] THEN
 217     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 / &2 pow (m + 1)` THEN
 218     REWRITE_TAC[SUM_BINSEQUENCE_UBOUND_LE] THEN
 219     REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN CONV_TAC REAL_FIELD;
 220     ALL_TAC] THEN
 221   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 222   DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
 223   REWRITE_TAC[GSYM SUM_SPLIT] THEN
 224   ASM_REWRITE_TAC[ADD_CLAUSES; SUM_1; REAL_ADD_RID] THEN
 225   MATCH_MP_TAC(REAL_ARITH `a = b /\ c < e - d ==> (a + c) + d < b + e`) THEN
 226   CONJ_TAC THENL
 227    [MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[LE_0; ADD_CLAUSES]; ALL_TAC] THEN
 228   MATCH_MP_TAC REAL_LET_TRANS THEN
 229   EXISTS_TAC `&2 / &2 pow (n + 1) - &2 / &2 pow ((n + 1) + r)` THEN
 230   REWRITE_TAC[SUM_BINSEQUENCE_UBOUND_SHARP] THEN
 231   MATCH_MP_TAC(REAL_ARITH `a = b /\ d < c ==> a - c < b - d`) THEN
 232   CONJ_TAC THENL
 233    [REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN CONV_TAC REAL_FIELD;
 234     MATCH_MP_TAC(REAL_FIELD `&0 < inv(x) ==> inv(x) < &2 / x`) THEN
 235     SIMP_TAC[REAL_LT_INV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]]);;
 236
 237 let UNCOUNTABLE_REALS = prove
 238  (`~countable(UNIV:real->bool)`,
 239   MP_TAC UNCOUNTABLE_CANONICAL THEN REWRITE_TAC[CONTRAPOS_THM] THEN
 240   REWRITE_TAC[countable] THEN DISCH_TAC THEN
 241   TRANS_TAC CARD_LE_TRANS `UNIV:real->bool` THEN
 242   ASM_REWRITE_TAC[] THEN POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[le_c] THEN
 243   EXISTS_TAC `\s. suminf(\n. if s(n) then inv(&2 pow n) else &0)` THEN
 244   REWRITE_TAC[IN_UNIV] THEN
 245   MAP_EVERY X_GEN_TAC [`s:num->bool`; `t:num->bool`] THEN
 246   REWRITE_TAC[canonical; IN_ELIM_THM] THEN STRIP_TAC THEN
 247   REWRITE_TAC[FUN_EQ_THM] THEN
 248   GEN_REWRITE_TAC I [MESON[] `(!x. P x) <=> ~(?x. ~P x)`] THEN
 249   ONCE_REWRITE_TAC[MINIMAL] THEN
 250   ABBREV_TAC `n = minimal x. ~(s x <=> t x)` THEN
 251   FIRST_X_ASSUM(K ALL_TAC o check (is_var o rhs o concl)) THEN
 252   ASM_CASES_TAC `(t:num->bool) n` THEN ASM_REWRITE_TAC[] THEN
 253   STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SYM) THENL
 254    [MATCH_MP_TAC(REAL_ARITH `b < a ==> a = b ==> F`);
 255     MATCH_MP_TAC(REAL_ARITH `a < b ==> a = b ==> F`)] THEN
 256   MATCH_MP_TAC SUMINF_INJ_LEMMA THEN ASM_MESON_TAC[]);;