(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: NJIUTIU                                                  *)
(*      Chaper    : Packing (Marchal cells)                                  *)
(*                                                                           *)
(* ========================================================================= *)


(* ========================================================================= *)

module Njiutiu = struct

open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;


let NJIUTIU_concl = 
 `!V ul vl.
         saturated V /\ packing V /\
         barV V 3 ul /\ barV V 3 vl /\
         rogers V ul = rogers V vl /\ aff_dim (rogers V ul) = &3 
        ==> (!i. 0 <= i /\ i <= 3 
                 ==> omega_list_n V ul i = omega_list_n V vl i)`;;

(* ========================================================================= *)
(* supporting lemmas *)

let CLOSEST_POINT_SUBSET_lemma = 
prove_by_refinement (
 `!(a:real^3) x S P. 
      (a = closest_point S x /\ a IN P /\ P SUBSET S /\ 
       convex P /\ closed P /\ closed S /\ ~(P = {})) 
     ==> (a = closest_point P x)`,

[(REPEAT STRIP_TAC);
 (ABBREV_TAC `s = closest_point P (x:real^3)`);
 (ASM_CASES_TAC `~(a:real^3 = s)`);
 (NEW_GOAL `dist (x:real^3, s) < dist (x, a)`);
 (EXPAND_TAC "s");
 (MATCH_MP_TAC CLOSEST_POINT_LT);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `s:real^3 IN P`);
 (EXPAND_TAC "s");
 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `dist (x, a) <= dist (x, s:real^3)`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC CLOSEST_POINT_LE);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[])]);;

(* ---------------------------------------------------------------------------*)
let AFF_DEPENDENT_AFF_DIM_4 = 
prove_by_refinement (
 `!a b c d:real^3. 
   affine_dependent {a,b,c,d} ==> aff_dim {a,b,c,d} <= &2`,

[(REWRITE_TAC[affine_dependent]);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `x = a:real^3`);
 (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `aff_dim {b,c,d:real^3} <= &(CARD {b,c,d}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (NEW_GOAL `&(CARD {b, c, d:real^3}) <= &3:int`);
 (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) 
             SUBSET affine hull {b, c, d}`);
 (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
 (ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `x = b:real^3`);
 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,a,c,d}`]);
 (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `aff_dim {a,c,d:real^3} <= &(CARD {a,c,d}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (NEW_GOAL `&(CARD {a, c, d:real^3}) <= &3:int`);
 (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) 
             SUBSET affine hull {a, c, d}`);
 (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
 (ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `x = c:real^3`);
 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {c,a,b,d}`]);
 (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `aff_dim {a,b,d:real^3} <= &(CARD {a,b,d}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (NEW_GOAL `&(CARD {a, b, d:real^3}) <= &3:int`);
 (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) 
             SUBSET affine hull {a, b, d}`);
 (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
 (ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `x = d:real^3`);
 (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]);
 (ONCE_REWRITE_TAC [AFF_DIM_INSERT]);
 (COND_CASES_TAC);
 (NEW_GOAL `aff_dim {a,b,c:real^3} <= &(CARD {a,b,c}) - &1`);
 (MATCH_MP_TAC AFF_DIM_LE_CARD);
 (REWRITE_TAC[Geomdetail.FINITE6]);
 (NEW_GOAL `&(CARD {a, b,c:real^3}) <= &3:int`);
 (REWRITE_TAC[INT_OF_NUM_LE; Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `F`);
 (NEW_GOAL `affine hull({a, b, c, d:real^3} DELETE x) 
             SUBSET affine hull {a, b, c}`);
 (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA);
 (ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[])]);;

(* ========================================================================== *)
(*        Main theorem                                                        *)
(* ========================================================================== *)

