(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: YNHYJIT                                                  *)
(*      Chaper    : Packing (Marchal cells)                                  *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
(*     


*)

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

module Ynhyjit = 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;;


let YNHYJIT_concl = 
`!V ul i p vl.
     saturated V /\ packing V /\ barV V 3 ul /\ i IN {2,3,4} /\
     hl (truncate_simplex (i-1) ul) < sqrt (&2) /\ sqrt (&2) <= hl ul /\
     p permutes 0..(i - 1) /\
     vl = left_action_list p ul
     ==> barV V 3 vl /\
        (!j. i-1 <= j/\ j <= 3 ==> omega_list_n V vl j = omega_list_n V ul j)`;;
(* ========================================================================= *)
let YNHYJIT = prove_by_refinement (YNHYJIT_concl,

[(REPEAT GEN_TAC THEN STRIP_TAC);
 (ASM_CASES_TAC `i = 2`);
 (NEW_GOAL   `vl IN barV V 3 /\
               omega_list_n V vl 1 = omega_list_n V ul 1 /\
               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_1_PROPERTIES);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[ARITH_RULE `2 - 1 = 1`]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `j = 1`);
 (REWRITE_TAC[ASSUME `j = 1`]);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `j = 2`);
 (REWRITE_TAC[ASSUME `j = 2`]);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `j = 3`);
 (REWRITE_TAC[ASSUME `j = 3`]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `i = 3`);
 (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[]);
 (ASM_MESON_TAC[ARITH_RULE `3 - 1 = 2`]);
 (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `j = 2`);
 (REWRITE_TAC[ASSUME `j = 2`]);
 (ASM_REWRITE_TAC[]);
 (ASM_CASES_TAC `j = 3`);
 (REWRITE_TAC[ASSUME `j = 3`]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `i = 4`);
 (ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `hl (truncate_simplex (i - 1) (ul:(real^3)list)) < sqrt (&2)`);
 (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`]);
 (REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`);
 (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[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
 (ASM_REAL_ARITH_TAC);
 (ASM_MESON_TAC[])]);;


end;;