(* ---------------------------------------------------------------------- *)
(*  Paper                                                                 *)
(* ---------------------------------------------------------------------- *)

(* ----------------------------  Chebychev  ----------------------------- *)

time REAL_QELIM_CONV
  `!x. --(&1) <= x /\ x <= &1 ==>
    -- (&1) <= &2 * x pow 2 - &1 /\ &2 * x pow 2 - &1 <= &1`;;

(*
DATE -------  HOL --------
5/20         4.92
5/22         4.67
*)

time REAL_QELIM_CONV
  `!x. --(&1) <= x /\ x <= &1 ==>
    -- (&1) <= &4 * x pow 3 - &3 * x /\ &4 * x pow 3 - &3 * x <= &1`;;

(*
DATE -------  HOL --------
5/20         14.38
5/22         13.65
*)

time REAL_QELIM_CONV
 `&1 < &2 /\ (!x. &1 < x ==> &1 < x pow 2) /\
 (!x y. &1 < x /\ &1 < y ==> &1 < x * (&1 + &2 * y))`;;


(*
DATE -------  HOL --------
5/22         23.61
*)

time REAL_QELIM_CONV
 `&0 <= b /\ &0 <= c /\ &0 < a * c ==> ?u. &0 < u /\ u * (u * c - a * c) -
   (u * a * c - (a pow 2 * c + b)) < a pow 2 * c + b`;;

(*
DATE -------  HOL --------
5/22         8.78
*)


(* ------------------------------------------------------------------------- *)
(* Examples.                                                                 *)
(* ------------------------------------------------------------------------- *)




(* ---------------------------------    --------------------------------- *)
(*
time real_qelim <<exists x. x^4 + x^2 + 1 = 0>>;;
0.01

let fm = `?x. x pow 4 + x pow 2 + &1 = &0`;;
let vars = []
*)


time REAL_QELIM_CONV `?x. x pow 4 + x pow 2 + &1 = &0`;;



(*
DATE -------  HOL --------
4/29/2005    3.19
5/19         2.2
5/20         1.96
5/22         1.53
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - x^2 + x - 1 = 0>>;;
0.01
*)

time REAL_QELIM_CONV `?x. x pow 3 - x pow 2 + x - &1 = &0`;;

(*
DATE -------  HOL --------
4/29/2005    3.83
5/22/2005    1.69
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<exists x y. x^3 - x^2 + x - 1 = 0 /\
              y^3 - y^2 + y - 1 = 0 /\ ~(x = y)>>;;
0.23
*)

time REAL_QELIM_CONV
 `?x y. (x pow 3 - x pow 2 + x - &1 = &0) /\
              (y pow 3 - y pow 2 + y - &1 = &0) /\ ~(x = y)`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   682.85          3000
5/17/2005   345.27
5/22        269
*)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim
 <<forall a f k. (forall e. k < e ==> f < a * e) ==> f <= a * k>>;;
0.02
*)

time REAL_QELIM_CONV
 `!a f k. (!e. k < e ==> f < a * e) ==> f <= a * k`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   20.91          1000
5/15/2005   17.98
5/17/2005   15.12
5/18/2005   12.87
5/22        12.09
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<exists x. a * x^2 + b * x + c = 0>>;;
0.01
*)

time REAL_QELIM_CONV
 `?x. a * x pow 2 + b * x + c = &0`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   10.99          1000
5/17/2005   6.42
5/18         5.39
5/22         4.74
*)

(* ---------------------------------    --------------------------------- *)
(*
time real_qelim
 <<forall a b c. (exists x. a * x^2 + b * x + c = 0) <=>
                 b^2 >= 4 * a * c>>;;
0.51
*)

time REAL_QELIM_CONV
 `!a b c. (?x. a * x pow 2 + b * x + c = &0) <=>
                 b pow 2 >= &4 * a * c`;;


(*
DATE -------  HOL -------- Factor
4/29/2005   1200.99          2400
5/17         878.25
*)


(* ---------------------------------    --------------------------------- *)
(*
time real_qelim
 <<forall a b c. (exists x. a * x^2 + b * x + c = 0) <=>
                 a = 0 /\ (~(b = 0) \/ c = 0) \/
                 ~(a = 0) /\ b^2 >= 4 * a * c>>;;

0.51
*)
time REAL_QELIM_CONV
 `!a b c. (?x. a * x pow 2 + b * x + c = &0) <=>
                 (a = &0) /\ (~(b = &0) \/ (c = &0)) \/
                 ~(a = &0) /\ b pow 2 >= &4 * a * c`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   1173.9          2400
