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


module Ddzuphj = 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;;
open Hdtfnfz;;
open Tezffsk;;
open Njiutiu;;

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

let DDZUPHJ_concl = 
`!V ul vl k. 
  saturated V /\ packing V /\ k IN {0,1,2,3,4} /\ 
  barV V 3 ul /\ barV  V 3 vl /\ rogers V ul = rogers V vl /\ 
  aff_dim (rogers V ul) = &3 /\ ~ (mcell k V ul = {})
  ==> (mcell k V ul = mcell k V vl)`;;

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

let RCONE_GT_EQ_EMPTY_LEMMA = 
prove_by_refinement (
 `!a:real^3 b r. r >= &1 ==> rcone_gt a b r = {}`,

[(REPEAT STRIP_TAC);
 (REWRITE_TAC[rcone_gt;rconesgn; 
   SET_RULE `{x | P x} = {} <=> (!x. P x ==> F)`]);
 (REWRITE_TAC[dist] THEN REPEAT STRIP_TAC);
 (NEW_GOAL `(x - a) dot (b - a) <= norm(x - a) * norm (b - a:real^3)`);
 (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
 (NEW_GOAL`norm (x - a) * norm (b:real^3 -a) * r >= norm (x-a) * norm (b-a)`);
 (REWRITE_TAC[REAL_ARITH `(a*b*c >= a * b) <=> &0 <= (a * b) * (c - &1)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (STRIP_TAC);
 (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[NORM_POS_LE]); 
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC)]);;
(* ========================================================================= *)
(*         Main theorem                                                      *)
(* ========================================================================= *)


let DDZUPHJ = prove_by_refinement (DDZUPHJ_concl,
[(REPEAT STRIP_TAC);
 (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[]);
 (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 UP_ASM_TAC THEN REPEAT STRIP_TAC);

(* ========================================================================= *)
(* Case k = 4 *)

 (ASM_CASES_TAC `k = 4`);
 (NEW_GOAL `hl (ul:(real^3)list) < sqrt (&2)`);
 (UNDISCH_TAC `~(mcell k V ul = {})` THEN 
  SIMP_TAC[ASSUME `k = 4`; MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]);
 (MESON_TAC[]);

 (NEW_GOAL `truncate_simplex 3 (ul:(real^3)list) = truncate_simplex 3 vl`);
 (MATCH_MP_TAC TEZFFSK);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (REWRITE_WITH `truncate_simplex 3 [u0; u1; u2; u3:real^3] = ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (REWRITE_WITH `truncate_simplex 3 (vl:(real^3)list) = vl`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (STRIP_TAC);
 (REWRITE_TAC[ASSUME `ul = (vl:(real^3)list)`]);

(* ========================================================================= *)
(* Case k = 3 *)
 (ASM_CASES_TAC `k = 3`);
 (NEW_GOAL `hl (truncate_simplex 2 ul) < sqrt (&2) /\ 
             sqrt (&2) <= hl (ul:(real^3)list)`);
 (UNDISCH_TAC `~(mcell k V ul = {})` THEN 
  SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT;mcell3]);
 (MESON_TAC[]);

 (NEW_GOAL `truncate_simplex 2 (ul:(real^3)list) = truncate_simplex 2 vl`);
 (MATCH_MP_TAC TEZFFSK);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);

 (NEW_GOAL `!i. 0 <= i /\ i <= 3
                  ==> omega_list_n V ul i = omega_list_n V vl i`);
 (MATCH_MP_TAC NJIUTIU);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 (STRIP_TAC);
 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
               GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `mxi V ul = mxi V vl`);
 (REWRITE_TAC[mxi]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (NEW_GOAL `F`);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[]);

 (SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME 
  `truncate_simplex 2 ul = truncate_simplex 2 (vl:(real^3)list)`)]);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

(* ========================================================================= *)
(* Case k = 2 *)

 (ASM_CASES_TAC `k = 2`);
 (NEW_GOAL `hl (truncate_simplex 1 ul) < sqrt (&2) /\ 
             sqrt (&2) <= hl (ul:(real^3)list)`);
 (UNDISCH_TAC `~(mcell k V ul = {})` THEN 
  SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT;mcell2]);
 (MESON_TAC[]);

 (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
 (MATCH_MP_TAC TEZFFSK);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);

 (NEW_GOAL `!i. 0 <= i /\ i <= 3
                  ==> omega_list_n V ul i = omega_list_n V vl i`);
 (MATCH_MP_TAC NJIUTIU);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 (STRIP_TAC);
 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
               GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `mxi V ul = mxi V vl`);
 (REWRITE_TAC[mxi]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (NEW_GOAL `F`);

 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 vl`);
 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (ASM_REAL_ARITH_TAC);

 (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 ul`);
 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V wl = omega_list_n V ul 2/\ HD wl = HD ul`);
 (EXPAND_TAC "wl");
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
   TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);

 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
 (REWRITE_WITH `omega_list V zl = omega_list_n V vl 2/\ HD zl = HD vl`);
 (EXPAND_TAC "zl");
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
   TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);

 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (COND_CASES_TAC);
 (NEW_GOAL `F`);

 (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`);
 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (ASM_REAL_ARITH_TAC);

 (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 vl`);
 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V wl = omega_list_n V vl 2/\ HD wl = HD vl`);
 (EXPAND_TAC "wl");
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`;
   TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);

 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`);
 (REWRITE_WITH `omega_list V zl = omega_list_n V ul 2/\ HD zl = HD ul`);
 (EXPAND_TAC "zl");
 (STRIP_TAC);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;
   TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`);
 (STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);

 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);

 (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (REWRITE_TAC[ASSUME 
   `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);

 (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (REWRITE_TAC[ASSUME 
   `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]);
 (REPEAT LET_TAC);
 (REWRITE_TAC[ASSUME `mxi V ul = mxi V vl`]);
 (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`);
 (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (ASM_REWRITE_TAC[HD;TL]);

 (NEW_GOAL `{u0, u1} = {v0, v1:real^3}`);
 (REWRITE_WITH `{u0,u1:real^3} = set_of_list(truncate_simplex 1 ul)`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; 
               ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (REWRITE_WITH `{v0,v1:real^3} = set_of_list(truncate_simplex 1 vl)`);
 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `u0 = v0:real^3`);
 (NEW_GOAL `u1 = v1:real^3`);
 (NEW_GOAL `~(u0 = u1:real^3)`);
 (STRIP_TAC);
 (NEW_GOAL `LENGTH (truncate_simplex 1 (ul:(real^3)list)) = 1 + 1 /\ 
             CARD (set_of_list (truncate_simplex 1 ul)) = 1 + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 (UP_ASM_TAC THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `u0 = u1:real^3`; 
   SET_RULE `{a,a} = {a}`; Geomdetail.CARD_SING; ARITH_RULE `~(1 = 1 + 1)`]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `u0 = v1:real^3`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (NEW_GOAL `u1 = v0:real^3`);
 (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);

 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME 
  `truncate_simplex 1 ul = truncate_simplex 1 (vl:(real^3)list)`)]);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

(* ========================================================================= *)
(* Case k = 1 *)

 (ASM_CASES_TAC `k = 1`);
 (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`);
 (UNDISCH_TAC `~(mcell k V ul = {})` THEN 
  SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT;mcell1]);
 (MESON_TAC[]);

 (NEW_GOAL `!i. 0 <= i /\ i <= 3
                  ==> omega_list_n V ul i = omega_list_n V vl i`);
 (MATCH_MP_TAC NJIUTIU);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `HD ul = HD (vl:(real^3)list)`);
 (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 `HD ul IN set_of_list (ul:(real^3)list)`);
 (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
 (REWRITE_TAC[IN]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 (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}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (SET_TAC[]);

 (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`);
 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 (STRIP_TAC);
 (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]);
 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`);
               GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);

 (ASM_CASES_TAC `hl (truncate_simplex 1 (ul:(real^3)list)) < sqrt (&2)`);
 (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`);
 (MATCH_MP_TAC TEZFFSK);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);

 (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (REWRITE_TAC[ASSUME 
   `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`; 
   ASSUME `HD ul = HD (vl:(real^3)list)`; ASSUME `rogers V ul = rogers V vl`]);
 (REWRITE_WITH `HD (TL ul) = EL 1 (truncate_simplex 1 (ul:(real^3)list))`);
 (REWRITE_TAC[ASSUME 
  `ul = [u0;u1;u2;u3:real^3]`;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
 (REWRITE_WITH `HD (TL vl) = EL 1 (truncate_simplex 1 (vl:(real^3)list))`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);


 (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (ul:(real^3)list))`);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (vl:(real^3)list))`);
 (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]);
 (STRIP_TAC);
 (ABBREV_TAC `zl = truncate_simplex 1 (vl:(real^3)list)`);
 (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`);
 (MATCH_MP_TAC WAUFCHE2);
 (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);

 (ABBREV_TAC `wl = truncate_simplex 1 (ul:(real^3)list)`);
 (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);

 (UP_ASM_TAC THEN 
   REWRITE_WITH `omega_list V wl = omega_list_n V ul 1 /\ HD wl = HD ul`);
 (STRIP_TAC);
 (EXPAND_TAC "wl");
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (EXPAND_TAC "wl");
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)` THEN 
   REWRITE_WITH `omega_list V zl = omega_list_n V vl 1 /\ HD zl = HD vl`);
 (STRIP_TAC);
 (EXPAND_TAC "zl");
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (EXPAND_TAC "zl");
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC);

 (REWRITE_WITH `omega_list_n V ul 1 = omega_list_n V  vl 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (REWRITE_TAC[ASSUME `HD (ul:(real^3)list) = HD (vl:(real^3)list)`]);
 (ASM_REAL_ARITH_TAC);

 (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);

 (REWRITE_WITH 
 `rcone_gt (HD (ul:(real^3)list)) (HD (TL ul)) 
  (hl (truncate_simplex 1 ul) / sqrt (&2)) = {}`);
 (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (ul:(real^3)list)) / sqrt (&2) 
    <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 ul)`);
 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT);
 (ARITH_TAC);
 (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);

 (REWRITE_WITH 
 `rcone_gt (HD (vl:(real^3)list)) (HD (TL vl)) 
  (hl (truncate_simplex 1 vl) / sqrt (&2)) = {}`);
 (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA);
 (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]);
 (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (vl:(real^3)list)) / sqrt (&2) 
    <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 vl)`);
 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
 (MATCH_MP_TAC SQRT_POS_LT);
 (ARITH_TAC);
 (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[]);

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

(* ========================================================================= *)
(* Case k = 0 *)

 (NEW_GOAL `k = 0`);
 (ASM_SET_TAC[]);
 (SIMP_TAC[ASSUME `k = 0`; MCELL_EXPLICIT; mcell0]);
 (REWRITE_TAC[ASSUME `rogers V ul = rogers V vl`]);

 (NEW_GOAL `!i. 0 <= i /\ i <= 3
                  ==> omega_list_n V ul i = omega_list_n V vl i`);
 (MATCH_MP_TAC NJIUTIU);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `HD ul = HD (vl:(real^3)list)`);
 (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 `HD ul IN set_of_list (ul:(real^3)list)`);
 (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_SET_TAC[]);
 (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`);
 (REWRITE_TAC[IN]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 (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}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (SET_TAC[])]);;

end;;