(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Author: John Harrison                                                      *)
(* Date: 2010-03-16                                                           *)
(*                                                                            *)
(* This proves theorems about closed Voronoi cells and transfers the main     *)
(* results proved in Pack1 by Nguyen Tat Thang from open to closed cells.     *)
(* ========================================================================== *)

module type Pack2_type = sig
end;;

flyspeck_needs "packing/pack1.hl";;

module Pack2  (* : Pack1_type *) = struct

(* ------------------------------------------------------------------------- *)
(* Slight variants of definitions, mainly to use IN.                         *)
(* ------------------------------------------------------------------------- *)


let PACKING = 
prove
 (`!s. packing s <=> !u v. u IN s /\ v IN s /\ dist(u,v) < &2 ==> u = v`,

  REWRITE_TAC[IN; GSYM REAL_NOT_LE] THEN MESON_TAC[Pack1.packing]);;


let VORONOI_OPEN = 
prove
 (`!s v. voronoi_open s v =
          {x | !w. w IN s /\ ~(w = v) ==> dist(x,v) < dist(x,w)}`,

  REWRITE_TAC[Sphere.voronoi_open; IN]);;


let VORONOI_CLOSED = 
prove
 (`!s v. voronoi_closed s v = {x | !w. w IN s ==> dist(x,v) <= dist(x,w)}`,

  REWRITE_TAC[Sphere.voronoi_closed; IN]);;

(* ------------------------------------------------------------------------- *)
(* Minor variant of KIUMVTC without 0 <= r condition.                        *)
(* ------------------------------------------------------------------------- *)


let KIUMVTC = 
prove
 (`!p r S. packing S ==> FINITE(S INTER ball(p,r))`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `&0 <= r` THENL
   [ASM_SIMP_TAC[Pack1.KIUMVTC];
    FIRST_ASSUM(MP_TAC o MATCH_MP (REAL_ARITH `~(&0 <= v) ==> v <= &0`)) THEN
    SIMP_TAC[INTER_EMPTY; BALL_EMPTY; FINITE_EMPTY]]);;

(* ------------------------------------------------------------------------- *)
(* The basic lemmas about closed Voronoi cells.                              *)
(* ------------------------------------------------------------------------- *)


let BIS_LE = 
prove
 (`!u v. bis_le u v =
           {x | (&2 % (v - u)) dot x <= norm(v) pow 2 - norm(u) pow 2}`,

  REPEAT GEN_TAC THEN REWRITE_TAC[Sphere.bis_le; dist; NORM_LE] THEN
  REWRITE_TAC[EXTENSION; IN_ELIM_THM; DOT_LMUL; DOT_LSUB; DOT_RSUB] THEN
  REWRITE_TAC[NORM_POW_2; DOT_SYM] THEN REAL_ARITH_TAC);;


let BIS_LT = 
prove
 (`!u v. bis_lt u v =
           {x | (&2 % (v - u)) dot x < norm(v) pow 2 - norm(u) pow 2}`,

  REPEAT GEN_TAC THEN REWRITE_TAC[Sphere.bis_lt; dist; NORM_LT] THEN
  REWRITE_TAC[EXTENSION; IN_ELIM_THM; DOT_LMUL; DOT_LSUB; DOT_RSUB] THEN
  REWRITE_TAC[NORM_POW_2; DOT_SYM] THEN REAL_ARITH_TAC);;


let VORONOI_CLOSED_ALT = 
prove
 (`!s v. voronoi_closed s v =
             {x | !w. w IN s /\ ~(w = v) ==> dist(x,v) <= dist(x,w)}`,

  REWRITE_TAC[VORONOI_CLOSED; EXTENSION; IN_ELIM_THM] THEN
  MESON_TAC[REAL_LE_REFL]);;


let VORONOI_CLOSED_AS_INTERSECTION = 
prove
 (`!s v. voronoi_closed s v = INTERS (IMAGE (bis_le v) (s DELETE v))`,

  REWRITE_TAC[Sphere.bis_le; VORONOI_CLOSED_ALT; INTERS_IMAGE] THEN
  REWRITE_TAC[IN_DELETE; IN_ELIM_THM]);;


