legacy/oldpacking/ch_packing/TSKAJXY.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                           *)
   5 (* Lemma: TSKAJXY                                                             *)
   6 (* Author:  Thomas Hales                                                      *)
   7 (* Date: 2011-07-31                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11
  12 TSKAJXY.
  13
  14 `!V X. saturated V /\ packing V /\ mcell_set V X /\ critical_edge V X = {} ==>
  15   gammaX V X lmfun >= &0`,
  16
  17 I proved a few lemmas, but I realized that I need RVFXZBU, before going
  18 very far, and this still hasn't been formalized.
  19 The theorem is needed for the proof that `cell_param (mcell k V ul) = (k,ul)`.
  20
  21 Return later.
  22  -thales
  23
  24 *)
  25
  26
  27 let exists_eq = prove_by_refinement(
  28   `!P Q. (!(x:A). (P x = Q x)) ==> ((?x. P x) <=> (?x. Q x))`,
  29   (* {{{ proof *)
  30   [
  31 MESON_TAC[]
  32   ]);;
  33   (* }}} *)
  34
  35 let mcell_set_alt = prove_by_refinement(
  36   `!V X. mcell_set V X = (?ul. (barV V 3 ul) /\ (X = mcell0 V ul \/ X = mcell1 V ul \/ X = mcell2 V ul \/ X = mcell3 V ul \/ X = mcell4 V ul))`,
  37   (* {{{ proof *)
  38   [
  39 REWRITE_TAC [Pack_defs.mcell_set;IN_ELIM_THM;IN] ;
  40 REPEAT STRIP_TAC ;
  41 ONCE_REWRITE_TAC[SWAP_EXISTS_THM];
  42 MATCH_MP_TAC exists_eq;
  43 GEN_TAC ;
  44 EQ_TAC;
  45 REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[];
  46 MP_TAC (ARITH_RULE `i=0 \/ i=1 \/ i=2 \/ i=3 \/ i>=4`);
  47 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC [Marchal_cells_2.MCELL_EXPLICIT];
  48 ASM_MESON_TAC [Marchal_cells_2.MCELL_EXPLICIT];
  49 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
  50 EXISTS_TAC `0` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
  51 EXISTS_TAC `1` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
  52 EXISTS_TAC `2` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
  53 EXISTS_TAC `3` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
  54 EXISTS_TAC `4` THEN (MESON_TAC[Marchal_cells_2.MCELL_EXPLICIT;ARITH_RULE `4 >= 4`])
  55   ]);;
  56   (* }}} *)
  57
  58 let mcell4_convex_hull = prove_by_refinement(
  59   `!V X ul. barV V 3 vl /\ hl vl < sqrt(&2) ==> ?u0 u1 u2 u3. (vl = [u0;u1;u2;u3] /\ (mcell4 V vl = convex hull {u0,u1,u2,u3}))`,
  60   (* {{{ proof *)
  61   [
  62 REPEAT STRIP_TAC ;
  63 ASM_REWRITE_TAC [Pack_defs.mcell4];
  64 SUBGOAL_THEN `?u0 u1 u2 u3. vl = [(u0:real^3);u1;u2;u3]` (fun t -> MP_TAC t THEN MESON_TAC[set_of_list]);
  65 MATCH_MP_TAC Marchal_cells.BARV_3_EXPLICIT;
  66 ASM_MESON_TAC []
  67   ]);;
  68   (* }}} *)
  69