1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
|
(*************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(*************************************************************)
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
(***********************************************************************
Root.v
Proof that a polynomial has at most n roots
************************************************************************)
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Require Import Coqprime.UList.
Require Import Coqprime.Tactic.
Require Import Coqprime.Permutation.
Open Scope Z_scope.
Section Root.
Variable A: Set.
Variable P: A -> Prop.
Variable plus mult: A -> A -> A.
Variable op: A -> A.
Variable zero one: A.
Let pol := list A.
Definition toA z :=
match z with
Z0 => zero
| Zpos p => iter_pos p _ (plus one) zero
| Zneg p => op (iter_pos p _ (plus one) zero)
end.
Fixpoint eval (p: pol) (x: A) {struct p} : A :=
match p with
nil => zero
| a::p1 => plus a (mult x (eval p1 x))
end.
Fixpoint div (p: pol) (x: A) {struct p} : pol * A :=
match p with
nil => (nil, zero)
| a::nil => (nil, a)
| a::p1 =>
(snd (div p1 x)::fst (div p1 x),
(plus a (mult x (snd (div p1 x)))))
end.
Hypothesis Pzero: P zero.
Hypothesis Pplus: forall x y, P x -> P y -> P (plus x y).
Hypothesis Pmult: forall x y, P x -> P y -> P (mult x y).
Hypothesis Pop: forall x, P x -> P (op x).
Hypothesis plus_zero: forall a, P a -> plus zero a = a.
Hypothesis plus_comm: forall a b, P a -> P b -> plus a b = plus b a.
Hypothesis plus_assoc: forall a b c, P a -> P b -> P c -> plus a (plus b c) = plus (plus a b) c.
Hypothesis mult_zero: forall a, P a -> mult zero a = zero.
Hypothesis mult_comm: forall a b, P a -> P b -> mult a b = mult b a.
Hypothesis mult_assoc: forall a b c, P a -> P b -> P c -> mult a (mult b c) = mult (mult a b) c.
Hypothesis mult_plus_distr: forall a b c, P a -> P b -> P c -> mult a (plus b c) = plus (mult a b) (mult a c).
Hypothesis plus_op_zero: forall a, P a -> plus a (op a) = zero.
Hypothesis mult_integral: forall a b, P a -> P b -> mult a b = zero -> a = zero \/ b = zero.
(* Not necessary in Set just handy *)
Hypothesis A_dec: forall a b: A, {a = b} + {a <> b}.
Theorem eval_P: forall p a, P a -> (forall i, In i p -> P i) -> P (eval p a).
intros p a Pa; elim p; simpl; auto with datatypes.
intros a1 l1 Rec H; apply Pplus; auto.
Qed.
Hint Resolve eval_P.
Theorem div_P: forall p a, P a -> (forall i, In i p -> P i) -> (forall i, In i (fst (div p a)) -> P i) /\ P (snd (div p a)).
intros p a Pa; elim p; auto with datatypes.
intros a1 l1; case l1.
simpl; intuition.
intros a2 p2 Rec Hi; split.
case Rec; auto with datatypes.
intros H H1 i.
replace (In i (fst (div (a1 :: a2 :: p2) a))) with
(snd (div (a2::p2) a) = i \/ In i (fst (div (a2::p2) a))); auto.
intros [Hi1 | Hi1]; auto.
rewrite <- Hi1; auto.
change ( P (plus a1 (mult a (snd (div (a2::p2) a))))); auto with datatypes.
apply Pplus; auto with datatypes.
apply Pmult; auto with datatypes.
case Rec; auto with datatypes.
Qed.
Theorem div_correct:
forall p x y, P x -> P y -> (forall i, In i p -> P i) -> eval p y = plus (mult (eval (fst (div p x)) y) (plus y (op x))) (snd (div p x)).
intros p x y; elim p; simpl.
intros; rewrite mult_zero; try rewrite plus_zero; auto.
intros a l; case l; simpl; auto.
intros _ px py pa; rewrite (fun x => mult_comm x zero); repeat rewrite mult_zero; try apply plus_comm; auto.
intros a1 l1.
generalize (div_P (a1::l1) x); simpl.
match goal with |- context[fst ?A] => case A end; simpl.
intros q r Hd Rec px py pi.
assert (pr: P r).
case Hd; auto.
assert (pa1: P a1).
case Hd; auto.
assert (pey: P (eval q y)).
apply eval_P; auto.
case Hd; auto.
rewrite Rec; auto with datatypes.
rewrite (fun x y => plus_comm x (plus a y)); try rewrite <- plus_assoc; auto.
apply f_equal2 with (f := plus); auto.
repeat rewrite mult_plus_distr; auto.
repeat (rewrite (fun x y => (mult_comm (plus x y))) || rewrite mult_plus_distr); auto.
rewrite (fun x => (plus_comm x (mult y r))); auto.
repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto.
2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x));
repeat rewrite mult_assoc; auto.
rewrite (fun z => (plus_comm z (mult (op x) r))); auto.
repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto.
2: apply f_equal2 with (f := mult); auto.
repeat rewrite (fun x => mult_comm x r); try rewrite <- mult_plus_distr; auto.
rewrite (plus_comm (op x)); try rewrite plus_op_zero; auto.
rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; auto.
Qed.
Theorem div_correct_factor:
forall p a, (forall i, In i p -> P i) -> P a ->
eval p a = zero -> forall x, P x -> eval p x = (mult (eval (fst (div p a)) x) (plus x (op a))).
intros p a Hp Ha H x px.
case (div_P p a); auto; intros Hd1 Hd2.
rewrite (div_correct p a x); auto.
generalize (div_correct p a a).
rewrite plus_op_zero; try rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; try rewrite H; auto.
intros H1; rewrite <- H1; auto.
rewrite (fun x => plus_comm x zero); auto.
Qed.
Theorem length_decrease: forall p x, p <> nil -> (length (fst (div p x)) < length p)%nat.
intros p x; elim p; simpl; auto.
intros H1; case H1; auto.
intros a l; case l; simpl; auto.
intros a1 l1.
match goal with |- context[fst ?A] => case A end; simpl; auto with zarith.
intros p1 _ H H1.
apply lt_n_S; apply H; intros; discriminate.
Qed.
Theorem root_max:
forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) ->
(forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, P x -> eval p x = zero.
intros p l; generalize p; elim l; clear l p; simpl; auto.
intros p; case p; simpl; auto.
intros a p1 _ _ _ _ H; contradict H; auto with arith.
intros a p1 Rec p; case p.
simpl; auto.
intros a1 p2 H H1 H2 H3 H4 x px.
assert (Hu: eval (a1 :: p2) a = zero); auto with datatypes.
rewrite (div_correct_factor (a1 :: p2) a); auto with datatypes.
match goal with |- mult ?X _ = _ => replace X with zero end; try apply mult_zero; auto.
apply sym_equal; apply Rec; auto with datatypes.
apply ulist_inv with (1 := H).
intros i Hi; case (div_P (a1 :: p2) a); auto.
intros x1 H5; case (mult_integral (eval (fst (div (a1 :: p2) a)) x1) (plus x1 (op a))); auto.
apply eval_P; auto.
intros i Hi; case (div_P (a1 :: p2) a); auto.
rewrite <- div_correct_factor; auto.
intros H6; case (ulist_app_inv _ (a::nil) p1 x1); simpl; auto.
left.
apply trans_equal with (plus zero x1); auto.
rewrite <- (plus_op_zero a); try rewrite <- plus_assoc; auto.
rewrite (fun x => plus_comm (op x)); try rewrite H6; try rewrite plus_comm; auto.
apply sym_equal; apply plus_zero; auto.
apply lt_n_Sm_le;apply lt_le_trans with (length (a1 :: p2)); auto with zarith.
apply length_decrease; auto with datatypes.
Qed.
Theorem root_max_is_zero:
forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) ->
(forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, (In x p) -> x = zero.
intros p l; generalize p; elim l; clear l p; simpl; auto.
intros p; case p; simpl; auto.
intros _ _ _ _ _ x H; case H.
intros a p1 _ _ _ _ H; contradict H; auto with arith.
intros a p1 Rec p; case p.
simpl; auto.
intros _ _ _ _ _ x H; case H.
simpl; intros a1 p2 H H1 H2 H3 H4 x H5.
assert (Ha1: a1 = zero).
assert (Hu: (eval (a1::p2) zero = zero)).
apply root_max with (l := a :: p1); auto.
rewrite <- Hu; simpl; rewrite mult_zero; try rewrite plus_comm; sauto.
case H5; clear H5; intros H5; subst; auto.
apply Rec with p2; auto with arith.
apply ulist_inv with (1 := H).
intros x1 Hx1.
case (In_dec A_dec zero p1); intros Hz.
case (in_permutation_ex _ zero p1); auto; intros p3 Hp3.
apply root_max with (l := a::p3); auto.
apply ulist_inv with zero.
apply ulist_perm with (a::p1); auto.
apply permutation_trans with (a:: (zero:: p3)); auto.
apply permutation_skip; auto.
apply permutation_sym; auto.
simpl; intros x2 [Hx2 | Hx2]; subst; auto.
apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes.
simpl; intros x2 [Hx2 | Hx2]; subst.
case (mult_integral x2 (eval p2 x2)); auto.
rewrite <- H3 with x2; sauto.
rewrite plus_zero; auto.
intros H6; case (ulist_app_inv _ (x2::nil) p1 x2) ; auto with datatypes.
rewrite H6; apply permutation_in with (1 := Hp3); auto with datatypes.
case (mult_integral x2 (eval p2 x2)); auto.
apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes.
apply eval_P; auto.
apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes.
rewrite <- H3 with x2; sauto; try right.
apply sym_equal; apply plus_zero; auto.
apply Pmult; auto.
apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes.
apply eval_P; auto.
apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes.
apply permutation_in with (1 := Hp3); auto with datatypes.
intros H6; case (ulist_app_inv _ (zero::nil) p3 x2) ; auto with datatypes.
simpl; apply ulist_perm with (1:= (permutation_sym _ _ _ Hp3)).
apply ulist_inv with (1 := H).
rewrite H6; auto with datatypes.
replace (length (a :: p3)) with (length (zero::p3)); auto.
rewrite permutation_length with (1 := Hp3); auto with arith.
case (mult_integral x1 (eval p2 x1)); auto.
rewrite <- H3 with x1; sauto; try right.
apply sym_equal; apply plus_zero; auto.
intros HH; case Hz; rewrite <- HH; auto.
Qed.
End Root.
|