let VORONOI_OPEN_AS_INTERSECTION = 
prove
 (`!s v. voronoi_open s v = INTERS (IMAGE (bis_lt v) (s DELETE v))`,

  REWRITE_TAC[Sphere.bis_lt; VORONOI_OPEN; INTERS_IMAGE] THEN
  REWRITE_TAC[IN_DELETE; IN_ELIM_THM]);;


let CLOSED_VORONOI_CLOSED = 
prove
 (`!s v. closed(voronoi_closed s v)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN
  MATCH_MP_TAC CLOSED_INTERS THEN
  REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CLOSED_HALFSPACE_LE]);;


let VORONOI_CLOSED_SUBSET_BALL = 
prove
 (`!s v:real^N. saturated s ==> voronoi_closed s v SUBSET ball(v,&2)`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[VORONOI_CLOSED; SUBSET] THEN
  REWRITE_TAC[IN_ELIM_THM; IN_BALL] THEN
  X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N` o GEN_REWRITE_RULE I
   [Pack1.saturated]) THEN
  DISCH_THEN(X_CHOOSE_THEN `y:real^N` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN
  ASM_REWRITE_TAC[] THEN NORM_ARITH_TAC);;


let BOUNDED_VORONOI_CLOSED = 
prove
 (`!s v. saturated s ==> bounded(voronoi_closed s v)`,


let COMPACT_VORONOI_CLOSED = 
prove
 (`!s v. saturated s ==> compact(voronoi_closed s v)`,


let CONVEX_VORONOI_CLOSED = 
prove
 (`!s v. convex(voronoi_closed s v)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN
  MATCH_MP_TAC CONVEX_INTERS THEN
  REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CONVEX_HALFSPACE_LE]);;


let BASE_IN_VORONOI_CLOSED = 
prove
 (`!s v. v IN voronoi_closed s v`,

  REWRITE_TAC[Sphere.voronoi_closed; DIST_REFL; DIST_POS_LE; IN_ELIM_THM]);;


let CBALL_SUBSET_VORONOI_CLOSED = 
prove
 (`!s v:real^3. packing s /\ v IN s ==> cball(v,&1) SUBSET voronoi_closed s v`,

  REWRITE_TAC[PACKING; SUBSET; VORONOI_CLOSED_ALT; IN_CBALL; IN_ELIM_THM] THEN
  REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `x:real^3` THEN
  DISCH_TAC THEN X_GEN_TAC `w:real^3` THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`v:real^3`; `w:real^3`]) THEN
  ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN NORM_ARITH_TAC);;


let VORONOI_CLOSED_PARTITION_STRONG = 
prove
 (`!s. closed s /\ ~(s = {})
       ==> UNIONS { voronoi_closed s v |v| v IN s} = (:real^3)`,

  GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
  REWRITE_TAC[UNIONS_IMAGE; EXTENSION; IN_UNIV; IN_ELIM_THM] THEN
  REWRITE_TAC[VORONOI_CLOSED; IN_ELIM_THM] THEN
  X_GEN_TAC `x:real^3` THEN EXISTS_TAC `closest_point s (x:real^3)` THEN
  MATCH_MP_TAC CLOSEST_POINT_EXISTS THEN ASM_REWRITE_TAC[]);;


let PACKING_IMP_CLOSED = 
prove
 (`!s. packing s ==> closed s`,

  REWRITE_TAC[PACKING; dist] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN EXISTS_TAC `&2` THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_MESON_TAC[NORM_SUB]);;


let SATURATED_IMP_NONEMPTY = 
prove
 (`!s. saturated s ==> ~(s = {})`,

  REWRITE_TAC[Pack1.saturated] THEN SET_TAC[]);;


let VORONOI_CLOSED_PARTITION = 
prove
 (`!s. packing s /\ saturated s
       ==> UNIONS { voronoi_closed s v |v| v IN s} = (:real^3)`,


let VORONOI_CLOSED_AS_FINITE_INTERSECTION = 
prove
 (`!s v. packing s /\ saturated s /\ v IN s
         ==> voronoi_closed s v =
                INTERS (IMAGE (bis_le v) ((s INTER ball(v,&4)) DELETE v))`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
   [REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN SET_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[SUBSET] THEN X_GEN_TAC `p:real^3` THEN
  DISCH_TAC THEN
  SUBGOAL_THEN
   `?p':real^3. aff_ge {v} {p} INTER voronoi_closed s v = segment[v,p']`
  STRIP_ASSUME_TAC THENL
   [MATCH_MP_TAC HALFLINE_INTER_COMPACT_SEGMENT THEN
    ASM_SIMP_TAC[COMPACT_VORONOI_CLOSED; CONVEX_VORONOI_CLOSED;
                 BASE_IN_VORONOI_CLOSED];
    ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
  SUBGOAL_THEN
   `(v:real^3) IN voronoi_closed s v /\ p' IN voronoi_closed s v /\
    p' IN aff_ge {v} {p}`
  STRIP_ASSUME_TAC THENL
   [ASM_MESON_TAC[ENDS_IN_SEGMENT; IN_INTER]; ALL_TAC] THEN
  SUBGOAL_THEN `p' IN ball(v:real^3,&2)` ASSUME_TAC THENL
   [ASM_MESON_TAC[VORONOI_CLOSED_SUBSET_BALL; SUBSET]; ALL_TAC] THEN
  SUBGOAL_THEN
   `?q:real^3.
       q IN ball(v,&2) /\
       q IN INTERS(IMAGE (bis_le v) ((s INTER ball (v,&4)) DELETE v)) /\
       ~(q IN voronoi_closed s v)`
  STRIP_ASSUME_TAC THENL
   [ASM_CASES_TAC `p IN ball(v:real^3,&2)` THENL
     [ASM_MESON_TAC[]; ALL_TAC] THEN
    ASM_CASES_TAC `p:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    SUBGOAL_THEN
     `?t. &0 <= t /\ t < &1 /\ p':real^3 = (&1 - t) % v + t % p`
    STRIP_ASSUME_TAC THENL
     [UNDISCH_TAC `(p':real^3) IN aff_ge {v} {p}` THEN
      ASM_REWRITE_TAC[HALFLINE; IN_SEGMENT; IN_ELIM_THM] THEN
      MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:real` THEN STRIP_TAC THEN
      SUBGOAL_THEN `dist(v:real^3,p') < dist(v,p)` MP_TAC THENL
       [ASM_MESON_TAC[IN_BALL; REAL_ARITH `x < &2 /\ ~(y < &2) ==> x < y`];
        ASM_REWRITE_TAC[]] THEN
      REWRITE_TAC[VECTOR_ARITH
       `(&1 - t) % x + t % y:real^N = x + t % (y - x)`] THEN
      REWRITE_TAC[NORM_ARITH `dist(v:real^N,v + x) = norm x`; NORM_MUL] THEN
      REWRITE_TAC[dist; NORM_SUB] THEN
      ONCE_REWRITE_TAC[REAL_ARITH `x * y < y <=> x * y < &1 * y`] THEN
      ASM_SIMP_TAC[REAL_LT_RMUL_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
      ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    MP_TAC(ISPECL [`v:real^3`; `&2`] OPEN_BALL) THEN
    REWRITE_TAC[open_def] THEN DISCH_THEN(MP_TAC o SPEC `p':real^3`) THEN
    ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; dist] THEN
    X_GEN_TAC `e:real` THEN STRIP_TAC THEN
    ABBREV_TAC `u = t + min (e / &2 / norm(p - v:real^3)) ((&1 - t) / &2)` THEN
    SUBGOAL_THEN `&0 < u /\ t < u /\ u < &1` STRIP_ASSUME_TAC THENL
     [EXPAND_TAC "u" THEN MATCH_MP_TAC(REAL_ARITH
       `&0 < x /\ &0 <= t /\ t < &1
        ==> &0 < t + min x ((&1 - t) / &2) /\ t < t + min x ((&1 - t) / &2) /\
            t + min x ((&1 - t) / &2) < &1`) THEN
      ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
      ALL_TAC] THEN
    EXISTS_TAC `(&1 - u) % v + u % p:real^3` THEN REPEAT CONJ_TAC THENL
     [FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT; VECTOR_SUB_EQ;
        VECTOR_ARITH
       `((&1 - u) % v + u % p) - ((&1 - t) % v + t % p):real^N =
        (u - t) % (p - v)`] THEN
      EXPAND_TAC "u" THEN REWRITE_TAC[REAL_ADD_SUB] THEN
      MATCH_MP_TAC(REAL_ARITH
       `&0 < z /\ &0 < y /\ x = z / &2 ==> abs(min x y) < z`) THEN
      ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ] THEN
      REWRITE_TAC[real_div; REAL_MUL_AC] THEN ASM_REAL_ARITH_TAC;
      MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC CONVEX_INTERS THEN
        REWRITE_TAC[FORALL_IN_IMAGE; BIS_LE; CONVEX_HALFSPACE_LE];
        UNDISCH_TAC `(v:real^3) IN voronoi_closed s v` THEN
        REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION] THEN SET_TAC[]];
      DISCH_TAC THEN
      SUBGOAL_THEN `((&1 - u) % v + u % p:real^3) IN
                    (aff_ge {v} {p} INTER voronoi_closed s v)`
      MP_TAC THENL
       [ASM_REWRITE_TAC[IN_INTER; HALFLINE; IN_ELIM_THM] THEN
        ASM_MESON_TAC[REAL_LT_IMP_LE];
        ASM_REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT] THEN
        REWRITE_TAC[between; VECTOR_ARITH
         `(&1 - u) % x + u % y:real^N = x + u % (y - x)`] THEN
        REWRITE_TAC[NORM_ARITH `dist(v:real^N,v + x) = norm x`;
                    NORM_ARITH `dist(v + x:real^N,v + y) = norm(x - y)`] THEN
        REWRITE_TAC[GSYM VECTOR_SUB_RDISTRIB; NORM_MUL] THEN
        ASM_REWRITE_TAC[REAL_ENTIRE; NORM_EQ_0; VECTOR_SUB_EQ; REAL_ARITH
         `x * a:real = y * a + z * a <=> a * (x - y - z) = &0`] THEN
        ASM_REAL_ARITH_TAC]];
    MP_TAC(ISPEC `s:real^3->bool` VORONOI_CLOSED_PARTITION) THEN
    ASM_REWRITE_TAC[EXTENSION; IN_UNIV] THEN
    DISCH_THEN(MP_TAC o SPEC `q:real^3`) THEN REWRITE_TAC[] THEN
    ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
    REWRITE_TAC[UNIONS_IMAGE; IN_ELIM_THM] THEN
    DISCH_THEN(X_CHOOSE_THEN `w:real^3` STRIP_ASSUME_TAC) THEN
    UNDISCH_TAC
     `(q:real^3) IN INTERS(IMAGE (bis_le v)
                                 ((s INTER ball(v,&4)) DELETE v))` THEN
    REWRITE_TAC[IN_INTERS; FORALL_IN_IMAGE] THEN
    DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN
    ASM_REWRITE_TAC[NOT_IMP; IN_DELETE; IN_INTER; IN_BALL] THEN
    ASM_CASES_TAC `w:real^3 = v` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
     [MATCH_MP_TAC(NORM_ARITH
       `!q. dist(q,w) <= dist(q,v) /\ dist(v,q) < &2 ==> dist(v,w) < &4`) THEN
      EXISTS_TAC `q:real^3` THEN
      RULE_ASSUM_TAC(REWRITE_RULE[VORONOI_CLOSED; IN_ELIM_THM; IN_BALL]) THEN
      ASM_SIMP_TAC[];
      REWRITE_TAC[Sphere.bis_le; IN_ELIM_THM] THEN
      RULE_ASSUM_TAC(REWRITE_RULE[VORONOI_CLOSED; IN_ELIM_THM]) THEN
      ASM_MESON_TAC[REAL_LE_TRANS]]]);;


