(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: Marchal cells                                            *)
(*      Chaper    : Packing (Clusters)                                       *)
(*      Date      : October 3, 2010                                          *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================== *)
(* This file contains some lemmas that support for marchalcells part.         *) 
(* ========================================================================== *)



(* dmtcp *)

flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "packing/pack_concl.hl";;
flyspeck_needs "packing/pack1.hl";;



module Marchal_cells = struct

open Pack_defs;;
open Pack_concl;;
open Vukhacky_tactics;;
open Pack1;;


let XNHPWAB1 = new_axiom XNHPWAB1_concl;;
let XNHPWAB4 = new_axiom XNHPWAB4_concl;;

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

let TRUNCATE_SIMPLEX_GENERAL_0 = 
prove_by_refinement (
 `!(xl:(real^3)list). ~(xl = []) ==> truncate_simplex 0 xl = [HD xl]`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 STRIP_TAC;

 (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (NEW_GOAL `(xl':(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (MESON[] `x = y ==> [x] = [y]`));
 (ASM_REWRITE_TAC[APPEND;HD]);
 STRIP_TAC;

 (ASM_REWRITE_TAC[LENGTH;HD;ARITH_RULE `SUC 0 = 0 + 1`]);

 (NEW_GOAL `?h:real^3 t. xl = CONS h t`);
 (ASM_MESON_TAC[list_CASES]);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (EXISTS_TAC `t:(real^3)list`);
 (ASM_REWRITE_TAC[HD;APPEND])]);;


let TRUNCATE_SIMPLEX_EXPLICIT_0 = 
prove_by_refinement (
 `!u0 u1 u2 u3:real^3. truncate_simplex 0 [u0] = [u0] /\ 
                        truncate_simplex 0 [u0;u1] = [u0] /\
                        truncate_simplex 0 [u0;u1;u2] = [u0] /\
                        truncate_simplex 0 [u0;u1;u2;u3] = [u0]`,

[ (REPEAT STRIP_TAC);
 (NEW_GOAL `~([u0:real^3] = [])`);
 (MESON_TAC[NOT_CONS_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
 (NEW_GOAL `~([u0:real^3;u1] = [])`);
 (MESON_TAC[NOT_CONS_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
 (NEW_GOAL `~([u0:real^3;u1;u2] = [])`);
 (MESON_TAC[NOT_CONS_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD]);
 (NEW_GOAL `~([u0:real^3;u1;u2;u3] = [])`);
 (MESON_TAC[NOT_CONS_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_0;HD])]);;

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


let TRUNCATE_SIMPLEX_GENERAL_1 = 
prove_by_refinement (
 `!ul vl a b:real^3. 
   (ul = APPEND [a;b] vl) ==> truncate_simplex 1 ul = [a;b]`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 STRIP_TAC;

 (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 1`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `(zl:(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (MESON[] `x = y /\ z = t ==> [x;z] = [y;t]`));
 (UNDISCH_TAC `ul:(real^3)list = APPEND y yl`);
 (ASM_REWRITE_TAC[APPEND]);
 (MESON_TAC[CONS_11]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
 (EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[])]);;

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

let TRUNCATE_SIMPLEX_EXPLICIT_1 = 
prove_by_refinement (
 `!a b c (d:real^3). truncate_simplex 1 [a;b] = [a;b] /\ 
                      truncate_simplex 1 [a;b;c] = [a;b] /\
                      truncate_simplex 1 [a;b;c;d] = [a;b]`,

[ (REPEAT STRIP_TAC);
 (NEW_GOAL `[a;b] = APPEND [a:real^3; b] []`);
 (MESON_TAC[APPEND_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1]);
 (NEW_GOAL `[a;b;c] = APPEND [a:real^3; b] [c]`);
 (REWRITE_TAC[APPEND]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1]);
 (NEW_GOAL `[a;b;c;d] = APPEND [a:real^3; b] [c;d]`);
 (REWRITE_TAC[APPEND]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_1])]);;

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

let TRUNCATE_SIMPLEX_GENERAL_2 = 
prove_by_refinement (
 `!a b c:real^3 ul vl. 
    ul = APPEND [a;b;c] vl ==> truncate_simplex 2 ul = [a;b;c]`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 STRIP_TAC;

 (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 2`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 1`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?t tl. (zl:(real^3)list) = CONS t tl /\ LENGTH tl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `(tl:(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (MESON[] `x = y /\ z = t /\ s = r ==> [x;z;s] = [y;t;r]`));
 (UNDISCH_TAC `ul:(real^3)list = APPEND y yl`);
 (ASM_REWRITE_TAC[APPEND;CONS_11]);
 (MESON_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[LENGTH;ARITH_RULE 
 `SUC (1 + 1) = 2 + 1 /\ SUC (SUC (SUC 0)) = 2 + 1`]);
 (EXISTS_TAC `vl:(real^3)list`);
 (ASM_REWRITE_TAC[])]);;

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

let TRUNCATE_SIMPLEX_EXPLICIT_2 = 
prove_by_refinement (
 `!a b c d:real^3.
         truncate_simplex 2 [a; b; c] = [a; b; c] /\
         truncate_simplex 2 [a; b; c; d] = [a; b; c]`,

[ (REPEAT STRIP_TAC);
 (NEW_GOAL `[a;b;c] = APPEND [a:real^3; b; c] []`);
 (MESON_TAC[APPEND_NIL]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_2]);
 (NEW_GOAL `[a;b;c;d] = APPEND [a:real^3; b; c] [d]`);
 (REWRITE_TAC[APPEND]);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_GENERAL_2])]);;

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

