(* ========================================================================= *)
(*                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;;