1 (* ========================================================================= *)
2 (* Some examples of full complex quantifier elimination. *)
3 (* ========================================================================= *)
6 (`!x y. (x pow 2 = Cx(&2)) /\ (y pow 2 = Cx(&3))
7 ==> ((x * y) pow 2 = Cx(&6))`,
8 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
11 (`!x a. (a pow 2 = Cx(&2)) /\ (x pow 2 + a * x + Cx(&1) = Cx(&0))
12 ==> (x pow 4 + Cx(&1) = Cx(&0))`,
13 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
16 (`!a x. (a pow 2 = Cx(&2)) /\ (x pow 2 + a * x + Cx(&1) = Cx(&0))
17 ==> (x pow 4 + Cx(&1) = Cx(&0))`,
18 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
21 (`~(?a x y. (a pow 2 = Cx(&2)) /\
22 (x pow 2 + a * x + Cx(&1) = Cx(&0)) /\
23 (y * (x pow 4 + Cx(&1)) + Cx(&1) = Cx(&0)))`,
24 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
27 (`!x. ?y. x pow 2 = y pow 3`,
28 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
31 (`!x y z a b. (a + b) * (x - y + z) - (a - b) * (x + y + z) =
32 Cx(&2) * (b * x + b * z - a * y)`,
33 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
36 (`!a b. ~(a = b) ==> ?x y. (y * x pow 2 = a) /\ (y * x pow 2 + x = b)`,
37 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
40 (`!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
41 (a * y pow 2 + b * y + c = Cx(&0)) /\
43 ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0))`,
44 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
47 (`~(!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
48 (a * y pow 2 + b * y + c = Cx(&0))
49 ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0)))`,
50 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
52 (** geometric example from ``Algorithms for Computer Algebra'':
53 right triangle where perp. bisector of hypotenuse passes through the
54 right angle is isoseles.
59 (y_1 = Cx(&2) * y_3) /\
60 (y_2 = Cx(&2) * y_4) /\
61 (y_1 * y_3 = y_2 * y_4)
62 ==> (y_1 pow 2 = y_2 pow 2)`,
63 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
65 (** geometric example: gradient condition for two lines to be non-parallel.
71 ==> ?x y. (a1 * x + b1 * y = c1) /\ (a2 * x + b2 * y = c2)`,
72 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
74 (*********** Apparently takes too long
77 (`!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
78 (a * y pow 2 + b * y + c = Cx(&0)) /\
79 (!z. (a * z pow 2 + b * z + c = Cx(&0))
80 ==> (z = x) \/ (z = y))
81 ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0))`,
82 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
86 (* ------------------------------------------------------------------------- *)
87 (* Any three points determine a circle. Not true in complex number version! *)
88 (* ------------------------------------------------------------------------- *)
90 (******** And it takes a lot of memory!
93 (`~(!x1 y1 x2 y2 x3 y3.
94 ?x0 y0. ((x1 - x0) pow 2 + (y1 - y0) pow 2 =
95 (x2 - x0) pow 2 + (y2 - y0) pow 2) /\
96 ((x2 - x0) pow 2 + (y2 - y0) pow 2 =
97 (x3 - x0) pow 2 + (y3 - y0) pow 2))`,
98 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
102 (* ------------------------------------------------------------------------- *)
103 (* To show we don't need to consider only closed formulas. *)
104 (* Can eliminate some, then deal with the rest manually and painfully. *)
105 (* ------------------------------------------------------------------------- *)
108 (`(?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
109 (a * y pow 2 + b * y + c = Cx(&0)) /\
111 (a = Cx(&0)) /\ (b = Cx(&0)) /\ (c = Cx(&0)) \/
112 ~(a = Cx(&0)) /\ ~(b pow 2 = Cx(&4) * a * c)`,
113 CONV_TAC(LAND_CONV FULL_COMPLEX_QUELIM_CONV) THEN
114 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_LID; COMPLEX_ADD_RID] THEN
115 REWRITE_TAC[COMPLEX_ENTIRE; CX_INJ; REAL_OF_NUM_EQ; ARITH] THEN
116 ASM_CASES_TAC `a = Cx(&0)` THEN
117 ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THENL
118 [ASM_CASES_TAC `b = Cx(&0)` THEN
119 ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO];
120 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH
121 `b * b * c * Cx(--(&1)) + a * c * c * Cx(&4) =
122 c * (Cx(&4) * a * c - b * b)`] THEN
123 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH
124 `b * b * b * Cx(--(&1)) + a * b * c * Cx (&4) =
125 b * (Cx(&4) * a * c - b * b)`] THEN
126 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH
127 `b * b * Cx (&1) + a * c * Cx(--(&4)) =
128 Cx(--(&1)) * (Cx(&4) * a * c - b * b)`] THEN
129 REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_SUB_0; CX_INJ] THEN
130 CONV_TAC REAL_RAT_REDUCE_CONV THEN
131 ASM_CASES_TAC `b = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
132 ASM_CASES_TAC `c = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
133 REWRITE_TAC[COMPLEX_POW_2; COMPLEX_MUL_RZERO; COMPLEX_MUL_LZERO] THEN
134 REWRITE_TAC[EQ_SYM_EQ]]);;
136 (* ------------------------------------------------------------------------- *)
137 (* Do the same thing directly. *)
138 (* ------------------------------------------------------------------------- *)
140 (**** This seems barely feasible
144 (?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
145 (a * y pow 2 + b * y + c = Cx(&0)) /\
147 (a = Cx(&0)) /\ (b = Cx(&0)) /\ (c = Cx(&0)) \/
148 ~(a = Cx(&0)) /\ ~(b pow 2 = Cx(&4) * a * c)`,
149 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
153 (* ------------------------------------------------------------------------- *)
154 (* More ambitious: determine a unique circle. Also not true over complexes. *)
155 (* (consider the points (k, k i) where i is the imaginary unit...) *)
156 (* ------------------------------------------------------------------------- *)
158 (********** Takes too long, I think, and too much memory too
161 (`~(!x1 y1 x2 y2 x3 y3 x0 y0 x0' y0'.
162 ((x1 - x0) pow 2 + (y1 - y0) pow 2 =
163 (x2 - x0) pow 2 + (y2 - y0) pow 2) /\
164 ((x2 - x0) pow 2 + (y2 - y0) pow 2 =
165 (x3 - x0) pow 2 + (y3 - y0) pow 2) /\
166 ((x1 - x0') pow 2 + (y1 - y0') pow 2 =
167 (x2 - x0') pow 2 + (y2 - y0') pow 2) /\
168 ((x2 - x0') pow 2 + (y2 - y0') pow 2 =
169 (x3 - x0') pow 2 + (y3 - y0') pow 2)
170 ==> (x0 = x0') /\ (y0 = y0'))`,
171 CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
175 (* ------------------------------------------------------------------------- *)
176 (* Side of a triangle in terms of its bisectors; Kapur survey 5.1. *)
177 (* ------------------------------------------------------------------------- *)
180 let th = time FULL_COMPLEX_QUELIM_CONV
181 `?b c. (p1 = ai pow 2 * (b + c) pow 2 - c * b * (c + b - a) * (c + b + a)) /\
182 (p2 = ae pow 2 * (c - b) pow 2 - c * b * (a + b - c) * (a - b + a)) /\
183 (p3 = be pow 2 * (c - a) pow 2 - a * c * (a + b - c) * (c + b - a))`;;