text_formalization/jordan/real_ext.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Jordan                                                               *)
   6 (* Copied from HOL Light jordan directory *)
   7 (* Author: Thomas C. Hales                                                    *)
   8 (* Date: 2010-07-08                                                           *)
   9 (* ========================================================================== *)
  10
  11 module Real_ext = struct
  12
  13 open Parse_ext_override_interface;;
  14 (* open Tactics_jordan;; *)
  15
  16
  17
  18 (* ------------------------------------------------------------------ *)
  19 (*   Theorems that construct and propagate equality and inequality    *)
  20 (* ------------------------------------------------------------------ *)
  21
  22 (* ------------------------------------------------------------------ *)
  23 (* Propagation of =EQUAL=  *)
  24 (* ------------------------------------------------------------------ *)
  25
  26 unambiguous_interface();;
  27 prioritize_num();;
  28
  29 let REAL_LE = REAL_OF_NUM_LE;;
  30
  31 let pow = real_pow;;
  32
  33 let REAL_LE_POW_2 = Collect_geom.REAL_LE_POW_2;;
  34
  35
  36 let REAL_INV2 = prove(
  37   `(inv(&. 2)*(&. 2) = (&.1)) /\ ((&. 2)*inv(&. 2) = (&.1))`,
  38   SUBGOAL_THEN `~((&.2) = (&.0))` MP_TAC
  39 THENL[
  40   REAL_ARITH_TAC;
  41   SIMP_TAC[REAL_MUL_RINV;REAL_MUL_LINV]]);;
  42
  43
  44
  45
  46 let REAL_MUL_LTIMES = prove (`!x a b. (x*.a = x*.b) ==> (~(x=(&.0))) ==> (a =b)`,
  47    MESON_TAC[REAL_EQ_MUL_LCANCEL]);;
  48
  49 let REAL_MUL_RTIMES = prove (`!x a b. (a*.x = b*.x) ==> (~(x=(&.0))) ==> (a =b)`,
  50    MESON_TAC[REAL_EQ_MUL_RCANCEL]);;
  51
  52 let REAL_PROP_EQ_LMUL = REAL_MUL_LTIMES;;
  53 let REAL_PROP_EQ_RMUL = REAL_MUL_RTIMES;;
  54
  55 let REAL_PROP_EQ_LMUL_' = REAL_EQ_MUL_LCANCEL (* |- !x y z. (x * y = x * z) = (x = &0) \/ (y = z) *);;
  56 let REAL_PROP_EQ_RMUL_' = REAL_EQ_MUL_LCANCEL (* |- !x y z. (x * z = y * z) = (x = y) \/ (z = &0) *);;
  57 (* see also minor variations REAL_LT_LMUL_EQ, REAL_LT_RMUL_EQ *)
  58
  59 let REAL_PROP_EQ_SQRT = SQRT_INJ;; (* |- !x y. &0 <= x /\ &0 <= y ==> ((sqrt x = sqrt y) = x = y) *)
  60
  61 (* ------------------------------------------------------------------ *)
  62 (* Construction of <=. *)
  63 (* ------------------------------------------------------------------ *)
  64 let REAL_MK_LE_SQUARE = Collect_geom.REAL_LE_SQUARE_POW ;; (*  |- !x. &0 <= x pow 2 *)
  65
  66 (* ------------------------------------------------------------------ *)
  67 (* Propagation of <=. *)
  68 (* ------------------------------------------------------------------ *)
  69
  70 let REAL_MUL_LTIMES_LE = prove (`!x a b. (x*.a <=. x*.b) ==> (&.0 < x) ==> (a <=. b)`,
  71    MESON_TAC[REAL_LE_LMUL_EQ]);;
  72   (* virtually identical to REAL_LE_LCANCEL_IMP, REAL_LE_LMUL_EQ *)
  73
  74 let REAL_MUL_RTIMES_LE = prove (`!x a b. (a*.x <=. b*.x) ==> (&.0 < x) ==> (a <=. b)`,
  75    MESON_TAC[REAL_LE_RMUL_EQ]);;
  76   (* virtually identical to REAL_LE_RCANCEL_IMP, REAL_LE_RMUL_EQ *)
  77
  78 let REAL_PROP_LE_LCANCEL = REAL_MUL_LTIMES_LE;;
  79 let REAL_PROP_LE_RCANCEL = REAL_MUL_RTIMES_LE;;
  80 let REAL_PROP_LE_LMUL = REAL_LE_LMUL (* |- !x y z. &0 <= x /\ y <= z ==> x * y <= x * z *);;
  81 let REAL_PROP_LE_RMUL = REAL_LE_RMUL (* |- !x y z. x <= y /\ &0 <= z ==> x * z <= y * z *);;
  82 let REAL_PROP_LE_LRMUL = REAL_LE_MUL2;; (* |- !w x y z. &0 <= w /\ w <= x /\ &0 <= y /\ y <= z ==> w * y <= x * z *)
  83 let REAL_PROP_LE_POW = REAL_POW_LE2;; (* 2010-07-08 thales: POW_LE;; *) (* |- !n x y. &0 <= x /\ x <= y ==> x pow n <= y pow n *)
  84 let REAL_PROP_LE_SQRT = SQRT_MONO_LE_EQ;; (* |- !x y. &0 <= x /\ &0 <= y ==> (sqrt x <= sqrt y = x <= y) *)
  85
  86 (* ------------------------------------------------------------------ *)
  87 (* Construction of LT *)
  88 (* ------------------------------------------------------------------ *)
  89
  90 let REAL_MK_LT_SQUARE  = REAL_LT_SQUARE;; (* |- !x. &0 < x * x = ~(x = &0) *)
  91
  92 (* ------------------------------------------------------------------ *)
  93 (* Propagation of LT *)
  94 (* ------------------------------------------------------------------ *)
  95
  96 let REAL_PROP_LT_LCANCEL = REAL_LT_LCANCEL_IMP (* |- !x y z. &0 < x /\ x * y < x * z ==> y < z *);;
  97 let REAL_PROP_LT_RCANCEL = REAL_LT_RCANCEL_IMP (* |- !x y z. &0 < z /\ x * z < y * z ==> x < y *);;
  98 let REAL_PROP_LT_LMUL = REAL_LT_LMUL (* |- !x y z. &0 < x /\ y < z ==> x * y < x * z *);;
  99 let REAL_PROP_LT_RMUL = REAL_LT_RMUL (* |- !x y z. x < y /\ &0 < z ==> x * z < y * z *);;
 100 (* minor variation REAL_LT_LMUL_IMP, REAL_LT_RMUL_IMP *)
 101
 102 let REAL_PROP_LT_LRMUL= REAL_LT_MUL2;; (* |- !w x y z. &0 <= w /\ w < x /\ &0 <= y /\ y < z ==> w * y < x * z *)
 103 let REAL_PROP_LT_SQRT = SQRT_MONO_LT_EQ;; (* |- !x y. &0 <= x /\ &0 <= y ==> (sqrt x < sqrt y = x < y) *)
 104
 105 (* ------------------------------------------------------------------ *)
 106 (* Constructors of Non-negative *)
 107 (* ------------------------------------------------------------------ *)
 108
 109 let REAL_MK_NN_SQUARE = REAL_LE_SQUARE;; (* |- !x. &0 <= x * x *)
 110 let REAL_MK_NN_ABS = REAL_ABS_POS;; (* 2010 *) (* |- !x. &0 <= abs x *)
 111
 112 (* moved here from float.hl *)
 113
 114 (* from 778 *)
 115
 116
 117 let REAL_LE_LMUL_LOCAL = prove(
 118   `!x y z. &0 < x ==> ((x * y) <= (x * z) <=> y <= z)`,
 119   REPEAT GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN
 120   AP_TERM_TAC THEN MATCH_MP_TAC REAL_LT_LMUL_EQ THEN ASM_REWRITE_TAC[]);;
 121
 122
 123 let ABS_TRIANGLE = prove(
 124   `!x y. abs(x + y) <= abs(x) + abs(y)`,
 125   REPEAT GEN_TAC THEN REWRITE_TAC[real_abs] THEN
 126   REPEAT COND_CASES_TAC THEN
 127   REWRITE_TAC[REAL_NEG_ADD; REAL_LE_REFL; REAL_LE_LADD; REAL_LE_RADD] THEN
 128   ASM_REWRITE_TAC[GSYM REAL_NEG_ADD; REAL_LE_NEGL; REAL_LE_NEGR] THEN
 129   RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
 130   TRY(MATCH_MP_TAC REAL_LT_IMP_LE) THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN
 131   TRY(UNDISCH_TAC `(x + y) < &0`) THEN SUBST1_TAC(SYM(SPEC `&0` REAL_ADD_LID))
 132   THEN REWRITE_TAC[REAL_NOT_LT] THEN
 133   MAP_FIRST MATCH_MP_TAC [REAL_LT_ADD2; REAL_LE_ADD2] THEN
 134   ASM_REWRITE_TAC[]);;
 135
 136 let REAL_LE_LMUL_IMP = prove(
 137   `!x y z. &0 <= x /\ y <= z ==> (x * y) <= (x * z)`,
 138   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 139   DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THENL
 140    [FIRST_ASSUM(fun th -> ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL_LOCAL th]);
 141     FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
 142     MATCH_ACCEPT_TAC REAL_LE_REFL]);;
 143
 144
 145 (*   from ? *)
 146
 147 let ABS_POS = prove(
 148   `!x. &0 <= abs(x)`,
 149   GEN_TAC THEN ASM_CASES_TAC `&0 <= x` THENL
 150    [ALL_TAC;
 151     MP_TAC(SPEC `x:real` REAL_LE_NEGTOTAL) THEN ASM_REWRITE_TAC[] THEN
 152     DISCH_TAC] THEN
 153   ASM_REWRITE_TAC[real_abs]);;
 154
 155
 156 let REAL_PROP_LE_LABS = prove(
 157   `!x y z. (y <=. z) ==> ((abs x)* y <=. (abs x) *z)`,(SIMP_TAC[REAL_LE_LMUL_IMP;ABS_POS]));;
 158
 159 let REAL_LE_RMUL_IMP = prove(
 160   `!x y z. &0 <= x /\ y <= z ==> (y * x) <= (z * x)`,
 161   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_LE_LMUL_IMP);;
 162
 163
 164 (* ------------------------------------------------------------------ *)
 165 (* Propagation of Non-negative *)
 166 (* ------------------------------------------------------------------ *)
 167
 168 let REAL_PROP_NN_POS = prove(`! x y. x<. y ==> x <= y`,MESON_TAC[REAL_LT_LE]);;
 169 let REAL_PROP_NN_ADD2 = REAL_LE_ADD (* |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x + y *);;
 170 let REAL_PROP_NN_DOUBLE = REAL_LE_DOUBLE (* |- !x. &0 <= x + x <=> &0 <= x *);;
 171 let REAL_PROP_NN_RCANCEL= prove(`!x y. &.0 <. x /\ (&.0) <=. y*.x ==> ((&.0) <=. y)`,
 172   MESON_TAC[REAL_PROP_LE_RCANCEL;REAL_MUL_LZERO]);;
 173 let REAL_PROP_NN_LCANCEL= prove(`!x y. &.0 <. x /\ (&.0) <=. x*.y ==> ((&.0) <=. y)`,
 174   MESON_TAC[REAL_PROP_LE_LCANCEL;REAL_MUL_RZERO]);;
 175 let REAL_PROP_NN_MUL2 = REAL_LE_MUL (* |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x * y *);;
 176 let REAL_PROP_NN_POW = REAL_POW_LE (* |- !x n. &0 <= x ==> &0 <= x pow n *);;
 177 let REAL_PROP_NN_SQUARE = Collect_geom.REAL_LE_POW_2;; (* |- !x. &0 <= x pow 2 *)
 178 let REAL_PROP_NN_SQRT = SQRT_POS_LE;; (* |- !x. &0 <= x ==> &0 <= sqrt x *)
 179 let REAL_PROP_NN_INV = REAL_LE_INV_EQ (* |- !x. &0 <= inv x = &0 <= x *);;
 180 let REAL_PROP_NN_SIN = SIN_POS_PI_LE;; (* |- !x. &0 <= x /\ x <= pi ==> &0 <= sin x *)
 181 let REAL_PROP_NN_ATN = ATN_POS_LE;; (* |- &0 <= atn x = &0 <= x *)
 182
 183
 184 (* ------------------------------------------------------------------ *)
 185 (* Constructor of POS *)
 186 (* ------------------------------------------------------------------ *)
 187
 188 let REAL_MK_POS_ABS = REAL_ABS_NZ (* |- !x. ~(x = &0) = &0 < abs x *);;
 189 let REAL_MK_POS_EXP = REAL_EXP_POS_LT;; (* |- !x. &0 < exp x *)
 190
 191 (* let REAL_MK_POS_LN = LN_POS_LT;; (* |- !x. &1 < x ==> &0 < ln x *)  *)
 192
 193 let REAL_MK_POS_PI = PI_POS;; (* |- &0 < pi *)
 194
 195
 196 (* ------------------------------------------------------------------ *)
 197 (* Propagation of POS *)
 198 (* ------------------------------------------------------------------ *)
 199
 200 let REAL_PROP_POS_ADD2 = REAL_LT_ADD (* |- !x y. &0 < x /\ &0 < y ==> &0 < x + y *);;
 201 let REAL_PROP_POS_LADD = REAL_LET_ADD (* |- !x y. &0 <= x /\ &0 < y ==> &0 < x + y *);;
 202 let REAL_PROP_POS_RADD = REAL_LTE_ADD (* |- !x y. &0 < x /\ &0 <= y ==> &0 < x + y *);;
 203 let REAL_PROP_POS_LMUL = REAL_LT_MUL_EQ;; (* REAL_LT_LMUL_0;; *) (* |- !x y. &0 < x ==> (&0 < x * y = &0 < y) *)
 204 let REAL_PROP_POS_RMUL = REAL_LT_MUL_EQ;; (* REAL_LT_RMUL_0;; *) (* |- !x y. &0 < y ==> (&0 < x * y = &0 < x) *)
 205 let REAL_PROP_POS_MUL2 = REAL_LT_MUL (* |- !x y. &0 < x /\ &0 < y ==> &0 < x * y *);;
 206 let REAL_PROP_POS_SQRT = SQRT_POS_LT;; (* |- !x. &0 < x ==> &0 < sqrt x *)
 207 let REAL_PROP_POS_POW =  REAL_POW_LT (*  |- !x n. &0 < x ==> &0 < x pow n *);;
 208 let REAL_PROP_POS_INV = REAL_LT_INV (* |- !x. &0 < x ==> &0 < inv x *);;
 209 let REAL_PROP_POS_SIN = SIN_POS_PI;; (*  |- !x. &0 < x /\ x < pi ==> &0 < sin x *)
 210 let REAL_PROP_POS_TAN = TAN_POS_PI2;; (* |- !x. &0 < x /\ x < pi / &2 ==> &0 < tan x *)
 211 let REAL_PROP_POS_ATN = ATN_POS_LT;; (* |- &0 < atn x = &0 < x *)
 212
 213 (* ------------------------------------------------------------------ *)
 214 (* Construction of NZ *)
 215 (* ------------------------------------------------------------------ *)
 216
 217 (* renamed from REAL_MK_NZ_OF_POS *)
 218 let REAL_MK_NZ_POS = REAL_POS_NZ (* |- !x. &0 < x ==> ~(x = &0) *);;
 219 let REAL_MK_NZ_EXP = REAL_EXP_NZ;; (*  |- !x. ~(exp x = &0) *)
 220
 221 (* ------------------------------------------------------------------ *)
 222 (* Propagation of NZ *)
 223 (* ------------------------------------------------------------------ *)
 224
 225 (* renamed from REAL_ABS_NZ, moved from float.ml *)
 226 let REAL_PROP_NZ_ABS =  prove(`!x. (~(x = (&.0))) ==> (~(abs(x) = (&.0)))`,
 227     REWRITE_TAC[REAL_ABS_ZERO]);;
 228 let REAL_PROP_NZ_POW = REAL_POW_NZ (*  |- !x n. ~(x = &0) ==> ~(x pow n = &0) *);;
 229
 230 (*
 231 let REAL_PROP_NZ_INV = REAL_INV_NZ;; (* |- !x. ~(x = &0) ==> ~(inv x = &0) *)
 232 *)
 233
 234 (* ------------------------------------------------------------------ *)
 235 (* Propagation of ZERO *)
 236 (* ------------------------------------------------------------------ *)
 237
 238 let REAL_PROP_ZERO_ABS = REAL_ABS_ZERO (* |- !x. (abs x = &0) = x = &0); *);;
 239 (* let REAL_PROP_ZERO_NEG = REAL_NEG_EQ_0 ;; (*  |- !x. (--x = &0) = x = &0 *) *)
 240 let REAL_PROP_ZERO_INV = REAL_INV_EQ_0 (* |- !x. (inv x = &0) = x = &0 *);;
 241 (* let REAL_PROP_ZERO_NEG = REAL_NEG_EQ0;; (* |- !x. (--x = &0) = x = &0 *) *)
 242 (* let REAL_PROP_ZERO_SUMSQ = REAL_SUMSQ;; (* |- !x y. (x * x + y * y = &0) = (x = &0) /\ (y = &0) *) *)
 243 let REAL_PROP_ZERO_POW = REAL_POW_EQ_0;; (* |- !x n. (x pow n = &0) = (x = &0) /\ ~(n = 0) *)
 244 let REAL_PROP_ZERO_SQRT = SQRT_EQ_0;; (* |- !x. &0 <= x ==> (x / sqrt x = sqrt x) *)
 245
 246 (* ------------------------------------------------------------------ *)
 247 (* Special values of functions *)
 248 (* ------------------------------------------------------------------ *)
 249
 250 let REAL_SV_LADD_0 = REAL_ADD_LID (* |- !x. &0 + x = x); *);;
 251 let REAL_SV_INV_0 = REAL_INV_0 (*  |- inv (&0) = &0 *);;
 252 let REAL_SV_RMUL_0 = REAL_MUL_RZERO (* |- !x. x * &0 = &0 *);;
 253 let REAL_SV_LMUL_0 = REAL_MUL_LZERO (* |- !x. &0 * x = &0 *);;
 254 let REAL_SV_NEG_0 = REAL_NEG_0 (*  |- -- &0 = &0 *);;
 255 let REAL_SV_ABS_0 = REAL_ABS_0 (* |- abs (&0) = &0 *);;
 256 let REAL_SV_EXP_0 = REAL_EXP_0;; (* |- exp (&0) = &1 *)
 257 (* let REAL_SV_LN_1 = LN_1;; (* |- ln (&1) = &0 *) *)
 258 let REAL_SV_SQRT_0 = SQRT_0;; (* |- sqrt (&0) = &0 *)
 259 let REAL_SV_TAN_0 = TAN_0;; (*  |- tan (&0) = &0 *)
 260 let REAL_SV_TAN_PI = TAN_PI;; (* |- tan pi = &0 *)
 261
 262 (* ------------------------------------------------------------------ *)
 263 (* A tactic that multiplies a real on the left *)
 264 (* ------------------------------------------------------------------ *)
 265
 266 (**
 267 #g `a:real = b:real`;;
 268 #e (REAL_LMUL_TAC `c:real`);;
 269 it : goalstack = 2 subgoals (2 total)
 270 `~(c = &0)`
 271
 272 `c * a = c * b`
 273
 274  0 [`~(c = &0)`]
 275 #
 276 **)
 277 (* ------------------------------------------------------------------ *)
 278
 279
 280
 281 let REAL_LMUL_TAC t =
 282   let REAL_MUL_LTIMES =
 283         prove ((`!x a b.
 284         (((~(x=(&0)) ==> (x*a = x*b)) /\ ~(x=(&0))) ==>  (a = b))`),
 285                 MESON_TAC[REAL_EQ_MUL_LCANCEL]) in
 286    (MATCH_MP_TAC (SPEC t REAL_MUL_LTIMES))
 287    THEN CONJ_TAC
 288    THENL [DISCH_TAC; ALL_TAC];;
 289
 290 (* ------------------------------------------------------------------ *)
 291 (* Right multiply by a real *)
 292 (* ------------------------------------------------------------------ *)
 293
 294 let REAL_RMUL_TAC t =
 295   let REAL_MUL_RTIMES =
 296         prove (`!x a b.
 297                 ((~(x=(&0))==>(a*x = b*x)) /\ ~(x=(&0))) ==>  (a = b)`,
 298                 MESON_TAC[REAL_EQ_MUL_RCANCEL]) in
 299    (MATCH_MP_TAC (SPEC t REAL_MUL_RTIMES))
 300    THEN CONJ_TAC
 301    THENL [DISCH_TAC; ALL_TAC];;
 302
 303
 304 pop_priority();;
 305
 306 end;;