5/17         848.4
5/20         816

1095 during depot update
*)


(*
time real_qelim <<exists x. 0 <= x /\ x <= 1 /\ (r * r * x * x - r * (1 + r) * x + (1 + r) = 0)
/\ ~(2 * r * x = 1 + r)>>
*)
time REAL_QELIM_CONV
  `?x. &0 <= x /\ x <= &1 /\ (r pow 2 * x pow 2 - r * (&1 + r) * x + (&1 + r) = &0)
   /\ ~(&2 * r * x = &1 + r)`;;

(*
DATE -------  HOL -------- Factor
5/20/2005   19021          1460

4000 line output
*)




(* ------------------------------------------------------------------------- *)
(* Termination ordering for group theory completion.                         *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Left this out                                                             *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* This one works better using DNF.                                          *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* And this                                                                  *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Linear examples.                                                          *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x - 1 > 0>>;;
0
*)

time REAL_QELIM_CONV `?x. x - &1 > &0`;;
(*
DATE -------  HOL
4/29/2005    .56
*)

(* ---------------------------------    --------------------------------- *)
(*
time real_qelim <<exists x. 3 - x > 0 /\ x - 1 > 0>>;;
0
*)

time REAL_QELIM_CONV `?x. &3 - x > &0 /\ x - &1 > &0`;;

(*
DATE -------  HOL
4/29/2005    1.66
*)

(* ------------------------------------------------------------------------- *)
(* Quadratics.                                                               *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)
(*
time real_qelim <<exists x. x^2 = 0>>;;
0
*)

time REAL_QELIM_CONV `?x. x pow 2 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.12
*)

(* ---------------------------------    --------------------------------- *)
(*
time real_qelim <<exists x. x^2 + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 + &1 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.11
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 - 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 - &1 = &0`;;