let POLYHEDRON_VORONOI_CLOSED = 
prove
 (`!s v. packing s /\ saturated s /\ v IN s
         ==> polyhedron(voronoi_closed s v)`,

  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[VORONOI_CLOSED_AS_FINITE_INTERSECTION] THEN
  MATCH_MP_TAC POLYHEDRON_INTERS THEN
  ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE; FINITE_INTER;
               KIUMVTC; FORALL_IN_IMAGE] THEN
  REWRITE_TAC[BIS_LE; POLYHEDRON_HALFSPACE_LE]);;


let POLYTOPE_VORONOI_CLOSED = 
prove
 (`!s v. packing s /\ saturated s /\ v IN s
         ==> polytope(voronoi_closed s v)`,


let MEASURABLE_VORONOI_CLOSED = 
prove
 (`!s v. saturated s ==> measurable(voronoi_closed s v)`,

(* ------------------------------------------------------------------------- *)
(* Relate closed and open Voronoi cells.                                     *)
(* ------------------------------------------------------------------------- *)


let CLOSED_BIS_LE = 
prove
 (`!u v. closed(bis_le u v)`,

  REWRITE_TAC[BIS_LE; CLOSED_HALFSPACE_LE]);;


let OPEN_BIS_LT = 
prove
 (`!u v. open(bis_lt u v)`,

  REWRITE_TAC[BIS_LT; OPEN_HALFSPACE_LT]);;


let INTERIOR_BIS_LE = 
prove
 (`!u v. ~(v = u) ==> interior(bis_le u v) = bis_lt u v`,

  SIMP_TAC[BIS_LE; BIS_LT; INTERIOR_HALFSPACE_LE;
           VECTOR_ARITH `&2 % (v - w):real^N = vec 0 <=> v = w`]);;


let CLOSURE_BIS_LT = 
prove
 (`!u v. ~(v = u) ==> closure(bis_lt u v) = bis_le u v`,

  SIMP_TAC[BIS_LE; BIS_LT; CLOSURE_HALFSPACE_LT;
           VECTOR_ARITH `&2 % (v - w):real^N = vec 0 <=> v = w`]);;


let CLOSURE_VORONOI_OPEN = 
prove
 (`!S v:real^N. closure(voronoi_open S v) = voronoi_closed S v`,

  SIMP_TAC[VORONOI_CLOSED_AS_INTERSECTION; VORONOI_OPEN_AS_INTERSECTION] THEN
  SIMP_TAC[CLOSURE_INTERS_CONVEX_OPEN; FORALL_IN_IMAGE; BIS_LT;
           OPEN_HALFSPACE_LT; CONVEX_HALFSPACE_LT] THEN
  REPEAT GEN_TAC THEN COND_CASES_TAC THENL
   [POP_ASSUM MP_TAC THEN MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
    EXISTS_TAC `v:real^N` THEN REWRITE_TAC[INTERS_IMAGE; IN_ELIM_THM] THEN
    SIMP_TAC[Sphere.bis_lt; IN_DELETE; IN_ELIM_THM; DIST_REFL; DIST_POS_LT];
    AP_TERM_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN MATCH_MP_TAC(SET_RULE
     `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN
    SIMP_TAC[IN_DELETE; o_THM; CLOSURE_BIS_LT]]);;


let INTERIOR_VORONOI_CLOSED_INTERIOR = 
prove
 (`!S v. interior(voronoi_closed S v) = interior(voronoi_open S v)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN] THEN
  MATCH_MP_TAC CONVEX_INTERIOR_CLOSURE THEN
  REWRITE_TAC[VORONOI_OPEN_AS_INTERSECTION] THEN
  MATCH_MP_TAC CONVEX_INTERS THEN
  REWRITE_TAC[FORALL_IN_IMAGE; BIS_LT; CONVEX_HALFSPACE_LT]);;


let INTERIOR_VORONOI_CLOSED = 
prove
 (`!S v. packing S /\ saturated S
         ==> interior(voronoi_closed S v) = voronoi_open S v`,

  SIMP_TAC[INTERIOR_VORONOI_CLOSED_INTERIOR; Pack1.open_voronoi;
           INTERIOR_OPEN]);;


let VORONOI_OPEN_AS_FINITE_INTERSECTION = 
prove
 (`!s v. packing s /\ saturated s /\ v IN s
         ==> voronoi_open s v =
                INTERS(IMAGE (bis_lt v) ((s INTER ball(v,&4)) DELETE v))`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM INTERIOR_VORONOI_CLOSED] THEN
  ASM_SIMP_TAC[VORONOI_CLOSED_AS_FINITE_INTERSECTION] THEN
  ASM_SIMP_TAC[INTERIOR_FINITE_INTERS; FINITE_IMAGE; KIUMVTC;
               FORALL_IN_IMAGE; FINITE_DELETE] THEN
  AP_TERM_TAC THEN REWRITE_TAC[GSYM IMAGE_o] THEN MATCH_MP_TAC(SET_RULE
   `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN
  SIMP_TAC[IN_DELETE; o_THM; INTERIOR_BIS_LE]);;


let VORONOI_OPEN_SUBSET_CLOSED = 
prove
 (`!S v:real^N. (voronoi_open S v) SUBSET (voronoi_closed S v)`,

  REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN; CLOSURE_SUBSET]);;

(* ------------------------------------------------------------------------- *)
(* And so.                                                                   *)
(* ------------------------------------------------------------------------- *)


let MEASURE_VORONOI_CLOSED_OPEN = 
prove
 (`!s v:real^N. measure(voronoi_closed s v) = measure(voronoi_open s v)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CLOSURE_VORONOI_OPEN] THEN
  MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
  MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
  EXISTS_TAC `frontier(voronoi_open s (v:real^N))` THEN
  SIMP_TAC[NEGLIGIBLE_CONVEX_FRONTIER; Geomdetail.VORONOI_CONV] THEN
  REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
   `i SUBSET s /\ s SUBSET c
    ==> (c DIFF s UNION s DIFF c) SUBSET (c DIFF i)`) THEN
  REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET]);;


