legacy/oldlocal/PQCSXWG_old.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Appendix                                                          *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Author: John Harrison                                                      *)
   6 (* Date: 2013-07-12                                                           *)
   7 (* ========================================================================== *)
   8
   9 module Pqcsxwg = struct
  10
  11
  12 let mk_simplex1 = new_definition `mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 =
  13   (let uinv = &1 / ups_x x1 x2 x6 in
  14   let d = delta_x x1 x2 x3 x4 x5 x6 in
  15   let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
  16   let d6 = delta_x4 x1 x2 x3 x4 x5 x6 in
  17   let vcross =  (v1 - v0) cross (v2 - v0) in
  18     v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d6 % (v2 - v0)))`;;
  19
  20 let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
  21   &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
  22   ~collinear {v0,v1,v2} /\
  23   x1 = dist(v1,v0) pow 2 /\
  24   x2 = dist(v2,v0) pow 2 /\
  25   x6 = dist(v1,v2) pow 2 /\
  26   &0 < delta_x x1 x2 x3 x4 x5 x6 /\
  27   v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
  28      (x3 = dist(v3,v0) pow 2 /\
  29       x5 = dist(v3,v1) pow 2 /\
  30       x4 = dist(v3,v2) pow 2 /\
  31       (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;
  32
  33 let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
  34   &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
  35   ~collinear {v0,v1,v2} /\
  36   x1 = dist(v1,v0) pow 2 /\
  37   x2 = dist(v2,v0) pow 2 /\
  38   x6 = dist(v1,v2) pow 2 /\
  39   &0 < delta_x x1 x2 x3 x4 x5 x6 /\
  40   v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
  41      (\q. mk_simplex1 v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* The main result.                                                          *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 let MK_SIMPLEX_TRANSLATION = prove
  48  (`!a v0 v1 v2 x1 x2 x3 x4 x5 x6.
  49         mk_simplex1 (a + v0) (a + v1) (a + v2) x1 x2 x3 x4 x5 x6 =
  50         a + mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6`,
  51   REPEAT GEN_TAC THEN REWRITE_TAC[mk_simplex1] THEN
  52   CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
  53   REWRITE_TAC[VECTOR_ARITH `(a + x) - (a + y):real^N = x - y`] THEN
  54   REWRITE_TAC[GSYM VECTOR_ADD_ASSOC]);;
  55
  56 add_translation_invariants [MK_SIMPLEX_TRANSLATION];;
  57
  58 let PQCSXWG1 = prove
  59  (PQCSXWG1_concl,
  60   GEOM_ORIGIN_TAC `v0:real^3` THEN REPEAT GEN_TAC THEN
  61   REWRITE_TAC[mk_simplex1; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
  62   REPEAT LET_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
  63   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC) THEN
  64   REWRITE_TAC[GSYM CONJ_ASSOC] THEN
  65   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  66   REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
  67   REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
  68   REWRITE_TAC[CROSS_RADD; CROSS_RMUL;
  69     VECTOR_ARITH `(a + x % b + c) - b:real^N = a + (x - &1) % b + c`;
  70     VECTOR_ARITH `(a + b + x % c) - c:real^N = a + b + (x - &1) % c`] THEN
  71   SUBGOAL_THEN
  72    `!a b c. norm(a % vcross + b % v1 + c % v2:real^3) pow 2 =
  73             norm(a % vcross) pow 2 + norm(b % v1 + c % v2) pow 2`
  74    (fun th -> REWRITE_TAC[th])
  75   THENL
  76    [REPEAT GEN_TAC THEN MATCH_MP_TAC NORM_ADD_PYTHAGOREAN THEN
  77     EXPAND_TAC "vcross" THEN REWRITE_TAC[orthogonal] THEN VEC3_TAC;
  78     ALL_TAC] THEN
  79   REWRITE_TAC[CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID; real_gt] THEN
  80   REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_CROSS_SELF] THEN
  81   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN
  82   REWRITE_TAC[VEC3_RULE `v1 dot (v2 cross v) = (v1 cross v2) dot v`] THEN
  83   SUBGOAL_THEN `~(vcross:real^3 = vec 0)` ASSUME_TAC THENL
  84    [EXPAND_TAC "vcross" THEN REWRITE_TAC[CROSS_EQ_0] THEN ASM_REWRITE_TAC[];
  85     ASM_SIMP_TAC[GSYM NORM_POW_2; NORM_POS_LT; REAL_POW_LT; REAL_LT_MUL_EQ;
  86               REAL_ARITH `&0 < x * &2 * y <=> &0 < x * y`; SQRT_POS_LT]] THEN
  87   SUBGOAL_THEN `&0 < ups_x x1 x2 x6` ASSUME_TAC THENL
  88    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
  89       [Collect_geom2.NOT_COL_EQ_UPS_X_POS]) THEN
  90     MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN REWRITE_TAC[DIST_SYM];
  91     EXPAND_TAC "uinv" THEN
  92     ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]] THEN
  93   REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS] THEN
  94   ASM_SIMP_TAC[SQRT_POW_2; REAL_LT_IMP_LE] THEN
  95   REWRITE_TAC[REAL_ARITH `x * &2 pow 2 * y = &4 * x * y`] THEN
  96   REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
  97    `(a + b) dot (a + b:real^3) = a dot a + b dot b + &2 * a dot b`] THEN
  98   REWRITE_TAC[DOT_LMUL] THEN REWRITE_TAC[DOT_RMUL] THEN
  99   ONCE_REWRITE_TAC[REAL_ARITH
 100    `x3:real = a + b /\ x5 = a + c /\ x4 = a + d <=>
 101     x3 = a + b /\ x3 - x5 = b - c /\ x3 - x4 = b - d`] THEN
 102   REWRITE_TAC[REAL_ARITH
 103    `(b * b * x + c * c * y + &2 * b * c * z) -
 104     ((b - &1) * (b - &1) * x + c * c * y + &2 * (b - &1) * c * z) =
 105     (&2 * b - &1) * x + &2 * c * z /\
 106     (b * b * x + c * c * y + &2 * b * c * z) -
 107     (b * b * x +  (c - &1) * (c - &1) * y + &2 * b * (c - &1) * z) =
 108     (&2 * c - &1) * y + &2 * b * z`] THEN
 109   RULE_ASSUM_TAC(REWRITE_RULE[DIST_0]) THEN
 110   ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_ARITH
 111    `x = (&2 * b - &1) * y + &2 * c * z <=>
 112     b * y + c * z = (y + x) / &2`] THEN
 113   EXPAND_TAC "vcross" THEN REWRITE_TAC[NORM_POW_2; DOT_CROSS] THEN
 114   ASM_REWRITE_TAC[GSYM NORM_POW_2] THEN
 115   SUBST1_TAC(VECTOR_ARITH `(v2:real^3) dot v1 = v1 dot v2`) THEN
 116   REWRITE_TAC[GSYM REAL_POW_2] THEN
 117   SUBGOAL_THEN `(v1:real^3) dot v2 = ((x1 + x2) - x6) / &2` SUBST1_TAC THENL
 118    [MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN
 119     REWRITE_TAC[dist; NORM_POW_2; DOT_RSUB; DOT_LSUB] THEN
 120     REWRITE_TAC[DOT_SYM] THEN REAL_ARITH_TAC;
 121     ALL_TAC] THEN
 122   REWRITE_TAC[REAL_ARITH
 123    `(&4 * u pow 2 * d) * x + (u * e) * (u * e) * y + (u * f) * (u * f) * z +
 124     &2 * (u * e) * (u * f) * j =
 125     u pow 2 * (&4 * d * x + e pow 2 * y + f pow 2 * z + &2 * e * f * j)`] THEN
 126   REWRITE_TAC[REAL_ARITH
 127    `(u * d) * x + (u * e) * y:real = z <=> u * (d * x + e * y) = z`] THEN
 128   EXPAND_TAC "uinv" THEN MATCH_MP_TAC(REAL_FIELD
 129    `&0 < u /\
 130     u pow 2 * x = y /\ u * a = b /\ u * c = d
 131     ==> x = (&1 / u) pow 2 * y /\
 132         (&1 / u) * b = a /\ (&1 / u) * d = c`) THEN
 133   ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["uinv"; "d"; "d5"; "d6"] THEN
 134   REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP REAL_LT_IMP_NZ)) THEN
 135   REWRITE_TAC[Nonlin_def.delta_x5; Nonlin_def.delta_x4] THEN
 136   REWRITE_TAC[Sphere.ups_x; Sphere.delta_x] THEN CONV_TAC REAL_RING);;
 137
 138 end;;