Examples/vitali.ml

   1 (* ========================================================================= *)
   2 (* Existence of a (bounded) non-measurable set of reals.                     *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/realanalysis.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Classic Vitali proof (positive case simplified via Steinhaus's theorem).  *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let NON_MEASURABLE_SET = prove
  12  (`?s. real_bounded s /\ ~real_measurable s`,
  13   MAP_EVERY ABBREV_TAC
  14    [`equiv = \x y. &0 <= x /\ x < &1 /\ &0 <= y /\ y < &1 /\ rational(x - y)`;
  15     `(canonize:real->real) = \x. @y. equiv x y`;
  16     `V = IMAGE (canonize:real->real) {x | &0 <= x /\ x < &1}`] THEN
  17   SUBGOAL_THEN `!x. equiv x x <=> &0 <= x /\ x < &1` ASSUME_TAC THENL
  18    [EXPAND_TAC "equiv" THEN REWRITE_TAC[REAL_SUB_REFL; RATIONAL_NUM; CONJ_ACI];
  19     ALL_TAC] THEN
  20   SUBGOAL_THEN `!x y:real. equiv x y ==> equiv y x` ASSUME_TAC THENL
  21    [EXPAND_TAC "equiv" THEN MESON_TAC[RATIONAL_NEG; REAL_NEG_SUB];
  22     ALL_TAC] THEN
  23   SUBGOAL_THEN `!x y z:real. equiv x y /\ equiv y z ==> equiv x z`
  24   ASSUME_TAC THENL
  25    [EXPAND_TAC "equiv" THEN MESON_TAC[RATIONAL_ADD;
  26         REAL_ARITH `x - z:real = (x - y) + (y - z)`];
  27     ALL_TAC] THEN
  28   SUBGOAL_THEN
  29    `!x. &0 <= x /\ x < &1 ==> (equiv:real->real->bool) x (canonize x)`
  30   ASSUME_TAC THENL
  31    [REPEAT STRIP_TAC THEN EXPAND_TAC "canonize" THEN ASM_MESON_TAC[];
  32     ALL_TAC] THEN
  33   SUBGOAL_THEN
  34    `!x y. x IN V /\ y IN V /\ rational(x - y) ==> x = y`
  35   ASSUME_TAC THENL
  36    [EXPAND_TAC "V" THEN
  37     REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
  38     REWRITE_TAC[IN_ELIM_THM] THEN
  39     X_GEN_TAC `x:real` THEN STRIP_TAC THEN
  40     X_GEN_TAC `y:real` THEN STRIP_TAC THEN STRIP_TAC THEN
  41     EXPAND_TAC "canonize" THEN AP_TERM_TAC THEN
  42     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `z:real` THEN
  43     SUBGOAL_THEN `equiv ((canonize:real->real) x) (canonize y) :bool`
  44      (fun th -> MP_TAC th THEN ASM_MESON_TAC[]) THEN
  45     EXPAND_TAC "equiv" THEN REWRITE_TAC[] THEN ASM_MESON_TAC[];
  46     ALL_TAC] THEN
  47   EXISTS_TAC `V:real->bool` THEN CONJ_TAC THENL
  48    [MATCH_MP_TAC REAL_BOUNDED_SUBSET THEN
  49     EXISTS_TAC `real_interval[&0,&1]` THEN
  50     REWRITE_TAC[REAL_BOUNDED_REAL_INTERVAL; SUBSET; IN_REAL_INTERVAL] THEN
  51     ASM SET_TAC[REAL_LT_IMP_LE];
  52     DISCH_TAC] THEN
  53   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HAS_REAL_MEASURE_MEASURE]) THEN
  54   FIRST_ASSUM(MP_TAC o MATCH_MP REAL_MEASURE_POS_LE) THEN
  55   REWRITE_TAC[REAL_ARITH `&0 <= x <=> &0 < x \/ x = &0`] THEN
  56   DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC SUBST1_TAC) THENL
  57    [MP_TAC(ISPEC `V:real->bool` REAL_STEINHAUS) THEN ASM_REWRITE_TAC[] THEN
  58     MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
  59     DISCH_THEN(X_CHOOSE_THEN `d:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  60     MP_TAC(ISPECL [`d / &2`; `d / &2`] RATIONAL_APPROXIMATION) THEN
  61     ASM_REWRITE_TAC[REAL_HALF; LEFT_IMP_EXISTS_THM] THEN
  62     X_GEN_TAC `q:real` THEN STRIP_TAC THEN
  63     REWRITE_TAC[SUBSET; IN_REAL_INTERVAL; IN_ELIM_THM] THEN
  64     DISCH_THEN(MP_TAC o SPEC `q:real`) THEN REWRITE_TAC[NOT_IMP] THEN
  65     CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  66     ASM_CASES_TAC `q = &0` THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  67     ASM_MESON_TAC[REAL_SUB_0];
  68     REWRITE_TAC[HAS_REAL_MEASURE_0] THEN DISCH_TAC THEN
  69     SUBGOAL_THEN `?r. rational = IMAGE r (:num)` STRIP_ASSUME_TAC THENL
  70      [MATCH_MP_TAC COUNTABLE_AS_IMAGE THEN REWRITE_TAC[COUNTABLE_RATIONAL] THEN
  71       REWRITE_TAC[FUN_EQ_THM; EMPTY] THEN MESON_TAC[RATIONAL_NUM];
  72       ALL_TAC] THEN
  73     MP_TAC(ISPEC `\n. IMAGE (\x. (r:num->real) n + x) V`
  74       REAL_NEGLIGIBLE_COUNTABLE_UNIONS) THEN
  75     ANTS_TAC THENL [ASM_SIMP_TAC[REAL_NEGLIGIBLE_TRANSLATION]; ALL_TAC] THEN
  76     SUBGOAL_THEN `~(real_negligible(real_interval(&0,&1)))` MP_TAC THENL
  77      [SIMP_TAC[GSYM REAL_MEASURABLE_REAL_MEASURE_EQ_0;
  78                REAL_MEASURABLE_REAL_INTERVAL; REAL_MEASURE_REAL_INTERVAL] THEN
  79       REAL_ARITH_TAC;
  80       ALL_TAC] THEN
  81     REWRITE_TAC[CONTRAPOS_THM] THEN
  82     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_NEGLIGIBLE_SUBSET) THEN
  83     REWRITE_TAC[SUBSET; IN_REAL_INTERVAL] THEN
  84     X_GEN_TAC `x:real` THEN STRIP_TAC THEN
  85     SUBGOAL_THEN `(equiv:real->real->bool) x (canonize x)` MP_TAC THENL
  86      [ASM_MESON_TAC[REAL_LT_IMP_LE]; ALL_TAC] THEN
  87     EXPAND_TAC "equiv" THEN ASM_REWRITE_TAC[] THEN
  88     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  89     GEN_REWRITE_TAC LAND_CONV [GSYM IN] THEN
  90     REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; IN_UNIV] THEN
  91     DISCH_THEN(X_CHOOSE_THEN `n:num` (ASSUME_TAC o SYM)) THEN
  92     ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN REWRITE_TAC[UNIONS_IMAGE] THEN
  93     REWRITE_TAC[IN_ELIM_THM; IN_IMAGE] THEN
  94     MAP_EVERY EXISTS_TAC [`n:num`; `(canonize:real->real) x`] THEN
  95     ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
  96     EXPAND_TAC "V" THEN MATCH_MP_TAC FUN_IN_IMAGE THEN
  97     REWRITE_TAC[IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC]);;