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

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
     
(* flyspeck_needs "packing/marchal_cells_2.hl";; *)

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


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

let RVFXZBU_concl = 
 `!V ul i p. 
     i IN {0,1,2,3,4} /\
     saturated V /\ packing V /\ barV V 3 ul /\ p permutes 0..i - 1
     ==> mcell i V (left_action_list p ul) = mcell i V ul`;;


let RVFXZBU = prove_by_refinement (RVFXZBU_concl,
[(REPEAT STRIP_TAC);
(* ======================== Case i = 4  ====================================*)

 (ASM_CASES_TAC `i = 4`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell4]);
 (NEW_GOAL `4 >= 4`);
 (ARITH_TAC);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell4]);
 (REWRITE_TAC[HL]);
 (REWRITE_WITH 
  `set_of_list (left_action_list p ul) = set_of_list  (ul:(real^3)list)`);
 (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);
 (REWRITE_WITH `LENGTH (ul:(real^3)list) = i`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `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[]);
 (ARITH_TAC);
 (ASM_REWRITE_TAC[]);

(* ======================== Case i = 0  ====================================*)

 (ASM_CASES_TAC `i = 0`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell0]);
 (UNDISCH_TAC `p permutes 0 ..i-1`);
 (ASM_REWRITE_TAC[ARITH_RULE `0 - 1 = 0`]);
 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 (DISCH_TAC);
 (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);

 (* ======================== Case i = 1  ====================================*)
 
 (ASM_CASES_TAC `i = 1`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell1]);
 (UNDISCH_TAC `p permutes 0 ..i-1`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`]);
 (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);
 (DISCH_TAC);
 (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);

 (* ======================== Case i = 2  ====================================*)

 (ASM_CASES_TAC `i = 2`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT]);
 (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`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_CASES_TAC `left_action_list p ul = (ul:(real^3)list)`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `left_action_list p ul = ul \/
             left_action_list p ul = [u1; u0; u2; u3:real^3]`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_1_EXPLICIT);
 (ASM_REWRITE_TAC[]);
 (ASM_MESON_TAC[ARITH_RULE `1 = 2 - 1`]);
 (NEW_GOAL `left_action_list p ul = [u1; u0; u2; u3:real^3]`);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[ASSUME `left_action_list p ul = [u1; u0; u2; u3:real^3]`; mcell2; HD; TL]);

 (COND_CASES_TAC);
 (COND_CASES_TAC);

(* Case 1 *)
 (ASM_REWRITE_TAC[mcell2; HD; TL]);
 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL; set_of_list]);
 (REWRITE_TAC[SET_RULE `{a,b} = {b, a} /\ {a,b,c,d} = {b,a,c,d}`]);
 (REPEAT LET_TAC);
 (REWRITE_WITH `mxi V [u1; u0; u2; u3:real^3] = mxi V ul /\ 
                 omega_list_n V [u1; u0; u2; u3] 3 = omega_list_n V ul 3`);
 (REWRITE_WITH `[u1; u0; u2; u3:real^3] IN barV V 3 /\
             omega_list_n V [u1; u0; u2; u3:real^3] 1 = omega_list_n V ul 1 /\
             omega_list_n V [u1; u0; u2; u3:real^3] 2 = omega_list_n V ul 2 /\
             omega_list_n V [u1; u0; u2; u3:real^3] 3 = omega_list_n V ul 3 /\
             mxi V [u1; u0; u2; u3:real^3] = mxi V ul`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_1_PROPERTIES);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);
 (ASM_REWRITE_TAC[]);
 (SET_TAC[]);
 (* Case 2 *)
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN   
   ASM_REWRITE_TAC[HL;set_of_list;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_WITH `{u1, u0} = {u0,u1:real^3} /\ {u1, u0, u2, u3} = {u0, u1, u2, u3}`);
 (SET_TAC[]);
 (ASM_MESON_TAC[]);

(* Case 3 *)
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN   
   ASM_REWRITE_TAC[HL;set_of_list;TRUNCATE_SIMPLEX_EXPLICIT_1]);
 (REWRITE_WITH `{u1, u0} = {u0,u1:real^3} /\ {u1, u0, u2, u3} = {u0, u1, u2, u3}`);
 (SET_TAC[]);
 (ASM_MESON_TAC[]);
 (SET_TAC[]);

(* ======================== Case i = 3  ====================================*)

 (ASM_CASES_TAC `i = 3`);
 (ASM_REWRITE_TAC[MCELL_EXPLICIT]);
 (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`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_TAC[mcell3]);
 (NEW_GOAL `set_of_list (truncate_simplex 2 (left_action_list p ul)) = 
    set_of_list (truncate_simplex 2 (ul:(real^3)list))`);
 (MATCH_MP_TAC  SET_OF_LIST_TRUN2_LEFT_ACTION_LIST2);
 (EXISTS_TAC `V:real^3->bool`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (ABBREV_TAC `xl:(real^3)list = left_action_list p ul`);
 (REWRITE_WITH `xl IN barV V 3 /\
             omega_list_n V xl 2 = omega_list_n V ul 2 /\
             omega_list_n V xl 3 = omega_list_n V ul 3 /\
             mxi V xl = mxi V ul`);
 (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);
 (EXISTS_TAC `p:num->num`);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[HL]);
 (REWRITE_WITH `set_of_list (left_action_list p [u0; u1; u2; u3:real^3]) =
   set_of_list [u0; u1; u2; u3]`);
 (MATCH_MP_TAC SET_OF_LIST_LEFT_ACTION_LIST_2);
 (REWRITE_WITH `LENGTH [u0; u1; u2; u3:real^3] = 4 /\ 4 -2 = 2`);
 (REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[ARITH_RULE `2 <= 4`]);
 (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);
 (ASM_MESON_TAC[]);

 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[HL]);
 (REWRITE_WITH `set_of_list (left_action_list p [u0; u1; u2; u3:real^3]) =
   set_of_list [u0; u1; u2; u3]`);
 (MATCH_MP_TAC SET_OF_LIST_LEFT_ACTION_LIST_2);
 (REWRITE_WITH `LENGTH [u0; u1; u2; u3:real^3] = 4 /\ 4 -2 = 2`);
 (REWRITE_TAC[LENGTH] THEN ARITH_TAC);
 (ASM_REWRITE_TAC[ARITH_RULE `2 <= 4`]);
 (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[]);

 (NEW_GOAL `F`);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[])]);;

end;;