colo12-c703.uibk.ac.at Git - Complex Analysis/.git/blob - Complex/grobner_examples.ml

   1 (* ========================================================================= *)
   2 (* Examples of using the Grobner basis procedure.                            *)
   3 (* ========================================================================= *)
   4
   5 time COMPLEX_ARITH
   6   `!a b c.
   7         (a * x pow 2 + b * x + c = Cx(&0)) /\
   8         (a * y pow 2 + b * y + c = Cx(&0)) /\
   9         ~(x = y)
  10         ==> (a * (x + y) + b = Cx(&0))`;;
  11
  12 time COMPLEX_ARITH
  13   `!a b c.
  14         (a * x pow 2 + b * x + c = Cx(&0)) /\
  15         (Cx(&2) * a * y pow 2 + Cx(&2) * b * y + Cx(&2) * c = Cx(&0)) /\
  16         ~(x = y)
  17         ==> (a * (x + y) + b = Cx(&0))`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Another example.                                                          *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 time COMPLEX_ARITH
  24  `~((y_1 = Cx(&2) * y_3) /\
  25     (y_2 = Cx(&2) * y_4) /\
  26     (y_1 * y_3 = y_2 * y_4) /\
  27     ((y_1 pow 2 - y_2 pow 2) * z = Cx(&1)))`;;
  28
  29 time COMPLEX_ARITH
  30   `!y_1 y_2 y_3 y_4.
  31        (y_1 = Cx(&2) * y_3) /\
  32        (y_2 = Cx(&2) * y_4) /\
  33        (y_1 * y_3 = y_2 * y_4)
  34        ==> (y_1 pow 2 = y_2 pow 2)`;;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Angle at centre vs. angle at circumference.                               *)
  38 (* Formulation from "Real quantifier elimination in practice" paper.         *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 time COMPLEX_ARITH
  42   `~((c pow 2 = a pow 2 + b pow 2) /\
  43      (c pow 2 = x0 pow 2 + (y0 - b) pow 2) /\
  44      (y0 * t1 = a + x0) /\
  45      (y0 * t2 = a - x0) /\
  46      ((Cx(&1) - t1 * t2) * t = t1 + t2) /\
  47      (u * (b * t - a) = Cx(&1)) /\
  48      (v1 * a + v2 * x0 + v3 * y0 = Cx(&1)))`;;
  49
  50 time COMPLEX_ARITH
  51   `(c pow 2 = a pow 2 + b pow 2) /\
  52    (c pow 2 = x0 pow 2 + (y0 - b) pow 2) /\
  53    (y0 * t1 = a + x0) /\
  54    (y0 * t2 = a - x0) /\
  55    ((Cx(&1) - t1 * t2) * t = t1 + t2) /\
  56    (~(a = Cx(&0)) \/ ~(x0 = Cx(&0)) \/ ~(y0 = Cx(&0)))
  57    ==> (b * t = a)`;;
  58
  59 time COMPLEX_ARITH
  60   `(c pow 2 = a pow 2 + b pow 2) /\
  61    (c pow 2 = x0 pow 2 + (y0 - b) pow 2) /\
  62    (y0 * t1 = a + x0) /\
  63    (y0 * t2 = a - x0) /\
  64    ((Cx(&1) - t1 * t2) * t = t1 + t2) /\
  65    (~(a = Cx(&0)) /\ ~(x0 = Cx(&0)) /\ ~(y0 = Cx(&0)))
  66    ==> (b * t = a)`;;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Another example (note we rule out points 1, 2 or 3 coinciding).           *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 time COMPLEX_ARITH
  73  `((x1 - x0) pow 2 + (y1 - y0) pow 2 =
  74    (x2 - x0) pow 2 + (y2 - y0) pow 2) /\
  75   ((x2 - x0) pow 2 + (y2 - y0) pow 2 =
  76    (x3 - x0) pow 2 + (y3 - y0) pow 2) /\
  77   ((x1 - x0') pow 2 + (y1 - y0') pow 2 =
  78    (x2 - x0') pow 2 + (y2 - y0') pow 2) /\
  79   ((x2 - x0') pow 2 + (y2 - y0') pow 2 =
  80    (x3 - x0') pow 2 + (y3 - y0') pow 2) /\
  81   (a12 * (x1 - x2) + b12 * (y1 - y2) = Cx(&1)) /\
  82   (a13 * (x1 - x3) + b13 * (y1 - y3) = Cx(&1)) /\
  83   (a23 * (x2 - x3) + b23 * (y2 - y3) = Cx(&1)) /\
  84   ~((x1 - x0) pow 2 + (y1 - y0) pow 2 = Cx(&0))
  85   ==> (x0' = x0) /\ (y0' = y0)`;;
  86
  87 time COMPLEX_ARITH
  88  `~(((x1 - x0) pow 2 + (y1 - y0) pow 2 =
  89    (x2 - x0) pow 2 + (y2 - y0) pow 2) /\
  90   ((x2 - x0) pow 2 + (y2 - y0) pow 2 =
  91    (x3 - x0) pow 2 + (y3 - y0) pow 2) /\
  92   ((x1 - x0') pow 2 + (y1 - y0') pow 2 =
  93    (x2 - x0') pow 2 + (y2 - y0') pow 2) /\
  94   ((x2 - x0') pow 2 + (y2 - y0') pow 2 =
  95    (x3 - x0') pow 2 + (y3 - y0') pow 2) /\
  96   (a12 * (x1 - x2) + b12 * (y1 - y2) = Cx(&1)) /\
  97   (a13 * (x1 - x3) + b13 * (y1 - y3) = Cx(&1)) /\
  98   (a23 * (x2 - x3) + b23 * (y2 - y3) = Cx(&1)) /\
  99   (z * (x0' - x0) = Cx(&1)) /\
 100   (z' * (y0' - y0) = Cx(&1)) /\
 101   (z'' * ((x1 - x0) pow 2 + (y1 - y0) pow 2) = Cx(&1)) /\
 102   (z''' * ((x1 - x09) pow 2 + (y1 - y09) pow 2) = Cx(&1)))`;;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* These are pure algebraic simplification.                                  *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let LAGRANGE_4 = time COMPLEX_ARITH
 109  `(((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) *
 110    ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2))) =
 111   ((((((x1*y1) - (x2*y2)) - (x3*y3)) - (x4*y4)) pow 2)  +
 112    (((((x1*y2) + (x2*y1)) + (x3*y4)) - (x4*y3)) pow 2)  +
 113    (((((x1*y3) - (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2)  +
 114    (((((x1*y4) + (x2*y3)) - (x3*y2)) + (x4*y1)) pow 2))`;;
 115
 116 let LAGRANGE_8 = time COMPLEX_ARITH
 117  `((p1 pow 2 + q1 pow 2 + r1 pow 2 + s1 pow 2 + t1 pow 2 + u1 pow 2 + v1 pow 2 + w1 pow 2) *
 118    (p2 pow 2 + q2 pow 2 + r2 pow 2 + s2 pow 2 + t2 pow 2 + u2 pow 2 + v2 pow 2 + w2 pow 2)) =
 119    ((p1 * p2 - q1 * q2 - r1 * r2 - s1 * s2 - t1 * t2 - u1 * u2 - v1 * v2 - w1* w2) pow 2 +
 120     (p1 * q2 + q1 * p2 + r1 * s2 - s1 * r2 + t1 * u2 - u1 * t2 - v1 * w2 + w1* v2) pow 2 +
 121     (p1 * r2 - q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 - v1 * t2 - w1* u2) pow 2 +
 122     (p1 * s2 + q1 * r2 - r1 * q2 + s1 * p2 + t1 * w2 - u1 * v2 + v1 * u2 - w1* t2) pow 2 +
 123     (p1 * t2 - q1 * u2 - r1 * v2 - s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 + w1* s2) pow 2 +
 124     (p1 * u2 + q1 * t2 - r1 * w2 + s1 * v2 - t1 * q2 + u1 * p2 - v1 * s2 + w1* r2) pow 2 +
 125     (p1 * v2 + q1 * w2 + r1 * t2 - s1 * u2 - t1 * r2 + u1 * s2 + v1 * p2 - w1* q2) pow 2 +
 126     (p1 * w2 - q1 * v2 + r1 * u2 + s1 * t2 - t1 * s2 - u1 * r2 + v1 * q2 + w1* p2) pow 2)`;;
 127
 128 let LIOUVILLE = time COMPLEX_ARITH
 129  `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2) =
 130   (Cx(&1 / &6) * ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
 131                 (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) +
 132    Cx(&1 / &6) * ((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
 133                 (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4))`;;
 134
 135 let FLECK = time COMPLEX_ARITH
 136  `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 3) =
 137   (Cx(&1 / &60) * ((x1 + x2 + x3) pow 6 + (x1 + x2 - x3) pow 6 +
 138                  (x1 - x2 + x3) pow 6 + (x1 - x2 - x3) pow 6 +
 139                  (x1 + x2 + x4) pow 6 + (x1 + x2 - x4) pow 6 +
 140                  (x1 - x2 + x4) pow 6 + (x1 - x2 - x4) pow 6 +
 141                  (x1 + x3 + x4) pow 6 + (x1 + x3 - x4) pow 6 +
 142                  (x1 - x3 + x4) pow 6 + (x1 - x3 - x4) pow 6 +
 143                  (x2 + x3 + x4) pow 6 + (x2 + x3 - x4) pow 6 +
 144                  (x2 - x3 + x4) pow 6 + (x2 - x3 - x4) pow 6) +
 145    Cx(&1 / &30) * ((x1 + x2) pow 6 + (x1 - x2) pow 6 +
 146                  (x1 + x3) pow 6 + (x1 - x3) pow 6 +
 147                  (x1 + x4) pow 6 + (x1 - x4) pow 6 +
 148                  (x2 + x3) pow 6 + (x2 - x3) pow 6 +
 149                  (x2 + x4) pow 6 + (x2 - x4) pow 6 +
 150                  (x3 + x4) pow 6 + (x3 - x4) pow 6) +
 151    Cx(&3 / &5) *  (x1 pow 6 + x2 pow 6 + x3 pow 6 + x4 pow 6))`;;
 152
 153 let HURWITZ = time COMPLEX_ARITH
 154  `!x1 x2 x3 x4.
 155     (x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 4 =
 156     Cx(&1 / &840) * ((x1 + x2 + x3 + x4) pow 8 +
 157                      (x1 + x2 + x3 - x4) pow 8 +
 158                      (x1 + x2 - x3 + x4) pow 8 +
 159                      (x1 + x2 - x3 - x4) pow 8 +
 160                      (x1 - x2 + x3 + x4) pow 8 +
 161                      (x1 - x2 + x3 - x4) pow 8 +
 162                      (x1 - x2 - x3 + x4) pow 8 +
 163                      (x1 - x2 - x3 - x4) pow 8) +
 164     Cx(&1 / &5040) * ((Cx(&2) * x1 + x2 + x3) pow 8 +
 165                       (Cx(&2) * x1 + x2 - x3) pow 8 +
 166                       (Cx(&2) * x1 - x2 + x3) pow 8 +
 167                       (Cx(&2) * x1 - x2 - x3) pow 8 +
 168                       (Cx(&2) * x1 + x2 + x4) pow 8 +
 169                       (Cx(&2) * x1 + x2 - x4) pow 8 +
 170                       (Cx(&2) * x1 - x2 + x4) pow 8 +
 171                       (Cx(&2) * x1 - x2 - x4) pow 8 +
 172                       (Cx(&2) * x1 + x3 + x4) pow 8 +
 173                       (Cx(&2) * x1 + x3 - x4) pow 8 +
 174                       (Cx(&2) * x1 - x3 + x4) pow 8 +
 175                       (Cx(&2) * x1 - x3 - x4) pow 8 +
 176                       (Cx(&2) * x2 + x3 + x4) pow 8 +
 177                       (Cx(&2) * x2 + x3 - x4) pow 8 +
 178                       (Cx(&2) * x2 - x3 + x4) pow 8 +
 179                       (Cx(&2) * x2 - x3 - x4) pow 8 +
 180                       (x1 + Cx(&2) * x2 + x3) pow 8 +
 181                       (x1 + Cx(&2) * x2 - x3) pow 8 +
 182                       (x1 - Cx(&2) * x2 + x3) pow 8 +
 183                       (x1 - Cx(&2) * x2 - x3) pow 8 +
 184                       (x1 + Cx(&2) * x2 + x4) pow 8 +
 185                       (x1 + Cx(&2) * x2 - x4) pow 8 +
 186                       (x1 - Cx(&2) * x2 + x4) pow 8 +
 187                       (x1 - Cx(&2) * x2 - x4) pow 8 +
 188                       (x1 + Cx(&2) * x3 + x4) pow 8 +
 189                       (x1 + Cx(&2) * x3 - x4) pow 8 +
 190                       (x1 - Cx(&2) * x3 + x4) pow 8 +
 191                       (x1 - Cx(&2) * x3 - x4) pow 8 +
 192                       (x2 + Cx(&2) * x3 + x4) pow 8 +
 193                       (x2 + Cx(&2) * x3 - x4) pow 8 +
 194                       (x2 - Cx(&2) * x3 + x4) pow 8 +
 195                       (x2 - Cx(&2) * x3 - x4) pow 8 +
 196                       (x1 + x2 + Cx(&2) * x3) pow 8 +
 197                       (x1 + x2 - Cx(&2) * x3) pow 8 +
 198                       (x1 - x2 + Cx(&2) * x3) pow 8 +
 199                       (x1 - x2 - Cx(&2) * x3) pow 8 +
 200                       (x1 + x2 + Cx(&2) * x4) pow 8 +
 201                       (x1 + x2 - Cx(&2) * x4) pow 8 +
 202                       (x1 - x2 + Cx(&2) * x4) pow 8 +
 203                       (x1 - x2 - Cx(&2) * x4) pow 8 +
 204                       (x1 + x3 + Cx(&2) * x4) pow 8 +
 205                       (x1 + x3 - Cx(&2) * x4) pow 8 +
 206                       (x1 - x3 + Cx(&2) * x4) pow 8 +
 207                       (x1 - x3 - Cx(&2) * x4) pow 8 +
 208                       (x2 + x3 + Cx(&2) * x4) pow 8 +
 209                       (x2 + x3 - Cx(&2) * x4) pow 8 +
 210                       (x2 - x3 + Cx(&2) * x4) pow 8 +
 211                       (x2 - x3 - Cx(&2) * x4) pow 8) +
 212      Cx(&1 / &84) * ((x1 + x2) pow 8 + (x1 - x2) pow 8 +
 213                      (x1 + x3) pow 8 + (x1 - x3) pow 8 +
 214                      (x1 + x4) pow 8 + (x1 - x4) pow 8 +
 215                      (x2 + x3) pow 8 + (x2 - x3) pow 8 +
 216                      (x2 + x4) pow 8 + (x2 - x4) pow 8 +
 217                      (x3 + x4) pow 8 + (x3 - x4) pow 8) +
 218      Cx(&1 / &840) * ((Cx(&2) * x1) pow 8 + (Cx(&2) * x2) pow 8 +
 219                       (Cx(&2) * x3) pow 8 + (Cx(&2) * x4) pow 8)`;;
 220
 221 let SCHUR = time COMPLEX_ARITH
 222  `Cx(&22680) * (x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 5 =
 223   Cx(&9) * ((Cx(&2) * x1) pow 10 +
 224             (Cx(&2) * x2) pow 10 +
 225             (Cx(&2) * x3) pow 10 +
 226             (Cx(&2) * x4) pow 10) +
 227   Cx(&180) * ((x1 + x2) pow 10 + (x1 - x2) pow 10 +
 228               (x1 + x3) pow 10 + (x1 - x3) pow 10 +
 229               (x1 + x4) pow 10 + (x1 - x4) pow 10 +
 230               (x2 + x3) pow 10 + (x2 - x3) pow 10 +
 231               (x2 + x4) pow 10 + (x2 - x4) pow 10 +
 232               (x3 + x4) pow 10 + (x3 - x4) pow 10) +
 233   ((Cx(&2) * x1 + x2 + x3) pow 10 +
 234    (Cx(&2) * x1 + x2 - x3) pow 10 +
 235    (Cx(&2) * x1 - x2 + x3) pow 10 +
 236    (Cx(&2) * x1 - x2 - x3) pow 10 +
 237    (Cx(&2) * x1 + x2 + x4) pow 10 +
 238    (Cx(&2) * x1 + x2 - x4) pow 10 +
 239    (Cx(&2) * x1 - x2 + x4) pow 10 +
 240    (Cx(&2) * x1 - x2 - x4) pow 10 +
 241    (Cx(&2) * x1 + x3 + x4) pow 10 +
 242    (Cx(&2) * x1 + x3 - x4) pow 10 +
 243    (Cx(&2) * x1 - x3 + x4) pow 10 +
 244    (Cx(&2) * x1 - x3 - x4) pow 10 +
 245    (Cx(&2) * x2 + x3 + x4) pow 10 +
 246    (Cx(&2) * x2 + x3 - x4) pow 10 +
 247    (Cx(&2) * x2 - x3 + x4) pow 10 +
 248    (Cx(&2) * x2 - x3 - x4) pow 10 +
 249    (x1 + Cx(&2) * x2 + x3) pow 10 +
 250    (x1 + Cx(&2) * x2 - x3) pow 10 +
 251    (x1 - Cx(&2) * x2 + x3) pow 10 +
 252    (x1 - Cx(&2) * x2 - x3) pow 10 +
 253    (x1 + Cx(&2) * x2 + x4) pow 10 +
 254    (x1 + Cx(&2) * x2 - x4) pow 10 +
 255    (x1 - Cx(&2) * x2 + x4) pow 10 +
 256    (x1 - Cx(&2) * x2 - x4) pow 10 +
 257    (x1 + Cx(&2) * x3 + x4) pow 10 +
 258    (x1 + Cx(&2) * x3 - x4) pow 10 +
 259    (x1 - Cx(&2) * x3 + x4) pow 10 +
 260    (x1 - Cx(&2) * x3 - x4) pow 10 +
 261    (x2 + Cx(&2) * x3 + x4) pow 10 +
 262    (x2 + Cx(&2) * x3 - x4) pow 10 +
 263    (x2 - Cx(&2) * x3 + x4) pow 10 +
 264    (x2 - Cx(&2) * x3 - x4) pow 10 +
 265    (x1 + x2 + Cx(&2) * x3) pow 10 +
 266    (x1 + x2 - Cx(&2) * x3) pow 10 +
 267    (x1 - x2 + Cx(&2) * x3) pow 10 +
 268    (x1 - x2 - Cx(&2) * x3) pow 10 +
 269    (x1 + x2 + Cx(&2) * x4) pow 10 +
 270    (x1 + x2 - Cx(&2) * x4) pow 10 +
 271    (x1 - x2 + Cx(&2) * x4) pow 10 +
 272    (x1 - x2 - Cx(&2) * x4) pow 10 +
 273    (x1 + x3 + Cx(&2) * x4) pow 10 +
 274    (x1 + x3 - Cx(&2) * x4) pow 10 +
 275    (x1 - x3 + Cx(&2) * x4) pow 10 +
 276    (x1 - x3 - Cx(&2) * x4) pow 10 +
 277    (x2 + x3 + Cx(&2) * x4) pow 10 +
 278    (x2 + x3 - Cx(&2) * x4) pow 10 +
 279    (x2 - x3 + Cx(&2) * x4) pow 10 +
 280    (x2 - x3 - Cx(&2) * x4) pow 10) +
 281   Cx(&9) * ((x1 + x2 + x3 + x4) pow 10 +
 282             (x1 + x2 + x3 - x4) pow 10 +
 283             (x1 + x2 - x3 + x4) pow 10 +
 284             (x1 + x2 - x3 - x4) pow 10 +
 285             (x1 - x2 + x3 + x4) pow 10 +
 286             (x1 - x2 + x3 - x4) pow 10 +
 287             (x1 - x2 - x3 + x4) pow 10 +
 288             (x1 - x2 - x3 - x4) pow 10)`;;
 289
 290 (* ------------------------------------------------------------------------- *)
 291 (* Intersection of diagonals of a parallelogram is their midpoint.           *)
 292 (* Kapur "...Dixon resultants, Groebner Bases, and Characteristic Sets", 3.1 *)
 293 (* ------------------------------------------------------------------------- *)
 294
 295 time COMPLEX_ARITH
 296  `(x1 = u3) /\
 297   (x1 * (u2 - u1) = x2 * u3) /\
 298   (x4 * (x2 - u1) = x1 * (x3 - u1)) /\
 299   (x3 * u3 = x4 * u2) /\
 300   ~(u1 = Cx(&0)) /\
 301   ~(u3 = Cx(&0))
 302   ==> (x3 pow 2 + x4 pow 2 = (u2 - x3) pow 2 + (u3 - x4) pow 2)`;;
 303
 304 (* ------------------------------------------------------------------------- *)
 305 (* Chou's formulation of same property.                                      *)
 306 (* ------------------------------------------------------------------------- *)
 307
 308 time COMPLEX_ARITH
 309  `(u1 * x1 - u1 * u3 = Cx(&0)) /\
 310   (u3 * x2 - (u2 - u1) * x1 = Cx(&0)) /\
 311   (x1 * x4 - (x2 - u1) * x3 - u1 * x1 = Cx(&0)) /\
 312   (u3 * x4 - u2 * x3 = Cx(&0)) /\
 313   ~(u1 = Cx(&0)) /\
 314   ~(u3 = Cx(&0))
 315   ==> (Cx(&2) * u2 * x4 + Cx(&2) * u3 * x3 - u3 pow 2 - u2 pow 2 = Cx(&0))`;;
 316
 317 (* ------------------------------------------------------------------------- *)
 318 (* Perpendicular lines property; from Kapur's earlier paper.                 *)
 319 (* ------------------------------------------------------------------------- *)
 320
 321 time COMPLEX_ARITH
 322  `(y1 * y3 + x1 * x3 = Cx(&0)) /\
 323   (y3 * (y2 - y3) + (x2 - x3) * x3 = Cx(&0)) /\
 324   ~(x3 = Cx(&0)) /\
 325   ~(y3 = Cx(&0))
 326   ==> (y1 * (x2 - x3) = x1 * (y2 - y3))`;;
 327
 328 (* ------------------------------------------------------------------------- *)
 329 (* Simson's theorem (Chou, p7).                                              *)
 330 (* ------------------------------------------------------------------------- *)
 331
 332 time COMPLEX_ARITH
 333  `(Cx(&2) * u2 * x2 + Cx(&2) * u3 * x1 - u3 pow 2 - u2 pow 2 = Cx(&0)) /\
 334   (Cx(&2) * u1 * x2 - u1 pow 2 = Cx(&0)) /\
 335   (--(x3 pow 2) + Cx(&2) * x2 * x3 + Cx(&2) * u4 * x1 - u4 pow 2 = Cx(&0)) /\
 336   (u3 * x5 + (--u2 + u1) * x4 - u1 * u3 = Cx(&0)) /\
 337   ((u2 - u1) * x5 + u3 * x4 + (--u2 + u1) * x3 - u3 * u4 = Cx(&0)) /\
 338   (u3 * x7 - u2 * x6 = Cx(&0)) /\
 339   (u2 * x7 + u3 * x6 - u2 * x3 - u3 * u4 = Cx(&0)) /\
 340   ~(Cx(&4) * u1 * u3 = Cx(&0)) /\
 341   ~(Cx(&2) * u1 = Cx(&0)) /\
 342   ~(--(u3 pow 2) - u2 pow 2 + Cx(&2) * u1 * u2 - u1 pow 2 = Cx(&0)) /\
 343   ~(u3 = Cx(&0)) /\
 344   ~(--(u3 pow 2) - u2 pow 2 = Cx(&0)) /\
 345   ~(u2 = Cx(&0))
 346   ==> (x4 * x7 + (--x5 + x3) * x6 - x3 * x4 = Cx(&0))`;;
 347
 348 (* ------------------------------------------------------------------------- *)
 349 (* Determinants from Coq convex hull paper (some require reals or order).    *)
 350 (* ------------------------------------------------------------------------- *)
 351
 352 let det3 = new_definition
 353   `det3(a11,a12,a13,
 354         a21,a22,a23,
 355         a31,a32,a33) =
 356     a11 * (a22 * a33 - a32 * a23) -
 357     a12 * (a21 * a33 - a31 * a23) +
 358     a13 * (a21 * a32 - a31 * a22)`;;
 359
 360 let DET_TRANSPOSE = prove
 361  (`det3(a1,b1,c1,a2,b2,c2,a3,b3,c3) =
 362    det3(a1,a2,a3,b1,b2,b3,c1,c2,c3)`,
 363   REWRITE_TAC[det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 364
 365 let sdet3 = new_definition
 366   `sdet3(p,q,r) = det3(FST p,SND p,Cx(&1),
 367                        FST q,SND q,Cx(&1),
 368                        FST r,SND r,Cx(&1))`;;
 369
 370 let SDET3_PERMUTE_1 = prove
 371  (`sdet3(p,q,r) = sdet3(q,r,p)`,
 372   REWRITE_TAC[sdet3; det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 373
 374 let SDET3_PERMUTE_2 = prove
 375  (`sdet3(p,q,r) = --(sdet3(p,r,q))`,
 376   REWRITE_TAC[sdet3; det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 377
 378 let SDET_SUM = prove
 379  (`sdet3(p,q,r) - sdet3(t,q,r) - sdet3(p,t,r) - sdet3(p,q,t) = Cx(&0)`,
 380   REWRITE_TAC[sdet3; det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 381
 382 let SDET_CRAMER = prove
 383  (`sdet3(s,t,q) * sdet3(t,p,r) = sdet3(t,q,r) * sdet3(s,t,p) +
 384                                  sdet3(t,p,q) * sdet3(s,t,r)`,
 385   REWRITE_TAC[sdet3; det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 386
 387 let SDET_NZ = prove
 388  (`!p q r. ~(sdet3(p,q,r) = Cx(&0))
 389            ==> ~(p = q) /\ ~(q = r) /\ ~(r = p)`,
 390   REWRITE_TAC[FORALL_PAIR_THM; PAIR_EQ; sdet3; det3] THEN
 391   CONV_TAC(time COMPLEX_ARITH));;
 392
 393 let SDET_LINCOMB = prove
 394  (`(FST p * sdet3(i,j,k) =
 395     FST i * sdet3(j,k,p) + FST j * sdet3(k,i,p) + FST k * sdet3(i,j,p)) /\
 396    (SND p * sdet3(i,j,k) =
 397     SND i * sdet3(j,k,p) + SND j * sdet3(k,i,p) + SND k * sdet3(i,j,p))`,
 398   REWRITE_TAC[sdet3; det3] THEN CONV_TAC(time COMPLEX_ARITH));;
 399
 400 (***** I'm not sure if this is true; there must be some
 401        sufficient degenerate conditions....
 402
 403 let th = prove
 404  (`~(~(xp pow 2 + yp pow 2 = Cx(&0)) /\
 405      ~(xq pow 2 + yq pow 2 = Cx(&0)) /\
 406      ~(xr pow 2 + yr pow 2 = Cx(&0)) /\
 407      (det3(xp,yp,Cx(&1),
 408            xq,yq,Cx(&1),
 409            xr,yr,Cx(&1)) = Cx(&0)) /\
 410      (det3(yp,xp pow 2 + yp pow 2,Cx(&1),
 411            yq,xq pow 2 + yq pow 2,Cx(&1),
 412            yr,xr pow 2 + yr pow 2,Cx(&1)) = Cx(&0)) /\
 413      (det3(xp,xp pow 2 + yp pow 2,Cx(&1),
 414            xq,xq pow 2 + yq pow 2,Cx(&1),
 415            xr,xr pow 2 + yr pow 2,Cx(&1)) = Cx(&0)))`,
 416   REWRITE_TAC[det3] THEN
 417   CONV_TAC(time COMPLEX_ARITH));;
 418
 419 ***************)
 420
 421 (* ------------------------------------------------------------------------- *)
 422 (* Some geometry concepts (just "axiomatic" in this file).                   *)
 423 (* ------------------------------------------------------------------------- *)
 424
 425 prioritize_real();;
 426
 427 let collinear = new_definition
 428   `collinear (a:real#real) b c <=>
 429         ((FST a - FST b) * (SND b - SND c) =
 430          (SND a - SND b) * (FST b - FST c))`;;
 431
 432 let parallel = new_definition
 433   `parallel (a,b) (c,d) <=>
 434      ((FST a - FST b) * (SND c - SND d) = (SND a - SND b) * (FST c - FST d))`;;
 435
 436 let perpendicular = new_definition
 437   `perpendicular (a,b) (c,d) <=>
 438      ((FST a - FST b) * (FST c - FST d) + (SND a - SND b) * (SND c - SND d) =
 439       &0)`;;
 440
 441 let oncircle_with_diagonal = new_definition
 442   `oncircle_with_diagonal a (b,c) = perpendicular (b,a) (c,a)`;;
 443
 444 let length = new_definition
 445   `length (a,b) = sqrt((FST a - FST b) pow 2 + (SND a - SND b) pow 2)`;;
 446
 447 let lengths_eq = new_definition
 448   `lengths_eq (a,b) (c,d) <=>
 449         ((FST a - FST b) pow 2 + (SND a - SND b) pow 2 =
 450          (FST c - FST d) pow 2 + (SND c - SND d) pow 2)`;;
 451
 452 let is_midpoint = new_definition
 453   `is_midpoint b (a,c) <=>
 454      (&2 * FST b = FST a + FST c) /\
 455      (&2 * SND b = SND a + SND c)`;;
 456
 457 (* ------------------------------------------------------------------------- *)
 458 (* Chou isn't explicit about this.                                           *)
 459 (* ------------------------------------------------------------------------- *)
 460
 461 let is_intersection = new_definition
 462   `is_intersection p (a,b) (c,d) <=>
 463       collinear a p b /\ collinear c p d`;;
 464
 465 (* ------------------------------------------------------------------------- *)
 466 (* This is used in some degenerate conditions. See Chou, p18.                *)
 467 (* ------------------------------------------------------------------------- *)
 468
 469 let isotropic = new_definition
 470   `isotropic (a,b) = perpendicular (a,b) (a,b)`;;
 471
 472 (* ------------------------------------------------------------------------- *)
 473 (* This increases degree, but sometimes makes complex assertion useful.      *)
 474 (* ------------------------------------------------------------------------- *)
 475
 476 let distinctpairs = new_definition
 477   `distinctpairs pprs <=>
 478      ~(ITLIST (\(a,b) pr. ((FST a - FST b) pow 2 + (SND a - SND b) pow 2) * pr)
 479               pprs (&1) = &0)`;;
 480
 481 (* ------------------------------------------------------------------------- *)
 482 (* Simple tactic to remove defined concepts and expand coordinates.          *)
 483 (* ------------------------------------------------------------------------- *)
 484
 485 let (EXPAND_COORDS_TAC:tactic) =
 486   let complex2_ty = `:real#real` in
 487   fun (asl,w) ->
 488     (let fvs = filter (fun v -> type_of v = complex2_ty) (frees w) in
 489      MAP_EVERY (fun v -> SPEC_TAC(v,v)) fvs THEN
 490      GEN_REWRITE_TAC DEPTH_CONV [FORALL_PAIR_THM; EXISTS_PAIR_THM] THEN
 491      REPEAT GEN_TAC) (asl,w);;
 492
 493 let PAIR_BETA_THM = prove
 494  (`(\(x,y). P x y) (a,b) = P a b`,
 495   CONV_TAC(LAND_CONV GEN_BETA_CONV) THEN REFL_TAC);;
 496
 497 let GEOM_TAC =
 498   EXPAND_COORDS_TAC THEN
 499   GEN_REWRITE_TAC TOP_DEPTH_CONV
 500    [collinear; parallel; perpendicular; oncircle_with_diagonal;
 501     length; lengths_eq; is_midpoint; is_intersection; distinctpairs;
 502     isotropic; ITLIST; PAIR_BETA_THM; BETA_THM; PAIR_EQ; FST; SND];;
 503
 504 (* ------------------------------------------------------------------------- *)
 505 (* Centroid (Chou, example 142).                                             *)
 506 (* ------------------------------------------------------------------------- *)
 507
 508 let CENTROID = time prove
 509  (`is_midpoint d (b,c) /\
 510    is_midpoint e (a,c) /\
 511    is_midpoint f (a,b) /\
 512    is_intersection m (b,e) (a,d)
 513    ==> collinear c f m`,
 514   GEOM_TAC THEN CONV_TAC GROBNER_REAL_ARITH);;
 515
 516 (* ------------------------------------------------------------------------- *)
 517 (* Gauss's theorem (Chou, example 15).                                       *)
 518 (* ------------------------------------------------------------------------- *)
 519
 520 let GAUSS = time prove
 521  (`collinear x a0 a3 /\
 522    collinear x a1 a2 /\
 523    collinear y a2 a3 /\
 524    collinear y a1 a0 /\
 525    is_midpoint m1 (a1,a3) /\
 526    is_midpoint m2 (a0,a2) /\
 527    is_midpoint m3 (x,y)
 528    ==> collinear m1 m2 m3`,
 529   GEOM_TAC THEN CONV_TAC GROBNER_REAL_ARITH);;
 530
 531 (* ------------------------------------------------------------------------- *)
 532 (* Simson's theorem (Chou, example 288).                                     *)
 533 (* ------------------------------------------------------------------------- *)
 534
 535 (**** These are all hideously slow. At least the first one works.
 536       I haven't had the patience to try the rest.
 537
 538 let SIMSON = time prove
 539  (`lengths_eq (O,a) (O,b) /\
 540    lengths_eq (O,a) (O,c) /\
 541    lengths_eq (d,O) (O,a) /\
 542    perpendicular (e,d) (b,c) /\
 543    collinear e b c /\
 544    perpendicular (f,d) (a,c) /\
 545    collinear f a c /\
 546    perpendicular (g,d) (a,b) /\
 547    collinear g a b /\
 548    ~(collinear a c b) /\
 549    ~(lengths_eq (a,b) (a,a)) /\
 550    ~(lengths_eq (a,c) (a,a)) /\
 551    ~(lengths_eq (b,c) (a,a))
 552    ==> collinear e f g`,
 553   GEOM_TAC THEN CONV_TAC GROBNER_REAL_ARITH);;
 554
 555 let SIMSON = time prove
 556  (`lengths_eq (O,a) (O,b) /\
 557    lengths_eq (O,a) (O,c) /\
 558    lengths_eq (d,O) (O,a) /\
 559    perpendicular (e,d) (b,c) /\
 560    collinear e b c /\
 561    perpendicular (f,d) (a,c) /\
 562    collinear f a c /\
 563    perpendicular (g,d) (a,b) /\
 564    collinear g a b /\
 565    ~(a = b) /\ ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d) /\ ~(c = d)
 566    ==> collinear e f g`,
 567   GEOM_TAC THEN CONV_TAC GROBNER_REAL_ARITH);;
 568
 569 let SIMSON = time prove
 570  (`lengths_eq (O,a) (O,b) /\
 571    lengths_eq (O,a) (O,c) /\
 572    lengths_eq (d,O) (O,a) /\
 573    perpendicular (e,d) (b,c) /\
 574    collinear e b c /\
 575    perpendicular (f,d) (a,c) /\
 576    collinear f a c /\
 577    perpendicular (g,d) (a,b) /\
 578    collinear g a b /\
 579    ~(collinear a c b) /\
 580    ~(isotropic (a,b)) /\
 581    ~(isotropic (a,c)) /\
 582    ~(isotropic (b,c)) /\
 583    ~(isotropic (a,d)) /\
 584    ~(isotropic (b,d)) /\
 585    ~(isotropic (c,d))
 586    ==> collinear e f g`,
 587   GEOM_TAC THEN CONV_TAC GROBNER_REAL_ARITH);;
 588
 589 ****************)