(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Authour : VU KHAC KY *) (* Book lemma: QZKSYKG *) (* Chaper : Packing *) (* *) (* ========================================================================= *) module Qzksykg = 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 Ynhyjit;; let CONVEX_HULL_4_IMP_3_1 = prove_by_refinement ( `!a:real^3 b c d x. x IN convex hull {a,b,c,d} ==> (?x1 t1 t2. x1 IN convex hull {a,b,c} /\ &0 <= t1 /\ &0 <= t2 /\ t1 + t2 = &1 /\ x = t1 % x1 + t2 % d)`, [(REWRITE_TAC[CONVEX_HULL_4; CONVEX_HULL_3;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ASM_CASES_TAC `z < &1`); (EXISTS_TAC `(u/ (u + v + w)) % a + (v/ (u+v+w)) % b + (w/(u+v+w)) % (c:real^3)`); (EXISTS_TAC `(u + v + w):real` THEN EXISTS_TAC `z:real`); (REPEAT STRIP_TAC); (EXISTS_TAC `u/(u+v+w)`); (EXISTS_TAC `v/(u+v+w)`); (EXISTS_TAC `w/(u+v+w)`); (REPEAT STRIP_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[REAL_ARITH `u / (u + v + w) + v / (u + v + w) + w / (u + v + w)= (u + v + w) / (u + v + w)`]); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REAL_ARITH_TAC); (REFL_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[VECTOR_ARITH `s % (s1 /s % a + s2 / s % b + s3/ s % c) = (s * s1 / s) % a + (s * s2 / s) % b + (s * s3 / s) % c`]); (REWRITE_TAC[REAL_ARITH `s * s1 / s = s1 * (s / s)`]); (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[REAL_MUL_RID] THEN VECTOR_ARITH_TAC); (NEW_GOAL `z = &1 /\ u = &0 /\ v = &0 /\ w = &0`); (ASM_REAL_ARITH_TAC); (EXISTS_TAC `a:real^3`); (EXISTS_TAC `&0` THEN EXISTS_TAC `&1`); (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &0 + &1 = &1`]); (STRIP_TAC); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &0 /\ &0 <= &1 /\ &1 + &0 + &0 = &1`]); (VECTOR_ARITH_TAC); (VECTOR_ARITH_TAC)]);; let BARV_2_EXPLICIT = prove_by_refinement ( `!V vl. barV V 2 vl ==> ?u0 u1 u2. vl = [u0;u1;u2]`, [(REWRITE_TAC[BARV] THEN REPEAT STRIP_TAC); (NEW_GOAL `?x0 xl. (vl:(real^3)list) = CONS x0 xl /\ LENGTH xl = 2`); (REWRITE_TAC[GSYM LENGTH_EQ_CONS]); (ASM_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `x0:real^3`); (NEW_GOAL `?x1 yl. (xl:(real^3)list) = CONS x1 yl /\ LENGTH yl = 1`); (REWRITE_TAC[GSYM LENGTH_EQ_CONS]); (ASM_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `x1:real^3`); (NEW_GOAL `?x2 zl. (yl:(real^3)list) = CONS x2 zl /\ LENGTH zl = 0`); (REWRITE_TAC[GSYM LENGTH_EQ_CONS]); (ASM_ARITH_TAC); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `x2:real^3`); (NEW_GOAL `(zl:(real^3)list) = []`); (ASM_MESON_TAC[LENGTH_EQ_NIL]); (ASM_REWRITE_TAC[])]);; let ROGERS_EXPLICIT_2 = prove_by_refinement ( `!V ul. saturated V /\ packing V /\ barV V 2 ul ==> rogers V ul = convex hull {HD ul, omega_list_n V ul 1, omega_list_n V ul 2}`, [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]); (NEW_GOAL `?u0 u1 u2. (ul:(real^3)list) = [u0:real^3;u1;u2]`); (MATCH_MP_TAC BARV_2_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2}`); (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) = 3`]); (SET_TAC[ARITH_RULE `0 < 3 /\ 1 < 3 /\ 2 < 3 /\ (!j. j < 3 ==> (j=0\/j=1\/j=2))`]); (REWRITE_TAC[IMAGE]); (AP_TERM_TAC); (REWRITE_TAC[SET_RULE `!x. x IN {0,1,2} <=> (x = 0 \/x = 1 \/x = 2)`]); (REWRITE_WITH `!y. (?x. (x = 0 \/ x = 1 \/ x = 2) /\ y = omega_list_n V ul x) <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/ (y = omega_list_n V ul 2)`); (SET_TAC[BETA_THM]); (REWRITE_WITH `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/ y = omega_list_n V ul 2} = {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`); (SET_TAC[]); (REWRITE_WITH `omega_list_n V ul 0 = HD ul`); (REWRITE_TAC[OMEGA_LIST_N])]);; let TWO_REARRANGEMENT_LEMMA = prove_by_refinement ( `!V ul p u0 u1 u2 u3. packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] ==> (?p. p permutes 0..1 /\ [u1;u0;u2;u3] = left_action_list p ul)`, [(REPEAT STRIP_TAC); (ABBREV_TAC `p = (\i. if i = 0 then 1 else if i = 1 then 0 else i)`); (EXISTS_TAC `p:num->num`); (NEW_GOAL `p 0 = 1`); (EXPAND_TAC "p"); (COND_CASES_TAC); (REFL_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `p 1 = 0`); (EXPAND_TAC "p"); (COND_CASES_TAC); (COND_CASES_TAC); (REFL_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `!i. 1 < i ==> p i = i`); (EXPAND_TAC "p"); (REPEAT STRIP_TAC); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (REFL_TAC); (NEW_GOAL `inverse p 0 = 1`); (REWRITE_TAC[inverse]); (MATCH_MP_TAC SELECT_UNIQUE); (GEN_TAC THEN EQ_TAC); (REWRITE_TAC[BETA_THM]); (ASM_CASES_TAC `y = 0`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (ASM_CASES_TAC `1 < y`); (ASM_SIMP_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]); (NEW_GOAL `inverse p 1 = 0`); (REWRITE_TAC[inverse]); (MATCH_MP_TAC SELECT_UNIQUE); (GEN_TAC THEN EQ_TAC); (REWRITE_TAC[BETA_THM]); (ASM_CASES_TAC `y = 1`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (ASM_CASES_TAC `1 < y`); (ASM_SIMP_TAC[]); (STRIP_TAC); (ASM_ARITH_TAC); (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]); (NEW_GOAL `!i. 1 < i ==> inverse p i = i`); (REPEAT STRIP_TAC); (REWRITE_TAC[inverse]); (MATCH_MP_TAC SELECT_UNIQUE); (GEN_TAC THEN EQ_TAC); (REWRITE_TAC[BETA_THM]); (ASM_CASES_TAC `y = 0`); (ASM_SIMP_TAC[]); (STRIP_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `y = 1`); (ASM_SIMP_TAC[]); (STRIP_TAC); (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `1 < y`); (ASM_ARITH_TAC); (STRIP_TAC); (NEW_GOAL `(p:num->num) y = y`); (UNDISCH_TAC `1 < y` THEN ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (STRIP_TAC THEN ASM_REWRITE_TAC[BETA_THM]); (ASM_MESON_TAC[]); (STRIP_TAC); (MATCH_MP_TAC Hypermap.lemma_permutes_via_surjetive); (REWRITE_WITH `0..1 = {0,1}`); (REWRITE_TAC[GSYM NUMSEG_LE; ARITH_RULE `x <= 1 <=> x = 0 \/ x = 1`]); (SET_TAC[]); (REWRITE_TAC[Geomdetail.FINITE6; SET_RULE `a IN {x,y} <=> a = x \/ a = y`]); (ASM_MESON_TAC[]); (ASM_REWRITE_TAC[left_action_list;LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]); (ASM_REWRITE_TAC[TABLE_4]); (ASM_SIMP_TAC[TABLE_4; EL;HD;TL; ARITH_RULE `1 < 2 /\ 1 < 3`]); (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`])]);; let SET_SUBSET_AFFINE_HULL = prove ( `!S:real^3->bool. S SUBSET affine hull S`, STRIP_TAC THEN MATCH_MP_TAC (SET_RULE `(?C. A SUBSET C /\ C SUBSET B) ==> A SUBSET B`) THEN EXISTS_TAC `convex hull S:real^3->bool` THEN REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL; SUBSET] THEN REWRITE_TAC[IN_SET_IMP_IN_CONVEX_HULL_SET]);; (* ========================================================================= *) let QZKSYKG1_concl = `!V ul vl k p. saturated V /\ packing V /\ barV V 3 ul /\ k IN {0,1,2,3,4} /\ ~ (mcell k V ul = {}) /\ p permutes 0..(k - 1) /\ vl = left_action_list p ul ==> barV V 3 vl`;; let QZKSYKG2_concl = `!V ul k. saturated V /\ packing V /\ barV V 3 ul /\ k IN {0,1,2,3,4} ==> (mcell k V ul SUBSET UNIONS{rogers V (left_action_list p ul) | p permutes 0..(k-1)})`;; (* ========================================================================= *) let QZKSYKG1 = prove_by_refinement (QZKSYKG1_concl, [(REPEAT STRIP_TAC); (ASM_CASES_TAC `k = 0 \/ k = 1`); (UNDISCH_TAC `p permutes 0..(k-1)`); (REWRITE_WITH `k - 1 = 0`); (ASM_ARITH_TAC); (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]); (STRIP_TAC); (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]); (NEW_GOAL `k IN {2,3,4}`); (ASM_SET_TAC[]); (* Cases k = 4 *) (ASM_CASES_TAC `k = 4`); (UNDISCH_TAC `~(mcell k V ul = {})`); (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (COND_CASES_TAC); (STRIP_TAC); (REWRITE_TAC[MESON[IN] `barV V 3 s <=> s IN barV V 3`]); (MATCH_MP_TAC Rogers.YIFVQDV_1); (ASM_REWRITE_TAC[IN]); (REWRITE_WITH `3 = k - 1`); (ASM_ARITH_TAC); (ASM_REWRITE_TAC[]); (MESON_TAC[]); (* Cases k = 3, k = 2 *) (REWRITE_WITH `barV V 3 vl /\ (!j. k - 1 <= j /\ j <= 3 ==> omega_list_n V vl j = omega_list_n V ul j)`); (MATCH_MP_TAC YNHYJIT); (EXISTS_TAC `p:num->num`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `~(mcell k V ul = {})`); (ASM_CASES_TAC `k = 3`); (SIMP_TAC [ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]); (COND_CASES_TAC); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`]); (ASM_REWRITE_TAC[]); (MESON_TAC[]); (NEW_GOAL `k = 2`); (ASM_SET_TAC[]); (SIMP_TAC [ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]); (COND_CASES_TAC); (LET_TAC); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]); (ASM_REWRITE_TAC[]); (MESON_TAC[])]);; (* ========================================================================= *) let QZKSYKG2 = prove_by_refinement ( QZKSYKG2_concl, [(REPEAT STRIP_TAC); (ASM_CASES_TAC `k = 0 \/ k = 1`); (REWRITE_WITH `k - 1 = 0`); (ASM_ARITH_TAC); (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]); (REWRITE_TAC[Packing3.SING_GSPEC_APP; UNIONS_1; Packing3.LEFT_ACTION_LIST_I]); (UP_ASM_TAC THEN STRIP_TAC); (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell0]); (SET_TAC[]); (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell1]); (COND_CASES_TAC); (SET_TAC[]); (SET_TAC[]); (* ======================================================================== *) (ASM_CASES_TAC `k = 4`); (REWRITE_WITH `k - 1 = 3`); (ASM_ARITH_TAC); (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`; mcell4]); (COND_CASES_TAC); (REWRITE_WITH `convex hull set_of_list ul = UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}`); (MATCH_MP_TAC Rogers.WQPRRDY); (ASM_REWRITE_TAC[IN]); (SET_TAC[]); (SET_TAC[]); (* ======================================================================== *) (ASM_CASES_TAC `k = 3`); (REWRITE_WITH `k - 1 = 2`); (ASM_ARITH_TAC); (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell3]); (COND_CASES_TAC); (ABBREV_TAC `m = mxi V ul`); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (REWRITE_TAC[SUBSET]); (GEN_TAC THEN DISCH_TAC); (NEW_GOAL `(?x1 t1 t2. x1 IN convex hull {u0, u1, u2:real^3} /\ &0 <= t1 /\ &0 <= t2 /\ t1 + t2 = &1 /\ x = t1 % x1 + t2 % m)`); (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_3_1]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[ASSUME `x:real^3 = t1 % x1 + t2 % m`]); (UNDISCH_TAC `x1 IN convex hull {u0, u1, u2:real^3}`); (REWRITE_WITH `convex hull {u0,u1,u2:real^3} = UNIONS {rogers V (left_action_list p (truncate_simplex 2 ul)) | p permutes 0..2}`); (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list (truncate_simplex 2 ul)`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (MATCH_MP_TAC Rogers.WQPRRDY); (ASM_REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (REWRITE_TAC[IN_UNIONS]); (REPEAT STRIP_TAC); (NEW_GOAL `?p:num->num. p permutes 0..2 /\ t = rogers V (left_action_list p (truncate_simplex 2 ul))`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ABBREV_TAC `zl:(real^3)list = left_action_list p (truncate_simplex 2 ul)`); (EXISTS_TAC `rogers V (left_action_list p ul)`); (STRIP_TAC); (ASM_SET_TAC[]); (ABBREV_TAC `vl:(real^3)list = left_action_list p ul`); (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}`); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]); (REWRITE_WITH `vl IN barV V 3 /\ omega_list_n V vl 2 = omega_list_n V ul 2 /\ omega_list_n V vl 3 = omega_list_n V ul 3 /\ mxi V vl = mxi V ul`); (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES); (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `zl = truncate_simplex 2 (vl:(real^3)list)`); (EXPAND_TAC "zl" THEN EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) = 3`; TABLE_4; ARITH_RULE `SUC 3 = 4`; ASSUME `ul = [u0;u1;u2;u3:real^3]`; left_action_list]); (REWRITE_WITH `EL (inverse p 0) [u0; u1; u2:real^3] = EL (inverse p 0) [u0; u1; u2; u3] /\ EL (inverse p 1) [u0; u1; u2:real^3] = EL (inverse p 1) [u0; u1; u2; u3] /\ EL (inverse p 2) [u0; u1; u2:real^3] = EL (inverse p 2) [u0; u1; u2; u3]`); (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 [u0; u1; u2; u3]`); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (NEW_GOAL `!i. i IN 0..2 ==> inverse p i IN 0..2`); (REPEAT STRIP_TAC); (ABBREV_TAC `y = inverse (p:num->num) i`); (ASM_CASES_TAC `y IN 0..2`); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (MP_TAC (ASSUME `p permutes 0..2`) THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]); (STRIP_TAC); (NEW_GOAL `(p:num->num) y = y`); (ASM_SIMP_TAC[]); (UP_ASM_TAC THEN EXPAND_TAC "y"); (REWRITE_WITH `(p:num->num) (inverse p i) = i`); (MESON_TAC[PERMUTES_INVERSES; ASSUME `p permutes 0..2`]); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REPEAT STRIP_TAC); (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX); (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]); (NEW_GOAL `inverse p 0 IN 0..2`); (FIRST_ASSUM MATCH_MP_TAC); (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]); (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX); (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]); (NEW_GOAL `inverse p 1 IN 0..2`); (FIRST_ASSUM MATCH_MP_TAC); (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]); (MATCH_MP_TAC Packing3.EL_TRUNCATE_SIMPLEX); (REWRITE_TAC[LENGTH; ARITH_RULE `2 + 1 <= SUC(SUC(SUC(SUC 0)))`]); (NEW_GOAL `inverse p 2 IN 0..2`); (FIRST_ASSUM MATCH_MP_TAC); (REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0]); (NEW_GOAL `rogers V zl = convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`); (MATCH_MP_TAC ROGERS_EXPLICIT_2); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN REWRITE_TAC[ARITH_RULE `2 <= 3`]); (REWRITE_TAC[MESON[IN] `barV V 3 vl <=> vl IN barV V 3`]); (REWRITE_WITH `vl IN barV V 3 /\ omega_list_n V vl 2 = omega_list_n V ul 2 /\ omega_list_n V vl 3 = omega_list_n V ul 3 /\ mxi V vl = mxi V ul`); (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES); (EXISTS_TAC `p:num->num` THEN ASM_REWRITE_TAC[]); (* ------------------------------ *) (NEW_GOAL `x1 IN convex hull {HD zl, omega_list_n V zl 1, omega_list_n V zl 2}`); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_3;IN;IN_ELIM_THM]); (STRIP_TAC); (ABBREV_TAC `q1 = omega_list_n V zl 1`); (ABBREV_TAC `q2 = omega_list_n V zl 2`); (ABBREV_TAC `s3 = omega_list_n V ul 3`); (ABBREV_TAC `q0 = HD (zl:(real^3)list)`); (NEW_GOAL `vl IN barV V 3 /\ omega_list_n V vl 2 = omega_list_n V ul 2 /\ omega_list_n V vl 3 = omega_list_n V ul 3 /\ mxi V vl = mxi V ul`); (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES); (EXISTS_TAC `p:num->num`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN] 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`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (NEW_GOAL `HD vl = q0:real^3`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (EXPAND_TAC "q0" THEN REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (NEW_GOAL `omega_list_n V vl 1 = q1`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (EXPAND_TAC "q1" THEN REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]); (REWRITE_TAC[ARITH_RULE `2 = 1 + 1`]); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (NEW_GOAL `omega_list_n V vl 2 = q2`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (EXPAND_TAC "q2" THEN REWRITE_TAC[ASSUME `zl:(real^3)list = truncate_simplex 2 vl`]); (REWRITE_WITH `truncate_simplex 2 (vl:(real^3)list) = truncate_simplex (2 + 0) vl`); (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (UNDISCH_TAC `omega_list_n V vl 2 = omega_list_n V ul 2` THEN ASM_REWRITE_TAC[]); (DISCH_TAC); (NEW_GOAL `between m (q2, s3:real^3)`); (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2; CONVEX_HULL_4]); (REPEAT STRIP_TAC); (EXISTS_TAC `t1 * u` THEN EXISTS_TAC `t1 * v`); (EXISTS_TAC `t1 * w + t2 * u'` THEN EXISTS_TAC `t2 * v'`); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]); (STRIP_TAC); (REWRITE_WITH `t1 * u + t1 * v + (t1 * w + t2 * u') + t2 * v' = t1 * (u + v + w) + t2 * (u' + v')`); (REAL_ARITH_TAC); (ASM_REWRITE_TAC[REAL_MUL_RID]); (VECTOR_ARITH_TAC); (SET_TAC[]); (* ========================================================================= *) (NEW_GOAL `k = 2`); (ASM_SET_TAC[]); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT THEN EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]); (COND_CASES_TAC); (LET_TAC); (ABBREV_TAC `m = mxi V ul`); (ABBREV_TAC `s2 = omega_list_n V ul 2`); (ABBREV_TAC `s3 = omega_list_n V ul 3`); (ASM_REWRITE_TAC[HD;TL; ARITH_RULE `2 - 1 = 1`]); (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`)); (EXISTS_TAC `convex hull {u0, u1, s2, s3:real^3}`); (REPEAT STRIP_TAC); (* Two subgoals *) (* ------------------------------------------------------ *) (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ A SUBSET C) ==> A SUBSET B`)); (EXISTS_TAC `rogers V ul UNION rogers V [u1;u0;u2;u3:real^3]`); (STRIP_TAC); (REWRITE_TAC[SUBSET; IN_UNIONS; IN_UNION]); (REPEAT STRIP_TAC); (REWRITE_TAC[IN;IN_ELIM_THM]); (EXISTS_TAC `rogers V ul`); (STRIP_TAC); (EXISTS_TAC `I:num->num`); (ASM_REWRITE_TAC[PERMUTES_I; Packing3.LEFT_ACTION_LIST_I]); (UP_ASM_TAC THEN REWRITE_TAC[IN]); (REWRITE_TAC[IN;IN_ELIM_THM]); (EXISTS_TAC `rogers V [u1;u0;u2;u3]`); (STRIP_TAC); (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`); (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (EXISTS_TAC `p:num->num`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN]); (NEW_GOAL `?p. p permutes 0..1 /\ [u1;u0;u2;u3:real^3] = left_action_list p ul`); (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ABBREV_TAC `vl = [u1;u0;u2;u3:real^3]`); (NEW_GOAL `barV V 3 vl /\ (!j. 1 <= j /\ j <= 3 ==> omega_list_n V vl j = omega_list_n V ul j)`); (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]); (MATCH_MP_TAC YNHYJIT); (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]); (ASM_REWRITE_TAC[SET_RULE `2 IN {2,3,4}`]); (UP_ASM_TAC THEN STRIP_TAC); (ABBREV_TAC `s1 = omega_list_n V ul 1`); (NEW_GOAL `rogers V ul = convex hull {HD ul, s1, s2, s3}`); (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3"); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (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}`); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (NEW_GOAL `omega_list_n V vl 1 = s1`); (EXPAND_TAC "s1" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (NEW_GOAL `omega_list_n V vl 2 = s2`); (EXPAND_TAC "s2" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (NEW_GOAL `omega_list_n V vl 3 = s3`); (EXPAND_TAC "s3" THEN FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (ASM_REWRITE_TAC[HD]); (REWRITE_TAC[GSYM (ASSUME `vl = left_action_list p (ul:(real^3)list)`); GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (NEW_GOAL `s1 = circumcenter {u1, u0:real^3}`); (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `hl [u1;u0:real^3] = hl (truncate_simplex 1 (ul:(real^3)list))`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL]); (REWRITE_TAC[set_of_list; SET_RULE `{a,b} = {b,a}`]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[SUBSET; CONVEX_HULL_4; IN; IN_ELIM_THM; IN_UNION]); (REPEAT STRIP_TAC); (ASM_CASES_TAC `u <= v:real`); (DISJ2_TAC); (EXISTS_TAC `v - u:real` THEN EXISTS_TAC `&2 * u`); (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`); (ASM_SIMP_TAC[REAL_ARITH `v - u + &2 * u + w + z = u + v + w + z`; REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]); (VECTOR_ARITH_TAC); (NEW_GOAL `v <= u:real`); (ASM_REAL_ARITH_TAC); (DISJ1_TAC); (EXISTS_TAC `u - v:real` THEN EXISTS_TAC `&2 * v`); (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`); (ASM_SIMP_TAC[REAL_ARITH `u - v + &2 * v + w + z = u + v + w + z`; REAL_LE_MUL; REAL_ARITH `&0 <= &2`; REAL_ARITH `&0 <= a - b <=> b <= a`]); (VECTOR_ARITH_TAC); (* ------------------------------------------------------ *) (REWRITE_TAC[SUBSET; IN_INTER]); (REPEAT STRIP_TAC); (ABBREV_TAC `s1 = omega_list_n V ul 1`); (NEW_GOAL `s1 = circumcenter {u0, u1:real^3}`); (EXPAND_TAC "s1" THEN MATCH_MP_TAC Marchal_cells_2_new.OMEGA_LIST_1_EXPLICIT_NEW); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[IN]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `hl [u0;u1:real^3] = hl (truncate_simplex 1 (ul:(real^3)list))`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]); (ASM_REWRITE_TAC[]); (ABBREV_TAC `vl:(real^3)list = truncate_simplex 1 ul`); (NEW_GOAL `s1:real^3 IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN EXPAND_TAC "s1"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s2:real^3 IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN EXPAND_TAC "s2"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s3:real^3 IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN EXPAND_TAC "s3"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `m IN voronoi_list V vl`); (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`); (REWRITE_WITH `m = s2:real^3`); (EXPAND_TAC "m" THEN REWRITE_TAC[mxi]); (COND_CASES_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s)`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC); (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {s2, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V vl <=> convex hull {s2, s3} SUBSET (convex hull (voronoi_list V vl))`); (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (NEW_GOAL `~(u0 = u1:real^3)`); (STRIP_TAC); (NEW_GOAL `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`]); (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`); (REWRITE_TAC[Geomdetail.CARD3]); (ASM_ARITH_TAC); (UNDISCH_TAC `x IN aff_ge {u0, u1} {m, s3:real^3}`); (REWRITE_WITH `aff_ge {u0, u1} {m, s3:real^3} = {y | ?t1 t2 t3 t4. &0 <= t3 /\ &0 <= t4 /\ t1 + t2 + t3 + t4 = &1 /\ y = t1 % u0 + t2 % u1 + t3 % m + t4 % s3}`); (MATCH_MP_TAC AFF_GE_2_2); (NEW_GOAL `~(m IN {u0, u1:real^3})`); (STRIP_TAC); (ASM_CASES_TAC `m = u0:real^3`); (UNDISCH_TAC `m IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]); (STRIP_TAC); (NEW_GOAL `m:real^3 IN voronoi_closed V u1`); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`); (FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`); (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]); (STRIP_TAC); (NEW_GOAL `dist (u0, u1:real^3) = &0`); (NEW_GOAL `&0 <= dist (u0, u1:real^3)`); (REWRITE_TAC[DIST_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `m = u1:real^3`); (UNDISCH_TAC `m IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]); (STRIP_TAC); (NEW_GOAL `m:real^3 IN voronoi_closed V u0`); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`); (FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`); (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]); (STRIP_TAC); (NEW_GOAL `dist (u1, u0:real^3) = &0`); (NEW_GOAL `&0 <= dist (u1, u0:real^3)`); (REWRITE_TAC[DIST_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]); (ASM_MESON_TAC[]); (ASM_SET_TAC[]); (NEW_GOAL `~(s3 IN {u0, u1:real^3})`); (STRIP_TAC); (ASM_CASES_TAC `s3 = u0:real^3`); (UNDISCH_TAC `s3 IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]); (STRIP_TAC); (NEW_GOAL `s3:real^3 IN voronoi_closed V u1`); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`); (FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`); (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]); (STRIP_TAC); (NEW_GOAL `dist (u0, u1:real^3) = &0`); (NEW_GOAL `&0 <= dist (u0, u1:real^3)`); (REWRITE_TAC[DIST_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `s3 = u1:real^3`); (UNDISCH_TAC `s3 IN voronoi_list V vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;set_of_list; ASSUME `ul = [u0;u1;u2;u3:real^3]`; VORONOI_LIST; VORONOI_SET]); (STRIP_TAC); (NEW_GOAL `s3:real^3 IN voronoi_closed V u0`); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `dist (u1, u0:real^3) <= dist (u1, u1)`); (FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `{u0, u1, u2, u3:real^3} SUBSET V`); (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[MESON[IN] `V u0 <=> u0 IN V`]); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]); (STRIP_TAC); (NEW_GOAL `dist (u1, u0:real^3) = &0`); (NEW_GOAL `&0 <= dist (u1, u0:real^3)`); (REWRITE_TAC[DIST_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]); (ASM_MESON_TAC[]); (ASM_SET_TAC[]); (REWRITE_TAC[DISJOINT]); (ASM_SET_TAC[]); (* ======================================================================== *) (* OK here *) (REWRITE_TAC[IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `&0 <= t1 /\ &0 <= t2`); (ASM_CASES_TAC `&0 < t3 + t4`); (ABBREV_TAC `t5 = t3 + t4:real`); (ABBREV_TAC `z = t3 / t5 % m + t4 / t5 % (s3:real^3)`); (NEW_GOAL `between z (m, s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (EXISTS_TAC `t3 / t5` THEN EXISTS_TAC `t4 / t5`); (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 < a ==> &0 <= a`]); (ASM_REWRITE_TAC[REAL_ARITH `a/b+c/b = (a+c)/b`]); (MATCH_MP_TAC REAL_DIV_REFL THEN ASM_REAL_ARITH_TAC); (NEW_GOAL `z IN voronoi_list V vl`); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {m, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V vl <=> convex hull {m, s3} SUBSET (convex hull (voronoi_list V vl))`); (REWRITE_WITH `convex hull (voronoi_list V vl) = voronoi_list V vl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (* ------------------------------------------------------------------------ *) (ASM_CASES_TAC `t1 < &0`); (NEW_GOAL `F`); (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`); (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]); (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]); (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5"); (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]); (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]); (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`; REAL_MUL_RID]); (REWRITE_TAC[dist]); (REWRITE_WITH `x - u1:real^3 = t1 % (u0 - u1) + t5 % (z - u1)`); (REWRITE_WITH `x - u1:real^3 = x - (t1 + t2 + t5) % u1`); (REWRITE_WITH `t1 + t2 + t5 = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]); (VECTOR_ARITH_TAC); (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]); (NEW_GOAL `(z - u1) dot (u0 - u1:real^3) <= norm (z - u1:real^3) * norm (u0 - u1) * a`); (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`); (NEW_GOAL `m = s2:real^3`); (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`); (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2; midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]); (VECTOR_ARITH_TAC); (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (NEW_GOAL `norm (s2 - u1) <= norm (z - u1:real^3)`); (REWRITE_WITH `norm (s2 - u1) <= norm (z - u1:real^3) <=> norm (s2 - u1) pow 2 <= norm (z - u1:real^3) pow 2`); (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]); (REWRITE_WITH `s2 - u1 = (s2 - s1) + (s1 - u1:real^3) /\ z - u1 = (z - s1) + (s1 - u1:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_WITH `norm (s2 - s1 + s1 - u1) pow 2 = norm (s2 - s1) pow 2 + norm (s1 - u1:real^3) pow 2`); (NEW_GOAL `(s2 - s1) dot (s1 - u1:real^3) = &0`); (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`); (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_WITH `norm (z - s1 + s1 - u1:real^3) pow 2 = norm (z - s1) pow 2 + norm (s1 - u1) pow 2`); (NEW_GOAL `(z - s1) dot (s1 - u1:real^3) = &0`); (REWRITE_WITH `s1 - u1 = u0 - s1:real^3`); (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]); (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]); (REWRITE_TAC[GSYM dist; DIST_SYM]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `!a b c d:real^3. dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`); (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]); (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]); (MATCH_MP_TAC CLOSEST_POINT_LE); (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `s2:real^3 IN voronoi_list V zl`); (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s3:real^3 IN voronoi_list V zl`); (EXPAND_TAC "zl" THEN EXPAND_TAC "s3"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {s2, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_MESON_TAC[]); (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 * norm (u0 - s1) pow 2`); (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) + (s1 - u1) dot (u0 - u1:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]); (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`); (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC); (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <= norm (s2 - u1) * norm (u0 - u1) * a`); (NEW_GOAL `norm (s2 - u1:real^3) >= sqrt (&2)`); (NEW_GOAL `norm (s2 - u1:real^3) >= hl (truncate_simplex 2 (ul:(real^3)list))`); (REWRITE_TAC[GSYM dist]); (NEW_GOAL `?p. p permutes 0..1 /\ [u1; u0; u2; u3:real^3] = left_action_list p ul`); (MATCH_MP_TAC TWO_REARRANGEMENT_LEMMA); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (ABBREV_TAC `ul' = [u1;u0;u2;u3:real^3]`); (NEW_GOAL `barV V 3 ul' /\ (!j. 1 <= j /\ j <= 3 ==> omega_list_n V ul' j = omega_list_n V ul j)`); (ONCE_REWRITE_TAC[ARITH_RULE `1 = 2 - 1`]); (MATCH_MP_TAC YNHYJIT); (EXISTS_TAC `p:num->num` THEN REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; SET_RULE `2 IN {2,3,4}`]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_WITH `s2 = omega_list_n V ul' 2 /\ u1 = HD ul'`); (STRIP_TAC); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] ); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); HD] ); (REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]); (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul'`); (REWRITE_WITH `hl (truncate_simplex 2 (ul:(real^3)list)) = hl (xl:(real^3)list)`); (EXPAND_TAC "xl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; GSYM (ASSUME `[u1;u0;u2;u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_TAC[HL; set_of_list; SET_RULE `{u0, u1, u2} = {u1,u0,u2}`]); (REWRITE_WITH `omega_list_n V ul' 2 = omega_list V xl`); (REWRITE_WITH `omega_list V xl = omega_list_n V xl 2`); (REWRITE_TAC[OMEGA_LIST]); (EXPAND_TAC "xl" THEN REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_TAC[LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`]); (EXPAND_TAC "xl"); (REWRITE_WITH `truncate_simplex 2 (ul':(real^3)list) = truncate_simplex (2 + 0) ul'`); (REWRITE_TAC[ARITH_RULE `2 + 0 = 2`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_N_LEMMA); (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]); (ARITH_TAC); (REWRITE_WITH `HD ul' = HD (xl:(real^3)list)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "xl"); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (REWRITE_TAC[GSYM (ASSUME `[u1; u0; u2; u3:real^3] = ul'`); LENGTH]); (ARITH_TAC); (MATCH_MP_TAC Rogers.WAUFCHE1); (EXISTS_TAC `2`); (REWRITE_TAC[IN] THEN EXPAND_TAC "xl"); (STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (ASM_REAL_ARITH_TAC); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `u0:real^3 = HD vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]); (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]); (REWRITE_WITH `abs (&2) = &2`); (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]); (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `&1 <= norm (s2 - u1) / sqrt (&2) <=> &1 * sqrt (&2) <= norm (s2 - u1:real^3)`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `norm (s2 - u1) * norm (u0 - u1:real^3) * a <= norm (z - u1) * norm (u0 - u1) * a`); (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> &0 <= (x * y) * (b - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV); (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (* ------------------------------------------------------------------------- *) (* OK here too *) (* ----------------------------------------------------- *) (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC); (NEW_GOAL `u0 - u1 = &2 % (u0 - s1:real^3)`); (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2; midpoint; VECTOR_ARITH `u0 - inv (&2) % (u0 + u1) = inv (&2) % (u0 - u1)`]); (VECTOR_ARITH_TAC); (NEW_GOAL `(z - s1) dot (u0 - s1:real^3) = &0`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (NEW_GOAL `between m (s2, z:real^3)`); (MATCH_MP_TAC BETWEEN_TRANS_2); (EXISTS_TAC `s3:real^3`); (STRIP_TAC); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `s2:real^3 IN voronoi_list V zl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "zl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s3:real^3 IN voronoi_list V zl`); (EXPAND_TAC "s3" THEN EXPAND_TAC "zl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `m:real^3 IN voronoi_list V zl`); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {s2, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (NEW_GOAL `z:real^3 IN voronoi_list V zl`); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {m, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (NEW_GOAL `norm (m - u1) <= norm (z - u1:real^3)`); (REWRITE_WITH `norm (m - u1) <= norm (z - u1:real^3) <=> norm (m - u1) pow 2 <= norm (z - u1:real^3) pow 2`); (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]); (REWRITE_WITH `m - u1 = (m - s2) + (s2 - u1:real^3) /\ z - u1 = (z - s2) + (s2 - u1:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_WITH `norm (m - s2 + s2 - u1) pow 2 = norm (m - s2) pow 2 + norm (s2 - u1:real^3) pow 2`); (NEW_GOAL `(m - s2) dot (s2 - u1:real^3) = &0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `(m - s2) dot (s2 - u1) = -- ((m - s2) dot (u1 - s2))`]); (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]); (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`); (REWRITE_WITH `s2:real^3 = omega_list V zl`); (EXPAND_TAC "s2"); (EXPAND_TAC "zl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`; Marchal_cells.OMEGA_LIST_TRUNCATE_2]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2`); (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V zl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (zl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_WITH `norm (z - s2 + s2 - u1) pow 2 = norm (z - s2) pow 2 + norm (s2 - u1:real^3) pow 2`); (NEW_GOAL `(z - s2) dot (s2 - u1:real^3) = &0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `(z - s2) dot (s2 - u1) = -- ((z - s2) dot (u1 - s2))`]); (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]); (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`); (REWRITE_WITH `s2:real^3 = omega_list V zl`); (EXPAND_TAC "s2"); (EXPAND_TAC "zl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`; Marchal_cells.OMEGA_LIST_TRUNCATE_2]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2`); (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V zl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (zl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]); (MP_TAC (ASSUME `between m (s2,z:real^3)`)); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC); (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]); (REWRITE_WITH `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]); (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`; REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[REAL_LE_POW_2]); (REWRITE_WITH `abs (v:real) = v`); (ASM_REWRITE_TAC[REAL_ABS_REFL]); (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]); (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Collect_geom.POW2_COND); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `norm (m - u1:real^3) = dist (u0, s:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM]); (ASM_REWRITE_TAC[GSYM dist]); (UNDISCH_TAC `m IN voronoi_list V zl`); (ASM_REWRITE_TAC[VORONOI_LIST; VORONOI_SET]); (EXPAND_TAC "zl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (STRIP_TAC); (NEW_GOAL `s:real^3 IN voronoi_closed V u0 /\ s IN voronoi_closed V u1`); (UP_ASM_TAC THEN SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`); (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`); (ASM_REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `dist (s,u0) <= dist (s,u1:real^3)`); (FIRST_ASSUM MATCH_MP_TAC); (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]); (ASM_SET_TAC[]); (NEW_GOAL `dist (s,u1) <= dist (s,u0:real^3)`); (FIRST_ASSUM MATCH_MP_TAC); (ONCE_REWRITE_TAC[MESON[IN] `V s <=> s IN V`]); (ASM_SET_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `norm (m - u1:real^3) = sqrt (&2)`); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `(z - u1) dot (u0 - u1:real^3) = &2 * norm (u0 - s1) pow 2`); (REWRITE_WITH `(z - u1) dot (u0 - u1) = (z - s1) dot (u0 - u1) + (s1 - u1) dot (u0 - u1:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; DOT_RMUL]); (REWRITE_WITH `(s1 - u1) = (u0 - s1:real^3)`); (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC); (NEW_GOAL `&2 * norm (u0 - s1:real^3) pow 2 <= norm (m - u1) * norm (u0 - u1) * a`); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `u0:real^3 = HD vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]); (REWRITE_TAC[ASSUME `u0 - u1 = &2 % (u0 - s1:real^3)`; NORM_MUL]); (REWRITE_WITH `abs (&2) = &2`); (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]); (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`)); (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]); (REAL_ARITH_TAC); (NEW_GOAL `norm (m - u1) * norm (u0 - u1:real^3) * a <= norm (z - u1) * norm (u0 - u1) * a`); (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> &0 <= (x * y) * (b - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV); (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 + t5 * ((z - u1) dot (u0 - u1)) <= t1 * norm (u0 - u1) pow 2 + t5 * (norm (z - u1) * norm (u0 - u1) * a)`); (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (NEW_GOAL `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a`); (REWRITE_TAC[REAL_ARITH `t1 * norm (u0 - u1) pow 2 + t5 * norm (z - u1:real^3) * norm (u0 - u1) * a < norm (t1 % (u0 - u1) + t5 % (z - u1)) * norm (u0 - u1) * a <=> &0 < (a * norm (t1 % (u0 - u1) + t5 % (z - u1)) - t1 * norm (u0 - u1) - t5 * a * norm (z - u1)) * norm (u0 - u1)`]); (MATCH_MP_TAC REAL_LT_MUL); (REPEAT STRIP_TAC); (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]); (NEW_GOAL `t1 * norm (u0 - u1) < a * t1 * norm (u0 - u1:real^3)`); (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b * (&1 - c)`]); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `); (MATCH_MP_TAC REAL_LT_LDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT); (REAL_ARITH_TAC); (ASM_REWRITE_TAC[REAL_MUL_LID]); (NEW_GOAL `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <= a * norm (t1 % (u0 - u1) + t5 % (z - u1:real^3))`); (REWRITE_TAC[REAL_ARITH `a * t1 * norm (u0 - u1) + t5 * a * norm (z - u1) <= a * norm (t1 % (u0 - u1) + t5 % (z - u1)) <=> &0 <= a * (norm (t1 % (u0 - u1) + t5 % (z - u1)) + (--t1 * norm (u0 - u1)) - t5 * norm (z - u1))`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u0:real^3)`); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `u0:real^3 = HD vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list; HD]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (REWRITE_TAC[DIST_POS_LE]); (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]); (ABBREV_TAC `k1 = t1 % (u0 - u1) + t5 % (z - u1:real^3)`); (REWRITE_WITH `t5 * norm (z - u1) = norm (t5 % (z - u1:real^3))`); (REWRITE_TAC[NORM_MUL]); (REWRITE_WITH `abs t5 = t5`); (REWRITE_TAC[REAL_ABS_REFL]); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `--t1 * norm (u0 - u1) = norm ((--t1) % (u0 - u1:real^3))`); (REWRITE_TAC[NORM_MUL]); (REWRITE_WITH `abs (--t1) = --t1`); (REWRITE_TAC[REAL_ABS_REFL]); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `t5 % (z - u1) = k1 + --t1 % (u0 - u1:real^3)`); (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC); (REWRITE_TAC[NORM_TRIANGLE]); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (* ----------------------------------------------------------------------- *) (* Half of the proof *) (ASM_CASES_TAC `t2 < &0`); (NEW_GOAL `F`); (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`); (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]); (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]); (NEW_GOAL `x = t1 % u0 + t2 % u1 + t5 % (z:real^3)`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "z" THEN EXPAND_TAC "t5"); (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]); (REWRITE_TAC[REAL_ARITH `a * b / a = b * (a / a)`]); (ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ARITH `&0 < y ==> ~(y = &0)`; REAL_MUL_RID]); (REWRITE_TAC[dist]); (REWRITE_WITH `x - u0:real^3 = t2 % (u1 - u0) + t5 % (z - u0)`); (REWRITE_WITH `x - u0:real^3 = x - (t1 + t2 + t5) % u0`); (REWRITE_WITH `t1 + t2 + t5 = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `x = t1 % u0 + t2 % u1 + t5 % z:real^3`]); (VECTOR_ARITH_TAC); (REWRITE_TAC[DOT_LADD; DOT_LMUL; GSYM NORM_POW_2]); (NEW_GOAL `(z - u0) dot (u1 - u0:real^3) <= norm (z - u0:real^3) * norm (u1 - u0) * a`); (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`); (NEW_GOAL `m = s2:real^3`); (EXPAND_TAC "m" THEN REWRITE_TAC[mxi] THEN COND_CASES_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`); (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2; midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]); (VECTOR_ARITH_TAC); (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (NEW_GOAL `norm (s2 - u0) <= norm (z - u0:real^3)`); (REWRITE_WITH `norm (s2 - u0) <= norm (z - u0:real^3) <=> norm (s2 - u0) pow 2 <= norm (z - u0:real^3) pow 2`); (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]); (REWRITE_WITH `s2 - u0 = (s2 - s1) + (s1 - u0:real^3) /\ z - u0 = (z - s1) + (s1 - u0:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_WITH `norm (s2 - s1 + s1 - u0) pow 2 = norm (s2 - s1) pow 2 + norm (s1 - u0:real^3) pow 2`); (NEW_GOAL `(s2 - s1) dot (s1 - u0:real^3) = &0`); (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`); (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_WITH `norm (z - s1 + s1 - u0:real^3) pow 2 = norm (z - s1) pow 2 + norm (s1 - u0) pow 2`); (NEW_GOAL `(z - s1) dot (s1 - u0:real^3) = &0`); (REWRITE_WITH `s1 - u0 = u1 - s1:real^3`); (ASM_REWRITE_TAC[CIRCUMCENTER_2; midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]); (REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)] THEN REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `2 = SUC 1`]); (REWRITE_TAC[ARITH_RULE `SUC 1 = 2`]); (REWRITE_TAC[GSYM dist; DIST_SYM]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `!a b c d:real^3. dist (a, b:real^3) pow 2 <= dist (c,d) pow 2 <=> dist (a,b) <= dist (c,d)`); (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]); (SIMP_TAC[Collect_geom.POW2_COND; DIST_POS_LE]); (MATCH_MP_TAC CLOSEST_POINT_LE); (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `s2:real^3 IN voronoi_list V zl`); (EXPAND_TAC "zl" THEN REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s3:real^3 IN voronoi_list V zl`); (EXPAND_TAC "zl" THEN EXPAND_TAC "s3"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {s2, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_MESON_TAC[]); (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 * norm (u1 - s1) pow 2`); (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]); (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`); (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC); (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <= norm (s2 - u0) * norm (u1 - u0) * a`); (NEW_GOAL `norm (s2 - u0:real^3) >= sqrt (&2)`); (NEW_GOAL `norm (s2 - u0:real^3) >= hl (truncate_simplex 2 (ul:(real^3)list))`); (REWRITE_TAC[GSYM dist]); (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]); (ABBREV_TAC `xl:(real^3)list = truncate_simplex 2 ul`); (REWRITE_WITH `s2 = omega_list V xl`); (ONCE_REWRITE_TAC[GSYM (ASSUME `omega_list_n V ul 2 = s2`)]); (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (EXPAND_TAC "xl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_WITH `u0:real^3 = HD xl`); (EXPAND_TAC "xl"); (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (MATCH_MP_TAC Rogers.WAUFCHE1); (EXISTS_TAC `2`); (REWRITE_TAC[IN] THEN EXPAND_TAC "xl"); (STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (ASM_REAL_ARITH_TAC); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!w:real^3. w IN set_of_list vl ==> dist (circumcenter (set_of_list vl),w) = hl vl`); (MATCH_MP_TAC Rogers.HL_PROPERTIES); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXPAND_TAC "vl"); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (SET_TAC[]); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]); (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]); (REWRITE_WITH `abs (&2) = &2`); (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]); (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `&1 <= norm (s2 - u0) / sqrt (&2) <=> &1 * sqrt (&2) <= norm (s2 - u0:real^3)`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `norm (s2 - u0) * norm (u1 - u0:real^3) * a <= norm (z - u0) * norm (u1 - u0) * a`); (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> &0 <= (x * y) * (b - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV); (REWRITE_WITH `hl vl = dist (circumcenter (set_of_list vl),(HD vl):real^3)`); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1` THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (* ------------------------------------------------------------------------- *) (* OK here too *) (* ----------------------------------------------------- *) (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN STRIP_TAC); (NEW_GOAL `u1 - u0 = &2 % (u1 - s1:real^3)`); (REWRITE_TAC[ASSUME `s1 = circumcenter {u0, u1:real^3}`; CIRCUMCENTER_2; midpoint; VECTOR_ARITH `u1 - inv (&2) % (u0 + u1) = inv (&2) % (u1 - u0)`]); (VECTOR_ARITH_TAC); (NEW_GOAL `(z - s1) dot (u1 - s1:real^3) = &0`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0,u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V vl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (vl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (NEW_GOAL `between m (s2, z:real^3)`); (MATCH_MP_TAC BETWEEN_TRANS_2); (EXISTS_TAC `s3:real^3`); (STRIP_TAC); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `s2:real^3 IN voronoi_list V zl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "zl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `s3:real^3 IN voronoi_list V zl`); (EXPAND_TAC "s3" THEN EXPAND_TAC "zl"); (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (NEW_GOAL `m:real^3 IN voronoi_list V zl`); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {s2, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {s2, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {s2, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (NEW_GOAL `z:real^3 IN voronoi_list V zl`); (MATCH_MP_TAC (SET_RULE `(?C. x IN C /\ C SUBSET B) ==> x IN B`)); (EXISTS_TAC `convex hull {m, s3:real^3}`); (STRIP_TAC); (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (REWRITE_WITH `convex hull {m, s3:real^3} SUBSET voronoi_list V zl <=> convex hull {m, s3} SUBSET (convex hull (voronoi_list V zl))`); (REWRITE_WITH `convex hull (voronoi_list V zl) = voronoi_list V zl`); (REWRITE_TAC[CONVEX_HULL_EQ]); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET); (ASM_SET_TAC[]); (NEW_GOAL `norm (m - u0) <= norm (z - u0:real^3)`); (REWRITE_WITH `norm (m - u0) <= norm (z - u0:real^3) <=> norm (m - u0) pow 2 <= norm (z - u0:real^3) pow 2`); (ASM_SIMP_TAC[Collect_geom.POW2_COND; NORM_POS_LE]); (REWRITE_WITH `m - u0 = (m - s2) + (s2 - u0:real^3) /\ z - u0 = (z - s2) + (s2 - u0:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_WITH `norm (m - s2 + s2 - u0) pow 2 = norm (m - s2) pow 2 + norm (s2 - u0:real^3) pow 2`); (NEW_GOAL `(m - s2) dot (s2 - u0:real^3) = &0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `(m - s2) dot (s2 - u0) = -- ((m - s2) dot (u0 - s2))`]); (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]); (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`); (REWRITE_WITH `s2:real^3 = omega_list V zl`); (EXPAND_TAC "s2"); (EXPAND_TAC "zl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`; Marchal_cells.OMEGA_LIST_TRUNCATE_2]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2`); (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V zl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (zl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_WITH `norm (z - s2 + s2 - u0) pow 2 = norm (z - s2) pow 2 + norm (s2 - u0:real^3) pow 2`); (NEW_GOAL `(z - s2) dot (s2 - u0:real^3) = &0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `(z - s2) dot (s2 - u0) = -- ((z - s2) dot (u0 - s2))`]); (REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]); (REWRITE_WITH `s2:real^3 = circumcenter (set_of_list zl)`); (REWRITE_WITH `s2:real^3 = omega_list V zl`); (EXPAND_TAC "s2"); (EXPAND_TAC "zl"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `(SUC (SUC (SUC 0)) - 1) = 2`; Marchal_cells.OMEGA_LIST_TRUNCATE_2]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2`); (REWRITE_TAC[IN; REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC Rogers.MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `voronoi_list V zl`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE `(?C. a IN C/\ C SUBSET B) ==> a IN B`)); (EXISTS_TAC `set_of_list (zl:(real^3)list)`); (ASM_REWRITE_TAC[SET_SUBSET_AFFINE_HULL]); (EXPAND_TAC "zl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (SET_TAC[]); (ASM_SIMP_TAC[Trigonometry2.PITHAGO_THEOREM]); (REWRITE_TAC[REAL_ARITH `a + b <= c + b <=> a <= c`]); (MP_TAC (ASSUME `between m (s2,z:real^3)`)); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN STRIP_TAC); (REWRITE_TAC[ASSUME `m = u % s2 + v % z:real^3`]); (REWRITE_WITH `(u % s2 + v % z) - s2 = (u % s2 + v % z) - (u + v) % s2:real^3`); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % z) - (u + v) % s2 = v % (z - s2)`]); (REWRITE_TAC[NORM_MUL; REAL_ARITH `(a*b) pow 2 = a pow 2 * b pow 2`; REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[REAL_LE_POW_2]); (REWRITE_WITH `abs (v:real) = v`); (ASM_REWRITE_TAC[REAL_ABS_REFL]); (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1 pow 2`]); (REWRITE_WITH ` v pow 2 <= &1 pow 2 <=> v <= &1`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Collect_geom.POW2_COND); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `norm (m - u0:real^3) = dist (u0, s:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM]); (ASM_REWRITE_TAC[GSYM dist]); (NEW_GOAL `norm (m - u0:real^3) = sqrt (&2)`); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `(z - u0) dot (u1 - u0:real^3) = &2 * norm (u1 - s1) pow 2`); (REWRITE_WITH `(z - u0) dot (u1 - u0) = (z - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; DOT_RMUL]); (REWRITE_WITH `(s1 - u0) = (u1 - s1:real^3)`); (ASM_REWRITE_TAC[CIRCUMCENTER_2;midpoint] THEN VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[NORM_POW_2] THEN REAL_ARITH_TAC); (NEW_GOAL `&2 * norm (u1 - s1:real^3) pow 2 <= norm (m - u0) * norm (u1 - u0) * a`); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!w:real^3. w IN set_of_list vl ==> dist (circumcenter (set_of_list vl),w) = hl vl`); (MATCH_MP_TAC Rogers.HL_PROPERTIES); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXPAND_TAC "vl"); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (SET_TAC[]); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]); (REWRITE_TAC[ASSUME `u1 - u0 = &2 % (u1 - s1:real^3)`; NORM_MUL]); (REWRITE_WITH `abs (&2) = &2`); (REWRITE_TAC[REAL_ABS_REFL; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `a * (&2 * b) * b / c = (&2 * b pow 2) * ( a / c)`]); (REWRITE_TAC[REAL_ARITH `a <= a * b <=> &0 <= a * (b - &1)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_POW_2; REAL_ARITH `&0 <= &2`]); (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `sqrt (&2) / sqrt (&2) = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`)); (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]); (REAL_ARITH_TAC); (NEW_GOAL `norm (m - u0) * norm (u1 - u0:real^3) * a <= norm (z - u0) * norm (u1 - u0) * a`); (REWRITE_TAC[REAL_ARITH `a * x * y <= b * x * y <=> &0 <= (x * y) * (b - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a" THEN MATCH_MP_TAC REAL_LE_DIV); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!w:real^3. w IN set_of_list vl ==> dist (circumcenter (set_of_list vl),w) = hl vl`); (MATCH_MP_TAC Rogers.HL_PROPERTIES); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXPAND_TAC "vl"); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (SET_TAC[]); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 + t5 * ((z - u0) dot (u1 - u0)) <= t2 * norm (u1 - u0) pow 2 + t5 * (norm (z - u0) * norm (u1 - u0) * a)`); (REWRITE_TAC[REAL_ARITH `a + b * c <= a + b * d <=> &0 <= b * (d - c)`]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (NEW_GOAL `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a`); (REWRITE_TAC[REAL_ARITH `t2 * norm (u1 - u0) pow 2 + t5 * norm (z - u0:real^3) * norm (u1 - u0) * a < norm (t2 % (u1 - u0) + t5 % (z - u0)) * norm (u1 - u0) * a <=> &0 < (a * norm (t2 % (u1 - u0) + t5 % (z - u0)) - t2 * norm (u1 - u0) - t5 * a * norm (z - u0)) * norm (u1 - u0)`]); (MATCH_MP_TAC REAL_LT_MUL); (REPEAT STRIP_TAC); (REWRITE_TAC[REAL_ARITH `&0 < a - b - c <=> b + c < a`]); (NEW_GOAL `t2 * norm (u1 - u0) < a * t2 * norm (u1 - u0:real^3)`); (REWRITE_TAC[REAL_ARITH `a * b < c * a * b <=> &0 < (--a) * b * (&1 - c)`]); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> b = a`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) / sqrt (&2) < &1 <=> hl vl < &1 * sqrt (&2) `); (MATCH_MP_TAC REAL_LT_LDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT); (REAL_ARITH_TAC); (ASM_REWRITE_TAC[REAL_MUL_LID]); (NEW_GOAL `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <= a * norm (t2 % (u1 - u0) + t5 % (z - u0:real^3))`); (REWRITE_TAC[REAL_ARITH `a * t2 * norm (u1 - u0) + t5 * a * norm (z - u0) <= a * norm (t2 % (u1 - u0) + t5 % (z - u0)) <=> &0 <= a * (norm (t2 % (u1 - u0) + t5 % (z - u0)) + (--t2 * norm (u1 - u0)) - t5 * norm (z - u0))`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (s1, u1:real^3)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_WITH `s1:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!w:real^3. w IN set_of_list vl ==> dist (circumcenter (set_of_list vl),w) = hl vl`); (MATCH_MP_TAC Rogers.HL_PROPERTIES); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXPAND_TAC "vl"); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]); (SET_TAC[]); (MATCH_MP_TAC REAL_LE_DIV); (REWRITE_TAC[DIST_POS_LE]); (ASM_SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ONCE_REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]); (ABBREV_TAC `k1 = t2 % (u1 - u0) + t5 % (z - u0:real^3)`); (REWRITE_WITH `t5 * norm (z - u0) = norm (t5 % (z - u0:real^3))`); (REWRITE_TAC[NORM_MUL]); (REWRITE_WITH `abs t5 = t5`); (REWRITE_TAC[REAL_ABS_REFL]); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `--t2 * norm (u1 - u0) = norm ((--t2) % (u1 - u0:real^3))`); (REWRITE_TAC[NORM_MUL]); (REWRITE_WITH `abs (--t2) = --t2`); (REWRITE_TAC[REAL_ABS_REFL]); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `t5 % (z - u0) = k1 + --t2 % (u1 - u0:real^3)`); (EXPAND_TAC "k1" THEN VECTOR_ARITH_TAC); (REWRITE_TAC[NORM_TRIANGLE]); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[NORM_POS_LT; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (* ------------------------------------------------------------------------ *) (NEW_GOAL `t3 = &0 /\ t4 = &0`); (ASM_REAL_ARITH_TAC); (ASM_CASES_TAC `t1 < &0`); (NEW_GOAL `F`); (UNDISCH_TAC `x:real^3 IN rcone_ge u1 u0 a`); (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]); (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]); (REWRITE_TAC[dist]); (REWRITE_WITH `x - u1 = t1 % (u0 - u1:real^3)`); (REWRITE_WITH `x - u1 = x - (t1 + t2) % u1:real^3`); (REWRITE_WITH `t1 + t2 = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]); (NEW_GOAL `t1 * norm (u0 - u1:real^3) pow 2 < &0`); (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]); (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (NEW_GOAL `&0 <= norm (t1 % (u0 - u1:real^3)) * norm (u0 - u1) * a`); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (circumcenter (set_of_list vl),HD vl)`); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_CASES_TAC `t2 < &0`); (NEW_GOAL `F`); (UNDISCH_TAC `x:real^3 IN rcone_ge u0 u1 a`); (REWRITE_TAC[rcone_ge;rconesgn; IN; IN_ELIM_THM]); (REWRITE_TAC[REAL_ARITH `~(a >= b) <=> a < b`]); (REWRITE_TAC[dist]); (REWRITE_WITH `x - u0 = t2 % (u1 - u0:real^3)`); (REWRITE_WITH `x - u0 = x - (t1 + t2) % u0:real^3`); (REWRITE_WITH `t1 + t2 = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (REWRITE_TAC[DOT_LMUL;GSYM NORM_POW_2]); (NEW_GOAL `t2 * norm (u1 - u0:real^3) pow 2 < &0`); (REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < (--a) * b`]); (MATCH_MP_TAC REAL_LT_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0]); (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (NEW_GOAL `&0 <= norm (t2 % (u1 - u0:real^3)) * norm (u1 - u0) * a`); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (EXPAND_TAC "a"); (REWRITE_WITH `hl (vl:(real^3)list) = dist (circumcenter (set_of_list vl),HD vl)`); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (ASM_REWRITE_TAC[] THEN EXPAND_TAC "vl"); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (REWRITE_TAC[DIST_POS_LE]); (SIMP_TAC[SQRT_POS_LE; REAL_ARITH `&0 <= &2`]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM]); (NEW_GOAL `between m (s2, s3:real^3)`); (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`); (EXPAND_TAC "m"); (REWRITE_TAC[mxi]); (COND_CASES_TAC); (ASM_REWRITE_TAC[BETWEEN_REFL]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s`); (MATCH_MP_TAC MXI_EXPLICIT); (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`); (REWRITE_TAC[REAL_ARITH `a < b <=> ~(a >= b)`]); (ASM_REWRITE_TAC[]); (FIRST_ASSUM CHOOSE_TAC THEN UP_ASM_TAC); (ASM_REWRITE_TAC[] THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`); (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t3 * v + t4`); (ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_ADD]); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `t1 + t2 + t3 * u + t3 * v + t4 = t1 + t2 + t3 * (u + v) + t4`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (VECTOR_ARITH_TAC); (SET_TAC[])]);; (* Finished *) end;;