Examples/lagrange_lemma.ml

   1 (* ========================================================================= *)
   2 (* Nice test for ring procedure and ordered rewriting: Lagrange lemma.       *)
   3 (* ========================================================================= *)
   4
   5 prioritize_real();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Do the problems the (relatively) efficient way using the normalizer.      *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let LAGRANGE_4 = time prove
  12  (`((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) *
  13    ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2)) =
  14      (((((x1*y1) - (x2*y2)) - (x3*y3)) - (x4*y4)) pow 2)  +
  15      (((((x1*y2) + (x2*y1)) + (x3*y4)) - (x4*y3)) pow 2)  +
  16      (((((x1*y3) - (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2)  +
  17      (((((x1*y4) + (x2*y3)) - (x3*y2)) + (x4*y1)) pow 2)`,
  18   CONV_TAC REAL_RING);;
  19
  20 let LAGRANGE_8 = time prove
  21  (`(p1 pow 2 + q1 pow 2 + r1 pow 2 + s1 pow 2 + t1 pow 2 + u1 pow 2 + v1 pow 2 + w1 pow 2) *
  22    (p2 pow 2 + q2 pow 2 + r2 pow 2 + s2 pow 2 + t2 pow 2 + u2 pow 2 + v2 pow 2 + w2 pow 2)
  23    = (p1 * p2 - q1 * q2 - r1 * r2 - s1 * s2 - t1 * t2 - u1 * u2 - v1 * v2 - w1 * w2) pow 2 +
  24      (p1 * q2 + q1 * p2 + r1 * s2 - s1 * r2 + t1 * u2 - u1 * t2 - v1 * w2 + w1 * v2) pow 2 +
  25      (p1 * r2 - q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 - v1 * t2 - w1 * u2) pow 2 +
  26      (p1 * s2 + q1 * r2 - r1 * q2 + s1 * p2 + t1 * w2 - u1 * v2 + v1 * u2 - w1 * t2) pow 2 +
  27      (p1 * t2 - q1 * u2 - r1 * v2 - s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 + w1 * s2) pow 2 +
  28      (p1 * u2 + q1 * t2 - r1 * w2 + s1 * v2 - t1 * q2 + u1 * p2 - v1 * s2 + w1 * r2) pow 2 +
  29      (p1 * v2 + q1 * w2 + r1 * t2 - s1 * u2 - t1 * r2 + u1 * s2 + v1 * p2 - w1 * q2) pow 2 +
  30      (p1 * w2 - q1 * v2 + r1 * u2 + s1 * t2 - t1 * s2 - u1 * r2 + v1 * q2 + w1 * p2) pow 2`,
  31   CONV_TAC REAL_RING);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Or we can just use REAL_ARITH, which is also reasonably fast.             *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let LAGRANGE_4 = time prove
  38  (`((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) *
  39    ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2)) =
  40      (((((x1*y1) - (x2*y2)) - (x3*y3)) - (x4*y4)) pow 2)  +
  41      (((((x1*y2) + (x2*y1)) + (x3*y4)) - (x4*y3)) pow 2)  +
  42      (((((x1*y3) - (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2)  +
  43      (((((x1*y4) + (x2*y3)) - (x3*y2)) + (x4*y1)) pow 2)`,
  44   REAL_ARITH_TAC);;
  45
  46 let LAGRANGE_8 = time prove
  47  (`(p1 pow 2 + q1 pow 2 + r1 pow 2 + s1 pow 2 + t1 pow 2 + u1 pow 2 + v1 pow 2 + w1 pow 2) *
  48    (p2 pow 2 + q2 pow 2 + r2 pow 2 + s2 pow 2 + t2 pow 2 + u2 pow 2 + v2 pow 2 + w2 pow 2)
  49    = (p1 * p2 - q1 * q2 - r1 * r2 - s1 * s2 - t1 * t2 - u1 * u2 - v1 * v2 - w1 * w2) pow 2 +
  50      (p1 * q2 + q1 * p2 + r1 * s2 - s1 * r2 + t1 * u2 - u1 * t2 - v1 * w2 + w1 * v2) pow 2 +
  51      (p1 * r2 - q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 - v1 * t2 - w1 * u2) pow 2 +
  52      (p1 * s2 + q1 * r2 - r1 * q2 + s1 * p2 + t1 * w2 - u1 * v2 + v1 * u2 - w1 * t2) pow 2 +
  53      (p1 * t2 - q1 * u2 - r1 * v2 - s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 + w1 * s2) pow 2 +
  54      (p1 * u2 + q1 * t2 - r1 * w2 + s1 * v2 - t1 * q2 + u1 * p2 - v1 * s2 + w1 * r2) pow 2 +
  55      (p1 * v2 + q1 * w2 + r1 * t2 - s1 * u2 - t1 * r2 + u1 * s2 + v1 * p2 - w1 * q2) pow 2 +
  56      (p1 * w2 - q1 * v2 + r1 * u2 + s1 * t2 - t1 * s2 - u1 * r2 + v1 * q2 + w1 * p2) pow 2`,
  57   REAL_ARITH_TAC);;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* But they can be done (slowly) simply by ordered rewriting.                *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let LAGRANGE_4 = time prove
  64  (`((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) *
  65    ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2)) =
  66      (((((x1*y1) - (x2*y2)) - (x3*y3)) - (x4*y4)) pow 2)  +
  67      (((((x1*y2) + (x2*y1)) + (x3*y4)) - (x4*y3)) pow 2)  +
  68      (((((x1*y3) - (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2)  +
  69      (((((x1*y4) + (x2*y3)) - (x3*y2)) + (x4*y1)) pow 2)`,
  70   REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB;
  71               REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB;
  72               REAL_ARITH `a + (b - c) = (a + b) - c`;
  73               REAL_ARITH `a - (b - c) = a + (c - b)`;
  74               REAL_ARITH `(a - b) + c = (a + c) - b`;
  75               REAL_ARITH `(a - b) - c = a - (b + c)`;
  76               REAL_ARITH `(a - b = c) = (a = b + c)`;
  77               REAL_ARITH `(a = b - c) = (a + c = b)`;
  78               REAL_ADD_AC; REAL_MUL_AC]);;
  79
  80 let LAGRANGE_8 = time prove
  81  (`(p1 pow 2 + q1 pow 2 + r1 pow 2 + s1 pow 2 + t1 pow 2 + u1 pow 2 + v1 pow 2 + w1 pow 2) *
  82    (p2 pow 2 + q2 pow 2 + r2 pow 2 + s2 pow 2 + t2 pow 2 + u2 pow 2 + v2 pow 2 + w2 pow 2)
  83    = (p1 * p2 - q1 * q2 - r1 * r2 - s1 * s2 - t1 * t2 - u1 * u2 - v1 * v2 - w1 * w2) pow 2 +
  84      (p1 * q2 + q1 * p2 + r1 * s2 - s1 * r2 + t1 * u2 - u1 * t2 - v1 * w2 + w1 * v2) pow 2 +
  85      (p1 * r2 - q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 - v1 * t2 - w1 * u2) pow 2 +
  86      (p1 * s2 + q1 * r2 - r1 * q2 + s1 * p2 + t1 * w2 - u1 * v2 + v1 * u2 - w1 * t2) pow 2 +
  87      (p1 * t2 - q1 * u2 - r1 * v2 - s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 + w1 * s2) pow 2 +
  88      (p1 * u2 + q1 * t2 - r1 * w2 + s1 * v2 - t1 * q2 + u1 * p2 - v1 * s2 + w1 * r2) pow 2 +
  89      (p1 * v2 + q1 * w2 + r1 * t2 - s1 * u2 - t1 * r2 + u1 * s2 + v1 * p2 - w1 * q2) pow 2 +
  90      (p1 * w2 - q1 * v2 + r1 * u2 + s1 * t2 - t1 * s2 - u1 * r2 + v1 * q2 + w1 * p2) pow 2`,
  91   REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB;
  92               REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB;
  93               REAL_ARITH `a + (b - c) = (a + b) - c`;
  94               REAL_ARITH `a - (b - c) = a + (c - b)`;
  95               REAL_ARITH `(a - b) + c = (a + c) - b`;
  96               REAL_ARITH `(a - b) - c = a - (b + c)`;
  97               REAL_ARITH `(a - b = c) = (a = b + c)`;
  98               REAL_ARITH `(a = b - c) = (a + c = b)`;
  99               REAL_ADD_AC; REAL_MUL_AC]);;