(*
DATE -------  HOL
4/29/2005    1.54
*)
(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 - 2 * x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 - &2 * x + &1 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.21
*)
(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 - 3 * x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 - &3 * x + &1 = &0`;;

(*
DATE -------  HOL
4/29/2005    1.75
*)


(* ------------------------------------------------------------------------- *)
(* Cubics.                                                                   *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - 1 > 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 3 - &1 > &0`;;

(*
DATE -------  HOL
4/29/2005    1.96
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - 3 * x^2 + 3 * x - 1 > 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 3 - &3 * x pow 2 + &3 * x - &1 > &0`;;
(*
DATE -------  HOL
4/29/2005    1.97
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - 4 * x^2 + 5 * x - 2 > 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 3 - &4 * x pow 2 + &5 * x - &2 > &0`;;
(*
DATE -------  HOL
4/29/2005    4.89
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - 6 * x^2 + 11 * x - 6 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 3 - &6 * x pow 2 + &11 * x - &6 = &0`;;
(*
DATE -------  HOL
4/29/2005    4.17
*)


(* ------------------------------------------------------------------------- *)
(* Quartics.                                                                 *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^4 - 1 > 0>>;;
*)

time REAL_QELIM_CONV `?x. x pow 4 - &1 > &0`;;
(*
DATE -------  HOL
4/29/2005    3.07
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^4 + 1 > 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 + &1 > &0`;;
(*
DATE -------  HOL
4/29/2005    2.47
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^4 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 = &0`;;
(*
DATE -------  HOL
4/29/2005    2.48
*)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x. x^4 - x^3 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 - x pow 3 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.76
*)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x. x^4 - x^2 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 - x pow 2 = &0`;;
(*
DATE -------  HOL
4/29/2005    2.16
*)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x. x^4 - 2 * x^2 + 2 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 - &2 * x pow 2 + &2 = &0`;;
(*
DATE -------  HOL
4/29/2005    6.87
5/16/2005    5.22
*)

(* ------------------------------------------------------------------------- *)
(* Quintics.                                                                 *)
(* ------------------------------------------------------------------------- *)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<exists x. x^5 - 15 * x^4 + 85 * x^3 - 225 * x^2 + 274 * x - 120 = 0>>;;
0.03

print_timers()
*)

time REAL_QELIM_CONV
  `?x. x pow 5 - &15 * x pow 4 + &85 * x pow 3 - &225 * x pow 2 + &274 * x - &120 = &0`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   65.64          2500
5/15/2005   55.93
5/16/2005   47.72
*)


(* ------------------------------------------------------------------------- *)
(* Sextics(?)                                                                *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x.
 x^6 - 21 * x^5 + 175 * x^4 - 735 * x^3 + 1624 * x^2 - 1764 * x + 720 = 0>>;;
0.15
*)

time REAL_QELIM_CONV `?x.
 x pow 6 - &21 * x pow 5 + &175 * x pow 4 - &735 * x pow 3 + &1624 * x pow 2 - &1764 * x + &720 = &0`;;
  `?x. x pow 5 - &15 * x pow 4 + &85 * x pow 3 - &225 * x pow 2 + &274 * x - &120 = &0`;;

(*
DATE -------  HOL -------- Factor
4/29/2005   1400.4          10000
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x.
 x^6 - 12 * x^5 + 56 * x^4 - 130 * x^3 + 159 * x^2 - 98 * x + 24 = 0>>;;
7.54
*)

(* NOT YET *)
(*
time REAL_QELIM_CONV `?x.
 x pow 6 - &12 * x pow 5 + &56 * x pow 4 - &130 * x pow 3 + &159 * x pow 2 - &98 * x + &24 = &0`;;
*)

(* ------------------------------------------------------------------------- *)
(* Multiple polynomials.                                                     *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 + 2 > 0 /\ x^3 - 11 = 0 /\ x + 131 >= 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 + &2 > &0 /\ (x pow 3 - &11 = &0) /\ x + &131 >= &0`;;
(*
DATE -------  HOL
4/29/2005    13.1
*)

(* ------------------------------------------------------------------------- *)
(* With more variables.                                                      *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. a * x^2 + b * x + c = 0>>;;
*)
time REAL_QELIM_CONV `?x. a * x pow 2 + b * x + c = &0`;;
(*
DATE -------  HOL
4/29/2005    10.94
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. a * x^3 + b * x^2 + c * x + d = 0>>;;
*)
time REAL_QELIM_CONV `?x. a * x pow 3 + b * x pow 2 + c * x + d = &0`;;
(*
DATE -------  HOL
4/29/2005    269.17
*)



(* ------------------------------------------------------------------------- *)
(* Constraint solving.                                                       *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x1 x2. x1^2 + x2^2 - u1 <= 0 /\ x1^2 - u2 > 0>>;;
*)
time REAL_QELIM_CONV `?x1 x2. x1 pow 2 + x2 pow 2 - u1 <= &0 /\ x1 pow 2 - u2 > &0`;;
(*
DATE -------  HOL
4/29/2005    89.97
*)

(* ------------------------------------------------------------------------- *)
(* Huet & Oppen (interpretation of group theory).                            *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x > 0 /\ y > 0 ==> x * (1 + 2 * y) > 0>>;;
*)
time REAL_QELIM_CONV `!x y. x > &0 /\ y > &0 ==> x * (&1 + &2 * y) > &0`;;
(*
DATE -------  HOL
4/29/2005    5.03
*)


(* ------------------------------------------------------------------------- *)
(* Other examples.                                                           *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 - x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 - x + &1 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.19
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^2 - 3 * x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 2 - &3 * x + &1 = &0`;;
(*
DATE -------  HOL
4/29/2005    1.65
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x > 6 /\ (x^2 - 3 * x + 1 = 0)>>;;
*)
time REAL_QELIM_CONV `?x. x > &6 /\ (x pow 2 - &3 * x + &1 = &0)`;;
(*
DATE -------  HOL
4/29/2005    3.63
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. 7 * x^2 - 5 * x + 3 > 0 /\
                            x^2 - 3 * x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. &7 * x pow 2 - &5 * x + &3 > &0 /\
                            (x pow 2 - &3 * x + &1 = &0)`;;

(*
DATE -------  HOL
4/29/2005    8.62
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. 11 * x^3 - 7 * x^2 - 2 * x + 1 = 0 /\
                            7 * x^2 - 5 * x + 3 > 0 /\
                            x^2 - 8 * x + 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. (&11 * x pow 3 - &7 * x pow 2 - &2 * x + &1 = &0) /\
                            &7 * x pow 2 - &5 * x + &3 > &0 /\
                            (x pow 2 - &8 * x + &1 = &0)`;;
(*
DATE -------  HOL
4/29/2005    221.4
*)


(* ------------------------------------------------------------------------- *)
(* Quadratic inequality from Liska and Steinberg                             *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x. -(1) <= x /\ x <= 1 ==>
      C * (x - 1) * (4 * x * a * C - x * C - 4 * a * C + C - 2) >= 0>>;;
*)
time REAL_QELIM_CONV
 `!x. -- &1 <= x /\ x <= &1 ==>
      C * (x - &1) * (&4 * x * a * C - x * C - &4 * a * C + C - &2) >= &0`;;
(*
DATE -------  HOL
4/29/2005    1493
*)


(* ------------------------------------------------------------------------- *)
(* Metal-milling example from Loos and Weispfenning                          *)
(* ------------------------------------------------------------------------- *)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<exists x y. 0 < x /\
                y < 0 /\
                x * r - x * t + t = q * x - s * x + s /\
                x * b - x * d + d = a * y - c * y + c>>;;
*)
time REAL_QELIM_CONV
  `?x y. &0 < x /\
                y < &0 /\
                (x * r - x * t + t = q * x - s * x + s) /\
                (x * b - x * d + d = a * y - c * y + c)`;;


(* ------------------------------------------------------------------------- *)
(* Linear example from Collins and Johnson                                   *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<exists r. 0 < r /\
      r < 1 /\
      0 < (1 - 3 * r) * (a^2 + b^2) + 2 * a * r /\
      (2 - 3 * r) * (a^2 + b^2) + 4 * a * r - 2 * a - r < 0>>;;
*)
time REAL_QELIM_CONV
 `?r. &0 < r /\
      r < &1 /\
      &0 < (&1 - &3 * r) * (a pow 2 + b pow 2) + &2 * a * r /\
      (&2 - &3 * r) * (a pow 2 + b pow 2) + &4 * a * r - &2 * a - r < &0`;;


(* ------------------------------------------------------------------------- *)
(* Dave Griffioen #4                                                         *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x y. (1 - t) * x <= (1 + t) * y /\ (1 - t) * y <= (1 + t) * x
         ==> 0 <= y>>;;
*)
time REAL_QELIM_CONV
 `!x y. (&1 - t) * x <= (&1 + t) * y /\ (&1 - t) * y <= (&1 + t) * x
         ==> &0 <= y`;;

(*
DATE -------  HOL
4/29/2005    893
*)


(* ------------------------------------------------------------------------- *)
(* Some examples from "Real Quantifier Elimination in practice".             *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x2. x1^2 + x2^2 <= u1 /\ x1^2 > u2>>;;
*)
time REAL_QELIM_CONV `?x2. x1 pow 2 + x2 pow 2 <= u1 /\ x1 pow 2 > u2`;;
(*
DATE -------  HOL
4/29/2005    4
*)

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x1 x2. x1^2 + x2^2 <= u1 /\ x1^2 > u2>>;;
*)
time REAL_QELIM_CONV `?x1 x2. x1 pow 2 + x2 pow 2 <= u1 /\ x1 pow 2 > u2`;;
(*
DATE -------  HOL
4/29/2005    90
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x1 x2. x1 + x2 <= 2 /\ x1 <= 1 /\ x1 >= 0 /\ x2 >= 0
           ==> 3 * (x1 + 3 * x2^2 + 2) <= 8 * (2 * x1 + x2 + 1)>>;;
*)
time REAL_QELIM_CONV
 `!x1 x2. x1 + x2 <= &2 /\ x1 <= &1 /\ x1 >= &0 /\ x2 >= &0
           ==> &3 * (x1 + &3 * x2 pow 2 + &2) <= &8 * (&2 * x1 + x2 + &1)`;;
(*
DATE -------  HOL
4/29/2005    18430
*)



(* ------------------------------------------------------------------------- *)
(* From Collins & Johnson's "Sign variation..." article.                     *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists r. 0 < r /\ r < 1 /\
                (1 - 3 * r) * (a^2 + b^2) + 2 * a * r > 0 /\
                (2 - 3 * r) * (a^2 + b^2) + 4 * a * r - 2 * a - r < 0>>;;
*)
time REAL_QELIM_CONV `?r. &0 < r /\ r < &1 /\
                (&1 - &3 * r) * (a pow 2 + b pow 2) + &2 * a * r > &0 /\
                (&2 - &3 * r) * (a pow 2 + b pow 2) + &4 * a * r - &2 * a - r < &0`;;
(*
DATE -------  HOL
4/29/2005    4595.11
*)


(* ------------------------------------------------------------------------- *)
(* From "Parallel implementation of CAD" article.                            *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. forall y. x^2 + y^2 > 1 /\ x * y >= 1>>;;
*)
time REAL_QELIM_CONV `?x. !y. x pow 2 + y pow 2 > &1 /\ x * y >= &1`;;
(*
DATE -------  HOL
4/29/2005    89.51
*)



(* ------------------------------------------------------------------------- *)
(* Other misc examples.                                                      *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x^2 + y^2 = 1 ==> 2 * x * y <= 1>>;;
*)
time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &1) ==> &2 * x * y <= &1`;;
(*
DATE -------  HOL
4/29/2005    83.02
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x^2 + y^2 = 1 ==> 2 * x * y < 1>>;;
*)
time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &1) ==> &2 * x * y < &1`;;
(*
DATE -------  HOL
4/29/2005    83.7
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x * y > 0 <=> x > 0 /\ y > 0 \/ x < 0 /\ y < 0>>;;
*)
time REAL_QELIM_CONV `!x y. x * y > &0 <=> x > &0 /\ y > &0 \/ x < &0 /\ y < &0`;;
(*
DATE -------  HOL
4/29/2005    27.4
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x y. x > y /\ x^2 < y^2>>;;
*)
time REAL_QELIM_CONV `?x y. x > y /\ x pow 2 < y pow 2`;;
(*
DATE -------  HOL
4/29/2005    1.19
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x < y ==> exists z. x < z /\ z < y>>;;
*)
time REAL_QELIM_CONV `!x y. x < y ==> ?z. x < z /\ z < y`;;
(*
DATE -------  HOL
4/29/2005    3.8
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x. 0 < x <=> exists y. x * y^2 = 1>>;;
*)
time REAL_QELIM_CONV `!x. &0 < x <=> ?y. x * y pow 2 = &1`;;
(*
DATE -------  HOL
4/29/2005    3.76
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x. 0 <= x <=> exists y. x * y^2 = 1>>;;
*)
time REAL_QELIM_CONV `!x. &0 <= x <=> ?y. x * y pow 2 = &1`;;
(*
DATE -------  HOL
4/29/2005    4.38
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x. 0 <= x <=> exists y. x = y^2>>;;
*)
time REAL_QELIM_CONV `!x. &0 <= x <=> ?y. x = y pow 2`;;
(*
DATE -------  HOL
4/29/2005    4.38
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. 0 < x /\ x < y ==> exists z. x < z^2 /\ z^2 < y>>;;
*)
time REAL_QELIM_CONV `!x y. &0 < x /\ x < y ==> ?z. x < z pow 2 /\ z pow 2 < y`;;
(*
DATE -------  HOL
4/29/2005    93.1
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x < y ==> exists z. x < z^2 /\ z^2 < y>>;;
*)
time REAL_QELIM_CONV `!x y. x < y ==> ?z. x < z pow 2 /\ z pow 2 < y`;;
(*
DATE -------  HOL
4/29/2005    93.22
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x^2 + y^2 = 0 ==> x = 0 /\ y = 0>>;;
*)
time REAL_QELIM_CONV `!x y. (x pow 2 + y pow 2 = &0) ==> (x = &0) /\ (y = &0)`;;
(*
DATE -------  HOL
4/29/2005    17.21
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y z. x^2 + y^2 + z^2 = 0 ==> x = 0 /\ y = 0 /\ z = 0>>;;
*)
time REAL_QELIM_CONV `!x y z. (x pow 2 + y pow 2 + z pow 2 = &0) ==> (x = &0) /\ (y = &0) /\ (z = &0)`;;


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall w x y z. w^2 + x^2 + y^2 + z^2 = 0
                      ==> w = 0 /\ x = 0 /\ y = 0 /\ z = 0>>;;
*)
time REAL_QELIM_CONV `!w x y z. (w pow 2 + x pow 2 + y pow 2 + z pow 2 = &0)
                      ==> (w = &0) /\ (x = &0) /\ (y = &0) /\ (z = &0)`;;
(*
DATE -------  HOL
4/29/2005    596
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall a. a^2 = 2 ==> forall x. ~(x^2 + a*x + 1 = 0)>>;;
*)
time REAL_QELIM_CONV `!a. (a pow 2 = &2) ==> !x. ~(x pow 2 + a*x + &1 = &0)`;;

(*
DATE -------  HOL
4/29/2005    8.7
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall a. a^2 = 2 ==> forall x. ~(x^2 - a*x + 1 = 0)>>;;
*)
time REAL_QELIM_CONV `!a. (a pow 2 = &2) ==> !x. ~(x pow 2 - a*x + &1 = &0)`;;
(*
DATE -------  HOL
4/29/2005    8.82
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. x^2 = 2 /\ y^2 = 3 ==> (x * y)^2 = 6>>;;
*)
time REAL_QELIM_CONV `!x y. (x pow 2 = &2) /\ (y pow 2 = &3) ==> ((x * y) pow 2 = &6)`;;
(*
DATE -------  HOL
4/29/2005    48.59
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x. exists y. x^2 = y^3>>;;
*)
time REAL_QELIM_CONV `!x. ?y. x pow 2 = y pow 3`;;
(*
DATE -------  HOL
4/29/2005    6.93
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x. exists y. x^3 = y^2>>;;
*)
time REAL_QELIM_CONV `!x. ?y. x pow 3 = y pow 2`;;
(*
DATE -------  HOL
4/29/2005    5.76
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall a b c.
        (a * x^2 + b * x + c = 0) /\
        (a * y^2 + b * y + c = 0) /\
        ~(x = y)
        ==> (a * (x + y) + b = 0)>>;;
*)
time REAL_QELIM_CONV
 `!a b c.
        (a * x pow 2 + b * x + c = &0) /\
        (a * y pow 2 + b * y + c = &0) /\
        ~(x = y)
        ==> (a * (x + y) + b = &0)`;;
(*
DATE -------  HOL
4/29/2005    76.5
*)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall y_1 y_2 y_3 y_4.
     (y_1 = 2 * y_3) /\
     (y_2 = 2 * y_4) /\
     (y_1 * y_3 = y_2 * y_4)
     ==> (y_1^2 = y_2^2)>>;;
*)
time REAL_QELIM_CONV
 `!y_1 y_2 y_3 y_4.
     (y_1 = &2 * y_3) /\
     (y_2 = &2 * y_4) /\
     (y_1 * y_3 = y_2 * y_4)
     ==> (y_1 pow 2 = y_2 pow 2)`;;
(*
time real_qelim <<forall x. x^2 < 1 <=> x^4 < 1>>;;
*)
(*
DATE -------  HOL
4/29/2005    1327
*)



(* ------------------------------------------------------------------------- *)
(* Counting roots.                                                           *)
(* ------------------------------------------------------------------------- *)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^3 - x^2 + x - 1 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 3 - x pow 2 + x - &1 = &0`;;
(*
DATE -------  HOL
4/29/2005    3.8
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<exists x y. x^3 - x^2 + x - 1 = 0 /\ y^3 - y^2 + y - 1 = 0 /\ ~(x = y)>>;;
*)
time REAL_QELIM_CONV
  `?x y. (x pow 3 - x pow 2 + x - &1 = &0) /\ (y pow 3 - y pow 2 + y - &1 = &0) /\ ~(x = y)`;;
(*
DATE -------  HOL
4/29/2005    670
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<exists x. x^4 + x^2 - 2 = 0>>;;
*)
time REAL_QELIM_CONV `?x. x pow 4 + x pow 2 - &2 = &0`;;
(*
DATE -------  HOL
4/29/2005     4.9
*)


(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<exists x y. x^4 + x^2 - 2 = 0 /\ y^4 + y^2 - 2 = 0 /\ ~(x = y)>>;;
*)
time REAL_QELIM_CONV
  `?x y. x pow 4 + x pow 2 - &2 = &0 /\ y pow 4 + y pow 2 - &2 = &0 /\ ~(x = y)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<exists x y. x^3 + x^2 - x - 1 = 0 /\ y^3 + y^2 - y - 1 = 0 /\ ~(x = y)>>;;
*)
time REAL_QELIM_CONV
  `?x y. (x pow 3 + x pow 2 - x - &1 = &0) /\ (y pow 3 + y pow 2 - y - &1 = &0) /\ ~(x = y)`;;

(* ---------------------------------    --------------------------------- *)


(*
time real_qelim <<exists x y z. x^3 + x^2 - x - 1 = 0 /\
                    y^3 + y^2 - y - 1 = 0 /\
                    z^3 + z^2 - z - 1 = 0 /\ ~(x = y) /\ ~(x = z)>>;;
*)
time REAL_QELIM_CONV `?x y z. (x pow 3 + x pow 2 - x - &1 = &0) /\
                    (y pow 3 + y pow 2 - y - &1 = &0) /\
                    (z pow 3 + z pow 2 - z - &1 = &0) /\ ~(x = y) /\ ~(x = z)`;;

(* ------------------------------------------------------------------------- *)
(* Existence of tangents, so to speak.                                       *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall x y. exists s c. s^2 + c^2 = 1 /\ s * x + c * y = 0>>;;
*)
time REAL_QELIM_CONV
  `!x y. ?s c. (s pow 2 + c pow 2 = &1) /\ s * x + c * y = &0`;;

(* ------------------------------------------------------------------------- *)
(* Another useful thing (componentwise ==> normwise accuracy etc.)           *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. (x + y)^2 <= 2 * (x^2 + y^2)>>;;
*)
time REAL_QELIM_CONV `!x y. (x + y) pow 2 <= &2 * (x pow 2 + y pow 2)`;;

(* ------------------------------------------------------------------------- *)
(* Some related quantifier elimination problems.                             *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall x y. (x + y)^2 <= c * (x^2 + y^2)>>;;
*)
time REAL_QELIM_CONV `!x y. (x + y) pow 2 <= c * (x pow 2 + y pow 2)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall c. (forall x y. (x + y)^2 <= c * (x^2 + y^2)) <=> 2 <= c>>;;
*)
time REAL_QELIM_CONV
  `!c. (!x y. (x + y) pow 2 <= c * (x pow 2 + y pow 2)) <=> &2 <= c`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim <<forall a b. a * b * c <= a^2 + b^2>>;;
*)
time REAL_QELIM_CONV `!a b. a * b * c <= a pow 2 + b pow 2`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall c. (forall a b. a * b * c <= a^2 + b^2) <=> c^2 <= 4>>;;
*)
time REAL_QELIM_CONV
  `!c. (!a b. a * b * c <= a pow 2 + b pow 2) <=> c pow 2 <= &4`;;

(* ------------------------------------------------------------------------- *)
(* Tedious lemmas I once proved manually in HOL.                             *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall a b c. 0 < a /\ 0 < b /\ 0 < c
                 ==> 0 < a * b /\ 0 < a * c /\ 0 < b * c>>;;
*)
time REAL_QELIM_CONV
 `!a b c. &0 < a /\ &0 < b /\ &0 < c
                 ==> &0 < a * b /\ &0 < a * c /\ &0 < b * c`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b c. a * b > 0 ==> (c * a < 0 <=> c * b < 0)>>;;
*)
time REAL_QELIM_CONV
  `!a b c. a * b > &0 ==> (c * a < &0 <=> c * b < &0)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b c. a * b > 0 ==> (a * c < 0 <=> b * c < 0)>>;;
*)
time REAL_QELIM_CONV
  `!a b c. a * b > &0 ==> (a * c < &0 <=> b * c < &0)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. a < 0 ==> (a * b > 0 <=> b < 0)>>;;
*)
time REAL_QELIM_CONV
  `!a b. a < &0 ==> (a * b > &0 <=> b < &0)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b c. a * b < 0 /\ ~(c = 0) ==> (c * a < 0 <=> ~(c * b < 0))>>;;
*)
time REAL_QELIM_CONV
  `!a b c. a * b < &0 /\ ~(c = &0) ==> (c * a < &0 <=> ~(c * b < &0))`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. a * b < 0 <=> a > 0 /\ b < 0 \/ a < 0 /\ b > 0>>;;
*)
time REAL_QELIM_CONV
  `!a b. a * b < &0 <=> a > &0 /\ b < &0 \/ a < &0 /\ b > &0`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. a * b <= 0 <=> a >= 0 /\ b <= 0 \/ a <= 0 /\ b >= 0>>;;
*)
time REAL_QELIM_CONV
  `!a b. a * b <= &0 <=> a >= &0 /\ b <= &0 \/ a <= &0 /\ b >= &0`;;

(* ------------------------------------------------------------------------- *)
(* Vaguely connected with reductions for Robinson arithmetic.                *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. ~(a <= b) <=> forall d. d <= b ==> d < a>>;;
*)
time REAL_QELIM_CONV
  `!a b. ~(a <= b) <=> !d. d <= b ==> d < a`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. ~(a <= b) <=> forall d. d <= b ==> ~(d = a)>>;;
*)
time REAL_QELIM_CONV
  `!a b. ~(a <= b) <=> !d. d <= b ==> ~(d = a)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
  <<forall a b. ~(a < b) <=> forall d. d < b ==> d < a>>;;