let TRUNCATE_SIMPLEX_EXPLICIT_3 = 
prove_by_refinement (
 `!a b c d:real^3.
         truncate_simplex 3 [a; b; c; d] = [a; b; c; d]`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[TRUNCATE_SIMPLEX;INITIAL_SUBLIST]);
 (MATCH_MP_TAC SELECT_UNIQUE);
 (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC);
 STRIP_TAC;

 (NEW_GOAL `?x xl. (y:(real^3)list) = CONS x xl /\ LENGTH xl = 3`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?z zl. (xl:(real^3)list) = CONS z zl /\ LENGTH zl = 2`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?t tl. (zl:(real^3)list) = CONS t tl /\ LENGTH tl = 1`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `?w wl. (tl:(real^3)list) = CONS w wl /\ LENGTH wl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);

 (NEW_GOAL `(wl:(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `LENGTH [a;b;c;d:real^3] = 
             LENGTH (y:(real^3)list) + LENGTH (yl:(real^3)list)`);
 (ASM_MESON_TAC[LENGTH_APPEND]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[LENGTH] THEN DISCH_TAC);
 (NEW_GOAL `(yl:(real^3)list) = ([]:(real^3)list)`);
 (REWRITE_TAC[GSYM LENGTH_EQ_NIL]);
 (ASM_ARITH_TAC);
 (ASM_REWRITE_TAC[APPEND]);

 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[LENGTH;ARITH_RULE 
  `SUC (2 + 1) = 3 + 1 /\ SUC (SUC (SUC 0)) = 2 + 1`]);

 (EXISTS_TAC `[]:(real^3)list`);
 (ASM_REWRITE_TAC[APPEND])]);;

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

let OMEGA_LIST_TRUNCATE_0 = 
prove_by_refinement (
 `!V u0:real^3 u1 u2 u3. 
     omega_list_n V [u0;u1;u2;u3] 0 = omega_list V [u0] `,

[ (REPEAT GEN_TAC);
 (REWRITE_TAC[OMEGA_LIST]);
 (REWRITE_WITH `LENGTH [u0:real^3] - 1 = 0`);
 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC 0 - 1 = 0`]);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (MESON_TAC[HD])]);;

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

let OMEGA_LIST_TRUNCATE_1 = 
prove_by_refinement (
 `!V u0:real^3 u1 u2 u3. 
     omega_list_n V [u0;u1;u2;u3] 1 = omega_list V [u0;u1] `,

[ (REPEAT GEN_TAC);
 (REWRITE_TAC[OMEGA_LIST]);
 (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);
 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`]);
 (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N]);
 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;


