1 (* ========================================================================= *)
2 (* Rob Arthan's "Descartes's Rule of Signs by an Easy Induction". *)
3 (* ========================================================================= *)
5 needs "Multivariate/realanalysis.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* A couple of handy lemmas. *)
9 (* ------------------------------------------------------------------------- *)
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
16 let VARIATION_SET_FINITE = prove
17 (`FINITE s ==> FINITE {p,q | p IN s /\ q IN s /\ P p q}`,
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]);;
23 (* ------------------------------------------------------------------------- *)
24 (* Variation in a sequence of coefficients. *)
25 (* ------------------------------------------------------------------------- *)
27 let variation = new_definition
28 `variation s (a:num->real) =
29 CARD {(p,q) | p IN s /\ q IN s /\ p < q /\
31 !i. i IN s /\ p < i /\ i < q ==> a(i) = &0 }`;;
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
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]);;
47 let VARIATION_SPLIT = prove
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
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
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);;
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]);;
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
95 `a /\ b /\ c /\ d /\ e <=> (a /\ b /\ c) /\ d /\ e`] THEN
96 ASM_SIMP_TAC[ARITH_RULE
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]]]);;
109 let VARIATION_3 = prove
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
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]);;
139 (* ------------------------------------------------------------------------- *)
140 (* The crucial lemma (roughly Lemma 2 in the paper). *)
141 (* ------------------------------------------------------------------------- *)
143 let ARTHAN_LEMMA = prove
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
154 FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
155 `~(n = 0) ==> n = 1 \/ 2 <= n`))
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
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
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;
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
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)
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
197 [MATCH_MP_TAC VARIATION_SPLIT_NUMSEG THEN EXPAND_TAC "a'" THEN
198 REWRITE_TAC[IN_NUMSEG] THEN ASM_ARITH_TAC;
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]);
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;
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;
231 SUBGOAL_THEN `variation(0..n) b = variation {0,p} b + variation(1..n) b`
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];
250 SUBGOAL_THEN `variation(0..n) b = variation {0,1} b + variation(1..n) b`
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
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;
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);;
282 (* ------------------------------------------------------------------------- *)
283 (* Relate even-ness or oddity of variation to signs of end coefficients. *)
284 (* ------------------------------------------------------------------------- *)
286 let VARIATION_OPPOSITE_ENDS = prove
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
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]]);;
314 (* ------------------------------------------------------------------------- *)
315 (* Polynomial with odd variation has at least one positive root. *)
316 (* This is the only "analytical" part of the proof. *)
317 (* ------------------------------------------------------------------------- *)
319 let REAL_POLYFUN_SGN_AT_INFINITY = prove
323 ==> real_sgn(sum(0..n) (\i. a i * x pow i)) =
324 real_sgn(a n * x pow n)`,
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];
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];
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
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
353 MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC]]]);;
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]]);;
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];
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);
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
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;
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));;
441 (* ------------------------------------------------------------------------- *)
442 (* Define root multiplicities. *)
443 (* ------------------------------------------------------------------------- *)
445 let multiplicity = new_definition
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)`;;
450 let MULTIPLICITY_UNIQUE = prove
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`,
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))
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`]
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;
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
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[]]);;
502 let MULTIPLICITY_WORKS = prove
504 (?i. i IN 0..n /\ ~(a i = &0))
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];
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[];
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`];
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]]);;
555 let MULTIPLICITY_OTHER_ROOT = prove
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
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
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)`
573 REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_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];
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
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]);;
601 (* ------------------------------------------------------------------------- *)
602 (* The main lemmas to be applied iteratively. *)
603 (* ------------------------------------------------------------------------- *)
605 let VARIATION_POSITIVE_ROOT_FACTOR = prove
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[];
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[];
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
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`]
633 ASM_SIMP_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_LT_IMP_NZ; REAL_NEG_0;
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
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];
656 MATCH_MP_TAC EQ_TRANS THEN
657 EXISTS_TAC `variation(0..n) (\i. --b i * r pow (i + 1))` THEN
659 [MATCH_MP_TAC VARIATION_EQ THEN SIMP_TAC[IN_NUMSEG];
661 MATCH_MP_TAC EQ_TRANS THEN
662 EXISTS_TAC `variation(0..n-1) (\i. --b i * r pow (i + 1))` THEN
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];
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]]);;
680 let VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR = prove
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[];
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);;
719 let VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR = prove
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) =
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) /\
729 variation(0..n) a = variation(0..m) b +
730 multiplicity (\x. sum(0..n) (\i. a i * x pow i)) r + d`,
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
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[]);;
742 (* ------------------------------------------------------------------------- *)
743 (* Hence the main theorem. *)
744 (* ------------------------------------------------------------------------- *)
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))
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
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
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
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];
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
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}`
806 [MATCH_MP_TAC(SET_RULE `x IN s /\ s DELETE x = t ==> s = x INSERT t`) THEN
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[]];
817 `FINITE {r | &0 < r /\ sum(0..m) (\i. b i * r pow i) = &0}`
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]);;