(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Authour : VU KHAC KY *) (* Book lemma: RDWKARC *) (* Chaper : Packing (Clusters) *) (* *) (* ========================================================================= *) (* FILES NEED TO BE LOADED *) (* UPFZBZM.hl *) (* ========================================================================= *) module Rdwkarc = struct open Sphere;; open Pack_defs;; open Pack_concl;; open Vukhacky_tactics;; open Pack1;; (*-------------------------------------------------------------------------- *) let RDWKARC_concl = `~kepler_conjecture /\ (!V. cell_cluster_estimate V) /\ TSKAJXY_statement ==> (?V. packing V /\ V SUBSET ball_annulus /\ ~lmfun_ineq_center V)`;; (* ------------------------------------------------------------------------- *) (* The following lemmas are necessary for the main theorem RDWKARC *) (* ------------------------------------------------------------------------- *) (* Lemma 1 *) let JGXZYGW_KY = prove_by_refinement ( `!S. packing S /\ saturated S /\ (?A. fcc_compatible A S /\ negligible_fun_0 A S) ==> (?c. !r. &1 <= r ==> vol (UNIONS {ball (v,&1) | v IN S} INTER ball (vec 0,r)) / vol (ball (vec 0,r)) <= pi / sqrt (&18) + c / r)`, [(MP_TAC JGXZYGW THEN DISCH_THEN (LABEL_TAC "asm1")); GEN_TAC; (REWRITE_TAC[negligible_fun_0]); (USE_THEN "asm1" (MP_TAC o SPEC `S:real^3->bool`)); (DISCH_THEN (LABEL_TAC "asm2")); (USE_THEN "asm2" (MP_TAC o SPEC `(vec 0):real^3`)); (MESON_TAC[])]);; (* ------------------------------------------------------------------------- *) (* Lemma 2 *) let PACKING_SUBSET = prove_by_refinement ( `!V S. packing V /\ S SUBSET V ==> packing S`, [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;SUBSET;IN_ELIM_THM]); (REPEAT STRIP_TAC); (MATCH_MP_TAC(ASSUME `!u:real^3 v. V u /\ V v /\ ~(u = v) ==> &2 <= dist (u,v)`) ); (ASM_REWRITE_TAC[]); (REWRITE_WITH `V (u:real^3) /\ V v <=> u IN V /\ v IN V`); (REWRITE_TAC[IN]); STRIP_TAC; (* Break into smaller subgoals *) (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) ); (ASM_REWRITE_TAC[IN]); (MATCH_MP_TAC(ASSUME `!(x:real^3). x IN S ==> x IN V`) ); (ASM_REWRITE_TAC[IN])]);; (* ------------------------------------------------------------------------ *) (* Lemma 3 *) let PACKING_TRANS = prove_by_refinement ( `! V (x:real^3). packing V ==> packing {u | (u + x) IN V}`, [(REPEAT GEN_TAC THEN REWRITE_TAC[packing;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ABBREV_TAC `u' = (u:real^3) + x`); (ABBREV_TAC `v' = (v:real^3) + x`); (NEW_GOAL `V (u':real^3) /\ V v' /\ ~(u' = v')`); (* New subgoal 1 *) (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[GSYM IN]); (ASM_REWRITE_TAC[GSYM IN]); (NEW_GOAL `u = v:real^3`); (REPLICATE_TAC 3 UP_ASM_TAC ); VECTOR_ARITH_TAC; (ASM_MESON_TAC[]); (* End subgoal 1 *) (REWRITE_WITH `dist (u:real^3, v) = dist (u', v':real^3)`); (* Subgoal 2 *) (EXPAND_TAC "u'" THEN EXPAND_TAC "v'"); (REWRITE_TAC[dist]); (NORM_ARITH_TAC); (* End subgoal 2 *) (UP_ASM_TAC THEN ASM_REWRITE_TAC[])]);; (* ------------------------------------------------------------------------- *) (* Lemma 4 *) let SATURATED_TRANS = prove_by_refinement ( `!V (x:real^3). saturated V ==> saturated {u | u + x IN V}`, [(REPEAT GEN_TAC THEN REWRITE_TAC[saturated]); (DISCH_THEN (LABEL_TAC "asm1")); (GEN_TAC); (USE_THEN "asm1" (MP_TAC o SPEC `(x':real^3) + x`)); (DEL_TAC THEN DISCH_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (EXISTS_TAC `y - (x:real^3)`); (REWRITE_TAC[IN_ELIM_THM; VECTOR_ARITH `y - x + x = (y:real^3)`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `dist (x',y - x) = dist (x'+ x,y:real^3)`); (* Subgoal 1 *) (REWRITE_TAC[dist]); (NORM_ARITH_TAC); (* End subgoal 1 *) (ASM_MESON_TAC[])]);; (* ------------------------------------------------------------------------- *) (* Lemma 5 *) let RADV_TRANS_EQ = prove ( `!u v:real^3 x. ~(u = v) ==> radV {u, v} = radV {u + x, v + x}`, REWRITE_TAC[GSYM set_of_list; GSYM HL; HL_2] THEN NORM_ARITH_TAC);; (* ========================================================================= *) (* MAIN THEOREM RDWKARC *) (* ========================================================================= *) let RDWKARC = prove_by_refinement (RDWKARC_concl, [ (REWRITE_TAC[kepler_conjecture]); (REWRITE_WITH `~(!V. packing V /\ saturated V ==> (?c. !r. &1 <= r ==> vol (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) / vol (ball (vec 0,r)) <= pi / sqrt (&18) + c / r)) <=> (?V. packing V /\ saturated V /\ ~(?c. !r. &1 <= r ==> vol (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) / vol (ball (vec 0,r)) <= pi / sqrt (&18) + c / r))`); (MESON_TAC[]); STRIP_TAC; (NEW_GOAL `~(lmfun_inequality (V:real^3->bool))`); STRIP_TAC; (NEW_GOAL `(?G. negligible_fun_0 G V /\ fcc_compatible G V)`); (ASM_MESON_TAC[UPFZBZM]); (NEW_GOAL `(?c. !r. &1 <= r ==> vol (UNIONS {ball (v,&1) | v IN V} INTER ball (vec 0,r)) / vol (ball (vec 0,r)) <= pi / sqrt (&18) + c / r)`); (MATCH_MP_TAC JGXZYGW_KY); (ASM_REWRITE_TAC[]); (CHOOSE_TAC (ASSUME `?G. negligible_fun_0 G V /\ fcc_compatible G V`)); (EXISTS_TAC `G:real^3->real`); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (* ---------------------------------------------------------------------- *) (UP_ASM_TAC THEN REWRITE_TAC[lmfun_inequality]); (REWRITE_WITH `~(!u:real^3. u IN V ==> sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0} (\v. lmfun (hl [u; v])) <= &12) <=> (?u. u IN V /\ ~(sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0} (\v. lmfun (hl [u; v])) <= &12))`); (MESON_TAC[]); (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]); (DISCH_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (ABBREV_TAC `V' = {v:real^3 | v + u IN V}`); (EXISTS_TAC `V':real^3->bool INTER ball_annulus`); (ASM_REWRITE_TAC[INTER_SUBSET]); (NEW_GOAL `packing (V':real^3->bool)`); (EXPAND_TAC "V'" THEN ASM_MESON_TAC[PACKING_TRANS]); STRIP_TAC; (ASM_MESON_TAC[PACKING_SUBSET;INTER_SUBSET]); (* -------------------------------------------------------------------------- *) (REWRITE_TAC[lmfun_ineq_center]); (REWRITE_TAC[REAL_ARITH `~(a <= b) <=> b < a`]); (EXPAND_TAC "V'" THEN REWRITE_TAC[ball_annulus]); (REWRITE_WITH `sum ({v | v + u IN V} INTER (cball (vec 0,&2 * h0) DIFF ball (vec 0,&2))) (\v. lmfun (hl [vec 0; v])) = sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0} (\v. lmfun (hl [u; v]))`); (MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES); (REWRITE_TAC[IN_ELIM_THM]); (EXISTS_TAC `(\x:real^3. x + u)`); (EXISTS_TAC `(\x:real^3. x - u)`); (REPEAT STRIP_TAC); (REWRITE_TAC[IN_ELIM_THM;cball;INTER]); (CONJ_TAC); (ASM_REWRITE_TAC[VECTOR_ARITH `y:real^3 - u + u = y`]); (REWRITE_TAC[DIFF;IN_ELIM_THM;ball]); (UP_ASM_TAC THEN REWRITE_TAC[dist]); (DISCH_TAC THEN CONJ_TAC); (UP_ASM_TAC THEN NORM_ARITH_TAC); (REWRITE_WITH `norm (vec 0 - (y:real^3 - u)) = dist (u,y)`); (REWRITE_TAC[dist]); (NORM_ARITH_TAC); (REWRITE_TAC[REAL_ARITH `~(a < b) <=> b <= a`]); (NEW_GOAL `V u /\ V y /\ ~(u = (y:real^3))`); (ASM_REWRITE_TAC[]); STRIP_TAC; (ONCE_REWRITE_TAC[GSYM IN]); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[GSYM IN]); (ASM_REWRITE_TAC[]); UP_ASM_TAC; (ASM_MESON_TAC[packing]); (REWRITE_TAC[BETA_THM]); VECTOR_ARITH_TAC; (REWRITE_TAC[BETA_THM]); (UP_ASM_TAC THEN REWRITE_TAC[INTER;IN_ELIM_THM]); (MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[IN_ELIM_THM]); (REWRITE_TAC[VECTOR_ARITH `(u = x + u:real^3) <=> (x = vec 0)`]); (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]); (REPEAT STRIP_TAC); (NEW_GOAL `dist(vec 0, x:real^3) = &0`); (ASM_REWRITE_TAC[dist]); NORM_ARITH_TAC; (ASM_REAL_ARITH_TAC); (REWRITE_TAC[BETA_THM;dist]); (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]); (REWRITE_TAC[IN_ELIM_THM;cball]); NORM_ARITH_TAC; (REWRITE_TAC[BETA_THM]); (VECTOR_ARITH_TAC); (REWRITE_TAC[BETA_THM]); (AP_TERM_TAC); (REWRITE_TAC[HL]); (REWRITE_WITH `!u v:real^3. set_of_list [u; v] = {u , v}`); (REWRITE_TAC[set_of_list]); (UP_ASM_TAC THEN REWRITE_TAC[INTER; DIFF;IN_ELIM_THM;ball]); (REPEAT STRIP_TAC); (NEW_GOAL `~(x:real^3 = vec 0)`); (REPEAT STRIP_TAC); (NEW_GOAL `dist(vec 0, x:real^3) = &0`); (ASM_REWRITE_TAC[dist]); NORM_ARITH_TAC; (ASM_REAL_ARITH_TAC); (REWRITE_WITH `radV {u:real^3, x + u} = radV {vec 0 + u, x + u}`); (MESON_TAC[VECTOR_ARITH `!u. u = vec 0 + u`]); (ASM_MESON_TAC[RADV_TRANS_EQ]); (ASM_REWRITE_TAC[]) ]);; (* Finish the Lemma *) end;;