(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Authour : VU KHAC KY *) (* Book lemma: DDZUPHJ *) (* Chaper : Packing *) (* *) (* ========================================================================= *) module Ddzuphj = struct open Rogers;; open Vukhacky_tactics;; open Pack_defs;; open Pack_concl;; open Pack1;; open Sphere;; open Marchal_cells;; open Emnwuus;; open Marchal_cells_2_new;; open Lepjbdj;; open Hdtfnfz;; open Tezffsk;; open Njiutiu;; (* ========================================================================= *) let DDZUPHJ_concl = `!V ul vl k. saturated V /\ packing V /\ k IN {0,1,2,3,4} /\ barV V 3 ul /\ barV V 3 vl /\ rogers V ul = rogers V vl /\ aff_dim (rogers V ul) = &3 /\ ~ (mcell k V ul = {}) ==> (mcell k V ul = mcell k V vl)`;; (* ========================================================================= *) let RCONE_GT_EQ_EMPTY_LEMMA = prove_by_refinement ( `!a:real^3 b r. r >= &1 ==> rcone_gt a b r = {}`, [(REPEAT STRIP_TAC); (REWRITE_TAC[rcone_gt;rconesgn; SET_RULE `{x | P x} = {} <=> (!x. P x ==> F)`]); (REWRITE_TAC[dist] THEN REPEAT STRIP_TAC); (NEW_GOAL `(x - a) dot (b - a) <= norm(x - a) * norm (b - a:real^3)`); (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]); (NEW_GOAL`norm (x - a) * norm (b:real^3 -a) * r >= norm (x-a) * norm (b-a)`); (REWRITE_TAC[REAL_ARITH `(a*b*c >= a * b) <=> &0 <= (a * b) * (c - &1)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[NORM_POS_LE]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC)]);; (* ========================================================================= *) (* Main theorem *) (* ========================================================================= *) let DDZUPHJ = prove_by_refinement (DDZUPHJ_concl, [(REPEAT STRIP_TAC); (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `?v0 v1 v2 v3. vl = [v0;v1;v2;v3:real^3]`); (MATCH_MP_TAC BARV_3_EXPLICIT); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC); (* ========================================================================= *) (* Case k = 4 *) (ASM_CASES_TAC `k = 4`); (NEW_GOAL `hl (ul:(real^3)list) < sqrt (&2)`); (UNDISCH_TAC `~(mcell k V ul = {})` THEN SIMP_TAC[ASSUME `k = 4`; MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (MESON_TAC[]); (NEW_GOAL `truncate_simplex 3 (ul:(real^3)list) = truncate_simplex 3 vl`); (MATCH_MP_TAC TEZFFSK); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `3 <= 3`]); (REWRITE_WITH `truncate_simplex 3 [u0; u1; u2; u3:real^3] = ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]); (REWRITE_WITH `truncate_simplex 3 (vl:(real^3)list) = vl`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]); (STRIP_TAC); (REWRITE_TAC[ASSUME `ul = (vl:(real^3)list)`]); (* ========================================================================= *) (* Case k = 3 *) (ASM_CASES_TAC `k = 3`); (NEW_GOAL `hl (truncate_simplex 2 ul) < sqrt (&2) /\ sqrt (&2) <= hl (ul:(real^3)list)`); (UNDISCH_TAC `~(mcell k V ul = {})` THEN SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT;mcell3]); (MESON_TAC[]); (NEW_GOAL `truncate_simplex 2 (ul:(real^3)list) = truncate_simplex 2 vl`); (MATCH_MP_TAC TEZFFSK); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `!i. 0 <= i /\ i <= 3 ==> omega_list_n V ul i = omega_list_n V vl i`); (MATCH_MP_TAC NJIUTIU); (ASM_REWRITE_TAC[]); (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`); (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]); (STRIP_TAC); (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`); (STRIP_TAC); (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`); GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `mxi V ul = mxi V vl`); (REWRITE_TAC[mxi]); (COND_CASES_TAC); (COND_CASES_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `F`); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 2 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 2 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (ASM_REWRITE_TAC[]); (SIMP_TAC[ASSUME `k = 3`; MCELL_EXPLICIT; mcell3]); (COND_CASES_TAC); (COND_CASES_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME `truncate_simplex 2 ul = truncate_simplex 2 (vl:(real^3)list)`)]); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (* ========================================================================= *) (* Case k = 2 *) (ASM_CASES_TAC `k = 2`); (NEW_GOAL `hl (truncate_simplex 1 ul) < sqrt (&2) /\ sqrt (&2) <= hl (ul:(real^3)list)`); (UNDISCH_TAC `~(mcell k V ul = {})` THEN SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT;mcell2]); (MESON_TAC[]); (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`); (MATCH_MP_TAC TEZFFSK); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (NEW_GOAL `!i. 0 <= i /\ i <= 3 ==> omega_list_n V ul i = omega_list_n V vl i`); (MATCH_MP_TAC NJIUTIU); (ASM_REWRITE_TAC[]); (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`); (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]); (STRIP_TAC); (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`); (STRIP_TAC); (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`); GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `mxi V ul = mxi V vl`); (REWRITE_TAC[mxi]); (COND_CASES_TAC); (COND_CASES_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `F`); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 vl`); (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (STRIP_TAC); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V wl = omega_list_n V ul 2/\ HD wl = HD ul`); (EXPAND_TAC "wl"); (STRIP_TAC); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`); (REWRITE_WITH `omega_list V zl = omega_list_n V vl 2/\ HD zl = HD vl`); (EXPAND_TAC "zl"); (STRIP_TAC); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`); (STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (COND_CASES_TAC); (NEW_GOAL `F`); (ABBREV_TAC `zl:(real^3)list = truncate_simplex 2 ul`); (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (STRIP_TAC); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `wl:(real^3)list = truncate_simplex 2 vl`); (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `2` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V wl = omega_list_n V vl 2/\ HD wl = HD vl`); (EXPAND_TAC "wl"); (STRIP_TAC); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_TAC[ASSUME `vl = [v0;v1;v2;v3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)`); (REWRITE_WITH `omega_list V zl = omega_list_n V ul 2/\ HD zl = HD ul`); (EXPAND_TAC "zl"); (STRIP_TAC); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2/\ HD ul = HD vl`); (STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[]); (REWRITE_WITH `omega_list_n V ul 2 = omega_list_n V vl 2`); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (REWRITE_WITH `HD (ul:(real^3)list) = HD (truncate_simplex 1 ul)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `HD (vl:(real^3)list) = HD (truncate_simplex 1 vl)`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_TAC[ASSUME `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]); (SIMP_TAC[ASSUME `k = 2`; MCELL_EXPLICIT; mcell2]); (COND_CASES_TAC); (COND_CASES_TAC); (REWRITE_TAC[ASSUME `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`]); (REPEAT LET_TAC); (REWRITE_TAC[ASSUME `mxi V ul = mxi V vl`]); (REWRITE_WITH `omega_list_n V ul 3 = omega_list_n V vl 3`); (FIRST_ASSUM MATCH_MP_TAC THEN ARITH_TAC); (ASM_REWRITE_TAC[HD;TL]); (NEW_GOAL `{u0, u1} = {v0, v1:real^3}`); (REWRITE_WITH `{u0,u1:real^3} = set_of_list(truncate_simplex 1 ul)`); (REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_WITH `{v0,v1:real^3} = set_of_list(truncate_simplex 1 vl)`); (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1]); (ASM_REWRITE_TAC[]); (ASM_CASES_TAC `u0 = v0:real^3`); (NEW_GOAL `u1 = v1:real^3`); (NEW_GOAL `~(u0 = u1:real^3)`); (STRIP_TAC); (NEW_GOAL `LENGTH (truncate_simplex 1 (ul:(real^3)list)) = 1 + 1 /\ CARD (set_of_list (truncate_simplex 1 ul)) = 1 + 1`); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (UP_ASM_TAC THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; ASSUME `ul = [u0;u1;u2;u3:real^3]`; ASSUME `u0 = u1:real^3`; SET_RULE `{a,a} = {a}`; Geomdetail.CARD_SING; ARITH_RULE `~(1 = 1 + 1)`]); (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `u0 = v1:real^3`); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (NEW_GOAL `u1 = v0:real^3`); (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (SET_TAC[]); (NEW_GOAL `F`); (UP_ASM_TAC THEN REWRITE_TAC[GSYM (ASSUME `truncate_simplex 1 ul = truncate_simplex 1 (vl:(real^3)list)`)]); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (* ========================================================================= *) (* Case k = 1 *) (ASM_CASES_TAC `k = 1`); (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`); (UNDISCH_TAC `~(mcell k V ul = {})` THEN SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT;mcell1]); (MESON_TAC[]); (NEW_GOAL `!i. 0 <= i /\ i <= 3 ==> omega_list_n V ul i = omega_list_n V vl i`); (MATCH_MP_TAC NJIUTIU); (ASM_REWRITE_TAC[]); (NEW_GOAL `HD ul = HD (vl:(real^3)list)`); (MATCH_MP_TAC ROGERS_INTER_V_LEMMA); (EXISTS_TAC `V:real^3->bool`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`); (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`); (REWRITE_TAC[IN]); (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]); (REWRITE_WITH `rogers V ul = convex hull {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET); (SET_TAC[]); (NEW_GOAL `sqrt (&2) <= hl (vl:(real^3)list)`); (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]); (STRIP_TAC); (NEW_GOAL `hl vl = dist (omega_list V vl,HD vl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (NEW_GOAL `hl ul <= dist (omega_list V ul,HD ul)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `3` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V ul = omega_list V vl /\ HD ul = HD vl`); (STRIP_TAC); (ASM_REWRITE_TAC[OMEGA_LIST; LENGTH]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`); GSYM (ASSUME `vl = [v0;v1;v2;v3:real^3]`)]); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_CASES_TAC `hl (truncate_simplex 1 (ul:(real^3)list)) < sqrt (&2)`); (NEW_GOAL `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`); (MATCH_MP_TAC TEZFFSK); (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]); (COND_CASES_TAC); (COND_CASES_TAC); (REWRITE_TAC[ASSUME `truncate_simplex 1 (ul:(real^3)list) = truncate_simplex 1 vl`; ASSUME `HD ul = HD (vl:(real^3)list)`; ASSUME `rogers V ul = rogers V vl`]); (REWRITE_WITH `HD (TL ul) = EL 1 (truncate_simplex 1 (ul:(real^3)list))`); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]); (REWRITE_WITH `HD (TL vl) = EL 1 (truncate_simplex 1 (vl:(real^3)list))`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[EL; HD; TL; ARITH_RULE `1 = SUC 0`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (ul:(real^3)list))`); (ASM_REAL_ARITH_TAC); (NEW_GOAL `sqrt (&2) <= hl (truncate_simplex 1 (vl:(real^3)list))`); (REWRITE_TAC[ARITH_RULE `a <= b <=> (b < a ==> F)`]); (STRIP_TAC); (ABBREV_TAC `zl = truncate_simplex 1 (vl:(real^3)list)`); (NEW_GOAL `hl zl = dist (omega_list V zl,HD zl)`); (MATCH_MP_TAC WAUFCHE2); (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "zl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (ABBREV_TAC `wl = truncate_simplex 1 (ul:(real^3)list)`); (NEW_GOAL `hl wl <= dist (omega_list V wl,HD wl)`); (MATCH_MP_TAC WAUFCHE1); (EXISTS_TAC `1` THEN REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]); (EXPAND_TAC "wl" THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (UP_ASM_TAC THEN REWRITE_WITH `omega_list V wl = omega_list_n V ul 1 /\ HD wl = HD ul`); (STRIP_TAC); (EXPAND_TAC "wl"); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (EXPAND_TAC "wl"); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (UNDISCH_TAC `hl zl = dist (omega_list V zl,HD zl)` THEN REWRITE_WITH `omega_list V zl = omega_list_n V vl 1 /\ HD zl = HD vl`); (STRIP_TAC); (EXPAND_TAC "zl"); (MATCH_MP_TAC Packing3.OMEGA_LIST_LEMMA); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (EXPAND_TAC "zl"); (MATCH_MP_TAC Packing3.HD_TRUNCATE_SIMPLEX); (ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC); (REWRITE_WITH `omega_list_n V ul 1 = omega_list_n V vl 1`); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (REWRITE_TAC[ASSUME `HD (ul:(real^3)list) = HD (vl:(real^3)list)`]); (ASM_REAL_ARITH_TAC); (SIMP_TAC[ASSUME `k = 1`; MCELL_EXPLICIT; mcell1]); (COND_CASES_TAC); (COND_CASES_TAC); (REWRITE_WITH `rcone_gt (HD (ul:(real^3)list)) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)) = {}`); (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA); (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]); (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (ul:(real^3)list)) / sqrt (&2) <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 ul)`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT); (ARITH_TAC); (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC); (REWRITE_WITH `rcone_gt (HD (vl:(real^3)list)) (HD (TL vl)) (hl (truncate_simplex 1 vl) / sqrt (&2)) = {}`); (MATCH_MP_TAC RCONE_GT_EQ_EMPTY_LEMMA); (ONCE_REWRITE_TAC[REAL_ARITH `a >= b <=> b <= a`]); (REWRITE_WITH `&1 <= hl (truncate_simplex 1 (vl:(real^3)list)) / sqrt (&2) <=> &1 * sqrt (&2) <= hl (truncate_simplex 1 vl)`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT); (ARITH_TAC); (REWRITE_TAC[REAL_MUL_LID] THEN ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (* ========================================================================= *) (* Case k = 0 *) (NEW_GOAL `k = 0`); (ASM_SET_TAC[]); (SIMP_TAC[ASSUME `k = 0`; MCELL_EXPLICIT; mcell0]); (REWRITE_TAC[ASSUME `rogers V ul = rogers V vl`]); (NEW_GOAL `!i. 0 <= i /\ i <= 3 ==> omega_list_n V ul i = omega_list_n V vl i`); (MATCH_MP_TAC NJIUTIU); (ASM_REWRITE_TAC[]); (REWRITE_WITH `HD ul = HD (vl:(real^3)list)`); (MATCH_MP_TAC ROGERS_INTER_V_LEMMA); (EXISTS_TAC `V:real^3->bool`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `HD ul IN set_of_list (ul:(real^3)list)`); (MATCH_MP_TAC Packing3.BARV_IMP_HD_IN_SET_OF_LIST); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (REWRITE_WITH `rogers V vl (HD ul) <=> HD ul IN rogers V vl`); (REWRITE_TAC[IN]); (REWRITE_TAC[GSYM (ASSUME `rogers V ul = rogers V vl`)]); (REWRITE_WITH `rogers V ul = convex hull {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET); (SET_TAC[])]);; end;;