*)
time REAL_QELIM_CONV
  `!a b. ~(a < b) <=> !d. d < b ==> d < a`;;

(* ------------------------------------------------------------------------- *)
(* Another nice problem.                                                     *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x y. x^2 + y^2 = 1 ==> (x + y)^2 <= 2>>;;
*)
time REAL_QELIM_CONV
 `!x y. (x pow 2 + y pow 2 = &1) ==> (x + y) pow 2 <= &2`;;

(* ------------------------------------------------------------------------- *)
(* Some variants / intermediate steps in Cauchy-Schwartz inequality.         *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x y. 2 * x * y <= x^2 + y^2>>;;
*)
time REAL_QELIM_CONV
 `!x y. &2 * x * y <= x pow 2 + y pow 2`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall a b c d. 2 * a * b * c * d <= a^2 * b^2 + c^2 * d^2>>;;
*)
time REAL_QELIM_CONV
 `!a b c d. &2 * a * b * c * d <= a pow 2 * b pow 2 + c pow 2 * d pow 2`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall x1 x2 y1 y2.
      (x1 * y1 + x2 * y2)^2 <= (x1^2 + x2^2) * (y1^2 + y2^2)>>;;
*)
time REAL_QELIM_CONV
 `!x1 x2 y1 y2.
      (x1 * y1 + x2 * y2) pow 2 <= (x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2)`;;