let NJIUTIU = prove_by_refinement (NJIUTIU_concl,

[(REPEAT GEN_TAC THEN STRIP_TAC);
 (NEW_GOAL 
 `rogers V ul =
  convex hull
    {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
 (ASM_MESON_TAC[ROGERS_EXPLICIT]);
 (NEW_GOAL 
 `rogers V vl =
  convex hull
    {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 (ASM_MESON_TAC[ROGERS_EXPLICIT]);
 (NEW_GOAL 
  `{HD (ul:(real^3)list), omega_list_n V ul 1, omega_list_n V ul 2, 
    omega_list_n V ul 3}
 = {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 (REWRITE_WITH 
 `{HD (ul:(real^3)list), omega_list_n V ul 1, omega_list_n V ul 2,
   omega_list_n V ul 3}
 = {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3} <=>
   convex hull 
   {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}
 = convex hull 
   {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.CONVEX_HULL_EQ_EQ_SET_EQ);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `aff_dim {HD (ul:(real^3)list), omega_list_n V ul 1, 
                      omega_list_n V ul 2, omega_list_n V ul 3} <= &2`);
 (MATCH_MP_TAC AFF_DEPENDENT_AFF_DIM_4);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[GSYM AFF_DIM_CONVEX_HULL]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul =
  convex hull
  {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`)]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `aff_dim {HD (vl:(real^3)list), omega_list_n V vl 1, 
                      omega_list_n V vl 2, omega_list_n V vl 3} <= &2`);
 (MATCH_MP_TAC AFF_DEPENDENT_AFF_DIM_4);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[GSYM AFF_DIM_CONVEX_HULL]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V vl =
  convex hull
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`)]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ABBREV_TAC `W = {HD (ul:(real^3)list), omega_list_n V ul 1, 
                    omega_list_n V ul 2, omega_list_n V ul 3}`);

 (NEW_GOAL `!i j.
                  i < 4 /\ j < 4 /\ ~(i = j)
                  ==> ~(omega_list_n V ul i = omega_list_n V ul j)`);
 (MATCH_MP_TAC Rogers.ROGERS_AFF_DIM_FULL);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL 
  `~(omega_list_n V ul 0 = omega_list_n V ul 1) /\
   ~(omega_list_n V ul 0 = omega_list_n V ul 2) /\
   ~(omega_list_n V ul 0 = omega_list_n V ul 3) /\
   ~(omega_list_n V ul 1 = omega_list_n V ul 2) /\
   ~(omega_list_n V ul 1 = omega_list_n V ul 3) /\
   ~(omega_list_n V ul 2 = omega_list_n V ul 3)`);
 (ASM_SIMP_TAC[ARITH_RULE 
  `0 < 4 /\ 1 < 4 /\ 2 < 4 /\ 3 < 4 /\ ~(0 = 1) /\ ~(0 = 2) /\ ~(0 = 3) /\
   ~(1 = 2) /\ ~(2 = 3) /\ ~(1 = 3)`]);

 (NEW_GOAL `(omega_list_n V ul 1) IN voronoi_list V (truncate_simplex 1 ul)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 (NEW_GOAL `(omega_list_n V ul 2) IN voronoi_list V (truncate_simplex 2 ul)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (NEW_GOAL `(omega_list_n V ul 3) IN voronoi_list V (truncate_simplex 3 ul)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `voronoi_list V (truncate_simplex 2 ul) SUBSET 
             voronoi_list V (truncate_simplex 1 ul) /\ 
             voronoi_list V (truncate_simplex 3 ul) SUBSET 
             voronoi_list V (truncate_simplex 1 ul) /\ 
             voronoi_list V (truncate_simplex 3 ul) SUBSET 
             voronoi_list V (truncate_simplex 2 ul)`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2; TRUNCATE_SIMPLEX_EXPLICIT_3; VORONOI_LIST;VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL `!i j.
                  i < 4 /\ j < 4 /\ ~(i = j)
                  ==> ~(omega_list_n V vl i = omega_list_n V vl j)`);
 (MATCH_MP_TAC Rogers.ROGERS_AFF_DIM_FULL);
 (ASM_MESON_TAC[]);
 (NEW_GOAL 
  `~(omega_list_n V vl 0 = omega_list_n V vl 1) /\
   ~(omega_list_n V vl 0 = omega_list_n V vl 2) /\
   ~(omega_list_n V vl 0 = omega_list_n V vl 3) /\
   ~(omega_list_n V vl 1 = omega_list_n V vl 2) /\
   ~(omega_list_n V vl 1 = omega_list_n V vl 3) /\
   ~(omega_list_n V vl 2 = omega_list_n V vl 3)`);
 (ASM_SIMP_TAC[ARITH_RULE 
  `0 < 4 /\ 1 < 4 /\ 2 < 4 /\ 3 < 4 /\ ~(0 = 1) /\ ~(0 = 2) /\ ~(0 = 3) /\
   ~(1 = 2) /\ ~(2 = 3) /\ ~(1 = 3)`]);

 (NEW_GOAL `(omega_list_n V vl 1) IN voronoi_list V (truncate_simplex 1 vl)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 (NEW_GOAL `(omega_list_n V vl 2) IN voronoi_list V (truncate_simplex 2 vl)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (NEW_GOAL `(omega_list_n V vl 3) IN voronoi_list V (truncate_simplex 3 vl)`);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_N_IN_VORONOI_LIST);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `voronoi_list V (truncate_simplex 2 vl) SUBSET 
             voronoi_list V (truncate_simplex 1 vl) /\ 
             voronoi_list V (truncate_simplex 3 vl) SUBSET 
             voronoi_list V (truncate_simplex 1 vl) /\ 
             voronoi_list V (truncate_simplex 3 vl) SUBSET 
             voronoi_list V (truncate_simplex 2 vl)`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2; TRUNCATE_SIMPLEX_EXPLICIT_3; VORONOI_LIST;VORONOI_SET; set_of_list]);
 (SET_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);

 (NEW_GOAL `HD (ul:(real^3)list) = HD vl`);
 (MATCH_MP_TAC ROGERS_INTER_V_LEMMA);
 (EXISTS_TAC `V:real^3->bool`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `set_of_list ul SUBSET (V:real^3->bool)`);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; HD] THEN SET_TAC[]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 (ONCE_REWRITE_TAC[MESON[IN] `rogers V ul s <=> s IN rogers V ul`]);
 (REWRITE_WITH `rogers V ul =
             convex hull
             {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V
                                                               ul
                                                               3}`);
 (ASM_SIMP_TAC[ROGERS_EXPLICIT]);
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (SET_TAC[]);
 (NEW_GOAL `omega_list_n V ul 0 = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_MESON_TAC[]);

(* Case 1: i = 1 *)
 (NEW_GOAL `omega_list_n V ul 1 = omega_list_n V vl 1`);
 (REWRITE_WITH `omega_list_n V ul 1 = 
      closest_point (convex hull (W DIFF {HD ul})) (omega_list_n V ul 0)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 0) ul)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `1 = SUC 0`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (EXPAND_TAC "W");
 (REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 0) ul) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 0) ul))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 0) ul) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 0) ul))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH `W:real^3->bool DIFF {HD ul} = 
  {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)

 (REWRITE_WITH `omega_list_n V vl 1 = 
      closest_point (convex hull (W DIFF {HD vl})) (omega_list_n V vl 0)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 0) vl)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `1 = SUC 0`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (EXPAND_TAC "W");
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 0) vl) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 0) vl))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 0) vl) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 0) vl))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH `W:real^3->bool DIFF {HD vl} = 
  {omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);

 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)
 (ASM_MESON_TAC[]);
 (* ------------------------------------------------------------------------- *)
(* Case 2: i = 2 *)
 (NEW_GOAL `omega_list_n V ul 2 = omega_list_n V vl 2`);
 (REWRITE_WITH `omega_list_n V ul 2 = 
      closest_point (convex hull (W DIFF {HD ul, omega_list_n V ul 1})) (omega_list_n V ul 1)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 1) ul)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (EXPAND_TAC "W");
 (REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 1) ul) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 1) ul))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 1) ul) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 1) ul))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH `W:real^3->bool DIFF {HD ul, omega_list_n V ul 1} = 
  {omega_list_n V ul 2, omega_list_n V ul 3}`);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)

 (REWRITE_WITH 
 `omega_list_n V vl 2 = 
  closest_point (convex hull (W DIFF {HD vl,  omega_list_n V vl 1}))   
 (omega_list_n V vl 1)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 1) vl)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 1) vl) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 1) vl))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 1) vl) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 1) vl))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH `W:real^3->bool DIFF {HD vl, omega_list_n V vl 1} = 
                 {omega_list_n V vl 2, omega_list_n V vl 3}`);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);

 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)
 (ASM_MESON_TAC[]);