let INTER_VORONOI_SUBSET_BISECTOR = 
prove
 (`!s u v:real^N.
        u IN s /\ v IN s
        ==> (voronoi_closed s u) INTER (voronoi_closed s v)
            SUBSET {x | (&2 % (u - v)) dot x = norm(u) pow 2 - norm(v) pow 2}`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `u:real^N = v` THENL
   [ASM_REWRITE_TAC[VECTOR_SUB_REFL; REAL_SUB_REFL; DOT_LZERO; DOT_LMUL;
                    REAL_MUL_RZERO] THEN
    SET_TAC[];
    REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION; INTERS_IMAGE] THEN
    REWRITE_TAC[IN_INTER; SUBSET; BIS_LE; IN_ELIM_THM] THEN
    X_GEN_TAC `w:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2
     (MP_TAC o SPEC `v:real^N`) (MP_TAC o SPEC `u:real^N`)) THEN
    ASM_REWRITE_TAC[IN_DELETE] THEN
    REWRITE_TAC[DOT_LMUL; DOT_LSUB] THEN REWRITE_TAC[DOT_SYM] THEN
    REAL_ARITH_TAC]);;


let NEGLIGIBLE_INTER_VORONOI_CLOSED = 
prove
 (`!s u v:real^N.
        u IN s /\ v IN s /\ ~(u = v)
        ==> negligible((voronoi_closed s u) INTER (voronoi_closed s v))`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN EXISTS_TAC
   `{x:real^N | (&2 % (u - v)) dot x = norm(u) pow 2 - norm(v) pow 2}` THEN
  ASM_SIMP_TAC[INTER_VORONOI_SUBSET_BISECTOR] THEN
  MATCH_MP_TAC NEGLIGIBLE_HYPERPLANE THEN
  ASM_SIMP_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ] THEN REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Transfer theorems from Pack1 to closed cells where applicable.            *)
(* ------------------------------------------------------------------------- *)


let voronoi_version2 = 
prove
 (`!(v:real^3) (S:real^3-> bool).
      voronoi_closed S v = INTERS {bis_le x y | y IN (S DELETE v) /\ x = v}`,

  REWRITE_TAC[VORONOI_CLOSED_AS_INTERSECTION; GSYM SIMPLE_IMAGE] THEN
  REPEAT GEN_TAC THEN AP_TERM_TAC THEN SET_TAC[]);;


let convex_voronoi = 
prove
 (`!(v:real^3) (S:real^3-> bool). convex(voronoi_closed S v)`,

  REWRITE_TAC[CONVEX_VORONOI_CLOSED]);;


let bound_voronoi = 
prove
 (`!(v:real^3) (S:real^3-> bool).
      saturated S ==>  bounded(voronoi_closed S v)`,


let finite_voronoi2 = 
prove
 (`!(v:real^3)(S:real^3 ->bool).
      packing S
      ==> FINITE {bis_le (x:real^3) (y:real^3) |
                  y IN (S DELETE v) /\ x = v /\ y IN ball(v, &4)}`,

  REWRITE_TAC[PACKING] THEN REPEAT STRIP_TAC THEN
  REWRITE_TAC[SET_RULE `{f x y | P y /\ x = v /\ Q y} =
                        IMAGE (f v) {y | P y /\ Q y}`] THEN
  MATCH_MP_TAC FINITE_IMAGE THEN MATCH_MP_TAC DISCRETE_BOUNDED_IMP_FINITE THEN
  EXISTS_TAC `&2` THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN CONJ_TAC THENL
   [REWRITE_TAC[IN_ELIM_THM; IN_DELETE; GSYM dist] THEN ASM_MESON_TAC[];
    MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC `ball(v:real^3,&4)` THEN
    REWRITE_TAC[BOUNDED_BALL] THEN SET_TAC[]]);;


let not_in_voronoi = 
prove
 (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
          ~(x IN voronoi_closed S v) <=>
          ?y. y IN S /\ ~ (y = v) /\ dist (x,y) < dist (x,v)`,

  REWRITE_TAC[VORONOI_CLOSED_ALT; IN_ELIM_THM] THEN MESON_TAC[REAL_NOT_LE]);;