let OMEGA_LIST_TRUNCATE_2 = 
prove_by_refinement (
 `!V u0:real^3 u1 u2 u3. 
     omega_list_n V [u0;u1;u2;u3] 2 = omega_list V [u0;u1;u2] `,

[ (REPEAT GEN_TAC);
 (REWRITE_TAC[OMEGA_LIST]);
 (REWRITE_WITH `LENGTH [u0:real^3;u1;u2] - 1 = 2`);
 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`]);
 (REWRITE_TAC[ARITH_RULE `2 = SUC 1`; OMEGA_LIST_N]);
 (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`;TRUNCATE_SIMPLEX_EXPLICIT_2;HD]);
 (REPEAT AP_TERM_TAC);
 (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N;HD]);
 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;

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

(* -------------------------------------------------------------------------- *)
let OMEGA_LIST_0_EXPLICIT = 
prove_by_refinement (
 `!a:real^3 b c V ul.
     saturated V /\
     packing V /\
     ul IN barV V 3 /\
     hl ul < sqrt (&2) /\
     ul = [a; b; c; d]
     ==> omega_list_n V ul 0 = a`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[OMEGA_LIST_N]);
 (ASM_MESON_TAC[HD])]);;
 


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

let OMEGA_LIST_1_EXPLICIT = 
prove_by_refinement (
 `!a:real^3 b c d V ul.
     saturated V /\
     packing V /\
     ul IN barV V 3 /\
     hl ul < sqrt (&2) /\
     ul = [a; b; c; d]
     ==> omega_list_n V ul 1 = circumcenter {a, b}`,

[ (REPEAT STRIP_TAC);
 (REWRITE_WITH `{a,b} = set_of_list [a;(b:real^3)]`);
 (MESON_TAC[set_of_list]);
 (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3]) = omega_list V [a:real^3; b]`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC XNHPWAB1);
 (EXISTS_TAC `1`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
 (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);

 (REPEAT STRIP_TAC);
 (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
 (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
 (UNDISCH_TAC `initial_sublist vl [a:real^3; b]`);
 (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
 (EXISTS_TAC `APPEND yl [c;d:real^3]`);
 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b] = APPEND vl yl`)]);
 (ASM_REWRITE_TAC[APPEND]);
 (ASM_MESON_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) < b /\ a < hl ul ==> a < b`));
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `[a;b:real^3] = truncate_simplex 1 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_WITH `[a;b;c;d:real^3] = truncate_simplex 3 ul`);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (NEW_GOAL `!i j.  i < j /\ j <= 3
                     ==> hl (truncate_simplex i (ul:(real^3)list)) 
                       < hl (truncate_simplex j ul)`);
 (MATCH_MP_TAC XNHPWAB4);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_1])]);;
(* -------------------------------------------------------------------------- *)

let OMEGA_LIST_2_EXPLICIT = 
prove_by_refinement (
 `!a:real^3 b c d V ul.
     saturated V /\
     packing V /\
     ul IN barV V 3 /\
     hl ul < sqrt (&2) /\
     ul = [a; b; c; d]
     ==> omega_list_n V ul 2 = circumcenter {a, b , c}`,

[ (REPEAT STRIP_TAC);
 (REWRITE_WITH `{a,b, c} = set_of_list [a;(b:real^3);c]`);
 (MESON_TAC[set_of_list]);
 (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3;c]) = omega_list V [a;b;c]`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC XNHPWAB1);
 (EXISTS_TAC `2`);
 (ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
 (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC 0)) = 2 + 1`]);
 (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
 (UNDISCH_TAC `initial_sublist vl [a:real^3; b;c]`);
 (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
 (EXISTS_TAC `APPEND yl [d:real^3]`);
 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b; c] = APPEND vl yl`)]);
 (ASM_REWRITE_TAC[APPEND]);
 (ASM_MESON_TAC[]);
 (MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) < b /\ a < hl ul ==> a < b`));
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `[a;b:real^3;c] = truncate_simplex 2 ul`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
 (REWRITE_WITH `[a;b;c;d:real^3] = truncate_simplex 3 ul`);
 (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);

 (NEW_GOAL `!i j.  i < j /\ j <= 3
                     ==> hl (truncate_simplex i (ul:(real^3)list)) 
                       < hl (truncate_simplex j ul)`);
 (MATCH_MP_TAC XNHPWAB4);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ARITH_TAC);
 (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_2])]);;

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


