100/descartes.ml

   1 (* ========================================================================= *)
   2 (* Rob Arthan's "Descartes's Rule of Signs by an Easy Induction".            *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/realanalysis.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* A couple of handy lemmas.                                                 *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let OPPOSITE_SIGNS = prove
  12  (`!a b:real. a * b < &0 <=> &0 < a /\ b < &0 \/ a < &0 /\ &0 < b`,
  13   REWRITE_TAC[REAL_ARITH `a * b < &0 <=> &0 < a * --b`; REAL_MUL_POS_LT] THEN
  14   REAL_ARITH_TAC);;
  15
  16 let VARIATION_SET_FINITE = prove
  17  (`FINITE s ==> FINITE {p,q | p IN s /\ q IN s /\ P p q}`,
  18   REWRITE_TAC[SET_RULE
  19    `{p,q | p IN s /\ q IN t /\ R p q} =
  20     {p,q | p IN s /\ q IN {q | q IN t /\ R p q}}`] THEN
  21   SIMP_TAC[FINITE_PRODUCT_DEPENDENT; FINITE_RESTRICT]);;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Variation in a sequence of coefficients.                                  *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let variation = new_definition
  28  `variation s (a:num->real) =
  29      CARD {(p,q) | p IN s /\ q IN s /\ p < q /\
  30                    a(p) * a(q) < &0 /\
  31                    !i. i IN s /\ p < i /\ i < q ==> a(i) = &0 }`;;
  32
  33 let VARIATION_EQ = prove
  34  (`!a b s. (!i. i IN s ==> a i = b i) ==> variation s a = variation s b`,
  35   REPEAT STRIP_TAC THEN REWRITE_TAC[variation] THEN AP_TERM_TAC THEN
  36   REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  37   ASM_MESON_TAC[]);;
  38
  39 let VARIATION_SUBSET = prove
  40  (`!a s t. t SUBSET s /\ (!i. i IN (s DIFF t) ==> a i = &0)
  41            ==> variation s a = variation t a`,
  42   REWRITE_TAC[IN_DIFF; SUBSET] THEN REPEAT STRIP_TAC THEN
  43   REWRITE_TAC[variation] THEN AP_TERM_TAC THEN
  44   REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
  45   ASM_MESON_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL]);;
  46
  47 let VARIATION_SPLIT = prove
  48  (`!a s n.
  49         FINITE s /\ n IN s /\ ~(a n = &0)
  50         ==> variation s a = variation {i | i IN s /\ i <= n} a +
  51                             variation {i | i IN s /\ n <= i} a`,
  52   REWRITE_TAC[variation] THEN REPEAT STRIP_TAC THEN
  53   CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
  54   ASM_SIMP_TAC[VARIATION_SET_FINITE; FINITE_RESTRICT] THEN
  55   REWRITE_TAC[EXTENSION; FORALL_PAIR_THM] THEN CONJ_TAC THENL
  56    [REWRITE_TAC[IN_INTER; NOT_IN_EMPTY; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
  57     REWRITE_TAC[IN_ELIM_THM] THEN ARITH_TAC;
  58     REWRITE_TAC[IN_UNION; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
  59     REPEAT GEN_TAC THEN EQ_TAC THENL
  60      [STRIP_TAC;
  61       STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
  62         MP_TAC(SPEC `n:num` th) THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC th) THEN
  63       SIMP_TAC[TAUT `~(a /\ b) <=> ~b \/ ~a`] THEN MATCH_MP_TAC MONO_OR] THEN
  64     RULE_ASSUM_TAC(REWRITE_RULE[IN_ELIM_THM]) THEN
  65     ASM_REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
  66     TRY(FIRST_ASSUM MATCH_MP_TAC) THEN
  67     FIRST_ASSUM(fun th -> MP_TAC(SPEC `n:num` th) THEN ASM_REWRITE_TAC[]) THEN
  68     ASM_ARITH_TAC]);;
  69
  70 let VARIATION_SPLIT_NUMSEG = prove
  71  (`!a m n p. n IN m..p /\ ~(a n = &0)
  72              ==> variation(m..p) a = variation(m..n) a + variation(n..p) a`,
  73   REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP
  74    (REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> b /\ c ==> a ==> d`]
  75      VARIATION_SPLIT)) THEN
  76   REWRITE_TAC[FINITE_NUMSEG] THEN DISCH_THEN SUBST1_TAC THEN
  77   BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  78   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
  79   RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]) THEN ASM_ARITH_TAC);;
  80
  81 let VARIATION_1 = prove
  82  (`!a n. variation {n} a = 0`,
  83   REWRITE_TAC[variation; IN_SING] THEN
  84   REWRITE_TAC[ARITH_RULE `p:num = n /\ q = n /\ p < q /\ X <=> F`] THEN
  85   MATCH_MP_TAC(MESON[CARD_CLAUSES] `s = {} ==> CARD s = 0`) THEN
  86   REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; NOT_IN_EMPTY]);;
  87
  88 let VARIATION_2 = prove
  89  (`!a m n. variation {m,n} a = if a(m) * a(n) < &0 then 1 else 0`,
  90   GEN_TAC THEN MATCH_MP_TAC WLOG_LT THEN REPEAT CONJ_TAC THENL
  91    [REWRITE_TAC[INSERT_AC; VARIATION_1; GSYM REAL_NOT_LE; REAL_LE_SQUARE];
  92     REWRITE_TAC[INSERT_AC; REAL_MUL_SYM];
  93     REPEAT STRIP_TAC THEN REWRITE_TAC[variation; IN_INSERT; NOT_IN_EMPTY] THEN
  94     ONCE_REWRITE_TAC[TAUT
  95      `a /\ b /\ c /\ d /\ e <=> (a /\ b /\ c) /\ d /\ e`] THEN
  96     ASM_SIMP_TAC[ARITH_RULE
  97      `m:num < n
  98       ==> ((p = m \/ p = n) /\ (q = m \/ q = n) /\ p < q <=>
  99            p = m /\ q = n)`] THEN
 100     REWRITE_TAC[MESON[] `(p = m /\ q = n) /\ X p q <=>
 101                          (p = m /\ q = n) /\ X m n`] THEN
 102     REWRITE_TAC[ARITH_RULE `(i:num = m \/ i = n) /\ m < i /\ i < n <=> F`] THEN
 103     ASM_CASES_TAC `a m * a(n:num) < &0` THEN ASM_REWRITE_TAC[] THENL
 104      [REWRITE_TAC[SET_RULE `{p,q | p = a /\ q = b} = {(a,b)}`] THEN
 105       SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH];
 106       MATCH_MP_TAC(MESON[CARD_CLAUSES] `s = {} ==> CARD s = 0`) THEN
 107       SIMP_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; NOT_IN_EMPTY]]]);;
 108
 109 let VARIATION_3 = prove
 110  (`!a m n p.
 111         m < n /\ n < p
 112         ==> variation {m,n,p} a = if a(n) = &0 then variation{m,p} a
 113                                   else variation {m,n} a + variation{n,p} a`,
 114   REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
 115    [MATCH_MP_TAC VARIATION_SUBSET THEN ASM SET_TAC[];
 116     MP_TAC(ISPECL [`a:num->real`; `{m:num,n,p}`; `n:num`] VARIATION_SPLIT) THEN
 117     ASM_SIMP_TAC[FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN
 118     DISCH_THEN SUBST1_TAC THEN BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 119     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
 120     ASM_ARITH_TAC]);;
 121
 122 let VARIATION_OFFSET = prove
 123  (`!p m n a. variation(m+p..n+p) a = variation(m..n) (\i. a(i + p))`,
 124   REPEAT GEN_TAC THEN REWRITE_TAC[variation] THEN
 125   MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN MAP_EVERY EXISTS_TAC
 126    [`\(i:num,j). i - p,j - p`; `\(i:num,j). i + p,j + p`] THEN
 127   REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_ELIM_PAIR_THM] THEN
 128   SIMP_TAC[VARIATION_SET_FINITE; FINITE_NUMSEG] THEN
 129   REWRITE_TAC[IN_NUMSEG; PAIR_EQ] THEN
 130   REPEAT STRIP_TAC THEN TRY ASM_ARITH_TAC THENL
 131    [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 132      `y < &0 ==> x = y ==> x < &0`)) THEN
 133     BINOP_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
 134     FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
 135     FIRST_X_ASSUM(MP_TAC o SPEC `i - p:num`) THEN
 136     ANTS_TAC THENL [ASM_ARITH_TAC; MATCH_MP_TAC EQ_IMP] THEN
 137     AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC]);;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* The crucial lemma (roughly Lemma 2 in the paper).                         *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let ARTHAN_LEMMA = prove
 144  (`!n a b.
 145         ~(a n = &0) /\ (b n = &0) /\ (!m. sum(0..m) a = b m)
 146         ==> ?d. ODD d /\ variation (0..n) a = variation (0..n) b + d`,
 147   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
 148   DISCH_THEN(LABEL_TAC "*") THEN
 149   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
 150    [FIRST_X_ASSUM(MP_TAC o SPEC `0`) THEN
 151     ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN
 152     ASM_MESON_TAC[];
 153     ALL_TAC] THEN
 154   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
 155    `~(n = 0) ==> n = 1 \/ 2 <= n`))
 156   THENL
 157    [FIRST_X_ASSUM SUBST_ALL_TAC THEN EXISTS_TAC `1` THEN
 158     CONV_TAC NUM_REDUCE_CONV THEN
 159     CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 160     REWRITE_TAC[VARIATION_2; OPPOSITE_SIGNS] THEN
 161     FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `0` th) THEN MP_TAC(SPEC `1` th)) THEN
 162     SIMP_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG] THEN
 163     CONV_TAC NUM_REDUCE_CONV THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
 164     ASM_ARITH_TAC;
 165     ALL_TAC] THEN
 166   SUBGOAL_THEN `?p. 1 < p /\ p <= n /\ ~(a p = &0)` MP_TAC THENL
 167    [ASM_MESON_TAC[ARITH_RULE `2 <= n ==> 1 < n`; LE_REFL];
 168     GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
 169     REWRITE_TAC[TAUT `a ==> ~(b /\ c /\ ~d) <=> a /\ b /\ c ==> d`] THEN
 170     STRIP_TAC] THEN
 171   REMOVE_THEN "*" (MP_TAC o SPEC `n - 1`) THEN
 172   ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPECL
 173    [`(\i. if i + 1 = 1 then a 0 + a 1 else a(i + 1)):num->real`;
 174     `(\i. b(i + 1)):num->real`]) THEN
 175   ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> ~(n = 1) /\ n - 1 + 1 = n`] THEN
 176   REWRITE_TAC[GSYM(SPEC `1` VARIATION_OFFSET)] THEN ANTS_TAC THENL
 177    [X_GEN_TAC `m:num` THEN MATCH_MP_TAC EQ_TRANS THEN
 178     EXISTS_TAC `sum(0..m+1) a` THEN CONJ_TAC THENL
 179      [SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; ARITH_RULE `0 + 1 <= n + 1`] THEN
 180       CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[REAL_ADD_ASSOC] THEN
 181       AP_TERM_TAC THEN REWRITE_TAC[ARITH_RULE `2 = 1 + 1`; SUM_OFFSET] THEN
 182       MATCH_MP_TAC SUM_EQ_NUMSEG THEN ARITH_TAC;
 183       ASM_REWRITE_TAC[]];
 184     ABBREV_TAC `a':num->real = \m. if m = 1 then a 0 + a 1 else a m` THEN
 185     ASM_SIMP_TAC[ARITH_RULE
 186      `2 <= n ==> n - 1 + 1 = n /\ n - 1 - 1 + 1 = n - 1`] THEN
 187     CONV_TAC NUM_REDUCE_CONV] THEN
 188   SUBGOAL_THEN
 189    `variation (1..n) a' = variation {1,p} a' + variation (p..n) a /\
 190     variation (0..n) a = variation {0,1,p} a + variation (p..n) a`
 191    (CONJUNCTS_THEN SUBST1_TAC)
 192   THENL
 193    [CONJ_TAC THEN MATCH_MP_TAC EQ_TRANS THENL
 194      [EXISTS_TAC `variation(1..p) a' + variation(p..n) a'`;
 195       EXISTS_TAC `variation(0..p) a + variation(p..n) a`] THEN
 196     (CONJ_TAC THENL
 197       [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN EXPAND_TAC "a'" THEN
 198        REWRITE_TAC[IN_NUMSEG] THEN ASM_ARITH_TAC;
 199        BINOP_TAC THENL
 200         [MATCH_MP_TAC VARIATION_SUBSET; MATCH_MP_TAC VARIATION_EQ] THEN
 201        EXPAND_TAC "a'" THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
 202        REWRITE_TAC[IN_NUMSEG] THEN TRY(GEN_TAC THEN ASM_ARITH_TAC) THEN
 203        (CONJ_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[IN_DIFF]]) THEN
 204        REWRITE_TAC[IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
 205        REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN
 206        TRY(FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_ARITH_TAC]);
 207     ALL_TAC] THEN
 208   DISCH_THEN(X_CHOOSE_THEN `d:num` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 209   REWRITE_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_ADD] THEN
 210   DISCH_THEN(ASSUME_TAC o MATCH_MP (INT_ARITH
 211    `a + b:int = c + d ==> c = (a + b) - d`)) THEN
 212   REWRITE_TAC[INT_ARITH `a + b:int = c + d <=> d = (a + b) - c`] THEN
 213   ASM_CASES_TAC `a 0 + a 1 = &0` THENL
 214    [SUBGOAL_THEN `!i. 0 < i /\ i < p ==> b i = &0` ASSUME_TAC THENL
 215      [REPEAT STRIP_TAC THEN
 216       FIRST_X_ASSUM(SUBST1_TAC o SYM o SPEC `i:num`) THEN
 217       ASM_SIMP_TAC[SUM_CLAUSES_LEFT; LE_0;
 218                    ARITH_RULE `0 < i ==> 0 + 1 <= i`] THEN
 219       CONV_TAC NUM_REDUCE_CONV THEN
 220       ASM_REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LID] THEN
 221       MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN REPEAT STRIP_TAC THEN
 222       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
 223       ALL_TAC] THEN
 224     SUBGOAL_THEN `(b:num->real) p = a p` ASSUME_TAC THENL
 225      [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
 226       SIMP_TAC[SUM_CLAUSES_RIGHT; ASSUME `1 < p`;
 227                  ARITH_RULE `1 < p ==> 0 < p /\ 0 <= p`] THEN
 228       ASM_REWRITE_TAC[REAL_EQ_ADD_RCANCEL_0] THEN
 229       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
 230       ALL_TAC] THEN
 231     SUBGOAL_THEN `variation(0..n) b = variation {0,p} b + variation(1..n) b`
 232     SUBST1_TAC THENL
 233      [MATCH_MP_TAC EQ_TRANS THEN
 234       EXISTS_TAC `variation(0..p) b + variation(p..n) b` THEN CONJ_TAC THENL
 235        [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN REWRITE_TAC[IN_NUMSEG] THEN
 236         CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 237         FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `p:num`) THEN
 238         SIMP_TAC[SUM_CLAUSES_RIGHT; ASSUME `1 < p`;
 239                  ARITH_RULE `1 < p ==> 0 < p /\ 0 <= p`] THEN
 240         ASM_REWRITE_TAC[] THEN
 241         FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 242          `~(ap = &0) ==> s = &0 ==> ~(s + ap = &0)`)) THEN
 243         FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
 244         BINOP_TAC THENL [ALL_TAC; CONV_TAC SYM_CONV] THEN
 245         MATCH_MP_TAC VARIATION_SUBSET THEN
 246         REWRITE_TAC[SUBSET; IN_DIFF; IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
 247         (CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC]) THEN
 248         FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC];
 249       ALL_TAC];
 250     SUBGOAL_THEN `variation(0..n) b = variation {0,1} b + variation(1..n) b`
 251     SUBST1_TAC THENL
 252      [MATCH_MP_TAC EQ_TRANS THEN
 253       EXISTS_TAC `variation(0..1) b + variation(1..n) b` THEN CONJ_TAC THENL
 254        [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN REWRITE_TAC[IN_NUMSEG] THEN
 255         CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 256         FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `1`) THEN
 257         SIMP_TAC[SUM_CLAUSES_NUMSEG; num_CONV `1`] THEN
 258         CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[];
 259         AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SUBSET THEN
 260         REWRITE_TAC[SUBSET; IN_DIFF; IN_NUMSEG; IN_INSERT; NOT_IN_EMPTY] THEN
 261         ARITH_TAC];
 262       SUBGOAL_THEN `(b:num->real) 1 = a 0 + a 1` ASSUME_TAC THENL
 263        [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM th]) THEN
 264         SIMP_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG] THEN
 265         CONV_TAC NUM_REDUCE_CONV;
 266         ALL_TAC]]] THEN
 267   REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `0`)) THEN CONV_TAC NUM_REDUCE_CONV THEN
 268   REWRITE_TAC[SUM_SING_NUMSEG] THEN DISCH_TAC THEN
 269   ASM_REWRITE_TAC[GSYM INT_OF_NUM_ADD] THEN
 270   ASM_SIMP_TAC[VARIATION_3; ARITH; OPPOSITE_SIGNS] THEN COND_CASES_TAC THEN
 271   REWRITE_TAC[VARIATION_2; OPPOSITE_SIGNS; REAL_LT_REFL] THEN
 272   EXPAND_TAC "a'" THEN CONV_TAC NUM_REDUCE_CONV THEN
 273   ASM_SIMP_TAC[ARITH_RULE `1 < p ==> ~(p = 1)`; REAL_LT_REFL] THEN
 274   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 275   CONV_TAC NUM_REDUCE_CONV THEN
 276   CONV_TAC(BINDER_CONV(RAND_CONV(RAND_CONV INT_POLY_CONV))) THEN
 277   REWRITE_TAC[INT_ARITH `x:int = y + --z <=> x + z = y`] THEN
 278   REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_EQ] THEN
 279   ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[UNWIND_THM2] THEN
 280   ASM_REWRITE_TAC[ODD_ADD; ARITH_ODD; ARITH_EVEN] THEN ASM_REAL_ARITH_TAC);;
 281
 282 (* ------------------------------------------------------------------------- *)
 283 (* Relate even-ness or oddity of variation to signs of end coefficients.     *)
 284 (* ------------------------------------------------------------------------- *)
 285
 286 let VARIATION_OPPOSITE_ENDS = prove
 287  (`!a m n.
 288     m <= n /\ ~(a m = &0) /\ ~(a n = &0)
 289     ==> (ODD(variation(m..n) a) <=> a m * a n < &0)`,
 290   REPEAT GEN_TAC THEN WF_INDUCT_TAC `n - m:num` THEN REPEAT STRIP_TAC THEN
 291   ASM_CASES_TAC `!i:num. m < i /\ i < n ==> a i = &0` THENL
 292    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `ODD(variation {m,n} a)` THEN
 293     CONJ_TAC THENL
 294      [AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SUBSET THEN
 295       ASM_REWRITE_TAC[INSERT_SUBSET; IN_NUMSEG; IN_DIFF; EMPTY_SUBSET] THEN
 296       REWRITE_TAC[LE_REFL; IN_INSERT; NOT_IN_EMPTY] THEN
 297       REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
 298       REWRITE_TAC[VARIATION_2] THEN COND_CASES_TAC THEN
 299       ASM_REWRITE_TAC[ARITH]];
 300     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
 301     REWRITE_TAC[NOT_IMP] THEN
 302     DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 303     FIRST_X_ASSUM(fun th ->
 304         MP_TAC(SPECL [`n:num`; `p:num`] th) THEN
 305         MP_TAC(SPECL [`p:num`; `m:num`] th)) THEN
 306     ASM_SIMP_TAC[LT_IMP_LE] THEN
 307     REPEAT(ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_TAC]) THEN
 308     MATCH_MP_TAC EQ_TRANS THEN
 309     EXISTS_TAC `ODD(variation(m..p) a + variation(p..n) a)` THEN CONJ_TAC THENL
 310      [AP_TERM_TAC THEN MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN
 311       ASM_SIMP_TAC[LT_IMP_LE; IN_NUMSEG];
 312       ASM_REWRITE_TAC[ODD_ADD; OPPOSITE_SIGNS] THEN ASM_REAL_ARITH_TAC]]);;
 313
 314 (* ------------------------------------------------------------------------- *)
 315 (* Polynomial with odd variation has at least one positive root.             *)
 316 (* This is the only "analytical" part of the proof.                          *)
 317 (* ------------------------------------------------------------------------- *)
 318
 319 let REAL_POLYFUN_SGN_AT_INFINITY = prove
 320  (`!a n. ~(a n = &0)
 321          ==> ?B. &0 < B /\
 322                  !x. B <= abs x
 323                      ==> real_sgn(sum(0..n) (\i. a i * x pow i)) =
 324                          real_sgn(a n * x pow n)`,
 325   let lemma = prove
 326    (`abs(x) < abs(y) ==> real_sgn(x + y) = real_sgn y`,
 327     REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC) in
 328   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
 329    [EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_LT_01; SUM_SING_NUMSEG];
 330     ALL_TAC] THEN
 331   ABBREV_TAC `B = sum (0..n-1) (\i. abs(a i)) / abs(a n)` THEN
 332   SUBGOAL_THEN `&0 <= B` ASSUME_TAC THENL
 333    [EXPAND_TAC "B" THEN SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS; SUM_POS_LE_NUMSEG];
 334     ALL_TAC] THEN
 335   EXISTS_TAC `&1 + B` THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 336   X_GEN_TAC `x:real` THEN STRIP_TAC THEN
 337   ASM_SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; LE_1] THEN MATCH_MP_TAC lemma THEN
 338   MATCH_MP_TAC REAL_LET_TRANS THEN
 339   EXISTS_TAC `sum(0..n-1) (\i. abs(a i)) * abs x pow (n - 1)` THEN
 340   CONJ_TAC THENL
 341    [REWRITE_TAC[GSYM SUM_RMUL] THEN MATCH_MP_TAC SUM_ABS_LE THEN
 342     REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
 343     X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_ABS_MUL] THEN
 344     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS; REAL_ABS_POW] THEN
 345     MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
 346     SUBGOAL_THEN `(x:real) pow n = x * x pow (n - 1)` SUBST1_TAC THENL
 347      [SIMP_TAC[GSYM(CONJUNCT2 real_pow)] THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
 348       REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_MUL_ASSOC] THEN
 349       MATCH_MP_TAC REAL_LT_RMUL THEN CONJ_TAC THENL
 350        [ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 351         ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ] THEN
 352         ASM_REAL_ARITH_TAC;
 353         MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC]]]);;
 354
 355 let REAL_POLYFUN_HAS_POSITIVE_ROOT = prove
 356  (`!a n. a 0 < &0 /\ &0 < a n
 357          ==> ?x. &0 < x /\ sum(0..n) (\i. a i * x pow i) = &0`,
 358   REPEAT STRIP_TAC THEN
 359   SUBGOAL_THEN `?x. &0 < x /\ &0 <= sum(0..n) (\i. a i * x pow i)`
 360   STRIP_ASSUME_TAC THENL
 361    [MP_TAC(ISPECL [`a:num->real`; `n:num`] REAL_POLYFUN_SGN_AT_INFINITY) THEN
 362     ASM_SIMP_TAC[REAL_LT_IMP_NZ] THEN MATCH_MP_TAC MONO_EXISTS THEN
 363     X_GEN_TAC `x:real` THEN
 364     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:real`)) THEN
 365     ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 366     SUBGOAL_THEN `real_sgn(a n * x pow n) = &1` SUBST1_TAC THEN
 367     ASM_SIMP_TAC[REAL_SGN_EQ; REAL_LT_MUL; REAL_POW_LT; real_gt] THEN
 368     REWRITE_TAC[REAL_LT_IMP_LE];
 369     MP_TAC(ISPECL [`\x. sum(0..n) (\i. a i * x pow i)`;
 370                    `&0`; `x:real`; `&0`] REAL_IVT_INCREASING) THEN
 371     ASM_SIMP_TAC[REAL_LT_IMP_LE; IN_REAL_INTERVAL;
 372                  REAL_POW_ZERO; COND_RAND] THEN
 373     REWRITE_TAC[REAL_MUL_RID; REAL_MUL_RZERO; SUM_DELTA; IN_NUMSEG; LE_0] THEN
 374     ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN ANTS_TAC THENL
 375      [MATCH_MP_TAC REAL_CONTINUOUS_ON_SUM THEN
 376       REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
 377       MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN
 378       MATCH_MP_TAC REAL_CONTINUOUS_ON_POW THEN
 379       REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
 380       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:real` THEN
 381       SIMP_TAC[REAL_LT_LE] THEN ASM_CASES_TAC `y:real = &0` THEN
 382       ASM_SIMP_TAC[REAL_POW_ZERO; COND_RAND; REAL_MUL_RZERO; REAL_MUL_RID] THEN
 383       REWRITE_TAC[SUM_DELTA; IN_NUMSEG; LE_0] THEN ASM_REAL_ARITH_TAC]]);;
 384
 385 let ODD_VARIATION_POSITIVE_ROOT = prove
 386  (`!a n. ODD(variation(0..n) a)
 387          ==> ?x. &0 < x /\ sum(0..n) (\i. a i * x pow i) = &0`,
 388   REPEAT STRIP_TAC THEN
 389   SUBGOAL_THEN `?M. !i. i IN 0..n /\ ~(a i = &0) ==> i <= M` MP_TAC THENL
 390    [EXISTS_TAC `n:num` THEN SIMP_TAC[IN_NUMSEG]; ALL_TAC] THEN
 391   SUBGOAL_THEN `?i. i IN 0..n /\ ~(a i = &0)` MP_TAC THENL
 392    [MATCH_MP_TAC(MESON[] `((!i. P i ==> Q i) ==> F) ==> ?i. P i /\ ~Q i`) THEN
 393     DISCH_TAC THEN SUBGOAL_THEN `variation (0..n) a = variation {0} a`
 394      (fun th -> SUBST_ALL_TAC th THEN ASM_MESON_TAC[VARIATION_1; ODD]) THEN
 395     MATCH_MP_TAC VARIATION_SUBSET THEN
 396     ASM_SIMP_TAC[IN_DIFF] THEN REWRITE_TAC[IN_NUMSEG; SING_SUBSET; LE_0];
 397     ALL_TAC] THEN
 398   ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> a ==> a /\ b ==> c`] THEN
 399   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN REWRITE_TAC[num_MAX] THEN
 400   REWRITE_TAC[TAUT `p ==> ~(q /\ r) <=> p /\ q ==> ~r`; IN_NUMSEG] THEN
 401   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 402   ONCE_REWRITE_TAC[TAUT `p /\ ~q ==> r <=> p /\ ~r ==> q`] THEN
 403   DISCH_THEN(X_CHOOSE_THEN `q:num` STRIP_ASSUME_TAC) THEN
 404   SUBGOAL_THEN `p:num <= q` ASSUME_TAC THENL
 405    [ASM_MESON_TAC[NOT_LT]; ALL_TAC] THEN
 406   SUBGOAL_THEN `(a:num->real) p * a q < &0` ASSUME_TAC THENL
 407    [ASM_SIMP_TAC[GSYM VARIATION_OPPOSITE_ENDS] THEN
 408     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
 409      `ODD p ==> p = q ==> ODD q`)) THEN
 410     MATCH_MP_TAC VARIATION_SUBSET THEN
 411     REWRITE_TAC[SUBSET_NUMSEG; IN_NUMSEG; IN_DIFF; DE_MORGAN_THM] THEN
 412     CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC] THEN
 413     FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN ASM_ARITH_TAC);
 414     ALL_TAC] THEN
 415   MP_TAC(ISPECL [`\i. (a:num->real)(p + i) / a q`; `q - p:num`]
 416         REAL_POLYFUN_HAS_POSITIVE_ROOT) THEN
 417   ASM_SIMP_TAC[ADD_CLAUSES; ARITH_RULE `p:num <= q ==> p + q - p = q`] THEN
 418   ANTS_TAC THENL
 419    [REWRITE_TAC[real_div; OPPOSITE_SIGNS; REAL_MUL_POS_LT] THEN
 420     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPPOSITE_SIGNS]) THEN
 421     REWRITE_TAC[REAL_ARITH `x < &0 <=> &0 < --x`; GSYM REAL_INV_NEG] THEN
 422     REWRITE_TAC[REAL_LT_INV_EQ] THEN REAL_ARITH_TAC;
 423     ALL_TAC] THEN
 424   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real` THEN
 425   MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_RING
 426    `!a. y = a * x ==> x = &0 ==> y = &0`) THEN
 427   EXISTS_TAC `(a:num->real) q * x pow p` THEN
 428   REWRITE_TAC[GSYM SUM_LMUL; REAL_ARITH
 429    `(aq * xp) * api / aq * xi:real = (aq / aq) * api * (xp * xi)`] THEN
 430   ASM_CASES_TAC `(a:num->real) q = &0` THENL
 431    [ASM_MESON_TAC[REAL_MUL_LZERO; REAL_LT_REFL]; ALL_TAC] THEN
 432   ASM_SIMP_TAC[GSYM REAL_POW_ADD; REAL_DIV_REFL; REAL_MUL_LID] THEN
 433   ONCE_REWRITE_TAC[ADD_SYM] THEN MP_TAC(SPEC `p:num` SUM_OFFSET) THEN
 434   DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN
 435   MATCH_MP_TAC SUM_SUPERSET THEN
 436   REWRITE_TAC[SUBSET_NUMSEG; IN_NUMSEG; IN_DIFF; DE_MORGAN_THM] THEN
 437   CONJ_TAC THENL [ASM_ARITH_TAC; REPEAT STRIP_TAC] THEN
 438   REWRITE_TAC[REAL_ENTIRE] THEN DISJ1_TAC THEN
 439   FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN ASM_ARITH_TAC));;
 440
 441 (* ------------------------------------------------------------------------- *)
 442 (* Define root multiplicities.                                               *)
 443 (* ------------------------------------------------------------------------- *)
 444
 445 let multiplicity = new_definition
 446  `multiplicity f r =
 447         @k. ?a n. ~(sum(0..n) (\i. a i * r pow i) = &0) /\
 448                   !x. f(x) = (x - r) pow k * sum(0..n) (\i. a i * x pow i)`;;
 449
 450 let MULTIPLICITY_UNIQUE = prove
 451  (`!f a r b m k.
 452         (!x. f(x) = (x - r) pow k * sum(0..m) (\j. b j * x pow j)) /\
 453         ~(sum(0..m) (\j. b j * r pow j) = &0)
 454         ==> k = multiplicity f r`,
 455   let lemma = prove
 456    (`!i j f g. f real_continuous_on (:real) /\ g real_continuous_on (:real) /\
 457                ~(f r = &0) /\ ~(g r = &0)
 458                ==> (!x. (x - r) pow i * f(x) = (x - r) pow j * g(x))
 459                    ==> j = i`,
 460     MATCH_MP_TAC WLOG_LT THEN
 461     REWRITE_TAC[] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
 462     MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN REPEAT STRIP_TAC THEN
 463     MATCH_MP_TAC(TAUT `F ==> p`) THEN
 464     MP_TAC(ISPECL [`atreal r`; `f:real->real`;
 465                    `(f:real->real) r`; `&0`]
 466           REALLIM_UNIQUE) THEN
 467     ASM_REWRITE_TAC[TRIVIAL_LIMIT_ATREAL] THEN CONJ_TAC THENL
 468      [REWRITE_TAC[GSYM REAL_CONTINUOUS_ATREAL] THEN
 469       ASM_MESON_TAC[REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REAL_OPEN_UNIV;
 470                     IN_UNIV];
 471       MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
 472       EXISTS_TAC `\x:real. (x - r) pow (j - i) * g x` THEN
 473       REWRITE_TAC[] THEN CONJ_TAC THENL
 474        [REWRITE_TAC[EVENTUALLY_ATREAL] THEN EXISTS_TAC `&1` THEN
 475         REWRITE_TAC[REAL_LT_01; REAL_ARITH `&0 < abs(x - r) <=> ~(x = r)`] THEN
 476         X_GEN_TAC `x:real` THEN STRIP_TAC THEN MATCH_MP_TAC(REAL_RING
 477          `!a. a * x = a * y /\ ~(a = &0) ==> x = y`) THEN
 478         EXISTS_TAC `(x - r:real) pow i` THEN
 479         ASM_REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD; REAL_POW_EQ_0] THEN
 480         ASM_SIMP_TAC[REAL_SUB_0; ARITH_RULE `i:num < j ==> i + j - i = j`];
 481         SUBST1_TAC(REAL_ARITH `&0 = &0 * (g:real->real) r`) THEN
 482         MATCH_MP_TAC REALLIM_MUL THEN CONJ_TAC THENL
 483          [REWRITE_TAC[] THEN MATCH_MP_TAC REALLIM_NULL_POW THEN
 484           REWRITE_TAC[GSYM REALLIM_NULL; REALLIM_ATREAL_ID] THEN ASM_ARITH_TAC;
 485           REWRITE_TAC[GSYM REAL_CONTINUOUS_ATREAL] THEN
 486           ASM_MESON_TAC[REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
 487                         REAL_OPEN_UNIV; IN_UNIV]]]]) in
 488   REPEAT STRIP_TAC THEN REWRITE_TAC[multiplicity] THEN
 489   CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 490   X_GEN_TAC `j:num` THEN EQ_TAC THEN ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THENL
 491    [REPEAT GEN_TAC THEN
 492     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 493     MATCH_MP_TAC lemma THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
 494     MATCH_MP_TAC REAL_CONTINUOUS_ON_SUM THEN
 495     REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
 496     MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN
 497     MATCH_MP_TAC REAL_CONTINUOUS_ON_POW THEN
 498     REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
 499     DISCH_THEN SUBST1_TAC THEN
 500     MAP_EVERY EXISTS_TAC [`b:num->real`; `m:num`] THEN ASM_REWRITE_TAC[]]);;
 501
 502 let MULTIPLICITY_WORKS = prove
 503  (`!r n a.
 504     (?i. i IN 0..n /\ ~(a i = &0))
 505     ==> ?b m.
 506         ~(sum(0..m) (\i. b i * r pow i) = &0) /\
 507         !x. sum(0..n) (\i. a i * x pow i) =
 508             (x - r) pow multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r *
 509             sum(0..m) (\i. b i * x pow i)`,
 510   REWRITE_TAC[multiplicity] THEN CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
 511   GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
 512   DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
 513   ASM_CASES_TAC `(a:num->real) n = &0` THENL
 514    [ASM_CASES_TAC `n = 0` THEN
 515     ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
 516     THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 517     DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
 518     ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 519     DISCH_THEN(MP_TAC o SPEC `a:num->real`) THEN
 520     ASM_SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; LE_1] THEN
 521     REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
 522     DISCH_THEN MATCH_MP_TAC THEN
 523     FIRST_X_ASSUM(X_CHOOSE_THEN `i:num` MP_TAC) THEN
 524     REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN
 525     EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[] THEN
 526     ASM_CASES_TAC `i:num = n` THENL [ASM_MESON_TAC[]; ASM_ARITH_TAC];
 527     ALL_TAC] THEN
 528   DISCH_THEN(K ALL_TAC) THEN
 529   ASM_CASES_TAC `sum(0..n) (\i. a i * r pow i) = &0` THENL
 530    [ASM_CASES_TAC `n = 0` THENL
 531      [UNDISCH_TAC `sum (0..n) (\i. a i * r pow i) = &0` THEN
 532       ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2; SUM_SING] THEN
 533       REWRITE_TAC[real_pow; REAL_MUL_RID] THEN ASM_MESON_TAC[];
 534       ALL_TAC] THEN
 535     MP_TAC(GEN `x:real` (ISPECL [`a:num->real`; `x:real`; `r:real`; `n:num`]
 536         REAL_SUB_POLYFUN)) THEN ASM_SIMP_TAC[LE_1; REAL_SUB_RZERO] THEN
 537     ABBREV_TAC `b j = sum (j + 1..n) (\i. a i * r pow (i - j - 1))` THEN
 538     DISCH_THEN(K ALL_TAC) THEN
 539     FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [GSYM FUN_EQ_THM]) THEN
 540     FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
 541     ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 542     DISCH_THEN(MP_TAC o SPEC `b:num->real`) THEN ANTS_TAC THENL
 543      [EXISTS_TAC `n - 1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0] THEN
 544       EXPAND_TAC "b" THEN REWRITE_TAC[] THEN
 545       ASM_SIMP_TAC[SUB_ADD; LE_1; SUM_SING_NUMSEG; real_pow; REAL_MUL_RID;
 546                    ARITH_RULE `n - (n - 1) - 1 = 0`];
 547       ALL_TAC] THEN
 548     DISCH_THEN(X_CHOOSE_THEN `k:num` (fun th ->
 549         EXISTS_TAC `SUC k` THEN MP_TAC th)) THEN
 550     REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
 551     STRIP_TAC THEN ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC];
 552     MAP_EVERY EXISTS_TAC [`0`; `a:num->real`; `n:num`] THEN
 553     ASM_REWRITE_TAC[real_pow; REAL_MUL_LID]]);;
 554
 555 let MULTIPLICITY_OTHER_ROOT = prove
 556  (`!a n r s.
 557     ~(r = s) /\ (?i. i IN 0..n /\ ~(a i = &0))
 558      ==> multiplicity (\x. (x - r) pow m * sum(0..n) (\i. a i * x pow i)) s =
 559          multiplicity (\x.  sum(0..n) (\i. a i * x pow i)) s`,
 560   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
 561   CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_UNIQUE THEN
 562   REWRITE_TAC[] THEN
 563   MP_TAC(ISPECL [`s:real`; `n:num`; `a:num->real`]
 564         MULTIPLICITY_WORKS) THEN
 565   ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 566   MAP_EVERY X_GEN_TAC [`c:num->real`; `p:num`] THEN
 567   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
 568   SUBGOAL_THEN
 569    `?b q. !x. sum(0..q) (\j. b j * x pow j) =
 570               (x - r) pow m * sum (0..p) (\i. c i * x pow i)`
 571   MP_TAC THENL
 572    [ALL_TAC;
 573     REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
 574     STRIP_TAC THEN
 575     ASM_REWRITE_TAC[REAL_RING `r * x = s * r * y <=> r = &0 \/ s * y = x`] THEN
 576     ASM_REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_SUB_0]] THEN
 577   MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`c:num->real`; `p:num`; `m:num`] THEN
 578   POP_ASSUM_LIST(K ALL_TAC) THEN INDUCT_TAC THEN REPEAT GEN_TAC THENL
 579    [MAP_EVERY EXISTS_TAC [`c:num->real`; `p:num`] THEN
 580     ASM_REWRITE_TAC[real_pow; REAL_MUL_LID];
 581     ALL_TAC] THEN
 582   FIRST_X_ASSUM(MP_TAC o SPECL [`p:num`; `c:num->real`]) THEN
 583   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 584   MAP_EVERY X_GEN_TAC [`a:num->real`; `n:num`] THEN
 585   DISCH_THEN(ASSUME_TAC o GSYM) THEN
 586   ASM_REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
 587   EXISTS_TAC `\i. (if 0 < i then a(i - 1) else &0) -
 588                   (if i <= n then r * a i else &0)` THEN
 589   EXISTS_TAC `n + 1` THEN
 590   REWRITE_TAC[REAL_SUB_RDISTRIB; SUM_SUB_NUMSEG] THEN X_GEN_TAC `x:real` THEN
 591   BINOP_TAC THENL
 592    [MP_TAC(ARITH_RULE `0 <= n + 1`) THEN SIMP_TAC[SUM_CLAUSES_LEFT] THEN
 593     DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[SUM_OFFSET; LT_REFL] THEN
 594     REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID; ARITH_RULE `0 < i + 1`] THEN
 595     REWRITE_TAC[GSYM SUM_LMUL; ADD_SUB; REAL_POW_ADD; REAL_POW_1];
 596     SIMP_TAC[SUM_CLAUSES_RIGHT; LE_0; ARITH_RULE `0 < n + 1`] THEN
 597     REWRITE_TAC[ADD_SUB; ARITH_RULE `~(n + 1 <= n)`] THEN
 598     SIMP_TAC[REAL_MUL_LZERO; REAL_ADD_RID; GSYM SUM_LMUL]] THEN
 599   MATCH_MP_TAC SUM_EQ_NUMSEG THEN REWRITE_TAC[REAL_MUL_AC]);;
 600
 601 (* ------------------------------------------------------------------------- *)
 602 (* The main lemmas to be applied iteratively.                                *)
 603 (* ------------------------------------------------------------------------- *)
 604
 605 let VARIATION_POSITIVE_ROOT_FACTOR = prove
 606  (`!a n r.
 607     ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
 608     ==> ?b. ~(b(n - 1) = &0) /\
 609             (!x. sum(0..n) (\i. a i * x pow i) =
 610                  (x - r) * sum(0..n-1) (\i. b i * x pow i)) /\
 611             ?d. ODD d /\ variation(0..n) a = variation(0..n-1) b + d`,
 612   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 613    [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; real_pow; REAL_MUL_RID] THEN MESON_TAC[];
 614     STRIP_TAC] THEN
 615   ABBREV_TAC `b = \j. sum (j + 1..n) (\i. a i * r pow (i - j - 1))` THEN
 616   EXISTS_TAC `b:num->real` THEN REPEAT CONJ_TAC THENL
 617    [EXPAND_TAC "b" THEN REWRITE_TAC[] THEN ASM_SIMP_TAC[SUB_ADD; LE_1] THEN
 618     ASM_SIMP_TAC[SUM_SING_NUMSEG; ARITH_RULE `n - (n - 1) - 1 = 0`] THEN
 619     ASM_REWRITE_TAC[real_pow; REAL_MUL_RID];
 620     MP_TAC(GEN `x:real` (SPECL [`a:num->real`; `x:real`; `r:real`; `n:num`]
 621         REAL_SUB_POLYFUN)) THEN
 622     ASM_SIMP_TAC[LE_1; REAL_SUB_RZERO] THEN DISCH_THEN(K ALL_TAC) THEN
 623     EXPAND_TAC "b" THEN REWRITE_TAC[];
 624     ALL_TAC] THEN
 625   SUBGOAL_THEN `(b:num->real) n = &0` ASSUME_TAC THENL
 626    [EXPAND_TAC "b" THEN REWRITE_TAC[] THEN MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN
 627     ARITH_TAC;
 628     ALL_TAC] THEN
 629   MP_TAC(ISPECL
 630    [`n:num`; `\i. if i <= n then a i * (r:real) pow i else &0`;
 631     `\i. if i <= n then --b i * (r:real) pow (i + 1) else &0`]
 632    ARTHAN_LEMMA) THEN
 633   ASM_SIMP_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_LT_IMP_NZ; REAL_NEG_0;
 634                LE_REFL] THEN
 635   ANTS_TAC THENL
 636    [X_GEN_TAC `j:num` THEN EXPAND_TAC "b" THEN REWRITE_TAC[] THEN
 637     ASM_CASES_TAC `j:num <= n` THEN ASM_REWRITE_TAC[] THENL
 638      [SUBGOAL_THEN `!i:num. i <= j ==> i <= n` MP_TAC THENL
 639        [ASM_ARITH_TAC; SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC)] THEN
 640       REWRITE_TAC[REAL_ARITH `a:real = --b * c <=> a + b * c = &0`] THEN
 641       REWRITE_TAC[GSYM SUM_RMUL; GSYM REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
 642       SIMP_TAC[ARITH_RULE `j + 1 <= k ==> k - j - 1 + j + 1 = k`] THEN
 643       ASM_SIMP_TAC[SUM_COMBINE_R; LE_0];
 644       REWRITE_TAC[GSYM SUM_RESTRICT_SET; IN_NUMSEG] THEN
 645       ASM_SIMP_TAC[ARITH_RULE
 646       `~(j <= n) ==> ((0 <= i /\ i <= j) /\ i <= n <=> 0 <= i /\ i <= n)`] THEN
 647       ASM_REWRITE_TAC[GSYM numseg]];
 648     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
 649     MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN MATCH_MP_TAC(ARITH_RULE
 650      `x':num = x /\ y' = y ==> x' = y' + d ==> x = y + d`) THEN
 651     CONJ_TAC THENL
 652      [MATCH_MP_TAC EQ_TRANS THEN
 653       EXISTS_TAC `variation(0..n) (\i. a i * r pow i)` THEN CONJ_TAC THENL
 654        [MATCH_MP_TAC VARIATION_EQ THEN SIMP_TAC[IN_NUMSEG];
 655         ALL_TAC];
 656       MATCH_MP_TAC EQ_TRANS THEN
 657       EXISTS_TAC `variation(0..n) (\i. --b i * r pow (i + 1))` THEN
 658       CONJ_TAC THENL
 659        [MATCH_MP_TAC VARIATION_EQ THEN SIMP_TAC[IN_NUMSEG];
 660         ALL_TAC] THEN
 661       MATCH_MP_TAC EQ_TRANS THEN
 662       EXISTS_TAC `variation(0..n-1) (\i. --b i * r pow (i + 1))` THEN
 663       CONJ_TAC THENL
 664        [MATCH_MP_TAC VARIATION_SUBSET THEN
 665         REWRITE_TAC[SUBSET_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
 666         CONJ_TAC THENL [ARITH_TAC; X_GEN_TAC `i:num` THEN STRIP_TAC] THEN
 667         SUBGOAL_THEN `i:num = n` SUBST_ALL_TAC THENL
 668          [ASM_ARITH_TAC; ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC];
 669         ALL_TAC]] THEN
 670     REWRITE_TAC[variation] THEN
 671     ONCE_REWRITE_TAC[REAL_ARITH
 672       `(a * x) * (b * x'):real = (x * x') * a * b`] THEN
 673     SIMP_TAC[NOT_IMP; GSYM CONJ_ASSOC; GSYM REAL_POW_ADD;
 674              REAL_ARITH `--x * --y:real = x * y`] THEN
 675     ONCE_REWRITE_TAC[REAL_ARITH `x * y < &0 <=> &0 < x * --y`] THEN
 676     ASM_SIMP_TAC[REAL_LT_MUL_EQ; REAL_POW_LT] THEN
 677     ASM_SIMP_TAC[REAL_MUL_RNEG; REAL_ENTIRE; REAL_NEG_EQ_0; REAL_POW_EQ_0] THEN
 678     ASM_SIMP_TAC[REAL_LT_IMP_NZ]]);;
 679
 680 let VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR = prove
 681  (`!r n a.
 682     ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
 683     ==> ?b k m. 0 < k /\ m < n /\ ~(b m = &0) /\
 684                 (!x. sum(0..n) (\i. a i * x pow i) =
 685                      (x - r) pow k * sum(0..m) (\i. b i * x pow i)) /\
 686                 ~(sum(0..m) (\j. b j * r pow j) = &0) /\
 687                 ?d. EVEN d /\ variation(0..n) a = variation(0..m) b + k + d`,
 688   GEN_TAC THEN MATCH_MP_TAC num_WF THEN
 689   X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `a:num->real` THEN
 690   ASM_CASES_TAC `n = 0` THENL
 691    [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; real_pow; REAL_MUL_RID] THEN MESON_TAC[];
 692     STRIP_TAC] THEN
 693   MP_TAC(ISPECL [`a:num->real`; `n:num`; `r:real`]
 694         VARIATION_POSITIVE_ROOT_FACTOR) THEN
 695   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `c:num->real` MP_TAC) THEN
 696   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 697   DISCH_THEN(X_CHOOSE_THEN `d:num` STRIP_ASSUME_TAC) THEN
 698   ASM_CASES_TAC `sum(0..n-1) (\i. c i * r pow i) = &0` THENL
 699    [FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
 700     ANTS_TAC THENL [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `c:num->real`)] THEN
 701     ASM_REWRITE_TAC[] THEN
 702     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:num->real` THEN
 703     ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 704     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
 705     DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
 706     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 707     DISCH_THEN(X_CHOOSE_THEN `e:num` STRIP_ASSUME_TAC) THEN
 708     EXISTS_TAC `SUC k` THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_ASSOC] THEN
 709     REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
 710     REWRITE_TAC[ADD1; ADD_ASSOC] THEN EXISTS_TAC `d - 1 + e`;
 711     MAP_EVERY EXISTS_TAC [`c:num->real`; `1`; `n - 1`] THEN
 712     ASM_REWRITE_TAC[REAL_POW_1] THEN
 713     REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
 714     EXISTS_TAC `d - 1`] THEN
 715   UNDISCH_TAC `ODD d` THEN GEN_REWRITE_TAC LAND_CONV [ODD_EXISTS] THEN
 716   DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST1_TAC) THEN
 717   ASM_REWRITE_TAC[SUC_SUB1; EVEN_ADD; EVEN_MULT; ARITH] THEN ARITH_TAC);;
 718
 719 let VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR = prove
 720  (`!r n a.
 721     ~(a n = &0) /\ &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0
 722     ==> ?b m. m < n /\ ~(b m = &0) /\
 723               (!x. sum(0..n) (\i. a i * x pow i) =
 724                    (x - r) pow
 725                    (multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r) *
 726                    sum(0..m) (\i. b i * x pow i)) /\
 727               ~(sum(0..m) (\j. b j * r pow j) = &0) /\
 728               ?d. EVEN d /\
 729                   variation(0..n) a = variation(0..m) b +
 730                      multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r + d`,
 731   REPEAT GEN_TAC THEN
 732   DISCH_THEN(MP_TAC o MATCH_MP VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR) THEN
 733   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:num->real` THEN
 734   DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
 735   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
 736   DISCH_TAC THEN
 737   SUBGOAL_THEN `multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r = k`
 738    (fun th -> ASM_REWRITE_TAC[th]) THEN
 739   CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_UNIQUE THEN
 740   MAP_EVERY EXISTS_TAC [`b:num->real`; `m:num`] THEN ASM_REWRITE_TAC[]);;
 741
 742 (* ------------------------------------------------------------------------- *)
 743 (* Hence the main theorem.                                                   *)
 744 (* ------------------------------------------------------------------------- *)
 745
 746 let DESCARTES_RULE_OF_SIGNS = prove
 747  (`!f a n. f = (\x. sum(0..n) (\i. a i * x pow i)) /\
 748            (?i. i IN 0..n /\ ~(a i = &0))
 749            ==> ?d. EVEN d /\
 750                    variation(0..n) a =
 751                    nsum {r | &0 < r /\ f(r) = &0} (\r. multiplicity f r) + d`,
 752   REPEAT GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 753   DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 754   MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`a:num->real`; `n:num`] THEN
 755   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 756   X_GEN_TAC `a:num->real` THEN ASM_CASES_TAC `(a:num->real) n = &0` THENL
 757    [ASM_CASES_TAC `n = 0` THEN
 758     ASM_REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2]
 759     THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
 760     FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN ANTS_TAC THENL
 761      [ASM_ARITH_TAC; DISCH_THEN(MP_TAC o SPEC `a:num->real`)] THEN
 762     ANTS_TAC THENL
 763      [ASM_MESON_TAC[IN_NUMSEG; ARITH_RULE `i <= n ==> i <= n - 1 \/ i = n`];
 764       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
 765       ASM_SIMP_TAC[LE_0; LE_1; SUM_CLAUSES_RIGHT] THEN
 766       REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
 767       DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
 768       MATCH_MP_TAC VARIATION_SUBSET THEN
 769       REWRITE_TAC[SUBSET_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
 770       CONJ_TAC THENL [ASM_ARITH_TAC; X_GEN_TAC `i:num` THEN STRIP_TAC] THEN
 771       SUBGOAL_THEN `i:num = n` (fun th -> ASM_REWRITE_TAC[th]) THEN
 772       ASM_ARITH_TAC];
 773     DISCH_THEN(K ALL_TAC)] THEN
 774   ASM_CASES_TAC `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} = {}` THENL
 775    [ASM_REWRITE_TAC[NSUM_CLAUSES; ADD_CLAUSES] THEN
 776     ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[UNWIND_THM1] THEN
 777     ONCE_REWRITE_TAC[GSYM NOT_ODD] THEN
 778     DISCH_THEN(MP_TAC o MATCH_MP ODD_VARIATION_POSITIVE_ROOT) THEN
 779     ASM SET_TAC[];
 780     ALL_TAC] THEN
 781   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 782   REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 783   X_GEN_TAC `r:real` THEN STRIP_TAC THEN
 784   MP_TAC(ISPECL [`r:real`; `n:num`; `a:num->real`]
 785     VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR) THEN
 786   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 787   MAP_EVERY X_GEN_TAC [`b:num->real`; `m:num`] THEN
 788   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
 789   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
 790   ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
 791   DISCH_THEN(MP_TAC o SPEC `b:num->real`) THEN ANTS_TAC THENL
 792    [EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0];
 793     ALL_TAC] THEN
 794   DISCH_THEN(X_CHOOSE_THEN `d1:num`
 795     (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
 796   FIRST_X_ASSUM(X_CHOOSE_THEN `d2:num`
 797     (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
 798   EXISTS_TAC `d1 + d2:num` THEN
 799   CONJ_TAC THENL [ASM_REWRITE_TAC[EVEN_ADD]; ALL_TAC] THEN
 800   MATCH_MP_TAC(ARITH_RULE
 801    `x + y = z ==> (x + d1) + (y + d2):num = z + d1 + d2`) THEN
 802   SUBGOAL_THEN
 803    `{r | &0 < r /\ sum(0..n) (\i. a i * r pow i) = &0} =
 804     r INSERT {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
 805   SUBST1_TAC THENL
 806    [MATCH_MP_TAC(SET_RULE `x IN s /\ s DELETE x = t ==> s = x INSERT t`) THEN
 807     CONJ_TAC THENL
 808      [REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
 809       ONCE_ASM_REWRITE_TAC[] THEN
 810       REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_SUB_0] THEN
 811       REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_DELETE] THEN
 812       X_GEN_TAC `s:real` THEN
 813       FIRST_X_ASSUM(K ALL_TAC o SPEC_VAR) THEN
 814       ASM_CASES_TAC `s:real = r` THEN ASM_REWRITE_TAC[]];
 815     ALL_TAC] THEN
 816   SUBGOAL_THEN
 817    `FINITE {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
 818   MP_TAC THENL
 819    [MATCH_MP_TAC FINITE_SUBSET THEN
 820     EXISTS_TAC `{r | sum(0..m) (\i. b i * r pow i) = &0}` THEN
 821     SIMP_TAC[SUBSET; IN_ELIM_THM; REAL_POLYFUN_FINITE_ROOTS] THEN
 822     EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[IN_NUMSEG; LE_0; LE_REFL];
 823     SIMP_TAC[NSUM_CLAUSES; IN_ELIM_THM] THEN DISCH_TAC] THEN
 824   FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [GSYM FUN_EQ_THM]) THEN
 825   ASM_REWRITE_TAC[] THEN
 826   MATCH_MP_TAC(ARITH_RULE `s1:num = s2 ==> s1 + m = m + s2`) THEN
 827   MATCH_MP_TAC NSUM_EQ THEN
 828   X_GEN_TAC `s:real` THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 829   FIRST_X_ASSUM(fun t -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [t]) THEN
 830   CONV_TAC SYM_CONV THEN MATCH_MP_TAC MULTIPLICITY_OTHER_ROOT THEN
 831   REWRITE_TAC[MESON[] `(?i. P i /\ Q i) <=> ~(!i. P i ==> ~Q i)`] THEN
 832   REPEAT STRIP_TAC THEN
 833   UNDISCH_TAC `~(sum (0..m) (\j. b j * r pow j) = &0)` THEN ASM_SIMP_TAC[] THEN
 834   REWRITE_TAC[REAL_MUL_LZERO; SUM_0]);;