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

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
(*     


*)

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

let TEZFFSK_concl = 
`!V ul vl k. 
    saturated V /\ packing V /\ barV V 3 ul /\ barV V 3 vl /\
    rogers V ul = rogers V vl /\ aff_dim (rogers V ul) = &3 /\
    k <= 3 /\ hl (truncate_simplex k ul) < sqrt (&2) 
    ==> truncate_simplex k ul = truncate_simplex k vl`;;

let TEZFFSK = prove_by_refinement (TEZFFSK_concl,
[(REPEAT STRIP_TAC);
 (ABBREV_TAC `s1 = omega_list_n V ul 1`);
 (ABBREV_TAC `s2 = omega_list_n V ul 2`);
 (ABBREV_TAC `s3 = omega_list_n V ul 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 `?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 `!i. i <= k 
   ==> hl (truncate_simplex i (ul:(real^3)list)) < sqrt (&2)`);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `wl:(real^3)list = truncate_simplex k ul`);
 (REWRITE_WITH `truncate_simplex i ul 
               = truncate_simplex i (wl:(real^3)list)`);
 (EXPAND_TAC "wl" THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.TRUNCATE_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `hl (truncate_simplex i wl) <= hl (wl:(real^3)list)`);
 (MATCH_MP_TAC Rogers.HL_DECREASE);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `k:num`);
 (ASM_REWRITE_TAC[IN]);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL `!i. i <= k 
   ==> omega_list_n V ul i = 
       circumcenter (set_of_list (truncate_simplex i ul))`);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `omega_list_n V ul i = omega_list V (truncate_simplex i ul)`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (MATCH_MP_TAC XNHPWAB1);
 (EXISTS_TAC `i:num` THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[IN]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (ASM_SIMP_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 `s1 = omega_list_n V vl 1`);
 (EXPAND_TAC "s1" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (NEW_GOAL `s2 = omega_list_n V vl 2`);
 (EXPAND_TAC "s2" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);
 (NEW_GOAL `s3 = omega_list_n V vl 3`);
 (EXPAND_TAC "s3" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC);

 (NEW_GOAL `HD ul = HD (vl:(real^3)list)`);
 (REWRITE_TAC[HD; ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
 (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[]);
 (SUBGOAL_THEN `set_of_list (ul:(real^3)list) SUBSET V` MP_TAC);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[set_of_list] THEN SET_TAC[]);
 (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]);
 (REWRITE_TAC[MESON[IN] `rogers V ul u0 <=> u0 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}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
 (ASM_REWRITE_TAC[HD] THEN SET_TAC[]);

 (ASM_CASES_TAC `1 <= k`);
 (ABBREV_TAC `wl:(real^3)list = truncate_simplex k ul`);
 (NEW_GOAL `hl (wl:(real^3)list) = dist (omega_list V wl,HD wl)`);
 (MATCH_MP_TAC Rogers.WAUFCHE2);
 (EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[IN]);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH `omega_list V wl = omega_list_n V ul k`);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (REWRITE_WITH `HD wl = HD (ul:(real^3)list)`);
 (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (DISCH_TAC);
 (ABBREV_TAC `zl = truncate_simplex k (vl:(real^3)list)`);

 (NEW_GOAL `hl (zl:(real^3)list) < sqrt (&2)`);
 (NEW_GOAL `hl (zl:(real^3)list) <= dist (omega_list_n V ul k, HD ul)`);
 (REWRITE_WITH `omega_list_n V ul k = omega_list_n V vl k`);
 (NEW_GOAL `k = 1 \/ k = 2 \/ k = 3`);
 (ASM_ARITH_TAC);
 (UP_ASM_TAC THEN ASM_MESON_TAC[]);
 (REWRITE_TAC[ASSUME `HD (ul:(real^3)list) = HD vl`]);
 (REWRITE_WITH `omega_list_n V vl k = omega_list V zl`);
 (EXPAND_TAC "zl" THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (REWRITE_WITH `HD vl = HD (zl:(real^3)list)`);
 (EXPAND_TAC "zl" THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH] THEN ASM_ARITH_TAC);
 (MATCH_MP_TAC WAUFCHE1);
 (EXISTS_TAC `k:num` THEN REWRITE_TAC[IN] THEN EXPAND_TAC "zl");
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
 (ASM_REAL_ARITH_TAC);


 (NEW_GOAL `!i. i <= k 
   ==> hl (truncate_simplex i (vl:(real^3)list)) < sqrt (&2)`);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `truncate_simplex i vl 
               = truncate_simplex i (zl:(real^3)list)`);
 (EXPAND_TAC "zl" THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC Packing3.TRUNCATE_TRUNCATE_SIMPLEX);
 (ASM_REWRITE_TAC[LENGTH]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `hl (truncate_simplex i zl) <= hl (zl:(real^3)list)`);
 (MATCH_MP_TAC Rogers.HL_DECREASE);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `k:num`);
 (ASM_REWRITE_TAC[IN]);
 (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (ASM_REAL_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
 (NEW_GOAL `~(affine_dependent {v0,v1,v2,v3:real^3})`);
 (REWRITE_WITH `{v0,v1,v2,v3:real^3} = set_of_list vl`);
 (ASM_REWRITE_TAC[set_of_list]);
 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3:num`);
 (ASM_REWRITE_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}`);
 (MATCH_MP_TAC ROGERS_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL 
`~(affine_dependent {HD ul, omega_list_n V ul 1, omega_list_n V ul 2,  
                     omega_list_n V ul 3})`);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim {HD ul, omega_list_n V ul 1, 
                      omega_list_n V ul 2, omega_list_n V ul 3} <= &2`);
 (ASM_SIMP_TAC [AFF_DEPENDENT_AFF_DIM_4]);
 (UP_ASM_TAC THEN REWRITE_TAC[] THEN 
   ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]);
 (STRIP_TAC);
 (NEW_GOAL `aff_dim (rogers V ul) <= aff_dim (affine hull
   {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3})`);
 (MATCH_MP_TAC AFF_DIM_SUBSET);
 (REWRITE_TAC[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}`;
   CONVEX_HULL_SUBSET_AFFINE_HULL]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `~(affine_dependent (
              set_of_list (truncate_simplex k (ul:(real^3)list))))`);
 (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `k:num`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);

 (NEW_GOAL `CARD {v0,v1,v2,v3:real^3} = 4`);
 (REWRITE_WITH `{v0,v1,v2,v3:real^3} = set_of_list vl`);
 (ASM_REWRITE_TAC[set_of_list]);
 (REWRITE_WITH `LENGTH (vl:(real^3)list) = 3 + 1 /\ 
                 CARD (set_of_list vl) = 3 + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (ARITH_TAC);

(* ------------------------------------------------------------------------- *)
 (NEW_GOAL `u0 = v0:real^3`);
 (UNDISCH_TAC `HD ul = HD (vl:(real^3)list)` THEN ASM_REWRITE_TAC[HD]);

 (NEW_GOAL `u1 = v1:real^3`);
 (ABBREV_TAC `S1 = {u0, u1:real^3}`);

 (NEW_GOAL `!u:real^3 v. u IN S1 /\ v IN V DIFF S1 
                         ==> dist (v,s1) > dist (u,s1)`);
 (MATCH_MP_TAC XYOFCGX);
 (REPEAT STRIP_TAC);  (* 5 new subgoals *)

 (ASM_REWRITE_TAC[]);                                 (* finish subgoal 1 *)
 (REWRITE_WITH `S1:real^3->bool = set_of_list (truncate_simplex 1 ul)`);
 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (ASM_MESON_TAC[]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `1` THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); 
                                                        (* finish subgoal 2 *)

 (UP_ASM_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET);
 (EXISTS_TAC `set_of_list (truncate_simplex k (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "wl");
 (ASM_CASES_TAC `k = 1`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `k = 1`]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 2`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `k = 2`]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 3`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_3; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `k = 3`]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);  (* finish subgoal 3 *)

 (EXPAND_TAC "s1" THEN EXPAND_TAC "S1");
 (MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW);
 (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
 (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=> (A/\B/\C/\D)/\E`]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `radV (S1:real^3->bool) 
               = hl (truncate_simplex 1 (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[HL;TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list]);
 (EXPAND_TAC "S1" THEN REWRITE_TAC[ASSUME `u0 = v0:real^3`]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);  (* finish subgoal 5 *)

 (NEW_GOAL `v1:real^3 IN S1`);
 (ASM_CASES_TAC `v1:real^3 IN S1`);
 (UP_ASM_TAC THEN MESON_TAC[]);

 (NEW_GOAL `F`);
 (NEW_GOAL `dist (v1,s1) > dist (u0,s1:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (STRIP_TAC);
 (EXPAND_TAC "S1" THEN SET_TAC[]);
 (ASM_REWRITE_TAC[IN_DIFF]);
 (NEW_GOAL `set_of_list vl 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]);
 (SET_TAC[]);

 (NEW_GOAL `s1 = circumcenter {v0,v1:real^3}`);
 (REWRITE_TAC[ASSUME `s1 = omega_list_n V vl 1`]);
 (MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW);
 (EXISTS_TAC `v2:real^3` THEN EXISTS_TAC `v3:real^3`);
 (REWRITE_WITH `[v0;v1:real^3] = truncate_simplex 1 vl`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=> (A/\B/\C/\D)/\E`]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[Rogers.CIRCUMCENTER_2; midpoint]);
 (STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[
   ASSUME `s1:real^3 = inv (&2) % (v0 + v1)`; ASSUME `u0 = v0:real^3`;dist]);
 (REWRITE_TAC[VECTOR_ARITH 
  `v1 - inv (&2) % (v0 + v1) = inv (&2) % (v1 - v0) /\ 
   v0 - inv (&2) % (v0 + v1) = (-- inv (&2)) % (v1 - v0)`; NORM_MUL; REAL_ABS_NEG] THEN REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `~(v1 = u0:real^3)`);
 (REWRITE_TAC[ASSUME `u0 = v0:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,a,b,c} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v2,v3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);
 (ASM_SET_TAC[]);

 (ASM_CASES_TAC `k = 1`);
 (EXPAND_TAC "wl" THEN EXPAND_TAC "zl" THEN REWRITE_TAC[ASSUME `k = 1`]);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);

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

 (NEW_GOAL `u2 = v2:real^3`);
 (ABBREV_TAC `S2 = {u0, u1, u2:real^3}`);

 (NEW_GOAL `!u:real^3 v. u IN S2 /\ v IN V DIFF S2 
                         ==> dist (v,s2) > dist (u,s2)`);
 (MATCH_MP_TAC XYOFCGX);
 (REPEAT STRIP_TAC);  (* 5 new subgoals *)

 (ASM_REWRITE_TAC[]);                                 (* finish subgoal 1 *)
 (REWRITE_WITH `S2:real^3->bool = set_of_list (truncate_simplex 2 ul)`);
 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (ASM_MESON_TAC[]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `2` THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); 
                                                        (* finish subgoal 2 *)
 (UP_ASM_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET);
 (EXISTS_TAC `set_of_list (truncate_simplex k (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "wl");
 (ASM_CASES_TAC `k = 2`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `k = 2`]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 3`);
 (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_3; 
   ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `k = 3`]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);  (* finish subgoal 3 *)

 (EXPAND_TAC "s2" THEN EXPAND_TAC "S2");
 (MATCH_MP_TAC OMEGA_LIST_2_EXPLICIT_NEW);
 (EXISTS_TAC `u3:real^3`);
 (REWRITE_WITH `[u0;u1;u2:real^3] = truncate_simplex 2 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=> (A/\B/\C/\D)/\E`]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);

 (REWRITE_WITH `radV (S2:real^3->bool) 
               = hl (truncate_simplex 2 (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[HL;TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]);
 (EXPAND_TAC "S2" THEN REWRITE_TAC[ASSUME `u0 = v0:real^3`; ASSUME `u1 = v1:real^3`]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);  (* finish subgoal 5 *)

 (NEW_GOAL `v2:real^3 IN S2`);
 (ASM_CASES_TAC `v2:real^3 IN S2`);
 (UP_ASM_TAC THEN MESON_TAC[]);

 (NEW_GOAL `F`);
 (NEW_GOAL `dist (v2,s2) > dist (u0,s2:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (STRIP_TAC);
 (EXPAND_TAC "S2" THEN SET_TAC[]);
 (ASM_REWRITE_TAC[IN_DIFF]);
 (NEW_GOAL `set_of_list vl 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]);
 (SET_TAC[]);

 (NEW_GOAL `s2 = circumcenter {v0,v1,v2:real^3}`);
 (REWRITE_TAC[ASSUME `s2 = omega_list_n V vl 2`]);
 (MATCH_MP_TAC OMEGA_LIST_2_EXPLICIT_NEW);
 (EXISTS_TAC `v3:real^3`);
 (REWRITE_WITH `[v0;v1;v2:real^3] = truncate_simplex 2 vl`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=> (A/\B/\C/\D)/\E`]);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!w:real^3. w IN {v0,v1,v2} 
             ==> radV {v0,v1,v2} = dist (s2:real^3,w)`);
 (REWRITE_TAC[ASSUME `s2 = circumcenter {v0, v1, v2:real^3}`]);
 (MATCH_MP_TAC Rogers.OAPVION2);
 (MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET);
 (EXISTS_TAC `{v0,v1,v2,v3:real^3}`);
 (ASM_REWRITE_TAC[] THEN SET_TAC[]);
 (NEW_GOAL `dist (u0,s2:real^3) = radV {v0, v1, v2:real^3}`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (v2,s2:real^3) = radV {v0, v1, v2:real^3}`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `~(v2 = u0:real^3)`);
 (REWRITE_TAC[ASSUME `u0 = v0:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,b,a,c} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v1,v3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);

 (NEW_GOAL `~(v2 = u1:real^3)`);
 (REWRITE_TAC[ASSUME `u1 = v1:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,b,b,c} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v1,v3:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);
 (ASM_SET_TAC[]);

 (ASM_CASES_TAC `k = 2`);
 (EXPAND_TAC "wl" THEN EXPAND_TAC "zl" THEN REWRITE_TAC[ASSUME `k = 2`]);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);

(* ------------------------------------------------------------------------ *) 

 (NEW_GOAL `k = 3`);
 (ASM_ARITH_TAC);
 (NEW_GOAL `u3 = v3:real^3`);
 (ABBREV_TAC `S3 = {u0, u1, u2, u3:real^3}`);

 (NEW_GOAL `!u:real^3 v. u IN S3 /\ v IN V DIFF S3 
                         ==> dist (v,s3) > dist (u,s3)`);
 (MATCH_MP_TAC XYOFCGX);
 (REPEAT STRIP_TAC);  (* 5 new subgoals *)

 (ASM_REWRITE_TAC[]);                                 (* finish subgoal 1 *)
 (REWRITE_WITH `S3:real^3->bool = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (ASM_MESON_TAC[]);
 (MATCH_MP_TAC Packing3.BARV_SUBSET);
 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);             (* finish subgoal 2 *)

 (UP_ASM_TAC THEN EXPAND_TAC "S3");
 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list (truncate_simplex k ul)`);
 (REWRITE_TAC[ASSUME `k = 3`; ASSUME `ul = [u0;u1;u2;u3:real^3]`; 
  set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (ASM_REWRITE_TAC[]);                                 (* finish subgoal 3 *)

 (EXPAND_TAC "s3" THEN EXPAND_TAC "S3");
 (MATCH_MP_TAC OMEGA_LIST_3_EXPLICIT);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=>(A/\B/\C/\E)/\D`] THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `hl (ul:(real^3)list) = hl (wl:(real^3)list)`);
 (EXPAND_TAC "wl" THEN REWRITE_TAC[ASSUME `k = 3`]);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_WITH `radV (S3:real^3->bool) 
               = hl (truncate_simplex 3 (ul:(real^3)list))`);
 (ASM_REWRITE_TAC[HL;TRUNCATE_SIMPLEX_EXPLICIT_3;set_of_list]);
 (EXPAND_TAC "S3" THEN REWRITE_TAC[ASSUME `u0 = v0:real^3`; 
   ASSUME `u1 = v1:real^3`; ASSUME `u2 = v2:real^3`]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);  (* finish subgoal 5 *)

 (NEW_GOAL `v3:real^3 IN S3`);
 (ASM_CASES_TAC `v3:real^3 IN S3`);
 (UP_ASM_TAC THEN MESON_TAC[]);

 (NEW_GOAL `F`);
 (NEW_GOAL `dist (v3,s3) > dist (u0,s3:real^3)`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (STRIP_TAC);
 (EXPAND_TAC "S3" THEN SET_TAC[]);
 (ASM_REWRITE_TAC[IN_DIFF]);
 (NEW_GOAL `set_of_list vl 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]);
 (SET_TAC[]);

 (NEW_GOAL `s3 = circumcenter {v0,v1,v2, v3:real^3}`);
 (REWRITE_TAC[ASSUME `s3 = omega_list_n V vl 3`]);
 (MATCH_MP_TAC OMEGA_LIST_3_EXPLICIT);
 (REWRITE_TAC[IN; MESON[] `A/\B/\C/\D/\E <=>(A/\B/\C/\E)/\D`] THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `hl (vl:(real^3)list) = hl (zl:(real^3)list)`);
 (EXPAND_TAC "zl" THEN REWRITE_TAC[ASSUME `k = 3`]);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!w:real^3. w IN {v0,v1,v2,v3} 
             ==> radV {v0,v1,v2,v3} = dist (s3:real^3,w)`);
 (REWRITE_TAC[ASSUME `s3 = circumcenter {v0, v1, v2, v3:real^3}`]);
 (MATCH_MP_TAC Rogers.OAPVION2);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `dist (u0,s3:real^3) = radV {v0, v1, v2, v3:real^3}`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_SET_TAC[]);
 (NEW_GOAL `dist (v3,s3:real^3) = radV {v0, v1, v2, v3:real^3}`);
 (ONCE_REWRITE_TAC[DIST_SYM]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (SET_TAC[]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `~(v3 = u0:real^3)`);
 (REWRITE_TAC[ASSUME `u0 = v0:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,b,c,a} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v1,v2:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);

 (NEW_GOAL `~(v3 = u1:real^3)`);
 (REWRITE_TAC[ASSUME `u1 = v1:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,b,c,b} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v1,v2:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);

 (NEW_GOAL `~(v3 = u2:real^3)`);
 (REWRITE_TAC[ASSUME `u2 = v2:real^3`]);
 (STRIP_TAC);
 (UNDISCH_TAC `CARD {v0,v1,v2,v3:real^3} = 4`);
 (ASM_REWRITE_TAC[SET_RULE `{a,b,c,c} = {a,b,c}`]);
 (NEW_GOAL `CARD {v0,v1,v2:real^3} <= 3`);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (UP_ASM_TAC THEN ARITH_TAC);
 (ASM_SET_TAC[]);

 (EXPAND_TAC "wl" THEN EXPAND_TAC "zl" THEN REWRITE_TAC[ASSUME `k = 3`]);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);

(* ------------------------------------------------------------------------ *) 

 (NEW_GOAL `k = 0`);
 (ASM_ARITH_TAC);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]);
 (REWRITE_WITH `u0:real^3 = HD ul /\ v0:real^3 = HD vl`);
 (ASM_MESON_TAC[HD]);
 (ASM_REWRITE_TAC[])]);;

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

end;;