text_formalization/packing/pack2.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Author: John Harrison                                                      *)
   6 (* Date: 2010-03-16                                                           *)
   7 (*                                                                            *)
   8 (* This proves theorems about closed Voronoi cells and transfers the main     *)
   9 (* results proved in Pack1 by Nguyen Tat Thang from open to closed cells.     *)
  10 (* ========================================================================== *)
  11
  12 module type Pack2_type = sig
  13 end;;
  14
  15 flyspeck_needs "packing/pack1.hl";;
  16
  17 module Pack2  (* : Pack1_type *) = struct
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Slight variants of definitions, mainly to use IN.                         *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let PACKING = prove
  24  (`!s. packing s <=> !u v. u IN s /\ v IN s /\ dist(u,v) < &2 ==> u = v`,
  25   REWRITE_TAC[IN; GSYM REAL_NOT_LE] THEN MESON_TAC[Pack1.packing]);;
  26
  27 let VORONOI_OPEN = prove
  28  (`!s v. voronoi_open s v =
  29           {x | !w. w IN s /\ ~(w = v) ==> dist(x,v) < dist(x,w)}`,
  30   REWRITE_TAC[Sphere.voronoi_open; IN]);;
  31
  32 let VORONOI_CLOSED = prove
  33  (`!s v. voronoi_closed s v = {x | !w. w IN s ==> dist(x,v) <= dist(x,w)}`,
  34   REWRITE_TAC[Sphere.voronoi_closed; IN]);;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Minor variant of KIUMVTC without 0 <= r condition.                        *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 let KIUMVTC = prove
  41  (`!p r S. packing S ==> FINITE(S INTER ball(p,r))`,
  42   REPEAT STRIP_TAC THEN ASM_CASES_TAC `&0 <= r` THENL
  43    [ASM_SIMP_TAC[Pack1.KIUMVTC];
  44     FIRST_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH `~(&0 <= v) ==> v <= &0`)) THEN
  45     SIMP_TAC[INTER_EMPTY; BALL_EMPTY; FINITE_EMPTY]]);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* The basic lemmas about closed Voronoi cells.                              *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 let BIS_LE = prove
  52  (`!u v. bis_le u v =
  53            {x | (&2 % (v - u)) dot x <= norm(v) pow 2 - norm(u) pow 2}`,
  54   REPEAT GEN_TAC THEN REWRITE_TAC[Sphere.bis_le; dist; NORM_LE] THEN
  55   REWRITE_TAC[EXTENSION; IN_ELIM_THM; DOT_LMUL; DOT_LSUB; DOT_RSUB] THEN
  56   REWRITE_TAC[NORM_POW_2; DOT_SYM] THEN REAL_ARITH_TAC);;
  57
  58 let BIS_LT = prove
  59  (`!u v. bis_lt u v =
  60            {x | (&2 % (v - u)) dot x < norm(v) pow 2 - norm(u) pow 2}`,
  61   REPEAT GEN_TAC THEN REWRITE_TAC[Sphere.bis_lt; dist; NORM_LT] THEN
  62   REWRITE_TAC[EXTENSION; IN_ELIM_THM; DOT_LMUL; DOT_LSUB; DOT_RSUB] THEN
  63   REWRITE_TAC[NORM_POW_2; DOT_SYM] THEN REAL_ARITH_TAC);;
  64
  65 let VORONOI_CLOSED_ALT = prove
  66  (`!s v. voronoi_closed s v =
  67              {x | !w. w IN s /\ ~(w = v) ==> dist(x,v) <= dist(x,w)}`,
  68   REWRITE_TAC[VORONOI_CLOSED; EXTENSION; IN_ELIM_THM] THEN
  69   MESON_TAC[REAL_LE_REFL]);;
  70
  71 let VORONOI_CLOSED_AS_INTERSECTION = prove
  72  (`!s v. voronoi_closed s v = INTERS (IMAGE (bis_le v) (s DELETE v))`,
  73   REWRITE_TAC[Sphere.bis_le; VORONOI_CLOSED_ALT; INTERS_IMAGE] THEN
  74   REWRITE_TAC[IN_DELETE; IN_ELIM_THM]);;
  75
  76 let VORONOI_OPEN_AS_INTERSECTION = prove
  77  (`!s v. voronoi_open s v = INTERS (IMAGE (bis_lt v) (s DELETE v))`,
  78   REWRITE_TAC[Sphere.bis_lt; VORONOI_OPEN; INTERS_IMAGE] THEN
  79   REWRITE_TAC[IN_DELETE; IN_ELIM_THM]);;
  80
  81 let CLOSED_VORONOI_CLOSED = prove
  82  (`!s v. closed(voronoi_closed s v)`,
  83   REPEAT GEN_TAC THEN REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN
  84   MATCH_MP_TAC CLOSED_INTERS THEN
  85   REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CLOSED_HALFSPACE_LE]);;
  86
  87 let VORONOI_CLOSED_SUBSET_BALL = prove
  88  (`!s v:real^N. saturated s ==> voronoi_closed s v SUBSET ball(v,&2)`,
  89   REPEAT STRIP_TAC THEN REWRITE_TAC[VORONOI_CLOSED; SUBSET] THEN
  90   REWRITE_TAC[IN_ELIM_THM; IN_BALL] THEN
  91   X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
  92   FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N` o GEN_REWRITE_RULE I
  93    [Pack1.saturated]) THEN
  94   DISCH_THEN(X_CHOOSE_THEN `y:real^N` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  95   FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN
  96   ASM_REWRITE_TAC[] THEN NORM_ARITH_TAC);;
  97
  98 let BOUNDED_VORONOI_CLOSED = prove
  99  (`!s v. saturated s ==> bounded(voronoi_closed s v)`,
 100   MESON_TAC[VORONOI_CLOSED_SUBSET_BALL; BOUNDED_SUBSET; BOUNDED_BALL]);;
 101
 102 let COMPACT_VORONOI_CLOSED = prove
 103  (`!s v. saturated s ==> compact(voronoi_closed s v)`,
 104   MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED; CLOSED_VORONOI_CLOSED;
 105             BOUNDED_VORONOI_CLOSED]);;
 106
 107 let CONVEX_VORONOI_CLOSED = prove
 108  (`!s v. convex(voronoi_closed s v)`,
 109   REPEAT GEN_TAC THEN REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN
 110   MATCH_MP_TAC CONVEX_INTERS THEN
 111   REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CONVEX_HALFSPACE_LE]);;
 112
 113 let BASE_IN_VORONOI_CLOSED = prove
 114  (`!s v. v IN voronoi_closed s v`,
 115   REWRITE_TAC[Sphere.voronoi_closed; DIST_REFL; DIST_POS_LE; IN_ELIM_THM]);;
 116
 117 let CBALL_SUBSET_VORONOI_CLOSED = prove
 118  (`!s v:real^3. packing s /\ v IN s ==> cball(v,&1) SUBSET voronoi_closed s v`,
 119   REWRITE_TAC[PACKING; SUBSET; VORONOI_CLOSED_ALT; IN_CBALL; IN_ELIM_THM] THEN
 120   REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `x:real^3` THEN
 121   DISCH_TAC THEN X_GEN_TAC `w:real^3` THEN STRIP_TAC THEN
 122   FIRST_X_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
 123   ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN NORM_ARITH_TAC);;
 124
 125 let VORONOI_CLOSED_PARTITION_STRONG = prove
 126  (`!s. closed s /\ ~(s = {})
 127        ==> UNIONS { voronoi_closed s v |v| v IN s} = (:real^3)`,
 128   GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
 129   REWRITE_TAC[UNIONS_IMAGE; EXTENSION; IN_UNIV; IN_ELIM_THM] THEN
 130   REWRITE_TAC[VORONOI_CLOSED; IN_ELIM_THM] THEN
 131   X_GEN_TAC `x:real^3` THEN EXISTS_TAC `closest_point s (x:real^3)` THEN
 132   MATCH_MP_TAC CLOSEST_POINT_EXISTS THEN ASM_REWRITE_TAC[]);;
 133
 134 let PACKING_IMP_CLOSED = prove
 135  (`!s. packing s ==> closed s`,
 136   REWRITE_TAC[PACKING; dist] THEN REPEAT STRIP_TAC THEN
 137   MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN EXISTS_TAC `&2` THEN
 138   CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_MESON_TAC[NORM_SUB]);;
 139
 140 let SATURATED_IMP_NONEMPTY = prove
 141  (`!s. saturated s ==> ~(s = {})`,
 142   REWRITE_TAC[Pack1.saturated] THEN SET_TAC[]);;
 143
 144 let VORONOI_CLOSED_PARTITION = prove
 145  (`!s. packing s /\ saturated s
 146        ==> UNIONS { voronoi_closed s v |v| v IN s} = (:real^3)`,
 147   SIMP_TAC[VORONOI_CLOSED_PARTITION_STRONG; PACKING_IMP_CLOSED;
 148            SATURATED_IMP_NONEMPTY]);;
 149
 150 let VORONOI_CLOSED_AS_FINITE_INTERSECTION = prove
 151  (`!s v. packing s /\ saturated s /\ v IN s
 152          ==> voronoi_closed s v =
 153                 INTERS (IMAGE (bis_le v) ((s INTER ball(v,&4)) DELETE v))`,
 154   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 155    [REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN SET_TAC[]; ALL_TAC] THEN
 156   REWRITE_TAC[SUBSET] THEN X_GEN_TAC `p:real^3` THEN
 157   DISCH_TAC THEN
 158   SUBGOAL_THEN
 159    `?p':real^3. aff_ge {v} {p} INTER voronoi_closed s v = segment[v,p']`
 160   STRIP_ASSUME_TAC THENL
 161    [MATCH_MP_TAC HALFLINE_INTER_COMPACT_SEGMENT THEN
 162     ASM_SIMP_TAC[COMPACT_VORONOI_CLOSED; CONVEX_VORONOI_CLOSED;
 163                  BASE_IN_VORONOI_CLOSED];
 164     ALL_TAC] THEN
 165   MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
 166   SUBGOAL_THEN
 167    `(v:real^3) IN voronoi_closed s v /\ p' IN voronoi_closed s v /\
 168     p' IN aff_ge {v} {p}`
 169   STRIP_ASSUME_TAC THENL
 170    [ASM_MESON_TAC[ENDS_IN_SEGMENT; IN_INTER]; ALL_TAC] THEN
 171   SUBGOAL_THEN `p' IN ball(v:real^3,&2)` ASSUME_TAC THENL
 172    [ASM_MESON_TAC[VORONOI_CLOSED_SUBSET_BALL; SUBSET]; ALL_TAC] THEN
 173   SUBGOAL_THEN
 174    `?q:real^3.
 175        q IN ball(v,&2) /\
 176        q IN INTERS(IMAGE (bis_le v) ((s INTER ball (v,&4)) DELETE v)) /\
 177        ~(q IN voronoi_closed s v)`
 178   STRIP_ASSUME_TAC THENL
 179    [ASM_CASES_TAC `p IN ball(v:real^3,&2)` THENL
 180      [ASM_MESON_TAC[]; ALL_TAC] THEN
 181     ASM_CASES_TAC `p:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 182     SUBGOAL_THEN
 183      `?t. &0 <= t /\ t < &1 /\ p':real^3 = (&1 - t) % v + t % p`
 184     STRIP_ASSUME_TAC THENL
 185      [UNDISCH_TAC `(p':real^3) IN aff_ge {v} {p}` THEN
 186       ASM_REWRITE_TAC[HALFLINE; IN_SEGMENT; IN_ELIM_THM] THEN
 187       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:real` THEN STRIP_TAC THEN
 188       SUBGOAL_THEN `dist(v:real^3,p') < dist(v,p)` MP_TAC THENL
 189        [ASM_MESON_TAC[IN_BALL; REAL_ARITH `x < &2 /\ ~(y < &2) ==> x < y`];
 190         ASM_REWRITE_TAC[]] THEN
 191       REWRITE_TAC[VECTOR_ARITH
 192        `(&1 - t) % x + t % y:real^N = x + t % (y - x)`] THEN
 193       REWRITE_TAC[NORM_ARITH `dist(v:real^N,v + x) = norm x`; NORM_MUL] THEN
 194       REWRITE_TAC[dist; NORM_SUB] THEN
 195       ONCE_REWRITE_TAC[REAL_ARITH `x * y < y <=> x * y < &1 * y`] THEN
 196       ASM_SIMP_TAC[REAL_LT_RMUL_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
 197       ASM_REAL_ARITH_TAC;
 198       ALL_TAC] THEN
 199     MP_TAC(ISPECL [`v:real^3`; `&2`] OPEN_BALL) THEN
 200     REWRITE_TAC[open_def] THEN DISCH_THEN(MP_TAC o SPEC `p':real^3`) THEN
 201     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; dist] THEN
 202     X_GEN_TAC `e:real` THEN STRIP_TAC THEN
 203     ABBREV_TAC `u = t + min (e / &2 / norm(p - v:real^3)) ((&1 - t) / &2)` THEN
 204     SUBGOAL_THEN `&0 < u /\ t < u /\ u < &1` STRIP_ASSUME_TAC THENL
 205      [EXPAND_TAC "u" THEN MATCH_MP_TAC(REAL_ARITH
 206        `&0 < x /\ &0 <= t /\ t < &1
 207         ==> &0 < t + min x ((&1 - t) / &2) /\ t < t + min x ((&1 - t) / &2) /\
 208             t + min x ((&1 - t) / &2) < &1`) THEN
 209       ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
 210       ALL_TAC] THEN
 211     EXISTS_TAC `(&1 - u) % v + u % p:real^3` THEN REPEAT CONJ_TAC THENL
 212      [FIRST_X_ASSUM MATCH_MP_TAC THEN
 213       ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT; VECTOR_SUB_EQ;
 214         VECTOR_ARITH
 215        `((&1 - u) % v + u % p) - ((&1 - t) % v + t % p):real^N =
 216         (u - t) % (p - v)`] THEN
 217       EXPAND_TAC "u" THEN REWRITE_TAC[REAL_ADD_SUB] THEN
 218       MATCH_MP_TAC(REAL_ARITH
 219        `&0 < z /\ &0 < y /\ x = z / &2 ==> abs(min x y) < z`) THEN
 220       ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ] THEN
 221       REWRITE_TAC[real_div; REAL_MUL_AC] THEN ASM_REAL_ARITH_TAC;
 222       MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 223       CONJ_TAC THENL
 224        [MATCH_MP_TAC CONVEX_INTERS THEN
 225         REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CONVEX_HALFSPACE_LE];
 226         UNDISCH_TAC `(v:real^3) IN voronoi_closed s v` THEN
 227         REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN SET_TAC[]];
 228       DISCH_TAC THEN
 229       SUBGOAL_THEN `((&1 - u) % v + u % p:real^3) IN
 230                     (aff_ge {v} {p} INTER voronoi_closed s v)`
 231       MP_TAC THENL
 232        [ASM_REWRITE_TAC[IN_INTER; HALFLINE; IN_ELIM_THM] THEN
 233         ASM_MESON_TAC[REAL_LT_IMP_LE];
 234         ASM_REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT] THEN
 235         REWRITE_TAC[between; VECTOR_ARITH
 236          `(&1 - u) % x + u % y:real^N = x + u % (y - x)`] THEN
 237         REWRITE_TAC[NORM_ARITH `dist(v:real^N,v + x) = norm x`;
 238                     NORM_ARITH `dist(v + x:real^N,v + y) = norm(x - y)`] THEN
 239         REWRITE_TAC[GSYM VECTOR_SUB_RDISTRIB; NORM_MUL] THEN
 240         ASM_REWRITE_TAC[REAL_ENTIRE; NORM_EQ_0; VECTOR_SUB_EQ; REAL_ARITH
 241          `x * a:real = y * a + z * a <=> a * (x - y - z) = &0`] THEN
 242         ASM_REAL_ARITH_TAC]];
 243     MP_TAC(ISPEC `s:real^3->bool` VORONOI_CLOSED_PARTITION) THEN
 244     ASM_REWRITE_TAC[EXTENSION; IN_UNIV] THEN
 245     DISCH_THEN(MP_TAC o SPEC `q:real^3`) THEN REWRITE_TAC[] THEN
 246     ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
 247     REWRITE_TAC[UNIONS_IMAGE; IN_ELIM_THM] THEN
 248     DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THEN
 249     UNDISCH_TAC
 250      `(q:real^3) IN INTERS(IMAGE (bis_le v)
 251                                  ((s INTER ball(v,&4)) DELETE v))` THEN
 252     REWRITE_TAC[IN_INTERS; FORALL_IN_IMAGE] THEN
 253     DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN
 254     ASM_REWRITE_TAC[NOT_IMP; IN_DELETE; IN_INTER; IN_BALL] THEN
 255     ASM_CASES_TAC `w:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 256     ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 257      [MATCH_MP_TAC(NORM_ARITH
 258        `!q. dist(q,w) <= dist(q,v) /\ dist(v,q) < &2 ==> dist(v,w) < &4`) THEN
 259       EXISTS_TAC `q:real^3` THEN
 260       RULE_ASSUM_TAC(REWRITE_RULE[VORONOI_CLOSED; IN_ELIM_THM; IN_BALL]) THEN
 261       ASM_SIMP_TAC[];
 262       REWRITE_TAC[Sphere.bis_le; IN_ELIM_THM] THEN
 263       RULE_ASSUM_TAC(REWRITE_RULE[VORONOI_CLOSED; IN_ELIM_THM]) THEN
 264       ASM_MESON_TAC[REAL_LE_TRANS]]]);;
 265
 266 let POLYHEDRON_VORONOI_CLOSED = prove
 267  (`!s v. packing s /\ saturated s /\ v IN s
 268          ==> polyhedron(voronoi_closed s v)`,
 269   REPEAT STRIP_TAC THEN
 270   ASM_SIMP_TAC[VORONOI_CLOSED_AS_FINITE_INTERSECTION] THEN
 271   MATCH_MP_TAC POLYHEDRON_INTERS THEN
 272   ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE; FINITE_INTER;
 273                KIUMVTC; FORALL_IN_IMAGE] THEN
 274   REWRITE_TAC[BIS_LE; POLYHEDRON_HALFSPACE_LE]);;
 275
 276 let POLYTOPE_VORONOI_CLOSED = prove
 277  (`!s v. packing s /\ saturated s /\ v IN s
 278          ==> polytope(voronoi_closed s v)`,
 279   SIMP_TAC[POLYTOPE_EQ_BOUNDED_POLYHEDRON; POLYHEDRON_VORONOI_CLOSED;
 280            BOUNDED_VORONOI_CLOSED]);;
 281
 282 let MEASURABLE_VORONOI_CLOSED = prove
 283  (`!s v. saturated s ==> measurable(voronoi_closed s v)`,
 284   SIMP_TAC[MEASURABLE_COMPACT; COMPACT_VORONOI_CLOSED]);;
 285
 286 (* ------------------------------------------------------------------------- *)
 287 (* Relate closed and open Voronoi cells.                                     *)
 288 (* ------------------------------------------------------------------------- *)
 289
 290 let CLOSED_BIS_LE = prove
 291  (`!u v. closed(bis_le u v)`,
 292   REWRITE_TAC[BIS_LE; CLOSED_HALFSPACE_LE]);;
 293
 294 let OPEN_BIS_LT = prove
 295  (`!u v. open(bis_lt u v)`,
 296   REWRITE_TAC[BIS_LT; OPEN_HALFSPACE_LT]);;
 297
 298 let INTERIOR_BIS_LE = prove
 299  (`!u v. ~(v = u) ==> interior(bis_le u v) = bis_lt u v`,
 300   SIMP_TAC[BIS_LE; BIS_LT; INTERIOR_HALFSPACE_LE;
 301            VECTOR_ARITH `&2 % (v - w):real^N = vec 0 <=> v = w`]);;
 302
 303 let CLOSURE_BIS_LT = prove
 304  (`!u v. ~(v = u) ==> closure(bis_lt u v) = bis_le u v`,
 305   SIMP_TAC[BIS_LE; BIS_LT; CLOSURE_HALFSPACE_LT;
 306            VECTOR_ARITH `&2 % (v - w):real^N = vec 0 <=> v = w`]);;
 307
 308 let CLOSURE_VORONOI_OPEN = prove
 309  (`!S v:real^N. closure(voronoi_open S v) = voronoi_closed S v`,
 310   SIMP_TAC[VORONOI_CLOSED_AS_INTERSECTION; VORONOI_OPEN_AS_INTERSECTION] THEN
 311   SIMP_TAC[CLOSURE_INTERS_CONVEX_OPEN; FORALL_IN_IMAGE; BIS_LT;
 312            OPEN_HALFSPACE_LT; CONVEX_HALFSPACE_LT] THEN
 313   REPEAT GEN_TAC THEN COND_CASES_TAC THENL
 314    [POP_ASSUM MP_TAC THEN MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
 315     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
 316     EXISTS_TAC `v:real^N` THEN REWRITE_TAC[INTERS_IMAGE; IN_ELIM_THM] THEN
 317     SIMP_TAC[Sphere.bis_lt; IN_DELETE; IN_ELIM_THM; DIST_REFL; DIST_POS_LT];
 318     AP_TERM_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN MATCH_MP_TAC(SET_RULE
 319      `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN
 320     SIMP_TAC[IN_DELETE; o_THM; CLOSURE_BIS_LT]]);;
 321
 322 let INTERIOR_VORONOI_CLOSED_INTERIOR = prove
 323  (`!S v. interior(voronoi_closed S v) = interior(voronoi_open S v)`,
 324   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN] THEN
 325   MATCH_MP_TAC CONVEX_INTERIOR_CLOSURE THEN
 326   REWRITE_TAC[VORONOI_OPEN_AS_INTERSECTION] THEN
 327   MATCH_MP_TAC CONVEX_INTERS THEN
 328   REWRITE_TAC[FORALL_IN_IMAGE; BIS_LT; CONVEX_HALFSPACE_LT]);;
 329
 330 let INTERIOR_VORONOI_CLOSED = prove
 331  (`!S v. packing S /\ saturated S
 332          ==> interior(voronoi_closed S v) = voronoi_open S v`,
 333   SIMP_TAC[INTERIOR_VORONOI_CLOSED_INTERIOR; Pack1.open_voronoi;
 334            INTERIOR_OPEN]);;
 335
 336 let VORONOI_OPEN_AS_FINITE_INTERSECTION = prove
 337  (`!s v. packing s /\ saturated s /\ v IN s
 338          ==> voronoi_open s v =
 339                 INTERS(IMAGE (bis_lt v) ((s INTER ball(v,&4)) DELETE v))`,
 340   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM INTERIOR_VORONOI_CLOSED] THEN
 341   ASM_SIMP_TAC[VORONOI_CLOSED_AS_FINITE_INTERSECTION] THEN
 342   ASM_SIMP_TAC[INTERIOR_FINITE_INTERS; FINITE_IMAGE; KIUMVTC;
 343                FORALL_IN_IMAGE; FINITE_DELETE] THEN
 344   AP_TERM_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN MATCH_MP_TAC(SET_RULE
 345    `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN
 346   SIMP_TAC[IN_DELETE; o_THM; INTERIOR_BIS_LE]);;
 347
 348 let VORONOI_OPEN_SUBSET_CLOSED = prove
 349  (`!S v:real^N. (voronoi_open S v) SUBSET (voronoi_closed S v)`,
 350   REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN; CLOSURE_SUBSET]);;
 351
 352 (* ------------------------------------------------------------------------- *)
 353 (* And so.                                                                   *)
 354 (* ------------------------------------------------------------------------- *)
 355
 356 let MEASURE_VORONOI_CLOSED_OPEN = prove
 357  (`!s v:real^N. measure(voronoi_closed s v) = measure(voronoi_open s v)`,
 358   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN] THEN
 359   MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
 360   MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
 361   EXISTS_TAC `frontier(voronoi_open s (v:real^N))` THEN
 362   SIMP_TAC[NEGLIGIBLE_CONVEX_FRONTIER; Geomdetail.VORONOI_CONV] THEN
 363   REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
 364    `i SUBSET s /\ s SUBSET c
 365     ==> (c DIFF s UNION s DIFF c) SUBSET (c DIFF i)`) THEN
 366   REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET]);;
 367
 368 let INTER_VORONOI_SUBSET_BISECTOR = prove
 369  (`!s u v:real^N.
 370         u IN s /\ v IN s
 371         ==> (voronoi_closed s u) INTER (voronoi_closed s v)
 372             SUBSET {x | (&2 % (u - v)) dot x = norm(u) pow 2 - norm(v) pow 2}`,
 373   REPEAT STRIP_TAC THEN ASM_CASES_TAC `u:real^N = v` THENL
 374    [ASM_REWRITE_TAC[VECTOR_SUB_REFL; REAL_SUB_REFL; DOT_LZERO; DOT_LMUL;
 375                     REAL_MUL_RZERO] THEN
 376     SET_TAC[];
 377     REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION; INTERS_IMAGE] THEN
 378     REWRITE_TAC[IN_INTER; SUBSET; BIS_LE; IN_ELIM_THM] THEN
 379     X_GEN_TAC `w:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2
 380      (MP_TAC o SPEC `v:real^N`) (MP_TAC o SPEC `u:real^N`)) THEN
 381     ASM_REWRITE_TAC[IN_DELETE] THEN
 382     REWRITE_TAC[DOT_LMUL; DOT_LSUB] THEN REWRITE_TAC[DOT_SYM] THEN
 383     REAL_ARITH_TAC]);;
 384
 385 let NEGLIGIBLE_INTER_VORONOI_CLOSED = prove
 386  (`!s u v:real^N.
 387         u IN s /\ v IN s /\ ~(u = v)
 388         ==> negligible((voronoi_closed s u) INTER (voronoi_closed s v))`,
 389   REPEAT STRIP_TAC THEN MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN EXISTS_TAC
 390    `{x:real^N | (&2 % (u - v)) dot x = norm(u) pow 2 - norm(v) pow 2}` THEN
 391   ASM_SIMP_TAC[INTER_VORONOI_SUBSET_BISECTOR] THEN
 392   MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE THEN
 393   ASM_SIMP_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ] THEN REAL_ARITH_TAC);;
 394
 395 (* ------------------------------------------------------------------------- *)
 396 (* Transfer theorems from Pack1 to closed cells where applicable.            *)
 397 (* ------------------------------------------------------------------------- *)
 398
 399 let voronoi_version2 = prove
 400  (`!(v:real^3) (S:real^3-> bool).
 401       voronoi_closed S v = INTERS {bis_le x y | y IN (S DELETE v) /\ x = v}`,
 402   REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION; GSYM SIMPLE_IMAGE] THEN
 403   REPEAT GEN_TAC THEN AP_TERM_TAC THEN SET_TAC[]);;
 404
 405 let convex_voronoi = prove
 406  (`!(v:real^3) (S:real^3-> bool). convex(voronoi_closed S v)`,
 407   REWRITE_TAC[CONVEX_VORONOI_CLOSED]);;
 408
 409 let bound_voronoi = prove
 410  (`!(v:real^3) (S:real^3-> bool).
 411       saturated S ==>  bounded(voronoi_closed S v)`,
 412   SIMP_TAC[BOUNDED_VORONOI_CLOSED]);;
 413
 414 let finite_voronoi2 = prove
 415  (`!(v:real^3)(S:real^3 ->bool).
 416       packing S
 417       ==> FINITE {bis_le (x:real^3) (y:real^3) |
 418                   y IN (S DELETE v) /\ x = v /\ y IN ball(v, &4)}`,
 419   REWRITE_TAC[PACKING] THEN REPEAT STRIP_TAC THEN
 420   REWRITE_TAC[SET_RULE `{f x y | P y /\ x = v /\ Q y} =
 421                         IMAGE (f v) {y | P y /\ Q y}`] THEN
 422   MATCH_MP_TAC FINITE_IMAGE THEN MATCH_MP_TAC DISCRETE_BOUNDED_IMP_FINITE THEN
 423   EXISTS_TAC `&2` THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN CONJ_TAC THENL
 424    [REWRITE_TAC[IN_ELIM_THM; IN_DELETE; GSYM dist] THEN ASM_MESON_TAC[];
 425     MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC `ball(v:real^3,&4)` THEN
 426     REWRITE_TAC[BOUNDED_BALL] THEN SET_TAC[]]);;
 427
 428 let not_in_voronoi = prove
 429  (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
 430           ~(x IN voronoi_closed S v) <=>
 431           ?y. y IN S /\ ~ (y = v) /\ dist (x,y) < dist (x,v)`,
 432   REWRITE_TAC[VORONOI_CLOSED_ALT; IN_ELIM_THM] THEN MESON_TAC[REAL_NOT_LE]);;
 433
 434 let voronoi_in_ball = prove
 435  (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
 436         packing S /\ saturated S /\ (x IN voronoi_closed S v)
 437         ==> dist(x,v) < &2`,
 438   REPEAT STRIP_TAC THEN
 439   MP_TAC(ISPECL [`S:real^3->bool`; `v:real^3`] VORONOI_CLOSED_SUBSET_BALL) THEN
 440   ASM_SIMP_TAC[SUBSET; IN_BALL; REAL_LT_IMP_LE; DIST_SYM]);;
 441
 442 let DRUQUFE = prove
 443  (`!(v:real^3)(S:real^3 -> bool).
 444        packing S /\ saturated S
 445        ==> convex (voronoi_closed S v) /\
 446            bounded (voronoi_closed S v) /\
 447            closed (voronoi_closed S v) /\
 448            measurable ( voronoi_closed S v)`,
 449   SIMP_TAC[CONVEX_VORONOI_CLOSED; BOUNDED_VORONOI_CLOSED;
 450            CLOSED_VORONOI_CLOSED; MEASURABLE_VORONOI_CLOSED]);;
 451
 452 let measurable_voronoi = prove
 453  (`!(v:real^3)(S:real^3 -> bool).
 454       packing S /\ saturated S ==> measurable ( voronoi_closed S v)`,
 455   SIMP_TAC[MEASURABLE_VORONOI_CLOSED]);;
 456
 457 let fcc_compatible = prove
 458  (`fcc_compatible f S <=>
 459      (!v. v IN S ==> sqrt(&32) <= measure(voronoi_closed S v) + f v)`,
 460   REWRITE_TAC[Pack1.fcc_compatible; MEASURE_VORONOI_CLOSED_OPEN]);;
 461
 462 let voronoi_subset_ball = prove
 463  (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
 464       packing S /\ saturated S ==> (voronoi_closed S v) SUBSET ball(v, &2)`,
 465   SIMP_TAC[VORONOI_CLOSED_SUBSET_BALL]);;
 466
 467 let all_voronoi_subset_ball = prove
 468  (`!(v:real^3)(S:real^3 ->bool)(p:real^3)(r:real).
 469         packing S /\ saturated S /\ v IN ball(p, r + &1)
 470         ==> (voronoi_closed S v) SUBSET ball(p, r + &3)`,
 471   REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
 472    `voronoi_closed (S:real^3 -> bool) (v:real^3) SUBSET ball(v:real^3, &2) /\
 473     ball(v:real^3, &2 ) SUBSET ball(p:real^3, r+ &3)
 474     ==> voronoi_closed S v SUBSET ball (p,r + &3)`) THEN
 475   ASM_SIMP_TAC[voronoi_subset_ball] THEN
 476   UNDISCH_TAC `((v:real^3) IN ball (p:real^3,r + &1)):bool` THEN
 477   REWRITE_TAC[ball;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
 478   MP_TAC(ISPECL [`p:real^3`;`v:real^3`;`x:real^3`] DIST_TRIANGLE) THEN
 479   ASM_MESON_TAC[REAL_ARITH
 480    ` a< (r:real) + &1 /\ b< &2 /\ c <= a + b ==> c < r + &3`]);;
 481
 482 let unions_voronoi_subset_ball = prove
 483  (`!(S:real^3 ->bool)(p:real^3)(r:real).
 484       packing S /\ saturated S
 485       ==> UNIONS {voronoi_closed S v | v IN ball(p, r+ &1)}
 486           SUBSET ball(p, r+ &3)`,
 487   REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN
 488   SIMP_TAC[all_voronoi_subset_ball]);;
 489
 490 let unions_voronoi_center_in_ball_subset_ball = prove
 491  (`!(S:real^3 ->bool)(p:real^3)(r:real).
 492         packing S /\ saturated S
 493         ==> UNIONS {voronoi_closed w v | v IN (S INTER ball(p, r+ &1)) /\
 494                                          w = S} SUBSET ball(p, r+ &3)`,
 495   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN
 496   EXISTS_TAC `UNIONS {voronoi_closed S (v:real^3) | v IN ball(p, r+ &1)}` THEN
 497   ASM_SIMP_TAC[unions_voronoi_subset_ball] THEN
 498   MATCH_MP_TAC SUBSET_UNIONS THEN
 499   REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
 500   REWRITE_TAC[IN_ELIM_THM; IN_INTER] THEN MESON_TAC[]);;
 501
 502 let finite_set_voronoi_center_in_ball = prove
 503  (`!(S:real^3 ->bool) (p:real^3) (r:real).
 504         &0 <= r /\ packing S
 505         ==>  FINITE({voronoi_closed w v | v IN (S INTER ball (p,r+ &1)) /\
 506                                           w = S})`,
 507   REPEAT STRIP_TAC THEN
 508   REWRITE_TAC[SET_RULE `{f x y | y IN t /\ x = s} = IMAGE (f s) t`] THEN
 509   MATCH_MP_TAC FINITE_IMAGE THEN ASM_SIMP_TAC[KIUMVTC]);;
 510
 511 let measurable_unions_voronoi = prove
 512  (`!(S:real^3 ->bool) (p:real^3) (r:real).
 513         &0 <= r /\ packing S /\ saturated S
 514         ==> measurable(UNIONS {voronoi_closed w v |
 515                                v IN (S INTER ball (p,r+ &1)) /\ w = S})`,
 516   REPEAT STRIP_TAC THEN
 517   MATCH_MP_TAC MEASURABLE_UNIONS THEN
 518   ASM_SIMP_TAC[finite_set_voronoi_center_in_ball] THEN
 519   GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
 520   ASM_MESON_TAC[measurable_voronoi]);;
 521
 522 let negligible_voronoi = prove
 523  (`!(S:real^3 ->bool)(p:real^3)(r:real). (!s t.
 524        s IN {voronoi_closed w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
 525        t IN {voronoi_closed w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
 526        ~(s = t)
 527        ==> negligible (s INTER t))`,
 528   REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 529   MATCH_MP_TAC NEGLIGIBLE_INTER_VORONOI_CLOSED THEN ASM_MESON_TAC[IN_INTER]);;
 530
 531 let measure_unions_sum_voronoi = prove
 532  (`!(S:real^3 ->bool)(p:real^3)(r:real).
 533         &0 <= r /\ packing S /\ saturated S
 534         ==> measure(UNIONS {voronoi_closed w v |
 535                             v IN (S INTER ball(p, r + &1)) /\ w = S}) =
 536             sum (S INTER ball(p, r + &1)) (\v. measure (voronoi_closed S v))`,
 537   REPEAT STRIP_TAC THEN
 538   REWRITE_TAC[SET_RULE `{f x y | y IN t /\ x = s} = IMAGE (f s) t`] THEN
 539   MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE THEN
 540   ASM_SIMP_TAC[MEASURABLE_VORONOI_CLOSED; KIUMVTC; IN_INTER] THEN
 541   REPEAT STRIP_TAC THEN MATCH_MP_TAC NEGLIGIBLE_INTER_VORONOI_CLOSED THEN
 542   ASM_REWRITE_TAC[]);;
 543
 544 let sum_measure_voronoi_le_ball = prove
 545  (`!(S:real^3 ->bool)(p:real^3)(r:real).
 546         &0<= r /\ packing S /\ saturated S
 547         ==> sum (S INTER ball (p,r + &1)) (\v. measure (voronoi_closed S v))
 548             <= measure (ball(p,r+ &3))`,
 549   REWRITE_TAC[MEASURE_VORONOI_CLOSED_OPEN;
 550               Pack1.sum_measure_voronoi_le_ball]);;
 551
 552 let ineq_lm5_3_step3 = prove
 553  (`!(S:real^3 ->bool)(p:real^3)(r:real)(A:real^3 ->real).
 554         &0 <= r /\ packing S /\ saturated S /\ (fcc_compatible A S)
 555         ==> sqrt(&32) * &(CARD(S INTER ball(p,r + &1)))
 556             <= sum (S INTER ball (p,r + &1))
 557                    (\v. (A v + measure (voronoi_closed S v)))`,
 558   REWRITE_TAC[MEASURE_VORONOI_CLOSED_OPEN;
 559               Pack1.ineq_lm5_3_step3]);;
 560
 561 end;;