(* ---------------------------------------------------------------------- *)
(* 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);;