Complex/quelim_examples.ml

   1 (* ========================================================================= *)
   2 (* Some examples of full complex quantifier elimination.                     *)
   3 (* ========================================================================= *)
   4
   5 let th = time prove
   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);;
   9
  10 let th = time prove
  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);;
  14
  15 let th = time prove
  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);;
  19
  20 let th = time prove
  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);;
  25
  26 let th = time prove
  27  (`!x. ?y. x pow 2 = y pow 3`,
  28   CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
  29
  30 let th = time prove
  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);;
  34
  35 let th = time prove
  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);;
  38
  39 let th = time prove
  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)) /\
  42                ~(x = y)
  43                ==> (a * x * y = c) /\ (a * (x + y) + b = Cx(&0))`,
  44   CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
  45
  46 let th = time prove
  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);;
  51
  52 (** geometric example from ``Algorithms for Computer Algebra'':
  53     right triangle where perp. bisector of hypotenuse passes through the
  54     right angle is isoseles.
  55  **)
  56
  57 let th = time prove
  58  (`!y_1 y_2 y_3 y_4.
  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);;
  64
  65 (** geometric example: gradient condition for two lines to be non-parallel.
  66  **)
  67
  68 let th = time prove
  69  (`!a1 b1 c1 a2 b2 c2.
  70         ~(a1 * b2 = a2 * b1)
  71         ==> ?x y. (a1 * x + b1 * y = c1) /\ (a2 * x + b2 * y = c2)`,
  72   CONV_TAC FULL_COMPLEX_QUELIM_CONV);;
  73
  74 (*********** Apparently takes too long
  75
  76 let th = time prove
  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);;
  83
  84 *************)
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* Any three points determine a circle. Not true in complex number version!  *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 (******** And it takes a lot of memory!
  91
  92 let th = time prove
  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);;
  99
 100  **************)
 101
 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 (* ------------------------------------------------------------------------- *)
 106
 107 let th = time prove
 108  (`(?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
 109           (a * y pow 2 + b * y + c = Cx(&0)) /\
 110           ~(x = y)) <=>
 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]]);;
 135
 136 (* ------------------------------------------------------------------------- *)
 137 (* Do the same thing directly.                                               *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 (**** This seems barely feasible
 141
 142 let th = time prove
 143  (`!a b c.
 144       (?x y. (a * x pow 2 + b * x + c = Cx(&0)) /\
 145              (a * y pow 2 + b * y + c = Cx(&0)) /\
 146              ~(x = y)) <=>
 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);;
 150
 151  ****)
 152
 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 (* ------------------------------------------------------------------------- *)
 157
 158 (********** Takes too long, I think, and too much memory too
 159
 160 let th = prove
 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);;
 172
 173  *************)
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Side of a triangle in terms of its bisectors; Kapur survey 5.1.           *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179 (*************
 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))`;;
 184
 185  *************)