let OMEGA_LIST_3_EXPLICIT = 
prove_by_refinement (
 `!a:real^3 b c d V ul.
     saturated V /\
     packing V /\
     ul IN barV V 3 /\
     hl ul < sqrt (&2) /\
     ul = [a; b; c; d]
     ==> omega_list_n V ul 3 = circumcenter {a, b , c, d}`,

[ (REPEAT STRIP_TAC);
 (REWRITE_WITH `{a,b, c,d} = set_of_list [a;(b:real^3);c;d]`);
 (MESON_TAC[set_of_list]);
 (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3;c;d]) = omega_list V [a;b;c;d]`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (MATCH_MP_TAC XNHPWAB1);
 (EXISTS_TAC `3`);
 (ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[OMEGA_LIST]);
 (REWRITE_WITH `LENGTH [a:real^3; b; c; d] - 1 = 3`);
 (REWRITE_TAC[LENGTH]);
 (ARITH_TAC);
 (ASM_REWRITE_TAC[])]);;

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

let BARV_3_EXPLICIT = 
prove_by_refinement (
 `!V vl. barV V 3 vl ==> ? u0 u1 u2 u3. vl = [u0;u1;u2;u3]`,

[(REPEAT GEN_TAC);
 (REWRITE_TAC[BARV]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 3`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (EXISTS_TAC `x0:real^3`);

 (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 2`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (EXISTS_TAC `x1:real^3`);

 (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 1`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (EXISTS_TAC `x2:real^3`);

 (NEW_GOAL `?x3 tl. (zl:(real^3)list) = CONS x3 tl /\ LENGTH tl = 0`);
 (REWRITE_TAC[GSYM LENGTH_EQ_CONS]);
 (ASM_ARITH_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (EXISTS_TAC `x3:real^3`);

 (NEW_GOAL `(tl:(real^3)list) = []`);
 (ASM_MESON_TAC[LENGTH_EQ_NIL]);
 (ASM_REWRITE_TAC[])]);;

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

let BARV_K_EXPLICIT = 
prove_by_refinement (
 `!V a b c d.
     barV V 3 [a; b; c; d]
     ==> barV V 2 [a; b; c] /\ barV V 1 [a; b] /\ barV V 0 [a]`,

[ (REPEAT GEN_TAC);
 (REWRITE_TAC[BARV]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC 0)) = 2 + 1`]);
 (MATCH_MP_TAC (ASSUME
  `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
           ==> voronoi_nondg V vl`));
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `initial_sublist vl [a; b; c:real^3]` THEN  
   REWRITE_TAC[INITIAL_SUBLIST]);
 (STRIP_TAC);
 (EXISTS_TAC `APPEND yl [d:real^3]`);
 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a; b; c:real^3] = APPEND vl yl`)]);
 (REWRITE_TAC[APPEND]);
 (REWRITE_TAC[LENGTH]);
 (ARITH_TAC);

 (MATCH_MP_TAC (ASSUME 
  `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
           ==> voronoi_nondg V vl`));
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `initial_sublist vl [a; b:real^3]` THEN  
   REWRITE_TAC[INITIAL_SUBLIST]);
 (STRIP_TAC);
 (EXISTS_TAC `APPEND yl [c;d:real^3]`);
 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a; b:real^3] = APPEND vl yl`)]);
 (REWRITE_TAC[APPEND]);
 (REWRITE_TAC[LENGTH]);
 (ARITH_TAC);

 (MATCH_MP_TAC (ASSUME 
  `!vl. initial_sublist vl [a:real^3; b; c; d] /\ 0 < LENGTH vl
           ==> voronoi_nondg V vl`));
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `initial_sublist vl [a:real^3]` THEN  
   REWRITE_TAC[INITIAL_SUBLIST]);
 (STRIP_TAC);
 (EXISTS_TAC `APPEND yl [b;c;d:real^3]`);
 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3] = APPEND vl yl`)]);
 (REWRITE_TAC[APPEND])]);;

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

