Rqe/examples.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Paper                                                                 *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 (* ----------------------------  Chebychev  ----------------------------- *)
   6
   7 time REAL_QELIM_CONV
   8   `!x. --(&1) <= x /\ x <= &1 ==>
   9     -- (&1) <= &2 * x pow 2 - &1 /\ &2 * x pow 2 - &1 <= &1`;;
  10
  11 (*
  12 DATE -------  HOL --------
  13 5/20         4.92
  14 5/22         4.67
  15 *)
  16
  17 time REAL_QELIM_CONV
  18   `!x. --(&1) <= x /\ x <= &1 ==>
  19     -- (&1) <= &4 * x pow 3 - &3 * x /\ &4 * x pow 3 - &3 * x <= &1`;;
  20
  21 (*
  22 DATE -------  HOL --------
  23 5/20         14.38
  24 5/22         13.65
  25 *)
  26
  27 time REAL_QELIM_CONV
  28  `&1 < &2 /\ (!x. &1 < x ==> &1 < x pow 2) /\
  29  (!x y. &1 < x /\ &1 < y ==> &1 < x * (&1 + &2 * y))`;;
  30
  31
  32 (*
  33 DATE -------  HOL --------
  34 5/22         23.61
  35 *)
  36
  37 time REAL_QELIM_CONV
  38  `&0 <= b /\ &0 <= c /\ &0 < a * c ==> ?u. &0 < u /\ u * (u * c - a * c) -
  39    (u * a * c - (a pow 2 * c + b)) < a pow 2 * c + b`;;
  40
  41 (*
  42 DATE -------  HOL --------
  43 5/22         8.78
  44 *)
  45
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* Examples.                                                                 *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51
  52
  53
  54 (* ---------------------------------    --------------------------------- *)
  55 (*
  56 time real_qelim <<exists x. x^4 + x^2 + 1 = 0>>;;
  57 0.01
  58
  59 let fm = `?x. x pow 4 + x pow 2 + &1 = &0`;;
  60 let vars = []
  61 *)
  62
  63
  64 time REAL_QELIM_CONV `?x. x pow 4 + x pow 2 + &1 = &0`;;
  65
  66
  67
  68 (*
  69 DATE -------  HOL --------
  70 4/29/2005    3.19
  71 5/19         2.2
  72 5/20         1.96
  73 5/22         1.53
  74 *)
  75
  76 (* ---------------------------------    --------------------------------- *)
  77
  78 (*
  79 time real_qelim <<exists x. x^3 - x^2 + x - 1 = 0>>;;
  80 0.01
  81 *)
  82
  83 time REAL_QELIM_CONV `?x. x pow 3 - x pow 2 + x - &1 = &0`;;
  84
  85 (*
  86 DATE -------  HOL --------
  87 4/29/2005    3.83
  88 5/22/2005    1.69
  89 *)
  90
  91 (* ---------------------------------    --------------------------------- *)
  92
  93 (*
  94 time real_qelim
  95  <<exists x y. x^3 - x^2 + x - 1 = 0 /\
  96               y^3 - y^2 + y - 1 = 0 /\ ~(x = y)>>;;
  97 0.23
  98 *)
  99
 100 time REAL_QELIM_CONV
 101  `?x y. (x pow 3 - x pow 2 + x - &1 = &0) /\
 102               (y pow 3 - y pow 2 + y - &1 = &0) /\ ~(x = y)`;;
 103
 104 (*
 105 DATE -------  HOL -------- Factor
 106 4/29/2005   682.85          3000
 107 5/17/2005   345.27
 108 5/22        269
 109 *)
 110
 111 (* ---------------------------------    --------------------------------- *)
 112
 113
 114 (*
 115 time real_qelim
 116  <<forall a f k. (forall e. k < e ==> f < a * e) ==> f <= a * k>>;;
 117 0.02
 118 *)
 119
 120 time REAL_QELIM_CONV
 121  `!a f k. (!e. k < e ==> f < a * e) ==> f <= a * k`;;
 122
 123 (*
 124 DATE -------  HOL -------- Factor
 125 4/29/2005   20.91          1000
 126 5/15/2005   17.98
 127 5/17/2005   15.12
 128 5/18/2005   12.87
 129 5/22        12.09
 130 *)
 131
 132 (* ---------------------------------    --------------------------------- *)
 133
 134 (*
 135 time real_qelim
 136  <<exists x. a * x^2 + b * x + c = 0>>;;
 137 0.01
 138 *)
 139
 140 time REAL_QELIM_CONV
 141  `?x. a * x pow 2 + b * x + c = &0`;;
 142
 143 (*
 144 DATE -------  HOL -------- Factor
 145 4/29/2005   10.99          1000
 146 5/17/2005   6.42
 147 5/18         5.39
 148 5/22         4.74
 149 *)
 150
 151 (* ---------------------------------    --------------------------------- *)
 152 (*
 153 time real_qelim
 154  <<forall a b c. (exists x. a * x^2 + b * x + c = 0) <=>
 155                  b^2 >= 4 * a * c>>;;
 156 0.51
 157 *)
 158
 159 time REAL_QELIM_CONV
 160  `!a b c. (?x. a * x pow 2 + b * x + c = &0) <=>
 161                  b pow 2 >= &4 * a * c`;;
 162
 163
 164 (*
 165 DATE -------  HOL -------- Factor
 166 4/29/2005   1200.99          2400
 167 5/17         878.25
 168 *)
 169
 170
 171 (* ---------------------------------    --------------------------------- *)
 172 (*
 173 time real_qelim
 174  <<forall a b c. (exists x. a * x^2 + b * x + c = 0) <=>
 175                  a = 0 /\ (~(b = 0) \/ c = 0) \/
 176                  ~(a = 0) /\ b^2 >= 4 * a * c>>;;
 177
 178 0.51
 179 *)
 180 time REAL_QELIM_CONV
 181  `!a b c. (?x. a * x pow 2 + b * x + c = &0) <=>
 182                  (a = &0) /\ (~(b = &0) \/ (c = &0)) \/
 183                  ~(a = &0) /\ b pow 2 >= &4 * a * c`;;
 184
 185 (*
 186 DATE -------  HOL -------- Factor
 187 4/29/2005   1173.9          2400
 188 5/17         848.4
 189 5/20         816
 190
 191 1095 during depot update
 192 *)
 193
 194
 195 (*
 196 time real_qelim <<exists x. 0 <= x /\ x <= 1 /\ (r * r * x * x - r * (1 + r) * x + (1 + r) = 0)
 197 /\ ~(2 * r * x = 1 + r)>>
 198 *)
 199 time REAL_QELIM_CONV
 200   `?x. &0 <= x /\ x <= &1 /\ (r pow 2 * x pow 2 - r * (&1 + r) * x + (&1 + r) = &0)
 201    /\ ~(&2 * r * x = &1 + r)`;;
 202
 203 (*
 204 DATE -------  HOL -------- Factor
 205 5/20/2005   19021          1460
 206
 207 4000 line output
 208 *)
 209
 210
 211
 212
 213 (* ------------------------------------------------------------------------- *)
 214 (* Termination ordering for group theory completion.                         *)
 215 (* ------------------------------------------------------------------------- *)
 216
 217 (* ------------------------------------------------------------------------- *)
 218 (* Left this out                                                             *)
 219 (* ------------------------------------------------------------------------- *)
 220
 221 (* ------------------------------------------------------------------------- *)
 222 (* This one works better using DNF.                                          *)
 223 (* ------------------------------------------------------------------------- *)
 224
 225 (* ------------------------------------------------------------------------- *)
 226 (* And this                                                                  *)
 227 (* ------------------------------------------------------------------------- *)
 228
 229 (* ------------------------------------------------------------------------- *)
 230 (* Linear examples.                                                          *)
 231 (* ------------------------------------------------------------------------- *)
 232
 233 (* ---------------------------------    --------------------------------- *)
 234
 235 (*
 236 time real_qelim <<exists x. x - 1 > 0>>;;
 237 0
 238 *)
 239
 240 time REAL_QELIM_CONV `?x. x - &1 > &0`;;
 241 (*
 242 DATE -------  HOL
 243 4/29/2005    .56
 244 *)
 245
 246 (* ---------------------------------    --------------------------------- *)
 247 (*
 248 time real_qelim <<exists x. 3 - x > 0 /\ x - 1 > 0>>;;
 249 0
 250 *)
 251
 252 time REAL_QELIM_CONV `?x. &3 - x > &0 /\ x - &1 > &0`;;
 253
 254 (*
 255 DATE -------  HOL
 256 4/29/2005    1.66
 257 *)
 258
 259 (* ------------------------------------------------------------------------- *)
 260 (* Quadratics.                                                               *)
 261 (* ------------------------------------------------------------------------- *)
 262
 263 (* ---------------------------------    --------------------------------- *)
 264 (*
 265 time real_qelim <<exists x. x^2 = 0>>;;
 266 0
 267 *)
 268
 269 time REAL_QELIM_CONV `?x. x pow 2 = &0`;;
 270 (*
 271 DATE -------  HOL
 272 4/29/2005    1.12
 273 *)
 274
 275 (* ---------------------------------    --------------------------------- *)
 276 (*
 277 time real_qelim <<exists x. x^2 + 1 = 0>>;;
 278 *)
 279 time REAL_QELIM_CONV `?x. x pow 2 + &1 = &0`;;
 280 (*
 281 DATE -------  HOL
 282 4/29/2005    1.11
 283 *)
 284
 285 (* ---------------------------------    --------------------------------- *)
 286
 287 (*
 288 time real_qelim <<exists x. x^2 - 1 = 0>>;;
 289 *)
 290 time REAL_QELIM_CONV `?x. x pow 2 - &1 = &0`;;
 291
 292 (*
 293 DATE -------  HOL
 294 4/29/2005    1.54
 295 *)
 296 (* ---------------------------------    --------------------------------- *)
 297
 298 (*
 299 time real_qelim <<exists x. x^2 - 2 * x + 1 = 0>>;;
 300 *)
 301 time REAL_QELIM_CONV `?x. x pow 2 - &2 * x + &1 = &0`;;
 302 (*
 303 DATE -------  HOL
 304 4/29/2005    1.21
 305 *)
 306 (* ---------------------------------    --------------------------------- *)
 307
 308 (*
 309 time real_qelim <<exists x. x^2 - 3 * x + 1 = 0>>;;
 310 *)
 311 time REAL_QELIM_CONV `?x. x pow 2 - &3 * x + &1 = &0`;;
 312
 313 (*
 314 DATE -------  HOL
 315 4/29/2005    1.75
 316 *)
 317
 318
 319 (* ------------------------------------------------------------------------- *)
 320 (* Cubics.                                                                   *)
 321 (* ------------------------------------------------------------------------- *)
 322
 323 (* ---------------------------------    --------------------------------- *)
 324
 325 (*
 326 time real_qelim <<exists x. x^3 - 1 > 0>>;;
 327 *)
 328 time REAL_QELIM_CONV `?x. x pow 3 - &1 > &0`;;
 329
 330 (*
 331 DATE -------  HOL
 332 4/29/2005    1.96
 333 *)
 334
 335 (* ---------------------------------    --------------------------------- *)
 336
 337 (*
 338 time real_qelim <<exists x. x^3 - 3 * x^2 + 3 * x - 1 > 0>>;;
 339 *)
 340 time REAL_QELIM_CONV `?x. x pow 3 - &3 * x pow 2 + &3 * x - &1 > &0`;;
 341 (*
 342 DATE -------  HOL
 343 4/29/2005    1.97
 344 *)
 345
 346 (* ---------------------------------    --------------------------------- *)
 347
 348 (*
 349 time real_qelim <<exists x. x^3 - 4 * x^2 + 5 * x - 2 > 0>>;;
 350 *)
 351 time REAL_QELIM_CONV `?x. x pow 3 - &4 * x pow 2 + &5 * x - &2 > &0`;;
 352 (*
 353 DATE -------  HOL
 354 4/29/2005    4.89
 355 *)
 356
 357 (* ---------------------------------    --------------------------------- *)
 358
 359 (*
 360 time real_qelim <<exists x. x^3 - 6 * x^2 + 11 * x - 6 = 0>>;;
 361 *)
 362 time REAL_QELIM_CONV `?x. x pow 3 - &6 * x pow 2 + &11 * x - &6 = &0`;;
 363 (*
 364 DATE -------  HOL
 365 4/29/2005    4.17
 366 *)
 367
 368
 369 (* ------------------------------------------------------------------------- *)
 370 (* Quartics.                                                                 *)
 371 (* ------------------------------------------------------------------------- *)
 372
 373 (* ---------------------------------    --------------------------------- *)
 374
 375 (*
 376 time real_qelim <<exists x. x^4 - 1 > 0>>;;
 377 *)
 378
 379 time REAL_QELIM_CONV `?x. x pow 4 - &1 > &0`;;
 380 (*
 381 DATE -------  HOL
 382 4/29/2005    3.07
 383 *)
 384
 385
 386 (* ---------------------------------    --------------------------------- *)
 387
 388 (*
 389 time real_qelim <<exists x. x^4 + 1 > 0>>;;
 390 *)
 391 time REAL_QELIM_CONV `?x. x pow 4 + &1 > &0`;;
 392 (*
 393 DATE -------  HOL
 394 4/29/2005    2.47
 395 *)
 396
 397
 398 (* ---------------------------------    --------------------------------- *)
 399
 400 (*
 401 time real_qelim <<exists x. x^4 = 0>>;;
 402 *)
 403 time REAL_QELIM_CONV `?x. x pow 4 = &0`;;
 404 (*
 405 DATE -------  HOL
 406 4/29/2005    2.48
 407 *)
 408
 409 (* ---------------------------------    --------------------------------- *)
 410
 411
 412 (*
 413 time real_qelim <<exists x. x^4 - x^3 = 0>>;;
 414 *)
 415 time REAL_QELIM_CONV `?x. x pow 4 - x pow 3 = &0`;;
 416 (*
 417 DATE -------  HOL
 418 4/29/2005    1.76
 419 *)
 420
 421 (* ---------------------------------    --------------------------------- *)
 422
 423
 424 (*
 425 time real_qelim <<exists x. x^4 - x^2 = 0>>;;
 426 *)
 427 time REAL_QELIM_CONV `?x. x pow 4 - x pow 2 = &0`;;
 428 (*
 429 DATE -------  HOL
 430 4/29/2005    2.16
 431 *)
 432
 433 (* ---------------------------------    --------------------------------- *)
 434
 435
 436 (*
 437 time real_qelim <<exists x. x^4 - 2 * x^2 + 2 = 0>>;;
 438 *)
 439 time REAL_QELIM_CONV `?x. x pow 4 - &2 * x pow 2 + &2 = &0`;;
 440 (*
 441 DATE -------  HOL
 442 4/29/2005    6.87
 443 5/16/2005    5.22
 444 *)
 445
 446 (* ------------------------------------------------------------------------- *)
 447 (* Quintics.                                                                 *)
 448 (* ------------------------------------------------------------------------- *)
 449
 450
 451 (* ---------------------------------    --------------------------------- *)
 452
 453 (*
 454 time real_qelim
 455   <<exists x. x^5 - 15 * x^4 + 85 * x^3 - 225 * x^2 + 274 * x - 120 = 0>>;;
 456 0.03
 457
 458 print_timers()
 459 *)
 460
 461 time REAL_QELIM_CONV
 462   `?x. x pow 5 - &15 * x pow 4 + &85 * x pow 3 - &225 * x pow 2 + &274 * x - &120 = &0`;;
 463
 464 (*
 465 DATE -------  HOL -------- Factor
 466 4/29/2005   65.64          2500
 467 5/15/2005   55.93
 468 5/16/2005   47.72
 469 *)
 470
 471
 472 (* ------------------------------------------------------------------------- *)
 473 (* Sextics(?)                                                                *)
 474 (* ------------------------------------------------------------------------- *)
 475
 476 (* ---------------------------------    --------------------------------- *)
 477
 478
 479 (*
 480 time real_qelim <<exists x.
 481  x^6 - 21 * x^5 + 175 * x^4 - 735 * x^3 + 1624 * x^2 - 1764 * x + 720 = 0>>;;
 482 0.15
 483 *)
 484
 485 time REAL_QELIM_CONV `?x.
 486  x pow 6 - &21 * x pow 5 + &175 * x pow 4 - &735 * x pow 3 + &1624 * x pow 2 - &1764 * x + &720 = &0`;;
 487   `?x. x pow 5 - &15 * x pow 4 + &85 * x pow 3 - &225 * x pow 2 + &274 * x - &120 = &0`;;
 488
 489 (*
 490 DATE -------  HOL -------- Factor
 491 4/29/2005   1400.4          10000
 492 *)
 493
 494 (* ---------------------------------    --------------------------------- *)
 495
 496 (*
 497 time real_qelim <<exists x.
 498  x^6 - 12 * x^5 + 56 * x^4 - 130 * x^3 + 159 * x^2 - 98 * x + 24 = 0>>;;
 499 7.54
 500 *)
 501
 502 (* NOT YET *)
 503 (*
 504 time REAL_QELIM_CONV `?x.
 505  x pow 6 - &12 * x pow 5 + &56 * x pow 4 - &130 * x pow 3 + &159 * x pow 2 - &98 * x + &24 = &0`;;
 506 *)
 507
 508 (* ------------------------------------------------------------------------- *)
 509 (* Multiple polynomials.                                                     *)
 510 (* ------------------------------------------------------------------------- *)
 511
 512 (* ---------------------------------    --------------------------------- *)
 513
 514 (*
 515 time real_qelim <<exists x. x^2 + 2 > 0 /\ x^3 - 11 = 0 /\ x + 131 >= 0>>;;
 516 *)
 517 time REAL_QELIM_CONV `?x. x pow 2 + &2 > &0 /\ (x pow 3 - &11 = &0) /\ x + &131 >= &0`;;
 518 (*
 519 DATE -------  HOL
 520 4/29/2005    13.1
 521 *)
 522
 523 (* ------------------------------------------------------------------------- *)
 524 (* With more variables.                                                      *)
 525 (* ------------------------------------------------------------------------- *)
 526
 527 (* ---------------------------------    --------------------------------- *)
 528
 529 (*
 530 time real_qelim <<exists x. a * x^2 + b * x + c = 0>>;;
 531 *)
 532 time REAL_QELIM_CONV `?x. a * x pow 2 + b * x + c = &0`;;
 533 (*
 534 DATE -------  HOL
 535 4/29/2005    10.94
 536 *)
 537
 538
 539 (* ---------------------------------    --------------------------------- *)
 540
 541 (*
 542 time real_qelim <<exists x. a * x^3 + b * x^2 + c * x + d = 0>>;;
 543 *)
 544 time REAL_QELIM_CONV `?x. a * x pow 3 + b * x pow 2 + c * x + d = &0`;;
 545 (*
 546 DATE -------  HOL
 547 4/29/2005    269.17
 548 *)
 549
 550
 551
 552 (* ------------------------------------------------------------------------- *)
 553 (* Constraint solving.                                                       *)
 554 (* ------------------------------------------------------------------------- *)
 555
 556 (* ---------------------------------    --------------------------------- *)
 557
 558 (*
 559 time real_qelim <<exists x1 x2. x1^2 + x2^2 - u1 <= 0 /\ x1^2 - u2 > 0>>;;
 560 *)
 561 time REAL_QELIM_CONV `?x1 x2. x1 pow 2 + x2 pow 2 - u1 <= &0 /\ x1 pow 2 - u2 > &0`;;
 562 (*
 563 DATE -------  HOL
 564 4/29/2005    89.97
 565 *)
 566
 567 (* ------------------------------------------------------------------------- *)
 568 (* Huet & Oppen (interpretation of group theory).                            *)
 569 (* ------------------------------------------------------------------------- *)
 570
 571 (* ---------------------------------    --------------------------------- *)
 572
 573 (*
 574 time real_qelim <<forall x y. x > 0 /\ y > 0 ==> x * (1 + 2 * y) > 0>>;;
 575 *)
 576 time REAL_QELIM_CONV `!x y. x > &0 /\ y > &0 ==> x * (&1 + &2 * y) > &0`;;
 577 (*
 578 DATE -------  HOL
 579 4/29/2005    5.03
 580 *)
 581
 582
 583 (* ------------------------------------------------------------------------- *)
 584 (* Other examples.                                                           *)
 585 (* ------------------------------------------------------------------------- *)
 586
 587 (* ---------------------------------    --------------------------------- *)
 588
 589 (*
 590 time real_qelim <<exists x. x^2 - x + 1 = 0>>;;
 591 *)
 592 time REAL_QELIM_CONV `?x. x pow 2 - x + &1 = &0`;;
 593 (*
 594 DATE -------  HOL
 595 4/29/2005    1.19
 596 *)
 597
 598 (* ---------------------------------    --------------------------------- *)
 599
 600 (*
 601 time real_qelim <<exists x. x^2 - 3 * x + 1 = 0>>;;
 602 *)
 603 time REAL_QELIM_CONV `?x. x pow 2 - &3 * x + &1 = &0`;;
 604 (*
 605 DATE -------  HOL
 606 4/29/2005    1.65
 607 *)
 608
 609 (* ---------------------------------    --------------------------------- *)
 610
 611 (*
 612 time real_qelim <<exists x. x > 6 /\ (x^2 - 3 * x + 1 = 0)>>;;
 613 *)
 614 time REAL_QELIM_CONV `?x. x > &6 /\ (x pow 2 - &3 * x + &1 = &0)`;;
 615 (*
 616 DATE -------  HOL
 617 4/29/2005    3.63
 618 *)
 619
 620 (* ---------------------------------    --------------------------------- *)
 621
 622 (*
 623 time real_qelim <<exists x. 7 * x^2 - 5 * x + 3 > 0 /\
 624                             x^2 - 3 * x + 1 = 0>>;;
 625 *)
 626 time REAL_QELIM_CONV `?x. &7 * x pow 2 - &5 * x + &3 > &0 /\
 627                             (x pow 2 - &3 * x + &1 = &0)`;;
 628
 629 (*
 630 DATE -------  HOL
 631 4/29/2005    8.62
 632 *)
 633
 634 (* ---------------------------------    --------------------------------- *)
 635
 636 (*
 637 time real_qelim <<exists x. 11 * x^3 - 7 * x^2 - 2 * x + 1 = 0 /\
 638                             7 * x^2 - 5 * x + 3 > 0 /\
 639                             x^2 - 8 * x + 1 = 0>>;;
 640 *)
 641 time REAL_QELIM_CONV `?x. (&11 * x pow 3 - &7 * x pow 2 - &2 * x + &1 = &0) /\
 642                             &7 * x pow 2 - &5 * x + &3 > &0 /\
 643                             (x pow 2 - &8 * x + &1 = &0)`;;
 644 (*
 645 DATE -------  HOL
 646 4/29/2005    221.4
 647 *)
 648
 649
 650 (* ------------------------------------------------------------------------- *)
 651 (* Quadratic inequality from Liska and Steinberg                             *)
 652 (* ------------------------------------------------------------------------- *)
 653
 654 (* ---------------------------------    --------------------------------- *)
 655
 656 (*
 657 time real_qelim
 658  <<forall x. -(1) <= x /\ x <= 1 ==>
 659       C * (x - 1) * (4 * x * a * C - x * C - 4 * a * C + C - 2) >= 0>>;;
 660 *)
 661 time REAL_QELIM_CONV
 662  `!x. -- &1 <= x /\ x <= &1 ==>
 663       C * (x - &1) * (&4 * x * a * C - x * C - &4 * a * C + C - &2) >= &0`;;
 664 (*
 665 DATE -------  HOL
 666 4/29/2005    1493
 667 *)
 668
 669
 670 (* ------------------------------------------------------------------------- *)
 671 (* Metal-milling example from Loos and Weispfenning                          *)
 672 (* ------------------------------------------------------------------------- *)
 673
 674
 675 (* ---------------------------------    --------------------------------- *)
 676
 677 (*
 678 time real_qelim
 679   <<exists x y. 0 < x /\
 680                 y < 0 /\
 681                 x * r - x * t + t = q * x - s * x + s /\
 682                 x * b - x * d + d = a * y - c * y + c>>;;
 683 *)
 684 time REAL_QELIM_CONV
 685   `?x y. &0 < x /\
 686                 y < &0 /\
 687                 (x * r - x * t + t = q * x - s * x + s) /\
 688                 (x * b - x * d + d = a * y - c * y + c)`;;
 689
 690
 691 (* ------------------------------------------------------------------------- *)
 692 (* Linear example from Collins and Johnson                                   *)
 693 (* ------------------------------------------------------------------------- *)
 694
 695 (* ---------------------------------    --------------------------------- *)
 696
 697 (*
 698 time real_qelim
 699  <<exists r. 0 < r /\
 700       r < 1 /\
 701       0 < (1 - 3 * r) * (a^2 + b^2) + 2 * a * r /\
 702       (2 - 3 * r) * (a^2 + b^2) + 4 * a * r - 2 * a - r < 0>>;;
 703 *)
 704 time REAL_QELIM_CONV
 705  `?r. &0 < r /\
 706       r < &1 /\
 707       &0 < (&1 - &3 * r) * (a pow 2 + b pow 2) + &2 * a * r /\
 708       (&2 - &3 * r) * (a pow 2 + b pow 2) + &4 * a * r - &2 * a - r < &0`;;
 709
 710
 711 (* ------------------------------------------------------------------------- *)
 712 (* Dave Griffioen #4                                                         *)
 713 (* ------------------------------------------------------------------------- *)
 714
 715 (* ---------------------------------    --------------------------------- *)
 716
 717 (*
 718 time real_qelim
 719  <<forall x y. (1 - t) * x <= (1 + t) * y /\ (1 - t) * y <= (1 + t) * x
 720          ==> 0 <= y>>;;
 721 *)
 722 time REAL_QELIM_CONV
 723  `!x y. (&1 - t) * x <= (&1 + t) * y /\ (&1 - t) * y <= (&1 + t) * x
 724          ==> &0 <= y`;;
 725
 726 (*
 727 DATE -------  HOL
 728 4/29/2005    893
 729 *)
 730
 731
 732 (* ------------------------------------------------------------------------- *)
 733 (* Some examples from "Real Quantifier Elimination in practice".             *)
 734 (* ------------------------------------------------------------------------- *)
 735
 736 (* ---------------------------------    --------------------------------- *)
 737
 738 (*
 739 time real_qelim <<exists x2. x1^2 + x2^2 <= u1 /\ x1^2 > u2>>;;
 740 *)
 741 time REAL_QELIM_CONV `?x2. x1 pow 2 + x2 pow 2 <= u1 /\ x1 pow 2 > u2`;;
 742 (*
 743 DATE -------  HOL
 744 4/29/2005    4
 745 *)
 746
 747 (* ---------------------------------    --------------------------------- *)
 748
 749
 750 (*
 751 time real_qelim <<exists x1 x2. x1^2 + x2^2 <= u1 /\ x1^2 > u2>>;;
 752 *)
 753 time REAL_QELIM_CONV `?x1 x2. x1 pow 2 + x2 pow 2 <= u1 /\ x1 pow 2 > u2`;;
 754 (*
 755 DATE -------  HOL
 756 4/29/2005    90
 757 *)
 758
 759
 760 (* ---------------------------------    --------------------------------- *)
 761
 762 (*
 763 time real_qelim
 764  <<forall x1 x2. x1 + x2 <= 2 /\ x1 <= 1 /\ x1 >= 0 /\ x2 >= 0
 765            ==> 3 * (x1 + 3 * x2^2 + 2) <= 8 * (2 * x1 + x2 + 1)>>;;
 766 *)
 767 time REAL_QELIM_CONV
 768  `!x1 x2. x1 + x2 <= &2 /\ x1 <= &1 /\ x1 >= &0 /\ x2 >= &0
 769            ==> &3 * (x1 + &3 * x2 pow 2 + &2) <= &8 * (&2 * x1 + x2 + &1)`;;
 770 (*
 771 DATE -------  HOL
 772 4/29/2005    18430
 773 *)
 774
 775
 776
 777 (* ------------------------------------------------------------------------- *)
 778 (* From Collins & Johnson's "Sign variation..." article.                     *)
 779 (* ------------------------------------------------------------------------- *)
 780
 781 (* ---------------------------------    --------------------------------- *)
 782
 783 (*
 784 time real_qelim <<exists r. 0 < r /\ r < 1 /\
 785                 (1 - 3 * r) * (a^2 + b^2) + 2 * a * r > 0 /\
 786                 (2 - 3 * r) * (a^2 + b^2) + 4 * a * r - 2 * a - r < 0>>;;
 787 *)
 788 time REAL_QELIM_CONV `?r. &0 < r /\ r < &1 /\
 789                 (&1 - &3 * r) * (a pow 2 + b pow 2) + &2 * a * r > &0 /\
 790                 (&2 - &3 * r) * (a pow 2 + b pow 2) + &4 * a * r - &2 * a - r < &0`;;
 791 (*
 792 DATE -------  HOL
 793 4/29/2005    4595.11
 794 *)
 795
 796
 797 (* ------------------------------------------------------------------------- *)
 798 (* From "Parallel implementation of CAD" article.                            *)
 799 (* ------------------------------------------------------------------------- *)
 800
 801 (* ---------------------------------    --------------------------------- *)
 802
 803 (*
 804 time real_qelim <<exists x. forall y. x^2 + y^2 > 1 /\ x * y >= 1>>;;
 805 *)
 806 time REAL_QELIM_CONV `?x. !y. x pow 2 + y pow 2 > &1 /\ x * y >= &1`;;
 807 (*
 808 DATE -------  HOL
 809 4/29/2005    89.51
 810 *)
 811
 812
 813
 814 (* ------------------------------------------------------------------------- *)
 815 (* Other misc examples.                                                      *)
 816 (* ------------------------------------------------------------------------- *)
 817
 818 (* ---------------------------------    --------------------------------- *)
 819
 820 (*
 821 time real_qelim <<forall x y. x^2 + y^2 = 1 ==> 2 * x * y <= 1>>;;
 822 *)
 823 time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &1) ==> &2 * x * y <= &1`;;
 824 (*
 825 DATE -------  HOL
 826 4/29/2005    83.02
 827 *)
 828
 829 (* ---------------------------------    --------------------------------- *)
 830
 831 (*
 832 time real_qelim <<forall x y. x^2 + y^2 = 1 ==> 2 * x * y < 1>>;;
 833 *)
 834 time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &1) ==> &2 * x * y < &1`;;
 835 (*
 836 DATE -------  HOL
 837 4/29/2005    83.7
 838 *)
 839
 840 (* ---------------------------------    --------------------------------- *)
 841
 842 (*
 843 time real_qelim <<forall x y. x * y > 0 <=> x > 0 /\ y > 0 \/ x < 0 /\ y < 0>>;;
 844 *)
 845 time REAL_QELIM_CONV `!x y. x * y > &0 <=> x > &0 /\ y > &0 \/ x < &0 /\ y < &0`;;
 846 (*
 847 DATE -------  HOL
 848 4/29/2005    27.4
 849 *)
 850
 851 (* ---------------------------------    --------------------------------- *)
 852
 853 (*
 854 time real_qelim <<exists x y. x > y /\ x^2 < y^2>>;;
 855 *)
 856 time REAL_QELIM_CONV `?x y. x > y /\ x pow 2 < y pow 2`;;
 857 (*
 858 DATE -------  HOL
 859 4/29/2005    1.19
 860 *)
 861
 862 (* ---------------------------------    --------------------------------- *)
 863
 864 (*
 865 time real_qelim <<forall x y. x < y ==> exists z. x < z /\ z < y>>;;
 866 *)
 867 time REAL_QELIM_CONV `!x y. x < y ==> ?z. x < z /\ z < y`;;
 868 (*
 869 DATE -------  HOL
 870 4/29/2005    3.8
 871 *)
 872
 873 (* ---------------------------------    --------------------------------- *)
 874
 875 (*
 876 time real_qelim <<forall x. 0 < x <=> exists y. x * y^2 = 1>>;;
 877 *)
 878 time REAL_QELIM_CONV `!x. &0 < x <=> ?y. x * y pow 2 = &1`;;
 879 (*
 880 DATE -------  HOL
 881 4/29/2005    3.76
 882 *)
 883
 884 (* ---------------------------------    --------------------------------- *)
 885
 886 (*
 887 time real_qelim <<forall x. 0 <= x <=> exists y. x * y^2 = 1>>;;
 888 *)
 889 time REAL_QELIM_CONV `!x. &0 <= x <=> ?y. x * y pow 2 = &1`;;
 890 (*
 891 DATE -------  HOL
 892 4/29/2005    4.38
 893 *)
 894
 895 (* ---------------------------------    --------------------------------- *)
 896
 897 (*
 898 time real_qelim <<forall x. 0 <= x <=> exists y. x = y^2>>;;
 899 *)
 900 time REAL_QELIM_CONV `!x. &0 <= x <=> ?y. x = y pow 2`;;
 901 (*
 902 DATE -------  HOL
 903 4/29/2005    4.38
 904 *)
 905
 906 (* ---------------------------------    --------------------------------- *)
 907
 908 (*
 909 time real_qelim <<forall x y. 0 < x /\ x < y ==> exists z. x < z^2 /\ z^2 < y>>;;
 910 *)
 911 time REAL_QELIM_CONV `!x y. &0 < x /\ x < y ==> ?z. x < z pow 2 /\ z pow 2 < y`;;
 912 (*
 913 DATE -------  HOL
 914 4/29/2005    93.1
 915 *)
 916
 917 (* ---------------------------------    --------------------------------- *)
 918
 919 (*
 920 time real_qelim <<forall x y. x < y ==> exists z. x < z^2 /\ z^2 < y>>;;
 921 *)
 922 time REAL_QELIM_CONV `!x y. x < y ==> ?z. x < z pow 2 /\ z pow 2 < y`;;
 923 (*
 924 DATE -------  HOL
 925 4/29/2005    93.22
 926 *)
 927
 928 (* ---------------------------------    --------------------------------- *)
 929
 930 (*
 931 time real_qelim <<forall x y. x^2 + y^2 = 0 ==> x = 0 /\ y = 0>>;;
 932 *)
 933 time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &0) ==> (x = &0) /\ (y = &0)`;;
 934 (*
 935 DATE -------  HOL
 936 4/29/2005    17.21
 937 *)
 938
 939 (* ---------------------------------    --------------------------------- *)
 940
 941 (*
 942 time real_qelim <<forall x y z. x^2 + y^2 + z^2 = 0 ==> x = 0 /\ y = 0 /\ z = 0>>;;
 943 *)
 944 time REAL_QELIM_CONV `!x y z. (x pow 2 + y pow 2 + z pow 2 = &0) ==> (x = &0) /\ (y = &0) /\ (z = &0)`;;
 945
 946
 947 (* ---------------------------------    --------------------------------- *)
 948
 949 (*
 950 time real_qelim <<forall w x y z. w^2 + x^2 + y^2 + z^2 = 0
 951                       ==> w = 0 /\ x = 0 /\ y = 0 /\ z = 0>>;;
 952 *)
 953 time REAL_QELIM_CONV `!w x y z. (w pow 2 + x pow 2 + y pow 2 + z pow 2 = &0)
 954                       ==> (w = &0) /\ (x = &0) /\ (y = &0) /\ (z = &0)`;;
 955 (*
 956 DATE -------  HOL
 957 4/29/2005    596
 958 *)
 959
 960
 961 (* ---------------------------------    --------------------------------- *)
 962
 963 (*
 964 time real_qelim <<forall a. a^2 = 2 ==> forall x. ~(x^2 + a*x + 1 = 0)>>;;
 965 *)
 966 time REAL_QELIM_CONV `!a. (a pow 2 = &2) ==> !x. ~(x pow 2 + a*x + &1 = &0)`;;
 967
 968 (*
 969 DATE -------  HOL
 970 4/29/2005    8.7
 971 *)
 972
 973
 974 (* ---------------------------------    --------------------------------- *)
 975
 976 (*
 977 time real_qelim <<forall a. a^2 = 2 ==> forall x. ~(x^2 - a*x + 1 = 0)>>;;
 978 *)
 979 time REAL_QELIM_CONV `!a. (a pow 2 = &2) ==> !x. ~(x pow 2 - a*x + &1 = &0)`;;
 980 (*
 981 DATE -------  HOL
 982 4/29/2005    8.82
 983 *)
 984
 985
 986 (* ---------------------------------    --------------------------------- *)
 987
 988 (*
 989 time real_qelim <<forall x y. x^2 = 2 /\ y^2 = 3 ==> (x * y)^2 = 6>>;;
 990 *)
 991 time REAL_QELIM_CONV `!x y. (x pow 2 = &2) /\ (y pow 2 = &3) ==> ((x * y) pow 2 = &6)`;;
 992 (*
 993 DATE -------  HOL
 994 4/29/2005    48.59
 995 *)
 996
 997 (* ---------------------------------    --------------------------------- *)
 998
 999 (*
1000 time real_qelim <<forall x. exists y. x^2 = y^3>>;;
1001 *)
1002 time REAL_QELIM_CONV `!x. ?y. x pow 2 = y pow 3`;;
1003 (*
1004 DATE -------  HOL
1005 4/29/2005    6.93
1006 *)
1007
1008 (* ---------------------------------    --------------------------------- *)
1009
1010 (*
1011 time real_qelim <<forall x. exists y. x^3 = y^2>>;;
1012 *)
1013 time REAL_QELIM_CONV `!x. ?y. x pow 3 = y pow 2`;;
1014 (*
1015 DATE -------  HOL
1016 4/29/2005    5.76
1017 *)
1018
1019 (* ---------------------------------    --------------------------------- *)
1020
1021 (*
1022 time real_qelim
1023  <<forall a b c.
1024         (a * x^2 + b * x + c = 0) /\
1025         (a * y^2 + b * y + c = 0) /\
1026         ~(x = y)
1027         ==> (a * (x + y) + b = 0)>>;;
1028 *)
1029 time REAL_QELIM_CONV
1030  `!a b c.
1031         (a * x pow 2 + b * x + c = &0) /\
1032         (a * y pow 2 + b * y + c = &0) /\
1033         ~(x = y)
1034         ==> (a * (x + y) + b = &0)`;;
1035 (*
1036 DATE -------  HOL
1037 4/29/2005    76.5
1038 *)
1039
1040 (* ---------------------------------    --------------------------------- *)
1041
1042 (*
1043 time real_qelim
1044  <<forall y_1 y_2 y_3 y_4.
1045      (y_1 = 2 * y_3) /\
1046      (y_2 = 2 * y_4) /\
1047      (y_1 * y_3 = y_2 * y_4)
1048      ==> (y_1^2 = y_2^2)>>;;
1049 *)
1050 time REAL_QELIM_CONV
1051  `!y_1 y_2 y_3 y_4.
1052      (y_1 = &2 * y_3) /\
1053      (y_2 = &2 * y_4) /\
1054      (y_1 * y_3 = y_2 * y_4)
1055      ==> (y_1 pow 2 = y_2 pow 2)`;;
1056 (*
1057 time real_qelim <<forall x. x^2 < 1 <=> x^4 < 1>>;;
1058 *)
1059 (*
1060 DATE -------  HOL
1061 4/29/2005    1327
1062 *)
1063
1064
1065
1066 (* ------------------------------------------------------------------------- *)
1067 (* Counting roots.                                                           *)
1068 (* ------------------------------------------------------------------------- *)
1069
1070
1071 (* ---------------------------------    --------------------------------- *)
1072
1073 (*
1074 time real_qelim <<exists x. x^3 - x^2 + x - 1 = 0>>;;
1075 *)
1076 time REAL_QELIM_CONV `?x. x pow 3 - x pow 2 + x - &1 = &0`;;
1077 (*
1078 DATE -------  HOL
1079 4/29/2005    3.8
1080 *)
1081
1082
1083 (* ---------------------------------    --------------------------------- *)
1084
1085 (*
1086 time real_qelim
1087   <<exists x y. x^3 - x^2 + x - 1 = 0 /\ y^3 - y^2 + y - 1 = 0 /\ ~(x = y)>>;;
1088 *)
1089 time REAL_QELIM_CONV
1090   `?x y. (x pow 3 - x pow 2 + x - &1 = &0) /\ (y pow 3 - y pow 2 + y - &1 = &0) /\ ~(x = y)`;;
1091 (*
1092 DATE -------  HOL
1093 4/29/2005    670
1094 *)
1095
1096
1097 (* ---------------------------------    --------------------------------- *)
1098
1099 (*
1100 time real_qelim <<exists x. x^4 + x^2 - 2 = 0>>;;
1101 *)
1102 time REAL_QELIM_CONV `?x. x pow 4 + x pow 2 - &2 = &0`;;
1103 (*
1104 DATE -------  HOL
1105 4/29/2005     4.9
1106 *)
1107
1108
1109 (* ---------------------------------    --------------------------------- *)
1110
1111 (*
1112 time real_qelim
1113   <<exists x y. x^4 + x^2 - 2 = 0 /\ y^4 + y^2 - 2 = 0 /\ ~(x = y)>>;;
1114 *)
1115 time REAL_QELIM_CONV
1116   `?x y. x pow 4 + x pow 2 - &2 = &0 /\ y pow 4 + y pow 2 - &2 = &0 /\ ~(x = y)`;;
1117
1118 (* ---------------------------------    --------------------------------- *)
1119
1120 (*
1121 time real_qelim
1122   <<exists x y. x^3 + x^2 - x - 1 = 0 /\ y^3 + y^2 - y - 1 = 0 /\ ~(x = y)>>;;
1123 *)
1124 time REAL_QELIM_CONV
1125   `?x y. (x pow 3 + x pow 2 - x - &1 = &0) /\ (y pow 3 + y pow 2 - y - &1 = &0) /\ ~(x = y)`;;
1126
1127 (* ---------------------------------    --------------------------------- *)
1128
1129
1130 (*
1131 time real_qelim <<exists x y z. x^3 + x^2 - x - 1 = 0 /\
1132                     y^3 + y^2 - y - 1 = 0 /\
1133                     z^3 + z^2 - z - 1 = 0 /\ ~(x = y) /\ ~(x = z)>>;;
1134 *)
1135 time REAL_QELIM_CONV `?x y z. (x pow 3 + x pow 2 - x - &1 = &0) /\
1136                     (y pow 3 + y pow 2 - y - &1 = &0) /\
1137                     (z pow 3 + z pow 2 - z - &1 = &0) /\ ~(x = y) /\ ~(x = z)`;;
1138
1139 (* ------------------------------------------------------------------------- *)
1140 (* Existence of tangents, so to speak.                                       *)
1141 (* ------------------------------------------------------------------------- *)
1142
1143 (* ---------------------------------    --------------------------------- *)
1144
1145 (*
1146 time real_qelim
1147   <<forall x y. exists s c. s^2 + c^2 = 1 /\ s * x + c * y = 0>>;;
1148 *)
1149 time REAL_QELIM_CONV
1150   `!x y. ?s c. (s pow 2 + c pow 2 = &1) /\ s * x + c * y = &0`;;
1151
1152 (* ------------------------------------------------------------------------- *)
1153 (* Another useful thing (componentwise ==> normwise accuracy etc.)           *)
1154 (* ------------------------------------------------------------------------- *)
1155
1156 (* ---------------------------------    --------------------------------- *)
1157
1158 (*
1159 time real_qelim <<forall x y. (x + y)^2 <= 2 * (x^2 + y^2)>>;;
1160 *)
1161 time REAL_QELIM_CONV `!x y. (x + y) pow 2 <= &2 * (x pow 2 + y pow 2)`;;
1162
1163 (* ------------------------------------------------------------------------- *)
1164 (* Some related quantifier elimination problems.                             *)
1165 (* ------------------------------------------------------------------------- *)
1166
1167 (* ---------------------------------    --------------------------------- *)
1168
1169 (*
1170 time real_qelim <<forall x y. (x + y)^2 <= c * (x^2 + y^2)>>;;
1171 *)
1172 time REAL_QELIM_CONV `!x y. (x + y) pow 2 <= c * (x pow 2 + y pow 2)`;;
1173
1174 (* ---------------------------------    --------------------------------- *)
1175
1176 (*
1177 time real_qelim
1178   <<forall c. (forall x y. (x + y)^2 <= c * (x^2 + y^2)) <=> 2 <= c>>;;
1179 *)
1180 time REAL_QELIM_CONV
1181   `!c. (!x y. (x + y) pow 2 <= c * (x pow 2 + y pow 2)) <=> &2 <= c`;;
1182
1183 (* ---------------------------------    --------------------------------- *)
1184
1185 (*
1186 time real_qelim <<forall a b. a * b * c <= a^2 + b^2>>;;
1187 *)
1188 time REAL_QELIM_CONV `!a b. a * b * c <= a pow 2 + b pow 2`;;
1189
1190 (* ---------------------------------    --------------------------------- *)
1191
1192 (*
1193 time real_qelim
1194   <<forall c. (forall a b. a * b * c <= a^2 + b^2) <=> c^2 <= 4>>;;
1195 *)
1196 time REAL_QELIM_CONV
1197   `!c. (!a b. a * b * c <= a pow 2 + b pow 2) <=> c pow 2 <= &4`;;
1198
1199 (* ------------------------------------------------------------------------- *)
1200 (* Tedious lemmas I once proved manually in HOL.                             *)
1201 (* ------------------------------------------------------------------------- *)
1202
1203 (* ---------------------------------    --------------------------------- *)
1204
1205 (*
1206 time real_qelim
1207  <<forall a b c. 0 < a /\ 0 < b /\ 0 < c
1208                  ==> 0 < a * b /\ 0 < a * c /\ 0 < b * c>>;;
1209 *)
1210 time REAL_QELIM_CONV
1211  `!a b c. &0 < a /\ &0 < b /\ &0 < c
1212                  ==> &0 < a * b /\ &0 < a * c /\ &0 < b * c`;;
1213
1214 (* ---------------------------------    --------------------------------- *)
1215
1216 (*
1217 time real_qelim
1218   <<forall a b c. a * b > 0 ==> (c * a < 0 <=> c * b < 0)>>;;
1219 *)
1220 time REAL_QELIM_CONV
1221   `!a b c. a * b > &0 ==> (c * a < &0 <=> c * b < &0)`;;
1222
1223 (* ---------------------------------    --------------------------------- *)
1224
1225 (*
1226 time real_qelim
1227   <<forall a b c. a * b > 0 ==> (a * c < 0 <=> b * c < 0)>>;;
1228 *)
1229 time REAL_QELIM_CONV
1230   `!a b c. a * b > &0 ==> (a * c < &0 <=> b * c < &0)`;;
1231
1232 (* ---------------------------------    --------------------------------- *)
1233
1234 (*
1235 time real_qelim
1236   <<forall a b. a < 0 ==> (a * b > 0 <=> b < 0)>>;;
1237 *)
1238 time REAL_QELIM_CONV
1239   `!a b. a < &0 ==> (a * b > &0 <=> b < &0)`;;
1240
1241 (* ---------------------------------    --------------------------------- *)
1242
1243 (*
1244 time real_qelim
1245   <<forall a b c. a * b < 0 /\ ~(c = 0) ==> (c * a < 0 <=> ~(c * b < 0))>>;;
1246 *)
1247 time REAL_QELIM_CONV
1248   `!a b c. a * b < &0 /\ ~(c = &0) ==> (c * a < &0 <=> ~(c * b < &0))`;;
1249
1250 (* ---------------------------------    --------------------------------- *)
1251
1252 (*
1253 time real_qelim
1254   <<forall a b. a * b < 0 <=> a > 0 /\ b < 0 \/ a < 0 /\ b > 0>>;;
1255 *)
1256 time REAL_QELIM_CONV
1257   `!a b. a * b < &0 <=> a > &0 /\ b < &0 \/ a < &0 /\ b > &0`;;
1258
1259 (* ---------------------------------    --------------------------------- *)
1260
1261 (*
1262 time real_qelim
1263   <<forall a b. a * b <= 0 <=> a >= 0 /\ b <= 0 \/ a <= 0 /\ b >= 0>>;;
1264 *)
1265 time REAL_QELIM_CONV
1266   `!a b. a * b <= &0 <=> a >= &0 /\ b <= &0 \/ a <= &0 /\ b >= &0`;;
1267
1268 (* ------------------------------------------------------------------------- *)
1269 (* Vaguely connected with reductions for Robinson arithmetic.                *)
1270 (* ------------------------------------------------------------------------- *)
1271
1272 (* ---------------------------------    --------------------------------- *)
1273
1274 (*
1275 time real_qelim
1276   <<forall a b. ~(a <= b) <=> forall d. d <= b ==> d < a>>;;
1277 *)
1278 time REAL_QELIM_CONV
1279   `!a b. ~(a <= b) <=> !d. d <= b ==> d < a`;;
1280
1281 (* ---------------------------------    --------------------------------- *)
1282
1283 (*
1284 time real_qelim
1285   <<forall a b. ~(a <= b) <=> forall d. d <= b ==> ~(d = a)>>;;
1286 *)
1287 time REAL_QELIM_CONV
1288   `!a b. ~(a <= b) <=> !d. d <= b ==> ~(d = a)`;;
1289
1290 (* ---------------------------------    --------------------------------- *)
1291
1292 (*
1293 time real_qelim
1294   <<forall a b. ~(a < b) <=> forall d. d < b ==> d < a>>;;
1295 *)
1296 time REAL_QELIM_CONV
1297   `!a b. ~(a < b) <=> !d. d < b ==> d < a`;;
1298
1299 (* ------------------------------------------------------------------------- *)
1300 (* Another nice problem.                                                     *)
1301 (* ------------------------------------------------------------------------- *)
1302
1303 (* ---------------------------------    --------------------------------- *)
1304
1305 (*
1306 time real_qelim
1307  <<forall x y. x^2 + y^2 = 1 ==> (x + y)^2 <= 2>>;;
1308 *)
1309 time REAL_QELIM_CONV
1310  `!x y. (x pow 2 + y pow 2 = &1) ==> (x + y) pow 2 <= &2`;;
1311
1312 (* ------------------------------------------------------------------------- *)
1313 (* Some variants / intermediate steps in Cauchy-Schwartz inequality.         *)
1314 (* ------------------------------------------------------------------------- *)
1315
1316 (* ---------------------------------    --------------------------------- *)
1317
1318 (*
1319 time real_qelim
1320  <<forall x y. 2 * x * y <= x^2 + y^2>>;;
1321 *)
1322 time REAL_QELIM_CONV
1323  `!x y. &2 * x * y <= x pow 2 + y pow 2`;;
1324
1325 (* ---------------------------------    --------------------------------- *)
1326
1327 (*
1328 time real_qelim
1329  <<forall a b c d. 2 * a * b * c * d <= a^2 * b^2 + c^2 * d^2>>;;
1330 *)
1331 time REAL_QELIM_CONV
1332  `!a b c d. &2 * a * b * c * d <= a pow 2 * b pow 2 + c pow 2 * d pow 2`;;
1333
1334 (* ---------------------------------    --------------------------------- *)
1335
1336 (*
1337 time real_qelim
1338  <<forall x1 x2 y1 y2.
1339       (x1 * y1 + x2 * y2)^2 <= (x1^2 + x2^2) * (y1^2 + y2^2)>>;;
1340 *)
1341 time REAL_QELIM_CONV
1342  `!x1 x2 y1 y2.
1343       (x1 * y1 + x2 * y2) pow 2 <= (x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2)`;;
1344
1345 (* ------------------------------------------------------------------------- *)
1346 (* The determinant example works OK here too.                                *)
1347 (* ------------------------------------------------------------------------- *)
1348
1349 (* ---------------------------------    --------------------------------- *)
1350
1351 (*
1352 time real_qelim
1353  <<exists w x y z. (a * w + b * y = 1) /\
1354                    (a * x + b * z = 0) /\
1355                    (c * w + d * y = 0) /\
1356                    (c * x + d * z = 1)>>;;
1357 *)
1358 time REAL_QELIM_CONV
1359  `?w x y z. (a * w + b * y = &1) /\
1360                    (a * x + b * z = &0) /\
1361                    (c * w + d * y = &0) /\
1362                    (c * x + d * z = &1)`;;
1363
1364 (* ---------------------------------    --------------------------------- *)
1365
1366 (*
1367 time real_qelim
1368  <<forall a b c d.
1369         (exists w x y z. (a * w + b * y = 1) /\
1370                          (a * x + b * z = 0) /\
1371                          (c * w + d * y = 0) /\
1372                          (c * x + d * z = 1))
1373         <=> ~(a * d = b * c)>>;;
1374 *)
1375 time REAL_QELIM_CONV
1376  `!a b c d.
1377         (?w x y z. (a * w + b * y = &1) /\
1378                          (a * x + b * z = &0) /\
1379                          (c * w + d * y = &0) /\
1380                          (c * x + d * z = &1))
1381         <=> ~(a * d = b * c)`;;
1382
1383 (* ------------------------------------------------------------------------- *)
1384 (* From applying SOLOVAY_VECTOR_TAC.                                         *)
1385 (* ------------------------------------------------------------------------- *)
1386
1387 let th = prove
1388  (`&0 <= c' /\ &0 <= c /\ &0 < h * c'
1389    ==> (?u. &0 < u /\
1390             (!v. &0 < v /\ v <= u
1391                  ==> v * (v * (h * h * c' + c) - h * c') - (v * h * c' - c') <
1392                      c'))`,
1393   W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
1394   CONV_TAC REAL_QELIM_CONV);;
1395
1396 (* ------------------------------------------------------------------------- *)
1397 (* Two notions of parallelism.                                               *)
1398 (* ------------------------------------------------------------------------- *)
1399
1400 time REAL_QELIM_CONV
1401   `!x1 x2 y1 y2. (?c. (x2 = c * x1) /\ (y2 = c * y1)) <=>
1402                  (x1 = &0 /\ y1 = &0 ==> x2 = &0 /\ y2 = &0) /\
1403                  x1 * y2 = x2 * y1`;;
1404
1405 (* ------------------------------------------------------------------------- *)
1406 (* From Behzad Akbarpour (takes about 300 seconds).                          *)
1407 (* ------------------------------------------------------------------------- *)
1408
1409 time REAL_QELIM_CONV
1410   `!x. &0 <= x /\ x <= &1
1411        ==> &0 < &1 - x + x pow 2 / &2 - x pow 3 / &6 /\
1412            &1 <= (&1 + x + x pow 2) *
1413            (&1 - x + x pow 2 / &2 - x pow 3 / &6)`;;
1414
1415 (* ------------------------------------------------------------------------- *)
1416 (* A natural simplification of "limit of a product" result.                  *)
1417 (* Takes about 450 seconds.                                                  *)
1418 (* ------------------------------------------------------------------------- *)
1419
1420 (*** Would actually like to get rid of abs internally and state it like this:
1421
1422 time REAL_QELIM_CONV
1423  `!x y e. &0 < e ==> ?d. &0 < d /\ abs((x + d) * (y + d) - x * y) < e`;;
1424
1425 ****)
1426
1427 time REAL_QELIM_CONV
1428  `!x y e. &0 < e ==> ?d. &0 < d /\ (x + d) * (y + d) - x * y < e /\
1429                                    x * y - (x + d) * (y + d) < e`;;