text_formalization/packing/YNHYJIT.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma: YNHYJIT                                                  *)\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 \r
  14 \r
  15 *)\r
  16 \r
  17 (* ========================================================================= *)\r
  18 \r
  19 module Ynhyjit = struct\r
  20 \r
  21 open Rogers;;\r
  22 open Vukhacky_tactics;;\r
  23 open Pack_defs;;\r
  24 open Pack_concl;; \r
  25 open Pack1;;\r
  26 open Sphere;; \r
  27 open Marchal_cells;;\r
  28 open Emnwuus;;\r
  29 open Marchal_cells_2_new;;\r
  30 open Lepjbdj;;\r
  31 \r
  32 \r
  33 let YNHYJIT_concl = \r
  34 `!V ul i p vl.\r
  35      saturated V /\ packing V /\ barV V 3 ul /\ i IN {2,3,4} /\\r
  36      hl (truncate_simplex (i-1) ul) < sqrt (&2) /\ sqrt (&2) <= hl ul /\\r
  37      p permutes 0..(i - 1) /\\r
  38      vl = left_action_list p ul\r
  39      ==> barV V 3 vl /\\r
  40         (!j. i-1 <= j/\ j <= 3 ==> omega_list_n V vl j = omega_list_n V ul j)`;;\r
  41 (* ========================================================================= *)\r
  42 let YNHYJIT = prove_by_refinement (YNHYJIT_concl,\r
  43 \r
  44 [(REPEAT GEN_TAC THEN STRIP_TAC);\r
  45  (ASM_CASES_TAC `i = 2`);\r
  46  (NEW_GOAL   `vl IN barV V 3 /\\r
  47                omega_list_n V vl 1 = omega_list_n V ul 1 /\\r
  48                omega_list_n V vl 2 = omega_list_n V ul 2 /\\r
  49                omega_list_n V vl 3 = omega_list_n V ul 3 /\\r
  50                mxi V vl = mxi V ul`);\r
  51  (MATCH_MP_TAC LEFT_ACTION_LIST_1_PROPERTIES);\r
  52  (EXISTS_TAC `p:num->num`);\r
  53  (ASM_REWRITE_TAC[]);\r
  54  (ASM_MESON_TAC[ARITH_RULE `2 - 1 = 1`]);\r
  55  (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC);\r
  56  (ASM_REWRITE_TAC[]);\r
  57  (ASM_CASES_TAC `j = 1`);\r
  58  (REWRITE_TAC[ASSUME `j = 1`]);\r
  59  (ASM_REWRITE_TAC[]);\r
  60  (ASM_CASES_TAC `j = 2`);\r
  61  (REWRITE_TAC[ASSUME `j = 2`]);\r
  62  (ASM_REWRITE_TAC[]);\r
  63  (ASM_CASES_TAC `j = 3`);\r
  64  (REWRITE_TAC[ASSUME `j = 3`]);\r
  65  (ASM_REWRITE_TAC[]);\r
  66  (NEW_GOAL `F`);\r
  67  (ASM_ARITH_TAC);\r
  68  (ASM_MESON_TAC[]);\r
  69 \r
  70  (ASM_CASES_TAC `i = 3`);\r
  71  (NEW_GOAL `vl IN barV V 3 /\\r
  72              omega_list_n V vl 2 = omega_list_n V ul 2 /\\r
  73              omega_list_n V vl 3 = omega_list_n V ul 3 /\\r
  74              mxi V vl = mxi V ul`);\r
  75  (MATCH_MP_TAC LEFT_ACTION_LIST_PROPERTIES);\r
  76  (EXISTS_TAC `p:num->num`);\r
  77  (ASM_REWRITE_TAC[]);\r
  78  (ASM_MESON_TAC[ARITH_RULE `3 - 1 = 2`]);\r
  79  (UP_ASM_TAC THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC);\r
  80  (ASM_REWRITE_TAC[]);\r
  81  (ASM_CASES_TAC `j = 2`);\r
  82  (REWRITE_TAC[ASSUME `j = 2`]);\r
  83  (ASM_REWRITE_TAC[]);\r
  84  (ASM_CASES_TAC `j = 3`);\r
  85  (REWRITE_TAC[ASSUME `j = 3`]);\r
  86  (ASM_REWRITE_TAC[]);\r
  87  (NEW_GOAL `F`);\r
  88  (ASM_ARITH_TAC);\r
  89  (ASM_MESON_TAC[]);\r
  90 \r
  91  (NEW_GOAL `i = 4`);\r
  92  (ASM_SET_TAC[]);\r
  93  (NEW_GOAL `F`);\r
  94  (UNDISCH_TAC `hl (truncate_simplex (i - 1) (ul:(real^3)list)) < sqrt (&2)`);\r
  95  (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`]);\r
  96  (REWRITE_WITH `truncate_simplex 3 (ul:(real^3)list) = ul`);\r
  97  (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);\r
  98  (MATCH_MP_TAC BARV_3_EXPLICIT);\r
  99  (EXISTS_TAC `V:real^3 ->bool` THEN ASM_REWRITE_TAC[]);\r
 100  (UP_ASM_TAC THEN STRIP_TAC);\r
 101  (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);\r
 102  (ASM_REAL_ARITH_TAC);\r
 103  (ASM_MESON_TAC[])]);;\r
 104 \r
 105 \r
 106 end;;\r
 107 \r