let AFF_DIM_LE_LENGTH = 
prove_by_refinement (
 `!xl n. LENGTH xl = n ==> aff_dim (set_of_list (xl:(real^3)list)) < &n`,

[ (REPEAT GEN_TAC THEN DISCH_TAC);
 (ABBREV_TAC `s = set_of_list (xl:(real^3)list)`);
 (NEW_GOAL `?b. ~affine_dependent b /\ b SUBSET (s:real^3->bool) /\ 
                 affine hull b = affine hull s`);
 (MESON_TAC[AFFINE_BASIS_EXISTS]);
 (FIRST_X_ASSUM CHOOSE_TAC);
 (NEW_GOAL `aff_dim (s:real^3->bool) = aff_dim (b:real^3->bool)`);
 (REWRITE_WITH `aff_dim (s:real^3->bool) = aff_dim (affine hull s) /\
                 aff_dim (b:real^3->bool) = aff_dim (affine hull b)`);
 (MESON_TAC[AFF_DIM_AFFINE_HULL]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `aff_dim (b:real^3->bool) = &(CARD b) - &1`);
 (ASM_SIMP_TAC[AFF_DIM_AFFINE_INDEPENDENT]);
 (NEW_GOAL `int_of_num (CARD (b:real^3->bool)) 
            <= int_of_num (CARD (s:real^3->bool))`);
 (MATCH_MP_TAC (ARITH_RULE `a <= b ==> int_of_num a <= int_of_num b`));
 (MATCH_MP_TAC CARD_SUBSET);
 (ASM_REWRITE_TAC[]);
 (EXPAND_TAC "s");
 (REWRITE_TAC[FINITE_SET_OF_LIST]);

 (NEW_GOAL `int_of_num (CARD  (s:real^3->bool)) 
          <= int_of_num (LENGTH (xl:(real^3)list))`);
 (MATCH_MP_TAC (ARITH_RULE `a <= b ==> int_of_num a <= int_of_num b`));
 (EXPAND_TAC "s");
 (REWRITE_TAC[CARD_SET_OF_LIST_LE]);
 (ASM_ARITH_TAC) ]);;

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

let CONVEX_HULL_SUBSET = 
prove_by_refinement (
 `!S (S':real^N->bool). 
     S SUBSET S' ==> (convex hull S) SUBSET (convex hull S')` ,

[(REWRITE_TAC[SUBSET;convex;hull;IN;IN_ELIM_THM;INTERS]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `!x. S (x:real^N) ==> u x`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC);
 (DISCH_THEN (LABEL_TAC "asm1"));
 (USE_THEN "asm1" (MP_TAC o SPEC `u:real^N->bool`) THEN DEL_TAC);
 (DISCH_TAC THEN DISCH_TAC THEN SWITCH_TAC THEN DISCH_TAC THEN SWITCH_TAC);
 (FIRST_X_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[])]);;

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

let BALL_CONVEX_HULL_LEMMA = 
prove_by_refinement (
 `!S s r x:real^N.
         (!x. S x ==> dist (s,x) < r)
         ==> (convex hull S) x
         ==> dist (s,x) < r`,

[ (REPEAT STRIP_TAC);
 (NEW_GOAL `S SUBSET ball (s:real^N, r)`);
 (ASM_REWRITE_TAC[ball;SUBSET;IN;IN_ELIM_THM]);
 (NEW_GOAL `(convex hull S) SUBSET ball (s:real^N, r)`);
 (NEW_GOAL `convex hull ball(s:real^N,r) = ball (s,r)`);
 (REWRITE_TAC[CONVEX_HULL_EQ;CONVEX_BALL]);
 (ASM_MESON_TAC[CONVEX_HULL_SUBSET]);
 (REWRITE_WITH `!a x r. dist (a,x:real^N) < r <=> x IN ball(a,r)`);
 (REWRITE_TAC[IN;IN_ELIM_THM;ball] );
 (ASM_SET_TAC[])]);;

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