(* ------------------------------------------------------------------------- *)
(* Case 3: i = 3 *)
 (NEW_GOAL `omega_list_n V ul 3 = omega_list_n V vl 3`);
 (REWRITE_WITH 
   `omega_list_n V ul 3 = closest_point 
      (convex hull (W DIFF {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}))
      (omega_list_n V ul 2)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 2) ul)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (EXPAND_TAC "W");
 (REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 2) ul) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 2) ul))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 2) ul) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 2) ul))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH 
  `W:real^3->bool DIFF {HD ul, omega_list_n V ul 1, omega_list_n V ul 2} = 
  {omega_list_n V ul 3}`);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (EXPAND_TAC "W" THEN REWRITE_WITH `HD ul = omega_list_n V ul 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)

 (REWRITE_WITH 
 `omega_list_n V vl 3 = 
  closest_point 
  (convex hull (W DIFF {HD vl,  omega_list_n V vl 1, omega_list_n V vl 2}))
  (omega_list_n V vl 2)`);
 (MATCH_MP_TAC CLOSEST_POINT_SUBSET_lemma);
 (EXISTS_TAC `voronoi_list V (truncate_simplex (SUC 2) vl)`);
 (REPEAT STRIP_TAC); (* 7 subgoals *)

 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]); (* finish subgoal 1 *)
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                      (* finish subgoal 2 *)

 (NEW_GOAL `voronoi_list V (truncate_simplex (SUC 2) vl) = 
             convex hull (voronoi_list V (truncate_simplex (SUC 2) vl))`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (REWRITE_TAC[CONVEX_HULL_EQ;Packing3.CONVEX_VORONOI_LIST]);
 (ONCE_REWRITE_TAC[ASSUME 
  `voronoi_list V (truncate_simplex (SUC 2) vl) = 
   convex hull (voronoi_list V (truncate_simplex (SUC 2) vl))`]);
 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
 (REWRITE_WITH 
  `W:real^3->bool DIFF {HD vl, omega_list_n V vl 1, omega_list_n V vl 2} 
   = {omega_list_n V vl 3}`);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);

 (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 3 *)
 (REWRITE_TAC[CONVEX_CONVEX_HULL]);                     (* finish subgoal 4 *)
 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);       
 (MATCH_MP_TAC FINITE_DIFF);
 (EXPAND_TAC "W" THEN REWRITE_TAC[Geomdetail.FINITE6]); (* finish subgoal 5 *)
 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);           (* finish subgoal 6 *)
 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
 (REWRITE_TAC[ASSUME `W:real^3->bool = 
  {HD vl, omega_list_n V vl 1, omega_list_n V vl 2, omega_list_n V vl 3}`]);
 (REWRITE_WITH `HD vl = omega_list_n V vl 0`);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_SET_TAC[]);                                       (* finish subgoal 7 *)
 (ASM_MESON_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `i = 0`);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `i = 1`);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `i = 2`);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `i = 3`);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[])]);;


end;;