let voronoi_in_ball = 
prove
 (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
        packing S /\ saturated S /\ (x IN voronoi_closed S v)
        ==> dist(x,v) < &2`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`S:real^3->bool`; `v:real^3`] VORONOI_CLOSED_SUBSET_BALL) THEN
  ASM_SIMP_TAC[SUBSET; IN_BALL; REAL_LT_IMP_LE; DIST_SYM]);;


let DRUQUFE = 
prove
 (`!(v:real^3)(S:real^3 -> bool).
       packing S /\ saturated S
       ==> convex (voronoi_closed S v) /\
           bounded (voronoi_closed S v) /\
           closed (voronoi_closed S v) /\
           measurable ( voronoi_closed S v)`,


let measurable_voronoi = 
prove
 (`!(v:real^3)(S:real^3 -> bool).
      packing S /\ saturated S ==> measurable ( voronoi_closed S v)`,


let fcc_compatible = 
prove
 (`fcc_compatible f S <=>
     (!v. v IN S ==> sqrt(&32) <= measure(voronoi_closed S v) + f v)`,

  REWRITE_TAC[Pack1.fcc_compatible; MEASURE_VORONOI_CLOSED_OPEN]);;


let voronoi_subset_ball = 
prove
 (`!(x:real^3)(v:real^3)(S:real^3 -> bool).
      packing S /\ saturated S ==> (voronoi_closed S v) SUBSET ball(v, &2)`,


let all_voronoi_subset_ball = 
prove
 (`!(v:real^3)(S:real^3 ->bool)(p:real^3)(r:real).
        packing S /\ saturated S /\ v IN ball(p, r + &1)
        ==> (voronoi_closed S v) SUBSET ball(p, r + &3)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
   `voronoi_closed (S:real^3 -> bool) (v:real^3) SUBSET ball(v:real^3, &2) /\
    ball(v:real^3, &2 ) SUBSET ball(p:real^3, r+ &3)
    ==> voronoi_closed S v SUBSET ball (p,r + &3)`) THEN
  ASM_SIMP_TAC[voronoi_subset_ball] THEN
  UNDISCH_TAC `((v:real^3) IN ball (p:real^3,r + &1)):bool` THEN
  REWRITE_TAC[ball;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`p:real^3`;`v:real^3`;`x:real^3`] DIST_TRIANGLE) THEN
  ASM_MESON_TAC[REAL_ARITH
   ` a< (r:real) + &1 /\ b< &2 /\ c <= a + b ==> c < r + &3`]);;