let CONVEX_RCONE_GT = 
prove_by_refinement (
 `!a:real^N b r. &0 <= r ==> convex (rcone_gt a b r)`,

[ (REPEAT STRIP_TAC);
 (REWRITE_TAC[rcone_gt;convex;rconesgn;IN;IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
 (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID; 
  VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
 (REWRITE_TAC[DOT_LADD;DOT_LMUL]);
 (ASM_CASES_TAC `&0 < u`);

  (* 2 Subgoals *)

 (NEW_GOAL 
  `u * ((x:real^N - a) dot (b - a)) + v * ((y - a) dot (b - a)) > 
   u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);
   (* Subgoal 1.1 *)

 (NEW_GOAL
  `u * ((x:real^N - a) dot (b - a)) > u * dist (x,a) * dist (b,a) * r`);
 (MATCH_MP_TAC (REAL_ARITH `&0 < a - b ==> a > b`));
 (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`; 
               REAL_ARITH `a * b - a * c = a * (b - c)`]);
 (MATCH_MP_TAC REAL_LT_MUL);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL
  `v * ((y:real^N - a) dot (b - a)) >= v * dist (y,a) * dist (b,a) * r`);
 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));
 (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`; 
               REAL_ARITH `a * b - a * c = a * (b - c)`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REAL_ARITH_TAC);
 (ASM_REAL_ARITH_TAC);

 (NEW_GOAL 
`dist (u % x + v % y,a) * dist (b,a:real^N) * r <= 
 u * dist (x,a) * dist (b,a) * r + v *  dist (y,a) * dist (b,a) * r`);
   (* Subgoal 1.2 *)

 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));
 (REWRITE_TAC[REAL_ARITH `(a * b * x + c * d * x) - e * x  = 
                            (a * b + c * d - e) * x`]);
 (MATCH_MP_TAC REAL_LE_MUL);
 STRIP_TAC;
 (REWRITE_TAC[dist]);
 (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
 (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID; 
   VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
 (REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
 (MATCH_MP_TAC (REAL_ARITH 
  `m <= norm (u % (x - a:real^N)) + norm (v % (y - a)) /\
   norm (u % (x - a)) = b /\   
   norm (v % (y - a)) = c ==> m <= b + c`));
 (REWRITE_TAC[NORM_TRIANGLE;NORM_MUL]);
 (REWRITE_WITH `abs u = u /\ abs v = v`);
 (ASM_SIMP_TAC[REAL_ABS_REFL]);

 (MATCH_MP_TAC REAL_LE_MUL);
 (ASM_REWRITE_TAC[DIST_POS_LE]);
 (ASM_REAL_ARITH_TAC);

(* Subgoal 2 *)

 (NEW_GOAL `u = &0`);
 (ASM_REAL_ARITH_TAC);
 (NEW_GOAL `v = &1`);
 (ASM_REAL_ARITH_TAC);
 (ASM_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_LID;REAL_MUL_LID]);
 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID;VECTOR_MUL_LID])]);;
 



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

let RCONE_GT_CONVEX_HULL_LEMMA = 
prove_by_refinement (
 `!a:real^N b r s. 
 (s SUBSET rcone_gt a b r) /\ &0 <= r ==> 
 (convex hull s SUBSET rcone_gt a b r)`,

[ (REPEAT STRIP_TAC);
 (ASM_MESON_TAC[CONVEX_HULL_SUBSET;CONVEX_RCONE_GT; CONVEX_HULL_EQ])]);;


end;;