100/quartic.ml

   1 prioritize_real();;
   2
   3 (* ------------------------------------------------------------------------- *)
   4 (* First the R = 0 case.                                                     *)
   5 (* ------------------------------------------------------------------------- *)
   6
   7 let QUARTIC_1 = prove
   8  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
   9    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  10    R pow 2 = a pow 2 / &4 - b + y /\
  11    R = &0 /\
  12    s pow 2 = y pow 2 - &4 * d /\
  13    D pow 2 = &3 * a pow 2 / &4 - &2 * b + &2 * s /\
  14    x = --a / &4 + R / &2 + D / &2
  15    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  16   CONV_TAC REAL_RING);;
  17
  18 let QUARTIC_2 = prove
  19  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  20    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  21    R pow 2 = a pow 2 / &4 - b + y /\
  22    R = &0 /\
  23    s pow 2 = y pow 2 - &4 * d /\
  24    D pow 2 = &3 * a pow 2 / &4 - &2 * b + &2 * s /\
  25    x = --a / &4 + R / &2 - D / &2
  26    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  27   CONV_TAC REAL_RING);;
  28
  29 let QUARTIC_3 = prove
  30  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  31    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  32    R pow 2 = a pow 2 / &4 - b + y /\
  33    R = &0 /\
  34    s pow 2 = y pow 2 - &4 * d /\
  35    E pow 2 = &3 * a pow 2 / &4 - &2 * b - &2 * s /\
  36    x = --a / &4 - R / &2 + E / &2
  37    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  38   CONV_TAC REAL_RING);;
  39
  40 let QUARTIC_4 = prove
  41  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  42    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  43    R pow 2 = a pow 2 / &4 - b + y /\
  44    R = &0 /\
  45    s pow 2 = y pow 2 - &4 * d /\
  46    E pow 2 = &3 * a pow 2 / &4 - &2 * b - &2 * s /\
  47    x = --a / &4 - R / &2 - E / &2
  48    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  49   CONV_TAC REAL_RING);;
  50
  51
  52 (* ------------------------------------------------------------------------- *)
  53 (* The R nonzero case.                                                       *)
  54 (* ------------------------------------------------------------------------- *)
  55
  56 let QUARTIC_1' = prove
  57  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  58    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  59    R pow 2 = a pow 2 / &4 - b + y /\
  60    ~(R = &0) /\
  61    D pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b +
  62              (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
  63    x = --a / &4 + R / &2 + D / &2
  64    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  65   CONV_TAC REAL_FIELD);;
  66
  67 let QUARTIC_2' = prove
  68  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  69    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  70    R pow 2 = a pow 2 / &4 - b + y /\
  71    ~(R = &0) /\
  72    D pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b +
  73              (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
  74    x = --a / &4 + R / &2 - D / &2
  75    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  76   CONV_TAC REAL_FIELD);;
  77
  78 let QUARTIC_3' = prove
  79  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  80    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  81    R pow 2 = a pow 2 / &4 - b + y /\
  82    ~(R = &0) /\
  83    E pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b -
  84              (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
  85    x = --a / &4 - R / &2 + E / &2
  86    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  87   CONV_TAC REAL_FIELD);;
  88
  89 let QUARTIC_4' = prove
  90  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
  91    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
  92    R pow 2 = a pow 2 / &4 - b + y /\
  93    ~(R = &0) /\
  94    E pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b -
  95              (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
  96    x = --a / &4 - R / &2 - E / &2
  97    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
  98   CONV_TAC REAL_FIELD);;
  99
 100 (* ------------------------------------------------------------------------- *)
 101 (* Combine them.                                                             *)
 102 (* ------------------------------------------------------------------------- *)
 103
 104 let QUARTIC_1 = prove
 105  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
 106    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
 107    R pow 2 = a pow 2 / &4 - b + y /\
 108    s pow 2 = y pow 2 - &4 * d /\
 109    (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
 110               else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
 111                    (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 112    x = --a / &4 + R / &2 + D / &2
 113    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
 114   CONV_TAC REAL_FIELD);;
 115
 116 (* ------------------------------------------------------------------------- *)
 117 (* A case split.                                                             *)
 118 (* ------------------------------------------------------------------------- *)
 119
 120 let QUARTIC_1 = prove
 121  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
 122    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
 123    R pow 2 = a pow 2 / &4 - b + y /\
 124    s pow 2 = y pow 2 - &4 * d /\
 125    (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
 126               else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
 127                    (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 128    (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
 129               else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
 130              (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 131    (x = --a / &4 + R / &2 + D / &2 \/
 132     x = --a / &4 - R / &2 + E / &2)
 133    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
 134   CONV_TAC REAL_FIELD);;
 135
 136 (* ------------------------------------------------------------------------- *)
 137 (* More general case split.                                                  *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 let QUARTIC_CASES = prove
 141  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
 142    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
 143    R pow 2 = a pow 2 / &4 - b + y /\
 144    s pow 2 = y pow 2 - &4 * d /\
 145    (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
 146               else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
 147                    (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 148    (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
 149               else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
 150              (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 151    (x = --a / &4 + R / &2 + D / &2 \/
 152     x = --a / &4 + R / &2 - D / &2 \/
 153     x = --a / &4 - R / &2 + E / &2 \/
 154     x = --a / &4 - R / &2 - E / &2)
 155    ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
 156   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
 157   CONV_TAC REAL_FIELD);;
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* Even this works --- great, that's nearly what we wanted.                  *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163 let QUARTIC_CASES = prove
 164  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
 165    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
 166    R pow 2 = a pow 2 / &4 - b + y /\
 167    s pow 2 = y pow 2 - &4 * d /\
 168    (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
 169               else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
 170                    (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 171    (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
 172               else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
 173              (&4 * a * b - &8 * c - a pow 3) / (&4 * R))
 174    ==> (x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0 <=>
 175         x = --a / &4 + R / &2 + D / &2 \/
 176         x = --a / &4 + R / &2 - D / &2 \/
 177         x = --a / &4 - R / &2 + E / &2 \/
 178         x = --a / &4 - R / &2 - E / &2)`,
 179   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
 180   CONV_TAC REAL_FIELD);;
 181
 182 (* ------------------------------------------------------------------------- *)
 183 (* This is the automatic proof.                                              *)
 184 (* ------------------------------------------------------------------------- *)
 185
 186 let QUARTIC_CASES = prove
 187  (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
 188    a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
 189    R pow 2 = a pow 2 / &4 - b + y /\
 190    s pow 2 = y pow 2 - &4 * d /\
 191    (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
 192               else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
 193                    (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
 194    (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
 195               else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
 196              (&4 * a * b - &8 * c - a pow 3) / (&4 * R))
 197    ==> (x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0 <=>
 198         x = --a / &4 + R / &2 + D / &2 \/
 199         x = --a / &4 + R / &2 - D / &2 \/
 200         x = --a / &4 - R / &2 + E / &2 \/
 201         x = --a / &4 - R / &2 - E / &2)`,
 202   CONV_TAC REAL_FIELD);;