text_formalization/local/LFJCIXP.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Local Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2012-04-01                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11
  12
  13 module  Lfjcixp = struct
  14
  15 open Sphere;;
  16 open Fan_defs;;
  17 open Hypermap;;
  18 open Vol1;;
  19 open Fan;;
  20 open Prove_by_refinement;;
  21 open Pack_defs;;
  22 open Collect_geom;;
  23
  24
  25 let LFJCIXP =prove(`(!y1 y2 y3 y4 y5 y6.
  26 &2 <= y1 /\ y1<= #2.52
  27 /\ &2 <= y2 /\ y2<= #2.52
  28 /\ &2 <= y3 /\ y3<= #2.52
  29 /\ &2 <= y4 /\ y4<= #4.52
  30 /\ y5= &2
  31 /\ y6= &2
  32 ==> (y4 <= #3.915 \/ delta (y1 pow 2) (y2 pow 2) (y3 pow 2) (y4 pow 2) (y5 pow 2) (y6 pow 2)< &0))
  33 /\ {v,u,w} SUBSET ball_annulus
  34 /\ packing {v,u,w}
  35 /\ ~(u=w)
  36 /\ norm(v-u)= &2
  37 /\ norm(v-w)= &2
  38 /\ norm (u - w) <= #4.52
  39 ==> norm(u-w)<= #3.915
  40 `,
  41 REPEAT STRIP_TAC
  42 THEN MRESAL_TAC Trigonometry.LBEVAKV[`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`][dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
  43 THEN POP_ASSUM MP_TAC
  44 THEN ONCE_REWRITE_TAC[NORM_SUB]
  45 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= a <=> ~(a< &0)`]
  46 THEN MP_TAC(SET_RULE`{v, u, w} SUBSET ball_annulus
  47 ==> v IN ball_annulus /\ u IN ball_annulus /\ w IN ball_annulus`)
  48 THEN ASM_REWRITE_TAC[]
  49 THEN REWRITE_TAC[IN_ELIM_THM;DIFF;ball_annulus;ball;cball;REAL_ARITH`~(a< &2)<=> &2<= a`;REAL_ARITH`&2 * #1.26= #2.52`;h0;dist;VECTOR_ARITH`a - vec 0= a`;NORM_NEG;NORM_SUB]
  50 THEN ASM_TAC
  51 THEN DISCH_THEN(LABEL_TAC"YEU")
  52 THEN REPEAT STRIP_TAC
  53 THEN FIND_ASSUM MP_TAC `packing {v,u,w:real^3}`
  54 THEN REWRITE_TAC[packing]
  55 THEN STRIP_TAC
  56 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`u:real^3`;`w:real^3`][SET_RULE`{v, u, w} u /\ {v, u, w} w`;dist])
  57 THEN REMOVE_THEN"YEU"(fun th-> MRESA_TAC th[`norm(w:real^3)`;`norm(u:real^3)`;`norm (v:real^3)`;`norm(u-w:real^3)`;`&2`;`&2`]));;
  58
  59
  60
  61
  62 end;;
  63
  64