text_formalization/packing/HDTFNFZ.hl

   1 (* ========================================================================= *)\r
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)\r
   3 (*                                                                           *)\r
   4 (*      Authour   : VU KHAC KY                                               *)\r
   5 (*      Book lemma: HDTFNFZ                                                  *)\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_new.hl";;                        *)\r
  14 (*  flyspeck_needs "packing/LEPJBDJ.hl";;                                    *)\r
  15 (* ========================================================================= *)\r
  16 \r
  17 module Hdtfnfz = struct\r
  18 \r
  19 \r
  20 open Rogers;;\r
  21 open Vukhacky_tactics;;\r
  22 open Pack_defs;;\r
  23 open Pack_concl;; \r
  24 open Pack1;;\r
  25 open Sphere;; \r
  26 open Marchal_cells;;\r
  27 open Emnwuus;;\r
  28 open Marchal_cells_2_new;;\r
  29 open Lepjbdj;;\r
  30 \r
  31 \r
  32 let HDTFNFZ_concl = \r
  33 `!V ul k v X.\r
  34      saturated V /\\r
  35      packing V /\\r
  36      barV V 3 ul /\\r
  37      X = mcell k V ul /\ ~(NULLSET X)\r
  38      ==> VX V X = V INTER X`;;\r
  39 \r
  40 let HDTFNFZ = prove_by_refinement (HDTFNFZ_concl,\r
  41 [(REPEAT STRIP_TAC);\r
  42  (REWRITE_TAC[VX]);\r
  43  (COND_CASES_TAC);\r
  44  (NEW_GOAL `F`);\r
  45  (ASM_MESON_TAC[]);\r
  46  (ASM_MESON_TAC[]);\r
  47  (LET_TAC);\r
  48  (COND_CASES_TAC);  (* break into 2 subgoals k' = 0 and k' > 0 *)\r
  49 \r
  50  (UNDISCH_TAC `cell_params V X = k',ul'`);\r
  51  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
  52  (REWRITE_TAC[cell_params]);\r
  53  (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);\r
  54  (DISCH_TAC);\r
  55  (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);\r
  56  (ASM_REWRITE_TAC[]);\r
  57  (MATCH_MP_TAC SELECT_AX);\r
  58  (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);\r
  59  (EXPAND_TAC "P");\r
  60  (COND_CASES_TAC);\r
  61  (REWRITE_TAC[BETA_THM]);\r
  62  (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);\r
  63  (ASM_ARITH_TAC);\r
  64  (REWRITE_TAC[BETA_THM]);\r
  65  (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);\r
  66  (REWRITE_WITH `mcell k V ul = mcell4 V ul`);\r
  67  (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);\r
  68  (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);\r
  69  (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);\r
  70  (UP_ASM_TAC THEN EXPAND_TAC "P");\r
  71  (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);\r
  72  (REWRITE_TAC[ASSUME `X = mcell k' V ul'`; ASSUME `k' = 0` ]);\r
  73  (MATCH_MP_TAC LEPJBDJ_0);\r
  74  (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);\r
  75    (* Finish the case k' = 0  *)\r
  76 \r
  77    (* Continue with the case k' > 0  *)\r
  78 \r
  79  (UNDISCH_TAC `cell_params V X = k',ul'`);\r
  80  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);\r
  81  (REWRITE_TAC[cell_params]);\r
  82  (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul)`);\r
  83  (DISCH_TAC);\r
  84  (NEW_GOAL `(P:(num#(real^3)list->bool)) (k',ul')`);\r
  85  (ASM_REWRITE_TAC[]);\r
  86  (MATCH_MP_TAC SELECT_AX);\r
  87  (EXISTS_TAC `((if (k <= 3) then k else 4),ul:(real^3)list)`);\r
  88  (EXPAND_TAC "P");\r
  89  (COND_CASES_TAC);\r
  90  (REWRITE_TAC[BETA_THM]);\r
  91  (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);\r
  92  (ASM_ARITH_TAC);\r
  93  (REWRITE_TAC[BETA_THM]);\r
  94  (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);\r
  95  (REWRITE_WITH `mcell k V ul = mcell4 V ul`);\r
  96  (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `~(k <= 3) ==> (k >= 4)`]);\r
  97  (REWRITE_WITH `mcell 4 V ul = mcell4 V ul`);\r
  98  (ASM_SIMP_TAC [MCELL_EXPLICIT; ARITH_RULE `(4 >= 4)`]);\r
  99  (UP_ASM_TAC THEN EXPAND_TAC "P");\r
 100  (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);\r
 101  (REWRITE_TAC[ASSUME `X = mcell k' V ul'`]);\r
 102  (MATCH_MP_TAC LEPJBDJ);\r
 103  (ASM_REWRITE_TAC[]);\r
 104  (REPEAT STRIP_TAC);\r
 105  (ASM_SET_TAC[]);\r
 106  (ASM_ARITH_TAC);\r
 107  (NEW_GOAL `X:real^3->bool = {}`);\r
 108  (ASM_MESON_TAC[]);\r
 109  (NEW_GOAL `NULLSET (X:real^3->bool)`);\r
 110  (ASM_MESON_TAC[NEGLIGIBLE_EMPTY]);\r
 111  (ASM_MESON_TAC[])]);;\r
 112 \r
 113 end;;\r
 114 \r