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