(* ------------------------------------------------------------------------- *)
(* The determinant example works OK here too.                                *)
(* ------------------------------------------------------------------------- *)

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<exists w x y z. (a * w + b * y = 1) /\
                   (a * x + b * z = 0) /\
                   (c * w + d * y = 0) /\
                   (c * x + d * z = 1)>>;;
*)
time REAL_QELIM_CONV
 `?w x y z. (a * w + b * y = &1) /\
                   (a * x + b * z = &0) /\
                   (c * w + d * y = &0) /\
                   (c * x + d * z = &1)`;;

(* ---------------------------------    --------------------------------- *)

(*
time real_qelim
 <<forall a b c d.
        (exists w x y z. (a * w + b * y = 1) /\
                         (a * x + b * z = 0) /\
                         (c * w + d * y = 0) /\
                         (c * x + d * z = 1))
        <=> ~(a * d = b * c)>>;;
*)
time REAL_QELIM_CONV
 `!a b c d.
        (?w x y z. (a * w + b * y = &1) /\
                         (a * x + b * z = &0) /\
                         (c * w + d * y = &0) /\
                         (c * x + d * z = &1))
        <=> ~(a * d = b * c)`;;

(* ------------------------------------------------------------------------- *)
(* From applying SOLOVAY_VECTOR_TAC.                                         *)
(* ------------------------------------------------------------------------- *)