let unions_voronoi_subset_ball = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real).
      packing S /\ saturated S
      ==> UNIONS {voronoi_closed S v | v IN ball(p, r+ &1)}
          SUBSET ball(p, r+ &3)`,

  REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN
  SIMP_TAC[all_voronoi_subset_ball]);;


let unions_voronoi_center_in_ball_subset_ball = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real).
        packing S /\ saturated S
        ==> UNIONS {voronoi_closed w v | v IN (S INTER ball(p, r+ &1)) /\
                                         w = S} SUBSET ball(p, r+ &3)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN
  EXISTS_TAC `UNIONS {voronoi_closed S (v:real^3) | v IN ball(p, r+ &1)}` THEN
  ASM_SIMP_TAC[unions_voronoi_subset_ball] THEN
  MATCH_MP_TAC SUBSET_UNIONS THEN
  REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
  REWRITE_TAC[IN_ELIM_THM; IN_INTER] THEN MESON_TAC[]);;


let finite_set_voronoi_center_in_ball = 
prove
 (`!(S:real^3 ->bool) (p:real^3) (r:real).
        &0 <= r /\ packing S
        ==>  FINITE({voronoi_closed w v | v IN (S INTER ball (p,r+ &1)) /\
                                          w = S})`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[SET_RULE `{f x y | y IN t /\ x = s} = IMAGE (f s) t`] THEN
  MATCH_MP_TAC FINITE_IMAGE THEN ASM_SIMP_TAC[KIUMVTC]);;


let measurable_unions_voronoi = 
prove
 (`!(S:real^3 ->bool) (p:real^3) (r:real).
        &0 <= r /\ packing S /\ saturated S
        ==> measurable(UNIONS {voronoi_closed w v |
                               v IN (S INTER ball (p,r+ &1)) /\ w = S})`,

  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC MEASURABLE_UNIONS THEN
  ASM_SIMP_TAC[finite_set_voronoi_center_in_ball] THEN
  GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
  ASM_MESON_TAC[measurable_voronoi]);;


let negligible_voronoi = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real). (!s t.
       s IN {voronoi_closed w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
       t IN {voronoi_closed w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
       ~(s = t)
       ==> negligible (s INTER t))`,

  REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC NEGLIGIBLE_INTER_VORONOI_CLOSED THEN ASM_MESON_TAC[IN_INTER]);;


