text_formalization/packing/RVFXZBU.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma: RVFXZBU                                                  *)\r
   6 (*      Chaper    : Packing (Marchal cells)                                  *)\r
   7 (*                                                                           *)\r
   8 (* ========================================================================= *)\r
   9 \r
  10 (* ========================================================================= *)\r
  11 (*                     FILES NEED TO BE LOADED                               *)\r
  12      \r
  13 (* flyspeck_needs "packing/marchal_cells_2.hl";; *)\r
  14 \r
  15 module Rvfxzbu = struct\r
  16 \r
  17 open Rogers;;\r
  18 open Vukhacky_tactics;;\r
  19 open Pack_defs;;\r
  20 open Pack_concl;; \r
  21 open Pack1;;\r
  22 open Sphere;; \r
  23 open Marchal_cells;;\r
  24 open Emnwuus;;\r
  25 open Marchal_cells_2_new;;\r
  26 open Lepjbdj;;\r
  27 open Hdtfnfz;;\r
  28 \r
  29 \r
  30 (* ========================================================================= *)\r
  31 \r
  32 let RVFXZBU_concl = \r
  33  `!V ul i p. \r
  34      i IN {0,1,2,3,4} /\\r
  35      saturated V /\ packing V /\ barV V 3 ul /\ p permutes 0..i - 1\r
  36      ==> mcell i V (left_action_list p ul) = mcell i V ul`;;\r
  37 \r
  38 \r
  39 let RVFXZBU = prove_by_refinement (RVFXZBU_concl,\r
  40 [(REPEAT STRIP_TAC);\r
  41 (* ======================== Case i = 4  ====================================*)\r
  42 \r
  43  (ASM_CASES_TAC `i = 4`);\r
  44  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell4]);\r
  45  (NEW_GOAL `4 >= 4`);\r
  46  (ARITH_TAC);\r
  47  (ASM_SIMP_TAC[MCELL_EXPLICIT; mcell4]);\r
  48  (REWRITE_TAC[HL]);\r
  49  (REWRITE_WITH \r
  50   `set_of_list (left_action_list p ul) = set_of_list  (ul:(real^3)list)`);\r
  51  (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);\r
  52  (REWRITE_WITH `LENGTH (ul:(real^3)list) = i`);\r
  53  (ASM_REWRITE_TAC[]);\r
  54  (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ \r
  55    CARD (set_of_list ul) = 3 + 1`);\r
  56  (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);\r
  57  (EXISTS_TAC `V:real^3 ->bool`);\r
  58  (ASM_REWRITE_TAC[]);\r
  59  (ARITH_TAC);\r
  60  (ASM_REWRITE_TAC[]);\r
  61 \r
  62 (* ======================== Case i = 0  ====================================*)\r
  63 \r
  64  (ASM_CASES_TAC `i = 0`);\r
  65  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell0]);\r
  66  (UNDISCH_TAC `p permutes 0 ..i-1`);\r
  67  (ASM_REWRITE_TAC[ARITH_RULE `0 - 1 = 0`]);\r
  68  (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);\r
  69  (DISCH_TAC);\r
  70  (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);\r
  71 \r
  72  (* ======================== Case i = 1  ====================================*)\r
  73  \r
  74  (ASM_CASES_TAC `i = 1`);\r
  75  (ASM_REWRITE_TAC[MCELL_EXPLICIT; mcell1]);\r
  76  (UNDISCH_TAC `p permutes 0 ..i-1`);\r
  77  (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`]);\r
  78  (REWRITE_TAC[Packing3.PERMUTES_TRIVIAL]);\r
  79  (DISCH_TAC);\r
  80  (ASM_REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]);\r
  81 \r
  82  (* ======================== Case i = 2  ====================================*)\r
  83 \r
  84  (ASM_CASES_TAC `i = 2`);\r
  85  (ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
  86  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);\r
  87  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
  88  (EXISTS_TAC `V:real^3->bool`);\r
  89  (ASM_REWRITE_TAC[]);\r
  90  (UP_ASM_TAC THEN STRIP_TAC);\r
  91  (ASM_CASES_TAC `left_action_list p ul = (ul:(real^3)list)`);\r
  92  (ASM_REWRITE_TAC[]);\r
  93  (NEW_GOAL `left_action_list p ul = ul \/\r
  94              left_action_list p ul = [u1; u0; u2; u3:real^3]`);\r
  95  (MATCH_MP_TAC LEFT_ACTION_LIST_1_EXPLICIT);\r
  96  (ASM_REWRITE_TAC[]);\r
  97  (ASM_MESON_TAC[ARITH_RULE `1 = 2 - 1`]);\r
  98  (NEW_GOAL `left_action_list p ul = [u1; u0; u2; u3:real^3]`);\r
  99  (ASM_MESON_TAC[]);\r
 100  (REWRITE_TAC[ASSUME `left_action_list p ul = [u1; u0; u2; u3:real^3]`; mcell2; HD; TL]);\r
 101 \r
 102  (COND_CASES_TAC);\r
 103  (COND_CASES_TAC);\r
 104 \r
 105 (* Case 1 *)\r
 106  (ASM_REWRITE_TAC[mcell2; HD; TL]);\r
 107  (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1; HL; set_of_list]);\r
 108  (REWRITE_TAC[SET_RULE `{a,b} = {b, a} /\ {a,b,c,d} = {b,a,c,d}`]);\r
 109  (REPEAT LET_TAC);\r
 110  (REWRITE_WITH `mxi V [u1; u0; u2; u3:real^3] = mxi V ul /\ \r
 111                  omega_list_n V [u1; u0; u2; u3] 3 = omega_list_n V ul 3`);\r
 112  (REWRITE_WITH `[u1; u0; u2; u3:real^3] IN barV V 3 /\\r
 113              omega_list_n V [u1; u0; u2; u3:real^3] 1 = omega_list_n V ul 1 /\\r
 114              omega_list_n V [u1; u0; u2; u3:real^3] 2 = omega_list_n V ul 2 /\\r
 115              omega_list_n V [u1; u0; u2; u3:real^3] 3 = omega_list_n V ul 3 /\\r
 116              mxi V [u1; u0; u2; u3:real^3] = mxi V ul`);\r
 117  (MATCH_MP_TAC LEFT_ACTION_LIST_1_PROPERTIES);\r
 118  (EXISTS_TAC `p:num->num`);\r
 119  (ASM_REWRITE_TAC[]);\r
 120  (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`]);\r
 121  (ASM_REWRITE_TAC[]);\r
 122  (SET_TAC[]);\r
 123  (* Case 2 *)\r
 124  (NEW_GOAL `F`);\r
 125  (UP_ASM_TAC THEN UP_ASM_TAC THEN   \r
 126    ASM_REWRITE_TAC[HL;set_of_list;TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 127  (REWRITE_WITH `{u1, u0} = {u0,u1:real^3} /\ {u1, u0, u2, u3} = {u0, u1, u2, u3}`);\r
 128  (SET_TAC[]);\r
 129  (ASM_MESON_TAC[]);\r
 130 \r
 131 (* Case 3 *)\r
 132  (COND_CASES_TAC);\r
 133  (NEW_GOAL `F`);\r
 134  (UP_ASM_TAC THEN UP_ASM_TAC THEN   \r
 135    ASM_REWRITE_TAC[HL;set_of_list;TRUNCATE_SIMPLEX_EXPLICIT_1]);\r
 136  (REWRITE_WITH `{u1, u0} = {u0,u1:real^3} /\ {u1, u0, u2, u3} = {u0, u1, u2, u3}`);\r
 137  (SET_TAC[]);\r
 138  (ASM_MESON_TAC[]);\r
 139  (SET_TAC[]);\r
 140 \r
 141 (* ======================== Case i = 3  ====================================*)\r
 142 \r
 143  (ASM_CASES_TAC `i = 3`);\r
 144  (ASM_REWRITE_TAC[MCELL_EXPLICIT]);\r
 145  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);\r
 146  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
 147  (EXISTS_TAC `V:real^3->bool`);\r
 148  (ASM_REWRITE_TAC[]);\r
 149  (UP_ASM_TAC THEN STRIP_TAC);\r
 150  (REWRITE_TAC[mcell3]);\r
 151  (NEW_GOAL `set_of_list (truncate_simplex 2 (left_action_list p ul)) = \r
 152     set_of_list (truncate_simplex 2 (ul:(real^3)list))`);\r
 153  (MATCH_MP_TAC  SET_OF_LIST_TRUN2_LEFT_ACTION_LIST2);\r
 154  (EXISTS_TAC `V:real^3->bool`);\r
 155  (ASM_REWRITE_TAC[]);\r
 156  (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);\r
 157  (COND_CASES_TAC);\r
 158  (COND_CASES_TAC);\r
 159  (ABBREV_TAC `xl:(real^3)list = left_action_list p ul`);\r
 160  (REWRITE_WITH `xl IN barV V 3 /\\r
 161              omega_list_n V xl 2 = omega_list_n V ul 2 /\\r
 162              omega_list_n V xl 3 = omega_list_n V ul 3 /\\r
 163              mxi V xl = mxi V ul`);\r
 164  (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);\r
 165  (EXISTS_TAC `p:num->num`);\r
 166  (ASM_REWRITE_TAC[]);\r
 167  (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);\r
 168  (ASM_REWRITE_TAC[]);\r
 169  (NEW_GOAL `F`);\r
 170  (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[HL]);\r
 171  (REWRITE_WITH `set_of_list (left_action_list p [u0; u1; u2; u3:real^3]) =\r
 172    set_of_list [u0; u1; u2; u3]`);\r
 173  (MATCH_MP_TAC SET_OF_LIST_LEFT_ACTION_LIST_2);\r
 174  (REWRITE_WITH `LENGTH [u0; u1; u2; u3:real^3] = 4 /\ 4 -2 = 2`);\r
 175  (REWRITE_TAC[LENGTH] THEN ARITH_TAC);\r
 176  (ASM_REWRITE_TAC[ARITH_RULE `2 <= 4`]);\r
 177  (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);\r
 178  (ASM_MESON_TAC[]);\r
 179 \r
 180  (COND_CASES_TAC);\r
 181  (NEW_GOAL `F`);\r
 182  (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[HL]);\r
 183  (REWRITE_WITH `set_of_list (left_action_list p [u0; u1; u2; u3:real^3]) =\r
 184    set_of_list [u0; u1; u2; u3]`);\r
 185  (MATCH_MP_TAC SET_OF_LIST_LEFT_ACTION_LIST_2);\r
 186  (REWRITE_WITH `LENGTH [u0; u1; u2; u3:real^3] = 4 /\ 4 -2 = 2`);\r
 187  (REWRITE_TAC[LENGTH] THEN ARITH_TAC);\r
 188  (ASM_REWRITE_TAC[ARITH_RULE `2 <= 4`]);\r
 189  (UNDISCH_TAC `p permutes 0..i-1` THEN ASM_REWRITE_TAC[ARITH_RULE `3 -1 =2`]);\r
 190  (ASM_MESON_TAC[]);\r
 191  (REWRITE_TAC[]);\r
 192 \r
 193  (NEW_GOAL `F`);\r
 194  (ASM_SET_TAC[]);\r
 195  (ASM_MESON_TAC[])]);;\r
 196 \r
 197 end;;\r
 198 \r