Rqe/rqe_real.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Reals                                                                 *)
   3 (* ---------------------------------------------------------------------- *)
   4 let real_ty = `:real`;;
   5 let rx = `x:real`;;
   6 let ry = `y:real`;;
   7 let rz = `z:real`;;
   8 let rzero = `&0`;;
   9 let req = `(=):real->real->bool`;;
  10 let rneq = `(<>):real->real->bool`;;
  11 let rlt = `(<):real->real->bool`;;
  12 let rgt = `(>):real->real->bool`;;
  13 let rle = `(<=):real->real->bool`;;
  14 let rge = `(>=):real->real->bool`;;
  15 let rm = `( * ):real->real->real`;;
  16 let rs = `(-):real->real->real`;;
  17 let rn = `(--):real->real`;;
  18 let rd = `(/):real->real->real`;;
  19 let rp = `(+):real->real->real`;;
  20 let rzero = `&0`;;
  21 let rone = `&1`;;
  22 let rlast = `LAST:(real) list -> real`;;
  23 let rappend = `APPEND:(real) list -> real list -> real list`;;
  24 let mk_rlist l = mk_list (l,real_ty);;
  25
  26 let diffl_tm = `(diffl)`;;
  27 let dest_diffl tm =
  28   try
  29     let l,var = dest_comb tm in
  30     let dp,p' = dest_comb l in
  31     let d,p = dest_comb dp in
  32     if not (d = diffl_tm) then failwith "dest_diffl: not a diffl" else
  33     let _,bod = dest_abs p in
  34       bod,p'
  35   with _ -> failwith "dest_diffl";;
  36
  37 let dest_mult =
  38   try
  39     dest_binop rm
  40   with _ -> failwith "dest_mult";;
  41
  42 let mk_mult = mk_binop rm;;
  43
  44 let pow_tm = `(pow)`;;
  45 let dest_pow =
  46   try
  47     dest_binop pow_tm
  48   with _ -> failwith "dest_pow";;
  49
  50 let mk_plus = mk_binop rp;;
  51 let mk_negative = curry mk_comb rn;;
  52
  53 let dest_plus =
  54   try
  55     dest_binop rp
  56   with _ -> failwith "dest_plus";;
  57
  58 let REAL_DENSE = prove(
  59   `!x y. x < y ==> ?z. x < z /\ z < y`,
  60 (* {{{ Proof *)
  61   REPEAT STRIP_TAC THEN
  62   CLAIM `&0 < y - x` THENL
  63   [REWRITE_TAC[REAL_LT_SUB_LADD;REAL_ADD_LID] THEN
  64      POP_ASSUM MATCH_ACCEPT_TAC;
  65    DISCH_THEN (ASSUME_TAC o (MATCH_MP REAL_DOWN)) THEN
  66      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
  67      EXISTS_TAC `e + x` THEN
  68      STRIP_TAC THENL
  69      [ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
  70       CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[GSYM REAL_ADD_RID])) THEN
  71       MATCH_MP_TAC REAL_LET_ADD2 THEN
  72       STRIP_TAC THENL
  73       [MATCH_ACCEPT_TAC REAL_LE_REFL;
  74        FIRST_ASSUM MATCH_ACCEPT_TAC];
  75       MATCH_EQ_MP_TAC ((GEN `y:real` (GEN `z:real` (ISPECL [`y:real`;`z:real`;`-- x`] REAL_LT_RADD)))) THEN
  76       REWRITE_TAC[GSYM REAL_ADD_ASSOC;REAL_ADD_RINV;REAL_ADD_RID] THEN
  77       REWRITE_TAC[GSYM real_sub] THEN
  78       FIRST_ASSUM MATCH_ACCEPT_TAC]]);;
  79 (* }}} *)
  80
  81 let REAL_LT_EXISTS = prove(
  82   `!x. ?y. x < y`,
  83 (* {{{ Proof *)
  84   GEN_TAC THEN
  85   EXISTS_TAC `x + &1` THEN
  86   REAL_ARITH_TAC);;
  87 (* }}} *)
  88
  89 let REAL_GT_EXISTS = prove(
  90   `!x. ?y. y < x`,
  91 (* {{{ Proof *)
  92   GEN_TAC THEN
  93   EXISTS_TAC `x - &1` THEN
  94   REAL_ARITH_TAC);;
  95 (* }}} *)
  96
  97 let REAL_DIV_DISTRIB_L = prove_by_refinement(
  98   `!x y z. x / (y * z) = (x / y) * (&1 / z)`,
  99 (* {{{ Proof *)
 100 [
 101   REWRITE_TAC[real_div;REAL_INV_MUL];
 102   REAL_ARITH_TAC;
 103 ]);;
 104 (* }}} *)
 105
 106 let REAL_DIV_DISTRIB_R = prove_by_refinement(
 107   `!x y z. x / (y * z) = (&1 / y) * (x / z)`,
 108 (* {{{ Proof *)
 109 [
 110   REWRITE_TAC[real_div;REAL_INV_MUL];
 111   REAL_ARITH_TAC;
 112 ]);;
 113 (* }}} *)
 114
 115 let REAL_DIV_DISTRIB_2 = prove_by_refinement(
 116   `!x y z. (x * w) / (y * z) = (x / y) * (w / z)`,
 117 (* {{{ Proof *)
 118 [
 119   REWRITE_TAC[real_div;REAL_INV_MUL];
 120   REAL_ARITH_TAC;
 121 ]);;
 122 (* }}} *)
 123
 124 let REAL_DIV_ADD_DISTRIB = prove_by_refinement(
 125   `!x y z. (x + y) / z = (x / z) + (y / z)`,
 126 (* {{{ Proof *)
 127 [
 128   REWRITE_TAC[real_div;REAL_INV_MUL];
 129   REAL_ARITH_TAC;
 130 ]);;
 131 (* }}} *)
 132
 133 let DIV_ID = prove_by_refinement(
 134  `!x. ~(x = &0) ==> (x / x = &1)`,
 135 (* {{{ Proof *)
 136
 137 [
 138   REPEAT STRIP_TAC;
 139   REWRITE_TAC[real_div];
 140   ASM_MESON_TAC[REAL_MUL_LINV;REAL_MUL_SYM];
 141 ]);;
 142
 143 (* }}} *)
 144
 145 let POS_POW = prove_by_refinement(
 146  `!c x. &0 < c /\ &0 < x ==> &0 < c * x pow k`,
 147 (* {{{ Proof *)
 148
 149 [
 150   MESON_TAC[REAL_POW_LT;REAL_LT_MUL]
 151 ]);;
 152
 153 (* }}} *)
 154
 155 let POS_NAT_POW = prove_by_refinement(
 156  `!c n. 0 < n /\ &0 < c ==> &0 < c * &n pow k`,
 157 (* {{{ Proof *)
 158
 159 [
 160   MESON_TAC[REAL_POW_LT;REAL_LT_MUL;REAL_LT;]
 161 ]);;
 162
 163 (* }}} *)
 164
 165 let REAL_NUM_LE_0 = prove_by_refinement(
 166   `!n. &0 <= (&n)`,
 167 (* {{{ Proof *)
 168 [
 169   INDUCT_TAC;
 170   REAL_ARITH_TAC;
 171   REWRITE_TAC[REAL];
 172   REAL_ARITH_TAC;
 173 ]);;
 174 (* }}} *)
 175
 176 let REAL_ARCH_SIMPLE_LT = prove_by_refinement(
 177   `!x. ?n. x < &n`,
 178 (* {{{ Proof *)
 179 [
 180   STRIP_TAC;
 181   CHOOSE_THEN ASSUME_TAC (ISPEC `x:real` REAL_ARCH_SIMPLE);
 182   EXISTS_TAC `SUC n`;
 183   REWRITE_TAC[REAL];
 184   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 185 ]);;
 186 (* }}} *)
 187
 188 let BINOMIAL_LEMMA_LT = prove_by_refinement(
 189    `!x y. &0 < x /\ &0 < y
 190            ==> !n. 0 < n ==> x pow n + y pow n <= (x + y) pow n`,
 191 (* {{{ Proof *)
 192
 193 [
 194   REPEAT GEN_TAC;
 195   STRIP_TAC;
 196   INDUCT_TAC;
 197   ARITH_TAC;
 198   REWRITE_TAC[real_pow];
 199   STRIP_TAC;
 200   CASES_ON `n = 0`;
 201   ASM_REWRITE_TAC[real_pow;REAL_MUL_RID;REAL_LE_REFL];
 202   CLAIM `0 < n`;
 203   POP_ASSUM MP_TAC THEN ARITH_TAC;
 204   DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
 205   MATCH_MP_TAC REAL_LE_TRANS;
 206   EXISTS_TAC `(x + y) * (x pow n + y pow n)`;
 207   STRIP_TAC;
 208   REWRITE_TAC[REAL_ADD_RDISTRIB];
 209   MATCH_MP_TAC REAL_LE_ADD2;
 210   CONJ_TAC;
 211   MATCH_MP_TAC REAL_LE_LMUL;
 212   STRIP_TAC;
 213   FIRST_ASSUM (fun x -> MP_TAC x THEN ARITH_TAC);
 214   MATCH_MP_TAC (REAL_ARITH `&0 <= y ==> x <= x + y`);
 215   MATCH_MP_TAC REAL_POW_LE;
 216   FIRST_ASSUM (fun x -> MP_TAC x THEN ARITH_TAC);
 217   REWRITE_TAC[REAL_ADD_LDISTRIB];
 218   MATCH_MP_TAC (REAL_ARITH `&0 <= y ==> x <= y + x`);
 219   MATCH_MP_TAC REAL_LE_MUL;
 220   CONJ_TAC;
 221   FIRST_ASSUM (fun x -> MP_TAC x THEN REAL_ARITH_TAC);
 222   MATCH_MP_TAC (REAL_ARITH `x < y ==> x <= y`);
 223   MATCH_MP_TAC REAL_POW_LT;
 224   FIRST_ASSUM MATCH_ACCEPT_TAC;
 225   MATCH_MP_TAC REAL_LE_LMUL;
 226   CONJ_TAC;
 227   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 228   FIRST_ASSUM MATCH_ACCEPT_TAC;
 229 ]);;
 230
 231 (* }}} *)
 232
 233 let BINOMIAL_LEMMA = prove_by_refinement(
 234    `!x y. &0 <= x /\ &0 <= y
 235            ==> !n. 0 < n ==> x pow n + y pow n <= (x + y) pow n`,
 236 (* {{{ Proof *)
 237
 238 [
 239   REPEAT GEN_TAC;
 240   STRIP_TAC;
 241   CASES_ON `(x = &0) \/ (y = &0)`;
 242   POP_ASSUM DISJ_CASES_TAC;
 243   ASM_REWRITE_TAC[real_pow;REAL_ADD_LID;POW_0];
 244   REPEAT STRIP_TAC;
 245   CLAIM `n = SUC (PRE n)`;
 246   POP_ASSUM MP_TAC THEN ARITH_TAC;
 247   STRIP_TAC;
 248   ONCE_ASM_REWRITE_TAC[];
 249   ASM_REWRITE_TAC[POW_0;REAL_ADD_LID;real_pow;REAL_LE_REFL];
 250   REPEAT STRIP_TAC;
 251   CLAIM `n = SUC (PRE n)`;
 252   POP_ASSUM MP_TAC THEN ARITH_TAC;
 253   STRIP_TAC;
 254   ONCE_ASM_REWRITE_TAC[];
 255   ASM_REWRITE_TAC[POW_0;REAL_ADD_LID;REAL_ADD_RID;real_pow;REAL_LE_REFL];
 256   POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC;
 257   MATCH_MP_TAC BINOMIAL_LEMMA_LT;
 258   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 259 ]);;
 260
 261 (* }}} *)
 262
 263 let NEG_ABS = prove_by_refinement(
 264   `!x. -- (abs x) <= &0`,
 265 (* {{{ Proof *)
 266 [
 267   REAL_ARITH_TAC;
 268 ]);;
 269 (* }}} *)
 270
 271 let REAL_MUL_LT = prove_by_refinement(
 272   `!x y. x * y < &0 <=> (x < &0 /\ &0 < y) \/ (&0 < x /\ y < &0)`,
 273 (* {{{ Proof *)
 274 [
 275   REPEAT STRIP_TAC;
 276   EQ_TAC;
 277   REPEAT STRIP_TAC;
 278   CCONTR_TAC;
 279   REWRITE_ASSUMS ([REAL_NOT_LT;DE_MORGAN_THM;] @ !REAL_REWRITES);
 280   POP_ASSUM MP_TAC THEN STRIP_TAC;
 281   CLAIM `x = &0`;
 282   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 283   DISCH_THEN (REWRITE_ASSUMS o list);
 284   REWRITE_ASSUMS !REAL_REWRITES;
 285   ASM_MESON_TAC !REAL_REWRITES;
 286   CLAIM `&0 * &0 <= x * y`;
 287   MATCH_MP_TAC REAL_LE_MUL2;
 288   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 289   REAL_SIMP_TAC;
 290   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 291   CLAIM `&0 * &0 <= --x * --y`;
 292   MATCH_MP_TAC REAL_LE_MUL2;
 293   REAL_SIMP_TAC;
 294   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 295   REAL_SIMP_TAC;
 296   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 297   CLAIM `y = &0`;
 298   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 299   DISCH_THEN (REWRITE_ASSUMS o list);
 300   REWRITE_ASSUMS !REAL_REWRITES;
 301   ASM_REWRITE_TAC[];
 302   EVERY_ASSUM MP_TAC THEN ARITH_TAC;
 303   (* save *)
 304   REPEAT STRIP_TAC;
 305   CLAIM `&0 < --x`;
 306   EVERY_ASSUM MP_TAC THEN ARITH_TAC;
 307   STRIP_TAC;
 308   CLAIM `&0 * &0 < --x * y`;
 309   MATCH_MP_TAC REAL_LT_MUL2;
 310   REAL_SIMP_TAC;
 311   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 312   REAL_SIMP_TAC;
 313   REWRITE_TAC[REAL_ARITH `--y * x = --(y * x)`];
 314   REAL_ARITH_TAC;
 315   CLAIM `&0 < --y`;
 316   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 317   STRIP_TAC;
 318   CLAIM `&0 * &0 < x * --y`;
 319   MATCH_MP_TAC REAL_LT_MUL2;
 320   REAL_SIMP_TAC;
 321   ASM_REWRITE_TAC[];
 322   REAL_SIMP_TAC;
 323   REWRITE_TAC[REAL_ARITH `x * --y = --(x * y)`];
 324   REAL_ARITH_TAC;
 325 ]);;
 326 (* }}} *)
 327
 328 let REAL_MUL_GT = prove_by_refinement(
 329   `!x y. &0 < x * y <=> (x < &0 /\ y < &0) \/ (&0 < x /\ &0 < y)`,
 330 (* {{{ Proof *)
 331 [
 332   REPEAT STRIP_TAC;
 333   EQ_TAC;
 334   REPEAT STRIP_TAC;
 335   ONCE_REWRITE_ASSUMS[ARITH_RULE `x < y <=> -- y < -- x`];
 336   REWRITE_ASSUMS[GSYM REAL_MUL_RNEG];
 337   REWRITE_ASSUMS[REAL_ARITH `-- &0 = &0`; REAL_MUL_LT];
 338   POP_ASSUM MP_TAC THEN REPEAT STRIP_TAC;
 339   DISJ1_TAC;
 340   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 341   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 342   REPEAT STRIP_TAC;
 343   ONCE_REWRITE_TAC [ARITH_RULE `x * y = --x * --y`];
 344   ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
 345   MATCH_MP_TAC REAL_LT_MUL2;
 346   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 347   ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
 348   MATCH_MP_TAC REAL_LT_MUL2;
 349   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 350 ]);;
 351 (* }}} *)
 352
 353 let REAL_DIV_INV = prove_by_refinement(
 354   `!y z. &0 < y /\ y < z ==> &1 / z < &1 / y`,
 355 (* {{{ Proof *)
 356 [
 357   REPEAT STRIP_TAC;
 358   REWRITE_TAC[real_div];
 359   REAL_SIMP_TAC;
 360   MATCH_MP_TAC REAL_LT_INV2;
 361   ASM_MESON_TAC[];
 362 ]);;
 363 (* }}} *)
 364
 365 let REAL_DIV_DENOM_LT = prove_by_refinement(
 366   `!x y z. &0 < x /\ &0 < y /\ y < z ==> x / z < x / y`,
 367 (* {{{ Proof *)
 368 [
 369   REPEAT STRIP_TAC;
 370   MATCH_MP_TAC REAL_LT_LCANCEL_IMP;
 371   EXISTS_TAC `inv x`;
 372   REPEAT STRIP_TAC;
 373   REAL_SOLVE_TAC;
 374   REWRITE_TAC[real_div];
 375   ASM_SIMP_TAC[REAL_LT_IMP_NZ;REAL_MUL_ASSOC;REAL_MUL_LINV;];
 376   REAL_SIMP_TAC;
 377   MATCH_MP_TAC (REWRITE_RULE [REAL_MUL_LID;real_div] REAL_DIV_INV);
 378   ASM_MESON_TAC[];
 379 ]);;
 380 (* }}} *)
 381
 382 let REAL_DIV_DENOM_LE = prove_by_refinement(
 383   `!x y z. &0 <= x /\ &0 < y /\ y <= z ==> x / z <= x / y`,
 384 (* {{{ Proof *)
 385 [
 386   REPEAT STRIP_TAC;
 387   CASES_ON `x = &0`;
 388   ASM_REWRITE_TAC[];
 389   REWRITE_TAC[real_div;REAL_MUL_LZERO;REAL_LE_REFL];
 390   MATCH_MP_TAC REAL_LE_LCANCEL_IMP;
 391   EXISTS_TAC `inv x`;
 392   REPEAT STRIP_TAC;
 393   MATCH_MP_TAC REAL_LT_INV;
 394   ASM_MESON_TAC[REAL_LT_LE];
 395   REWRITE_TAC[real_div];
 396   ASM_SIMP_TAC[REAL_LT_IMP_NZ;REAL_MUL_ASSOC;REAL_MUL_LINV;];
 397   REAL_SIMP_TAC;
 398   MATCH_MP_TAC REAL_LE_INV2;
 399   ASM_REWRITE_TAC[];
 400 ]);;
 401 (* }}} *)
 402
 403 let REAL_NEG_DIV = prove_by_refinement(
 404   `!x y. -- x / -- y = x / y`,
 405 (* {{{ Proof *)
 406 [
 407   REWRITE_TAC[real_div];
 408   REWRITE_TAC[REAL_INV_NEG];
 409   REAL_ARITH_TAC;
 410 ]);;
 411 (* }}} *)
 412
 413 let REAL_GT_IMP_NZ = prove(
 414   `!x. x < &0 ==> ~(x = &0)`,
 415 (* {{{ Proof *)
 416  REAL_ARITH_TAC);;
 417 (* }}} *)
 418
 419 let REAL_NEG_NZ = prove(
 420   `!x. x < &0 ==> ~(x = &0)`,
 421 (* {{{ Proof *)
 422   REAL_ARITH_TAC);;
 423 (* }}} *)
 424
 425 let PARITY_POW_LT = prove_by_refinement(
 426   `!a n. a < &0 ==> (EVEN n ==> a pow n > &0) /\ (ODD n ==> a pow n < &0)`,
 427 (* {{{ Proof *)
 428
 429 [
 430   STRIP_TAC;
 431   INDUCT_TAC;
 432   REWRITE_TAC[EVEN;ODD;real_pow];
 433   REAL_ARITH_TAC;
 434   DISCH_THEN (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
 435   REWRITE_TAC[EVEN;ODD;real_pow;NOT_EVEN;NOT_ODD];
 436   DISJ_CASES_TAC (ISPEC `n:num` EVEN_OR_ODD);
 437   ASM_REWRITE_TAC[];
 438   REPEAT STRIP_TAC;
 439   ASM_REWRITE_TAC[real_gt;REAL_MUL_GT];
 440   ASM_MESON_TAC[EVEN_AND_ODD];
 441   ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
 442   ASM_MESON_TAC[real_gt];
 443   ASM_REWRITE_TAC[];
 444   ASM_REWRITE_TAC[real_gt;REAL_MUL_LT;REAL_MUL_GT];
 445   REPEAT STRIP_TAC;
 446   ASM_MESON_TAC[];
 447   ASM_MESON_TAC[EVEN_AND_ODD];
 448 ]);;
 449
 450 (* }}} *)
 451
 452 let EVEN_ODD_POW = prove_by_refinement(
 453   `!a n.  a <> &0 ==>
 454           (EVEN n ==> a pow n > &0) /\
 455           (ODD n ==> a < &0 ==> a pow n < &0) /\
 456           (ODD n ==> a > &0 ==> a pow n > &0)`,
 457 (* {{{ Proof *)
 458 [
 459   REWRITE_TAC[NEQ];
 460   REPEAT_N 2 STRIP_TAC;
 461   CLAIM `a < &0 \/ a > &0 \/ (a = &0)`;
 462   REAL_ARITH_TAC;
 463   ASM_REWRITE_TAC[];
 464   STRIP_TAC;
 465   REPEAT STRIP_TAC;
 466   ASM_MESON_TAC[PARITY_POW_LT];
 467   ASM_MESON_TAC[PARITY_POW_LT];
 468   ASM_MESON_TAC[REAL_POW_LT;real_gt];
 469   REPEAT STRIP_TAC;
 470   ASM_MESON_TAC[REAL_POW_LT;real_gt];
 471   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 472   ASM_MESON_TAC[REAL_POW_LT;real_gt];
 473   ASM_REWRITE_TAC[];
 474 ]);;
 475 (* }}} *)