(* ========================================================================= *) (* Some examples of full complex quantifier elimination. *) (* ========================================================================= *) let th = time prove (`!x y. (x pow 2 = Cx(&2)) /\ (y pow 2 = Cx(&3)) ==> ((x * y) pow 2 = Cx(&6))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!x a. (a pow 2 = Cx(&2)) /\ (x pow 2 + a * x + Cx(&1) = Cx(&0)) ==> (x pow 4 + Cx(&1) = Cx(&0))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!a x. (a pow 2 = Cx(&2)) /\ (x pow 2 + a * x + Cx(&1) = Cx(&0)) ==> (x pow 4 + Cx(&1) = Cx(&0))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`~(?a x y. (a pow 2 = Cx(&2)) /\ (x pow 2 + a * x + Cx(&1) = Cx(&0)) /\ (y * (x pow 4 + Cx(&1)) + Cx(&1) = Cx(&0)))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!x. ?y. x pow 2 = y pow 3`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!x y z a b. (a + b) * (x - y + z) - (a - b) * (x + y + z) = Cx(&2) * (b * x + b * z - a * y)`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!a b. ~(a = b) ==> ?x y. (y * x pow 2 = a) /\ (y * x pow 2 + x = b)`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\ (a * y pow 2 + b * y + c = Cx(&0)) /\ ~(x = y) ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; let th = time prove (`~(!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\ (a * y pow 2 + b * y + c = Cx(&0)) ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0)))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; (** geometric example from ``Algorithms for Computer Algebra'': right triangle where perp. bisector of hypotenuse passes through the right angle is isoseles. **) let th = time prove (`!y_1 y_2 y_3 y_4. (y_1 = Cx(&2) * y_3) /\ (y_2 = Cx(&2) * y_4) /\ (y_1 * y_3 = y_2 * y_4) ==> (y_1 pow 2 = y_2 pow 2)`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; (** geometric example: gradient condition for two lines to be non-parallel. **) let th = time prove (`!a1 b1 c1 a2 b2 c2. ~(a1 * b2 = a2 * b1) ==> ?x y. (a1 * x + b1 * y = c1) /\ (a2 * x + b2 * y = c2)`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; (*********** Apparently takes too long let th = time prove (`!a b c x y. (a * x pow 2 + b * x + c = Cx(&0)) /\ (a * y pow 2 + b * y + c = Cx(&0)) /\ (!z. (a * z pow 2 + b * z + c = Cx(&0)) ==> (z = x) \/ (z = y)) ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; *************) (* ------------------------------------------------------------------------- *) (* Any three points determine a circle. Not true in complex number version! *) (* ------------------------------------------------------------------------- *) (******** And it takes a lot of memory! let th = time prove (`~(!x1 y1 x2 y2 x3 y3. ?x0 y0. ((x1 - x0) pow 2 + (y1 - y0) pow 2 = (x2 - x0) pow 2 + (y2 - y0) pow 2) /\ ((x2 - x0) pow 2 + (y2 - y0) pow 2 = (x3 - x0) pow 2 + (y3 - y0) pow 2))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; **************) (* ------------------------------------------------------------------------- *) (* To show we don't need to consider only closed formulas. *) (* Can eliminate some, then deal with the rest manually and painfully. *) (* ------------------------------------------------------------------------- *) let th = time prove (`(?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\ (a * y pow 2 + b * y + c = Cx(&0)) /\ ~(x = y)) <=> (a = Cx(&0)) /\ (b = Cx(&0)) /\ (c = Cx(&0)) \/ ~(a = Cx(&0)) /\ ~(b pow 2 = Cx(&4) * a * c)`, CONV_TAC(LAND_CONV FULL_COMPLEX_QUELIM_CONV) THEN REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_LID; COMPLEX_ADD_RID] THEN REWRITE_TAC[COMPLEX_ENTIRE; CX_INJ; REAL_OF_NUM_EQ; ARITH] THEN ASM_CASES_TAC `a = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THENL [ASM_CASES_TAC `b = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO]; ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `b * b * c * Cx(--(&1)) + a * c * c * Cx(&4) = c * (Cx(&4) * a * c - b * b)`] THEN ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `b * b * b * Cx(--(&1)) + a * b * c * Cx (&4) = b * (Cx(&4) * a * c - b * b)`] THEN ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `b * b * Cx (&1) + a * c * Cx(--(&4)) = Cx(--(&1)) * (Cx(&4) * a * c - b * b)`] THEN REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_SUB_0; CX_INJ] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_CASES_TAC `b = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `c = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[COMPLEX_POW_2; COMPLEX_MUL_RZERO; COMPLEX_MUL_LZERO] THEN REWRITE_TAC[EQ_SYM_EQ]]);; (* ------------------------------------------------------------------------- *) (* Do the same thing directly. *) (* ------------------------------------------------------------------------- *) (**** This seems barely feasible let th = time prove (`!a b c. (?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\ (a * y pow 2 + b * y + c = Cx(&0)) /\ ~(x = y)) <=> (a = Cx(&0)) /\ (b = Cx(&0)) /\ (c = Cx(&0)) \/ ~(a = Cx(&0)) /\ ~(b pow 2 = Cx(&4) * a * c)`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; ****) (* ------------------------------------------------------------------------- *) (* More ambitious: determine a unique circle. Also not true over complexes. *) (* (consider the points (k, k i) where i is the imaginary unit...) *) (* ------------------------------------------------------------------------- *) (********** Takes too long, I think, and too much memory too let th = prove (`~(!x1 y1 x2 y2 x3 y3 x0 y0 x0' y0'. ((x1 - x0) pow 2 + (y1 - y0) pow 2 = (x2 - x0) pow 2 + (y2 - y0) pow 2) /\ ((x2 - x0) pow 2 + (y2 - y0) pow 2 = (x3 - x0) pow 2 + (y3 - y0) pow 2) /\ ((x1 - x0') pow 2 + (y1 - y0') pow 2 = (x2 - x0') pow 2 + (y2 - y0') pow 2) /\ ((x2 - x0') pow 2 + (y2 - y0') pow 2 = (x3 - x0') pow 2 + (y3 - y0') pow 2) ==> (x0 = x0') /\ (y0 = y0'))`, CONV_TAC FULL_COMPLEX_QUELIM_CONV);; *************) (* ------------------------------------------------------------------------- *) (* Side of a triangle in terms of its bisectors; Kapur survey 5.1. *) (* ------------------------------------------------------------------------- *) (************* let th = time FULL_COMPLEX_QUELIM_CONV `?b c. (p1 = ai pow 2 * (b + c) pow 2 - c * b * (c + b - a) * (c + b + a)) /\ (p2 = ae pow 2 * (c - b) pow 2 - c * b * (a + b - c) * (a - b + a)) /\ (p3 = be pow 2 * (c - a) pow 2 - a * c * (a + b - c) * (c + b - a))`;; *************)