text_formalization/local/PQCSXWG.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 (*  open Xbjrphc;; *)
  12 (* ------------------------------------------------------------------------- *)
  13 (* Suite of continuity properties for sqrt.                                  *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let CONTINUOUS_WITHIN_SQRT_COMPOSE = prove
  17  (`!f s a:real^N.
  18         (\x. lift(f x)) continuous (at a within s) /\
  19         (&0 < f a \/ !x. x IN s ==> &0 <= f x)
  20         ==> (\x. lift(sqrt(f x))) continuous (at a within s)`,
  21   REPEAT GEN_TAC THEN
  22   SUBGOAL_THEN
  23    `(\x:real^N. lift(sqrt(f x))) = (lift o sqrt o drop) o (lift o f)`
  24   SUBST1_TAC THENL [REWRITE_TAC[o_DEF; LIFT_DROP]; ALL_TAC] THEN
  25   REPEAT STRIP_TAC THEN
  26   (MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN
  27    CONJ_TAC THENL [ASM_REWRITE_TAC[o_DEF]; ALL_TAC])
  28   THENL
  29    [MATCH_MP_TAC CONTINUOUS_AT_WITHIN THEN
  30     MATCH_MP_TAC CONTINUOUS_AT_SQRT THEN ASM_REWRITE_TAC[o_DEF; LIFT_DROP];
  31     MATCH_MP_TAC CONTINUOUS_WITHIN_LIFT_SQRT THEN
  32     ASM_REWRITE_TAC[FORALL_IN_IMAGE; o_DEF; LIFT_DROP]]);;
  33
  34 let CONTINUOUS_AT_SQRT_COMPOSE = prove
  35  (`!f a:real^N.
  36         (\x. lift(f x)) continuous (at a) /\ (&0 < f a \/ !x. &0 <= f x)
  37         ==> (\x. lift(sqrt(f x))) continuous (at a)`,
  38   REPEAT GEN_TAC THEN
  39   MP_TAC(ISPECL [`f:real^N->real`; `(:real^N)`; `a:real^N`]
  40         CONTINUOUS_WITHIN_SQRT_COMPOSE) THEN
  41   REWRITE_TAC[WITHIN_UNIV; IN_UNIV]);;
  42
  43 let REAL_CONTINUOUS_WITHIN_SQRT_COMPOSE = prove
  44  (`!f s a:real^N.
  45         f real_continuous (at a within s) /\
  46         (&0 < f a \/ !x. x IN s ==> &0 <= f x)
  47         ==> (\x. sqrt(f x)) real_continuous (at a within s)`,
  48   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
  49   REWRITE_TAC[CONTINUOUS_WITHIN_SQRT_COMPOSE]);;
  50
  51 let REAL_CONTINUOUS_AT_SQRT_COMPOSE = prove
  52  (`!f a:real^N.
  53         f real_continuous (at a) /\
  54         (&0 < f a \/ !x. &0 <= f x)
  55         ==> (\x. sqrt(f x)) real_continuous (at a)`,
  56   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
  57   REWRITE_TAC[CONTINUOUS_AT_SQRT_COMPOSE]);;
  58
  59 let CONTINUOUS_WITHINREAL_SQRT_COMPOSE = prove
  60  (`!f s a. (\x. lift(f x)) continuous (atreal a within s) /\
  61            (&0 < f a \/ !x. x IN s ==> &0 <= f x)
  62            ==> (\x. lift(sqrt(f x))) continuous (atreal a within s)`,
  63   REWRITE_TAC[(* Xbjrphc. *)CONTINUOUS_CONTINUOUS_WITHINREAL] THEN
  64   REWRITE_TAC[o_DEF] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
  65   MATCH_MP_TAC CONTINUOUS_WITHIN_SQRT_COMPOSE THEN
  66   ASM_REWRITE_TAC[FORALL_IN_IMAGE; LIFT_DROP]);;
  67
  68 let CONTINUOUS_ATREAL_SQRT_COMPOSE = prove
  69  (`!f a. (\x. lift(f x)) continuous (atreal a) /\ (&0 < f a \/ !x. &0 <= f x)
  70          ==> (\x. lift(sqrt(f x))) continuous (atreal a)`,
  71   REPEAT GEN_TAC THEN
  72   MP_TAC(ISPECL [`f:real->real`; `(:real)`; `a:real`]
  73         CONTINUOUS_WITHINREAL_SQRT_COMPOSE) THEN
  74   REWRITE_TAC[WITHINREAL_UNIV; IN_UNIV]);;
  75
  76 let REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE = prove
  77  (`!f s a. f real_continuous (atreal a within s) /\
  78            (&0 < f a \/ !x. x IN s ==> &0 <= f x)
  79            ==> (\x. sqrt(f x)) real_continuous (atreal a within s)`,
  80   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
  81   REWRITE_TAC[CONTINUOUS_WITHINREAL_SQRT_COMPOSE]);;
  82
  83 let REAL_CONTINUOUS_ATREAL_SQRT_COMPOSE = prove
  84  (`!f a. f real_continuous (atreal a) /\
  85          (&0 < f a \/ !x. &0 <= f x)
  86          ==> (\x. sqrt(f x)) real_continuous (atreal a)`,
  87   REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1; o_DEF] THEN
  88   REWRITE_TAC[CONTINUOUS_ATREAL_SQRT_COMPOSE]);;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Flyspeck definition of mk_simplex (corrected).                            *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let mk_simplex1 = new_definition `mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 =
  95   (let uinv = &1 / ups_x x1 x2 x6 in
  96   let d = delta_x x1 x2 x3 x4 x5 x6 in
  97   let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
  98   let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
  99   let vcross =  (v1 - v0) cross (v2 - v0) in
 100     v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d4 % (v2 - v0)))`;;
 101
 102 let MK_SIMPLEX_TRANSLATION = prove
 103  (`!a v0 v1 v2 x1 x2 x3 x4 x5 x6.
 104         mk_simplex1 (a + v0) (a + v1) (a + v2) x1 x2 x3 x4 x5 x6 =
 105         a + mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6`,
 106   REPEAT GEN_TAC THEN REWRITE_TAC[mk_simplex1] THEN
 107   CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
 108   REWRITE_TAC[VECTOR_ARITH `(a + x) - (a + y):real^N = x - y`] THEN
 109   REWRITE_TAC[GSYM VECTOR_ADD_ASSOC]);;
 110
 111 add_translation_invariants [MK_SIMPLEX_TRANSLATION];;
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* The first part of PQCSXWG.                                                *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
 118   &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
 119   ~collinear {v0,v1,v2} /\
 120   x1 = dist(v1,v0) pow 2 /\
 121   x2 = dist(v2,v0) pow 2 /\
 122   x6 = dist(v1,v2) pow 2 /\
 123   &0 < delta_x x1 x2 x3 x4 x5 x6 /\
 124   v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
 125      (x3 = dist(v3,v0) pow 2 /\
 126       x5 = dist(v3,v1) pow 2 /\
 127       x4 = dist(v3,v2) pow 2 /\
 128       (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;
 129
 130 let PQCSXWG1 = prove
 131  (PQCSXWG1_concl,
 132   GEOM_ORIGIN_TAC `v0:real^3` THEN REPEAT GEN_TAC THEN
 133   REWRITE_TAC[mk_simplex1; VECTOR_SUB_RZERO; VECTOR_ADD_LID] THEN
 134   REPEAT LET_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
 135   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC) THEN
 136   REWRITE_TAC[GSYM CONJ_ASSOC] THEN
 137   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 138   REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
 139   REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
 140   REWRITE_TAC[CROSS_RADD; CROSS_RMUL;
 141     VECTOR_ARITH `(a + x % b + c) - b:real^N = a + (x - &1) % b + c`;
 142     VECTOR_ARITH `(a + b + x % c) - c:real^N = a + b + (x - &1) % c`] THEN
 143   SUBGOAL_THEN
 144    `!a b c. norm(a % vcross + b % v1 + c % v2:real^3) pow 2 =
 145             norm(a % vcross) pow 2 + norm(b % v1 + c % v2) pow 2`
 146    (fun th -> REWRITE_TAC[th])
 147   THENL
 148    [REPEAT GEN_TAC THEN MATCH_MP_TAC NORM_ADD_PYTHAGOREAN THEN
 149     EXPAND_TAC "vcross" THEN REWRITE_TAC[orthogonal] THEN VEC3_TAC;
 150     ALL_TAC] THEN
 151   REWRITE_TAC[CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID; real_gt] THEN
 152   REWRITE_TAC[DOT_RADD; DOT_RMUL; DOT_CROSS_SELF] THEN
 153   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN
 154   REWRITE_TAC[VEC3_RULE `v1 dot (v2 cross v) = (v1 cross v2) dot v`] THEN
 155   SUBGOAL_THEN `~(vcross:real^3 = vec 0)` ASSUME_TAC THENL
 156    [EXPAND_TAC "vcross" THEN REWRITE_TAC[CROSS_EQ_0] THEN ASM_REWRITE_TAC[];
 157     ASM_SIMP_TAC[GSYM NORM_POW_2; NORM_POS_LT; REAL_POW_LT; REAL_LT_MUL_EQ;
 158               REAL_ARITH `&0 < x * &2 * y <=> &0 < x * y`; SQRT_POS_LT]] THEN
 159   SUBGOAL_THEN `&0 < ups_x x1 x2 x6` ASSUME_TAC THENL
 160    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
 161       [Collect_geom2.NOT_COL_EQ_UPS_X_POS]) THEN
 162     MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN REWRITE_TAC[DIST_SYM];
 163     EXPAND_TAC "uinv" THEN
 164     ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]] THEN
 165   REWRITE_TAC[NORM_MUL; REAL_POW_MUL; REAL_POW2_ABS] THEN
 166   ASM_SIMP_TAC[SQRT_POW_2; REAL_LT_IMP_LE] THEN
 167   REWRITE_TAC[REAL_ARITH `x * &2 pow 2 * y = &4 * x * y`] THEN
 168   REWRITE_TAC[NORM_POW_2; VECTOR_ARITH
 169    `(a + b) dot (a + b:real^3) = a dot a + b dot b + &2 * a dot b`] THEN
 170   REWRITE_TAC[DOT_LMUL] THEN REWRITE_TAC[DOT_RMUL] THEN
 171   ONCE_REWRITE_TAC[REAL_ARITH
 172    `x3:real = a + b /\ x5 = a + c /\ x4 = a + d <=>
 173     x3 = a + b /\ x3 - x5 = b - c /\ x3 - x4 = b - d`] THEN
 174   REWRITE_TAC[REAL_ARITH
 175    `(b * b * x + c * c * y + &2 * b * c * z) -
 176     ((b - &1) * (b - &1) * x + c * c * y + &2 * (b - &1) * c * z) =
 177     (&2 * b - &1) * x + &2 * c * z /\
 178     (b * b * x + c * c * y + &2 * b * c * z) -
 179     (b * b * x +  (c - &1) * (c - &1) * y + &2 * b * (c - &1) * z) =
 180     (&2 * c - &1) * y + &2 * b * z`] THEN
 181   RULE_ASSUM_TAC(REWRITE_RULE[DIST_0]) THEN
 182   ASM_REWRITE_TAC[GSYM NORM_POW_2; REAL_ARITH
 183    `x = (&2 * b - &1) * y + &2 * c * z <=>
 184     b * y + c * z = (y + x) / &2`] THEN
 185   EXPAND_TAC "vcross" THEN REWRITE_TAC[NORM_POW_2; DOT_CROSS] THEN
 186   ASM_REWRITE_TAC[GSYM NORM_POW_2] THEN
 187   SUBST1_TAC(VECTOR_ARITH `(v2:real^3) dot v1 = v1 dot v2`) THEN
 188   REWRITE_TAC[GSYM REAL_POW_2] THEN
 189   SUBGOAL_THEN `(v1:real^3) dot v2 = ((x1 + x2) - x6) / &2` SUBST1_TAC THENL
 190    [MAP_EVERY EXPAND_TAC ["x1"; "x2"; "x6"] THEN
 191     REWRITE_TAC[dist; NORM_POW_2; DOT_RSUB; DOT_LSUB] THEN
 192     REWRITE_TAC[DOT_SYM] THEN REAL_ARITH_TAC;
 193     ALL_TAC] THEN
 194   REWRITE_TAC[REAL_ARITH
 195    `(&4 * u pow 2 * d) * x + (u * e) * (u * e) * y + (u * f) * (u * f) * z +
 196     &2 * (u * e) * (u * f) * j =
 197     u pow 2 * (&4 * d * x + e pow 2 * y + f pow 2 * z + &2 * e * f * j)`] THEN
 198   REWRITE_TAC[REAL_ARITH
 199    `(u * d) * x + (u * e) * y:real = z <=> u * (d * x + e * y) = z`] THEN
 200   EXPAND_TAC "uinv" THEN MATCH_MP_TAC(REAL_FIELD
 201    `&0 < u /\
 202     u pow 2 * x = y /\ u * a = b /\ u * c = d
 203     ==> x = (&1 / u) pow 2 * y /\
 204         (&1 / u) * b = a /\ (&1 / u) * d = c`) THEN
 205   ASM_REWRITE_TAC[] THEN MAP_EVERY EXPAND_TAC ["uinv"; "d"; "d5"; "d4"] THEN
 206   REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP REAL_LT_IMP_NZ)) THEN
 207   REWRITE_TAC[Nonlin_def.delta_x5; Nonlin_def.delta_x4] THEN
 208   REWRITE_TAC[Sphere.ups_x; Sphere.delta_x] THEN CONV_TAC REAL_RING);;
 209
 210 (* ------------------------------------------------------------------------- *)
 211 (* The continuity part.                                                      *)
 212 (* ------------------------------------------------------------------------- *)
 213
 214 let CONTINUOUS_MK_SIMPLEX_WITHINREAL = prove
 215  (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 s a.
 216         ~(ups_x (x1 a) (x2 a) (x6 a) = &0) /\
 217         &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
 218         v0 continuous (atreal a within s) /\
 219         v1 continuous (atreal a within s) /\
 220         v2 continuous (atreal a within s) /\
 221         x1 real_continuous (atreal a within s) /\
 222         x2 real_continuous (atreal a within s) /\
 223         x3 real_continuous (atreal a within s) /\
 224         x4 real_continuous (atreal a within s) /\
 225         x5 real_continuous (atreal a within s) /\
 226         x6 real_continuous (atreal a within s)
 227         ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
 228                             (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
 229             continuous (atreal a within s)`,
 230   let POLY_CONT_TAC =
 231     REPEAT((MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE
 232             MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE
 233             MATCH_MP_TAC REAL_CONTINUOUS_SUB) THEN CONJ_TAC) THEN
 234     ASM_SIMP_TAC[REAL_CONTINUOUS_NEG; REAL_CONTINUOUS_CONST] in
 235   REPEAT STRIP_TAC THEN REWRITE_TAC[mk_simplex1] THEN
 236   CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
 237   MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_REWRITE_TAC[] THEN
 238   MATCH_MP_TAC CONTINUOUS_MUL THEN CONJ_TAC THENL
 239    [REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1; real_div; REAL_MUL_LID] THEN
 240     MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
 241     ASM_REWRITE_TAC[] THEN REWRITE_TAC[Sphere.ups_x] THEN POLY_CONT_TAC;
 242     ALL_TAC] THEN
 243   MATCH_MP_TAC CONTINUOUS_ADD THEN CONJ_TAC THENL
 244    [MATCH_MP_TAC CONTINUOUS_MUL THEN
 245     ASM_SIMP_TAC[CONTINUOUS_CROSS; CONTINUOUS_SUB] THEN
 246     REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
 247     MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
 248     MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE THEN
 249     ASM_REWRITE_TAC[] THEN REWRITE_TAC[Sphere.delta_x] THEN POLY_CONT_TAC;
 250     MATCH_MP_TAC CONTINUOUS_ADD THEN
 251     REWRITE_TAC[Nonlin_def.delta_x5; Nonlin_def.delta_x4] THEN
 252     CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_MUL THEN
 253     ASM_SIMP_TAC[CONTINUOUS_SUB; GSYM REAL_CONTINUOUS_CONTINUOUS1] THEN
 254     POLY_CONT_TAC]);;
 255
 256 let PQCSXWG2_WITHINREAL = prove
 257  (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 s a.
 258         ~collinear {v0 a,v1 a,v2 a} /\
 259         x1 a = dist(v1 a,v0 a) pow 2 /\
 260         x2 a = dist(v2 a,v0 a) pow 2 /\
 261         x6 a = dist(v1 a,v2 a) pow 2 /\
 262         &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
 263         v0 continuous (atreal a within s) /\
 264         v1 continuous (atreal a within s) /\
 265         v2 continuous (atreal a within s) /\
 266         x1 real_continuous (atreal a within s) /\
 267         x2 real_continuous (atreal a within s) /\
 268         x3 real_continuous (atreal a within s) /\
 269         x4 real_continuous (atreal a within s) /\
 270         x5 real_continuous (atreal a within s) /\
 271         x6 real_continuous (atreal a within s)
 272         ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
 273                             (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
 274             continuous (atreal a within s)`,
 275   REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 276   MATCH_MP_TAC CONTINUOUS_MK_SIMPLEX_WITHINREAL THEN
 277   ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
 278       [Collect_geom2.NOT_COL_EQ_UPS_X_POS]) THEN
 279   REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN REWRITE_TAC[DIST_SYM] THEN
 280   REAL_ARITH_TAC);;
 281
 282 let PQCSXWG2_ATREAL = prove
 283  (`!v0 v1 v2 x1 x2 x3 x4 x5 x6 a.
 284         ~collinear {v0 a,v1 a,v2 a} /\
 285         x1 a = dist(v1 a,v0 a) pow 2 /\
 286         x2 a = dist(v2 a,v0 a) pow 2 /\
 287         x6 a = dist(v1 a,v2 a) pow 2 /\
 288         &0 < delta_x (x1 a) (x2 a) (x3 a) (x4 a) (x5 a) (x6 a) /\
 289         v0 continuous (atreal a) /\
 290         v1 continuous (atreal a) /\
 291         v2 continuous (atreal a) /\
 292         x1 real_continuous (atreal a) /\
 293         x2 real_continuous (atreal a) /\
 294         x3 real_continuous (atreal a) /\
 295         x4 real_continuous (atreal a) /\
 296         x5 real_continuous (atreal a) /\
 297         x6 real_continuous (atreal a)
 298         ==> (\t. mk_simplex1 (v0 t) (v1 t) (v2 t)
 299                             (x1 t) (x2 t) (x3 t) (x4 t) (x5 t) (x6 t))
 300             continuous (atreal a)`,
 301   ONCE_REWRITE_TAC[GSYM WITHINREAL_UNIV] THEN
 302   REWRITE_TAC[PQCSXWG2_WITHINREAL]);;
 303
 304 let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
 305   &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
 306   ~collinear {v0,v1,v2} /\
 307   x1 = dist(v1,v0) pow 2 /\
 308   x2 = dist(v2,v0) pow 2 /\
 309   x6 = dist(v1,v2) pow 2 /\
 310   &0 < delta_x x1 x2 x3 x4 x5 x6 /\
 311   v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
 312      (\q. mk_simplex1 v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
 313
 314 let PQCSXWG2 = prove
 315  (PQCSXWG2_concl,
 316   REPEAT STRIP_TAC THEN MATCH_MP_TAC PQCSXWG2_ATREAL THEN
 317   ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST; CONTINUOUS_CONST;
 318                   REAL_CONTINUOUS_AT_ID]);;
 319
 320 end;;