let measure_unions_sum_voronoi = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real).
        &0 <= r /\ packing S /\ saturated S
        ==> measure(UNIONS {voronoi_closed w v |
                            v IN (S INTER ball(p, r + &1)) /\ w = S}) =
            sum (S INTER ball(p, r + &1)) (\v. measure (voronoi_closed S v))`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[SET_RULE `{f x y | y IN t /\ x = s} = IMAGE (f s) t`] THEN
  MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE THEN
  ASM_SIMP_TAC[MEASURABLE_VORONOI_CLOSED; KIUMVTC; IN_INTER] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC NEGLIGIBLE_INTER_VORONOI_CLOSED THEN
  ASM_REWRITE_TAC[]);;


let sum_measure_voronoi_le_ball = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real).
        &0<= r /\ packing S /\ saturated S
        ==> sum (S INTER ball (p,r + &1)) (\v. measure (voronoi_closed S v))
            <= measure (ball(p,r+ &3))`,

  REWRITE_TAC[MEASURE_VORONOI_CLOSED_OPEN;
              Pack1.sum_measure_voronoi_le_ball]);;


let ineq_lm5_3_step3 = 
prove
 (`!(S:real^3 ->bool)(p:real^3)(r:real)(A:real^3 ->real).
        &0 <= r /\ packing S /\ saturated S /\ (fcc_compatible A S)
        ==> sqrt(&32) * &(CARD(S INTER ball(p,r + &1)))
            <= sum (S INTER ball (p,r + &1))
                   (\v. (A v + measure (voronoi_closed S v)))`,

  REWRITE_TAC[MEASURE_VORONOI_CLOSED_OPEN;
              Pack1.ineq_lm5_3_step3]);;

end;;