let th = prove
 (`&0 <= c' /\ &0 <= c /\ &0 < h * c'
   ==> (?u. &0 < u /\
            (!v. &0 < v /\ v <= u
                 ==> v * (v * (h * h * c' + c) - h * c') - (v * h * c' - c') <
                     c'))`,
  W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
  CONV_TAC REAL_QELIM_CONV);;

(* ------------------------------------------------------------------------- *)
(* Two notions of parallelism.                                               *)
(* ------------------------------------------------------------------------- *)

time REAL_QELIM_CONV
  `!x1 x2 y1 y2. (?c. (x2 = c * x1) /\ (y2 = c * y1)) <=>
                 (x1 = &0 /\ y1 = &0 ==> x2 = &0 /\ y2 = &0) /\
                 x1 * y2 = x2 * y1`;;

(* ------------------------------------------------------------------------- *)
(* From Behzad Akbarpour (takes about 300 seconds).                          *)
(* ------------------------------------------------------------------------- *)

time REAL_QELIM_CONV
  `!x. &0 <= x /\ x <= &1
       ==> &0 < &1 - x + x pow 2 / &2 - x pow 3 / &6 /\
           &1 <= (&1 + x + x pow 2) *
           (&1 - x + x pow 2 / &2 - x pow 3 / &6)`;;

(* ------------------------------------------------------------------------- *)
(* A natural simplification of "limit of a product" result.                  *)
(* Takes about 450 seconds.                                                  *)
(* ------------------------------------------------------------------------- *)

(*** Would actually like to get rid of abs internally and state it like this:

time REAL_QELIM_CONV
 `!x y e. &0 < e ==> ?d. &0 < d /\ abs((x + d) * (y + d) - x * y) < e`;;

****)

time REAL_QELIM_CONV
 `!x y e. &0 < e ==> ?d. &0 < d /\ (x + d) * (y + d) - x * y < e /\
                                   x * y - (x + d) * (y + d) < e`;;