QuantumLib.Polynomial
Require Import Psatz.
Require Import String.
Require Export Complex.
Require Import List.
Require Import Setoid.
Declare Scope poly_scope.
Delimit Scope poly_scope with P.
Open Scope poly_scope.
Lemma diff_pow_n : ∀ (n : nat) (a b : C),
(a^(S n) - b^(S n)) = (a - b) × (big_sum (fun i ⇒ a^i × b^(n - i)) (S n)).
Lemma destruct_from_last : ∀ {X} (n : nat) (d : X) (l : list X),
length l = S n → l = (firstn n l) ++ [nth n l d].
Lemma ind_from_end_helper : ∀ {X} (p : list X → Prop) (n : nat),
p [] →
(∀ (x : X) (l : list X), p l → p (l ++ [x])) →
∀ l, length l = n → p l.
Lemma ind_from_end : ∀ {X} (p : list X → Prop),
p [] →
(∀ (x : X) (l : list X), p l → p (l ++ [x])) →
∀ l, p l.
Definition Polynomial := list C.
Definition Peval (p : Polynomial) (x : Complex.C):=
big_sum (fun i ⇒ (nth i p C0)* x^i) (length p).
Definition Peq (p1 p2 : Polynomial) :=
Peval p1 = Peval p2.
Fixpoint Pplus (p1 p2 : Polynomial) : Polynomial :=
match p1 with
| [] ⇒ p2
| (a1 :: p1') ⇒
match p2 with
| [] ⇒ p1
| (a2 :: p2') ⇒ (a1 + a2) :: (Pplus p1' p2')
end
end.
Fixpoint Pmult (p1 p2 : Polynomial) : Polynomial :=
match p1 with
| [] ⇒ []
| (a1 :: p1') ⇒ Pplus (map (Cmult a1) p2) (C0 :: (Pmult p1' p2))
end.
Definition Popp (p : Polynomial) : Polynomial :=
Pmult [-C1] p.
Program Instance P_is_monoid : Monoid Polynomial :=
{ Gzero := []
; Gplus := Pplus
}.
Solve All Obligations with program_simpl; try lca.
Infix "≅" := Peq (at level 70) : poly_scope.
Infix "+," := Pplus (at level 50, left associativity) : poly_scope.
Infix "*," := Pmult (at level 40, left associativity) : poly_scope.
Notation "-, P" := (Popp P) (at level 30) : poly_scope.
Notation "P [[ x ]]" := (Peval P x) (at level 0) : poly_scope.
Lemma cons_eval : ∀ (p1 : Polynomial) (a c : C),
(a :: p1)[[c]] = a + c × (p1[[c]]).
Lemma Pplus_eval : ∀ (p1 p2 : Polynomial) (c : C),
(p1 +, p2)[[c]] = p1[[c]] + p2[[c]].
Lemma Pmult_eval : ∀ (p1 p2 : Polynomial) (c : C),
(p1 *, p2)[[c]] = p1[[c]] × p2[[c]].
Lemma Psum_eval : ∀ (f : nat → Polynomial) (n : nat) (c : C),
(big_sum f n)[[c]] = big_sum (fun i ⇒ (f i)[[c]]) n.
Lemma app_eval : ∀ (f g : Polynomial),
Peval (f ++ g) = (fun c ⇒ f [[ c ]] + ((repeat C0 (length f)) ++ g) [[ c ]]).
Lemma nth_repeat : ∀ {X} (x : X) (i n : nat),
(nth i (repeat x n) x) = x.
Lemma mul_by_x_to_n : ∀ (f : Polynomial) (n : nat) (c : C),
((repeat C0 n) ++ f)[[c]] = f[[c]] × c^n.
Lemma app_eval_to_mul : ∀ (f g : Polynomial) (c : C),
(f ++ g)[[c]] = f[[c]] + c^(length f) × g[[c]].
Lemma Peq_refl : ∀ (p : Polynomial), p ≅ p.
Lemma Peq_symm : ∀ (p1 p2 : Polynomial), p1 ≅ p2 → p2 ≅ p1.
Lemma Peq_trans : ∀ (p1 p2 p3 : Polynomial),
p1 ≅ p2 → p2 ≅ p3 → p1 ≅ p3.
Lemma Pplus_eq_compat : ∀ (p1 p1' p2 p2' : Polynomial),
p1 ≅ p1' → p2 ≅ p2' → p1 +, p2 ≅ p1' +, p2'.
Lemma Pmult_eq_compat : ∀ (p1 p1' p2 p2' : Polynomial),
p1 ≅ p1' → p2 ≅ p2' → p1 *, p2 ≅ p1' *, p2'.
Add Parametric Relation : Polynomial Peq
reflexivity proved by Peq_refl
symmetry proved by Peq_symm
transitivity proved by Peq_trans
as Peq_equiv_rel.
Add Parametric Morphism : Pplus
with signature Peq ==> Peq ==> Peq as Pplus_mor.
Add Parametric Morphism : Pmult
with signature Peq ==> Peq ==> Peq as Pmult_mor.
Add Parametric Morphism : cons
with signature eq ==> Peq ==> Peq as cons_mor.
Lemma Pplus_comm : ∀ (p1 p2 : Polynomial),
p1 +, p2 = p2 +, p1.
Lemma Pplus_assoc : ∀ (p1 p2 p3 : Polynomial),
(p1 +, p2) +, p3 = p1 +, (p2 +, p3).
Lemma Pplus_0_r : ∀ (p : Polynomial),
p +, [] = p.
Lemma C0_Peq_nil : [C0] ≅ [].
Lemma Pmult_0_r : ∀ (p : Polynomial),
p *, [] ≅ [].
Lemma Pscale_comm_nempty : ∀ (a : C) (p : Polynomial),
p ≠ [] → [a] *, p = p *, [a].
Lemma Pmult_comm_helper : ∀ (n : nat) (p1 p2 : Polynomial),
(length p1 + length p2 ≤ n)%nat →
p1 *, p2 ≅ p2 *, p1.
Lemma Pmult_comm : ∀ (p1 p2 : Polynomial),
p1 *, p2 ≅ p2 *, p1.
Lemma map_comm_distr_l : ∀ (p1 p2 : Polynomial) (c : C),
map (Cmult c) (p1 +, p2) = map (Cmult c) p1 +, map (Cmult c) p2.
Lemma Pmult_plus_distr_l : ∀ (p1 p2 p3 : Polynomial),
p1 *, (p2 +, p3) ≅ p1 *, p2 +, p1 *, p3.
Lemma Pmult_plus_distr_r : ∀ (p1 p2 p3 : Polynomial),
(p2 +, p3) *, p1 ≅ p2 *, p1 +, p3 *, p1.
Lemma cons_simplify : ∀ (p : Polynomial) (a : C),
(a :: p) = [a] +, (C0 :: p).
Lemma cons_0_mult : ∀ (p1 p2 : Polynomial),
(C0 :: p1) *, p2 ≅ C0 :: (p1 *, p2).
Lemma cons_singleton_mult : ∀ (p : Polynomial) (a : C),
[a] *, p ≅ map (Cmult a) p.
Lemma Pmult_assoc_singleton : ∀ (a1 : C) (p2 p3 : Polynomial),
([a1] *, p2) *, p3 ≅ [a1] *, (p2 *, p3).
Lemma Pmult_assoc : ∀ (p1 p2 p3 : Polynomial),
(p1 *, p2) *, p3 ≅ p1 *, (p2 *, p3).
Lemma map_1_id : ∀ (p : Polynomial),
map (Cmult C1) p = p.
Lemma Pmult_1_l : ∀ (p : Polynomial),
[C1] *, p ≅ p.
Lemma Pmult_1_r : ∀ (p : Polynomial),
p *, [C1] ≅ p.
Lemma Pplus_opp_r : ∀ (p : Polynomial),
p +, -,p ≅ [].
Lemma Pplus_opp_l : ∀ (p : Polynomial),
-,p +, p ≅ [].
Lemma head_0_Pmult_x : ∀ (p : Polynomial),
(C0 :: p) ≅ [C0; C1] *, p.
Definition limit_at_point (f : C → C) (a L : C) : Prop :=
∀ ϵ : R, ϵ > 0 → ∃ δ, (δ > 0 ∧ ∀ x, x ≠ a → Cmod (x - a) < δ → Cmod (f(x) - L) < ϵ).
Definition continuous_at (f : C → C) (a : C) : Prop :=
limit_at_point f a (f a).
Lemma limit_unique : ∀ (f : C → C) (a L1 L2 : C),
limit_at_point f a L1 → limit_at_point f a L2 →
L1 = L2.
Lemma limit_const : ∀ (a x : C),
limit_at_point (fun c ⇒ a) x a.
Lemma limit_const_poly : ∀ (a x : C),
limit_at_point (Peval [a]) x a.
Lemma limit_linear_poly : ∀ (a x : C),
limit_at_point (Peval [C0;a]) x (a × x).
Lemma limit_scale : ∀ (f : C → C) (a c L : C),
limit_at_point f a L →
limit_at_point (fun x ⇒ c × f x) a (c × L).
Lemma limit_plus : ∀ (f1 f2 : C → C) (a L1 L2 : C),
limit_at_point f1 a L1 → limit_at_point f2 a L2 →
limit_at_point (fun c ⇒ f1 c + f2 c) a (L1 + L2).
Lemma limit_mult_0 : ∀ (f1 f2 : C → C) (a : C),
limit_at_point f1 a C0 → limit_at_point f2 a C0 →
limit_at_point (fun c ⇒ f1 c × f2 c) a C0.
Lemma limit_mult : ∀ (f1 f2 : C → C) (a L1 L2 : C),
limit_at_point f1 a L1 → limit_at_point f2 a L2 →
limit_at_point (fun c ⇒ f1 c × f2 c) a (L1 × L2).
Lemma continuous_plus : ∀ (f1 f2 : C → C) (a : C),
continuous_at f1 a → continuous_at f2 a →
continuous_at (fun c ⇒ f1 c + f2 c) a.
Lemma continuous_mult : ∀ (f1 f2 : C → C) (a : C),
continuous_at f1 a → continuous_at f2 a →
continuous_at (fun c ⇒ f1 c × f2 c) a.
Lemma constant_continuous_poly : ∀ (c a : C),
continuous_at (Peval [c]) a.
Lemma linear_continuous_poly : ∀ (c a : C),
continuous_at (Peval [C0; c]) a.
Lemma power_x_eval : ∀ (n : nat) (a x : C),
(repeat C0 n ++ [a]) [[x]] = a × x^n.
Lemma power_x_mul_x : ∀ (n : nat) (a : C),
(repeat C0 (S n) ++ [a]) ≅ [C0; C1] *, (repeat C0 n ++ [a]).
Lemma continuous_power_x : ∀ (n : nat) (a b : C),
continuous_at (Peval ((repeat C0 n) ++ [b])) a.
Lemma polynomial_continuous : ∀ (p : Polynomial) (a : C),
(fun p ⇒ continuous_at (Peval p) a) p.
Lemma constant_ae_continuous : ∀ (f : C → C) (a c : C),
continuous_at f c → (∀ x, x ≠ c → f x = a) →
f c = a.
Lemma almost_0_implies_0 : ∀ (p : Polynomial),
(∀ c, c ≠ C0 → p[[c]] = C0) → p ≅ [].
Lemma almost_Peq_implies_Peq : ∀ (p1 p2 : Polynomial),
(∀ c, c ≠ C0 → p1[[c]] = p2[[c]]) → p1 ≅ p2.
Lemma Peq_head_eq : ∀ (p1 p2 : Polynomial) (a1 a2 : C),
(a1 :: p1) ≅ (a2 :: p2) → a1 = a2.
Lemma Peq_tail_Peq_helper : ∀ (p1 p2 : Polynomial),
(C0 :: p1) ≅ (C0 :: p2) → p1 ≅ p2.
Lemma Peq_tail_Peq : ∀ (p1 p2 : Polynomial) (a1 a2 : C),
(a1 :: p1) ≅ (a2 :: p2) → p1 ≅ p2.
Lemma Peq_app_Peq : ∀ (p p1 p2 : Polynomial),
(p ++ p1) ≅ (p ++ p2) → p1 ≅ p2.
Lemma Peq_length_eq_helper : ∀ (n : nat) (p1 p2 : Polynomial),
p1 ≅ p2 →
length p1 = n → length p2 = n →
p1 = p2.
Lemma Peq_length_eq : ∀ (n : nat) (p1 p2 : Polynomial),
p1 ≅ p2 → length p1 = length p2 →
p1 = p2.
Lemma Peq_nil_reduce : ∀ (p : Polynomial) (a : C),
(a :: p) ≅ [] → a = C0 ∧ p ≅ [].
Lemma Peq_nil_contains_C0 : ∀ (p : Polynomial),
p ≅ [] → (∀ c, In c p → c = C0).
Lemma same_elem_same_rev : ∀ (p : Polynomial),
(∀ c, In c p → c = C0) → p = repeat C0 (length p).
Lemma Peq_0_eq_repeat_0 : ∀ (p : Polynomial),
p ≅ [] → p = repeat C0 (length p).
Lemma Peq_nil_rev_Peq_nil : ∀ (p : Polynomial),
p ≅ [] → rev p = p.
Lemma last_C0_Peq_front : ∀ (p : Polynomial),
p ++ [C0] ≅ p.
Lemma repeat_C0_Peq_front : ∀ (n : nat) (p : Polynomial),
p ++ (repeat C0 n) ≅ p.
Lemma Peq_firstn_eq : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → (length p1 ≤ length p2)%nat →
p1 = firstn (length p1) p2.
Lemma Peq_skipn_Peq_nil : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → (length p1 ≤ length p2)%nat →
skipn (length p1) p2 ≅ [].
Local Open Scope nat_scope.
Fixpoint prune (p : Polynomial) : Polynomial :=
match p with
| [] ⇒ []
| (a :: p') ⇒
match (Ceq_dec a C0) with
| left _ ⇒ prune p'
| right _ ⇒ p
end
end.
Definition compactify (p : Polynomial) : Polynomial :=
rev (prune (rev p)).
Lemma prune_idempotent : ∀ (p : Polynomial),
prune (prune p) = prune p.
Lemma prune_length : ∀ (p : Polynomial),
length (prune p) ≤ length p.
Lemma compactify_length : ∀ (p : Polynomial),
length (compactify p) ≤ length p.
Lemma compactify_idempotent : ∀ (p : Polynomial),
compactify (compactify p) = compactify p.
Lemma prune_0_reduce : ∀ (p : Polynomial),
prune p = [] → prune (p ++ [C0]) = [].
Lemma Peq_0_prune_0 : ∀ (p : Polynomial),
p ≅ [] → prune p = [].
Lemma Peq_0_compactify_0 : ∀ (p : Polynomial),
p ≅ [] → compactify p = [].
Lemma app_C0_compactify_reduce : ∀ (n : nat) (p : Polynomial),
compactify (p ++ (repeat C0 n)) = compactify p.
Lemma app_C0_compactify_reduce_1 : ∀ (p : Polynomial),
compactify (p ++ [C0]) = compactify p.
Lemma app_nonzero_compactify_reduce : ∀ (p : Polynomial) (a : C),
a ≠ C0 → compactify (p ++ [a]) = p ++ [a].
Lemma Peq_compactify_eq_helper : ∀ (p1 p2 : Polynomial),
length p1 ≤ length p2 →
p1 ≅ p2 → compactify p1 = compactify p2.
Lemma Peq_compactify_eq : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → compactify p1 = compactify p2.
Add Parametric Morphism : compactify
with signature Peq ==> eq as compactify_mor.
Lemma p_Peq_compactify_p : ∀ (p : Polynomial),
(fun p0 ⇒ p0 ≅ compactify p0) p.
Lemma compactify_eq_Peq : ∀ (p1 p2 : Polynomial),
compactify p1 = compactify p2 → p1 ≅ p2.
Lemma Peq_0_dec : ∀ (p : Polynomial),
{ p ≅ [] } + { ~( p ≅ [] ) }.
Lemma Peq_dec : ∀ (p1 p2 : Polynomial),
{ p1 ≅ p2 } + { ~(p1 ≅ p2) }.
Lemma Pplus_length1 : ∀ (p1 p2 : Polynomial),
length (p1 +, p2) = max (length p1) (length p2).
Lemma Pplus_length2 : ∀ (p1 p2 : Polynomial),
length p1 ≤ length p2 →
length (p1 +, p2) = length p2.
Lemma Pplus_lt_app : ∀ (a : C) (p1 p2 : Polynomial),
length p1 ≤ length p2 →
p1 +, (p2 ++ [a]) = (p1 +, p2) ++ [a].
Lemma Pmult_leading_terms : ∀ (a1 a2 : C) (p1 p2 : Polynomial),
∃ p : Polynomial, (p1 ++ [a1]) *, (p2 ++ [a2]) = p ++ [(a1 × a2)%C] ∧
length p2 ≤ length p.
Lemma Pmult_length_le : ∀ (p1 p2 : Polynomial),
p2 ≠ [] →
length p1 ≤ length (p2 *, p1).
Lemma Pmult_length_helper : ∀ (n : nat) (a1 a2 : C) (p1 p2 : Polynomial),
length p1 ≤ n →
length ((a1 :: p1) *, (a2 :: p2)) = (length (a1 :: p1)) + (length (a2 :: p2)) - 1.
Lemma Pmult_length : ∀ (p1 p2 : Polynomial),
p1 ≠ [] → p2 ≠ [] →
length (p1 *, p2) = length p1 + length p2 - 1.
Lemma compactify_neq_nil : ∀ (a : C) (p : Polynomial),
a ≠ C0 → (fun p0 ⇒ compactify (a :: p0) ≠ []) p.
Lemma compactify_Pscale : ∀ (a b : C) (p : Polynomial),
a ≠ C0 → b ≠ C0 → (fun p0 ⇒ [a] *, compactify (b :: p0) = compactify ([a] *, (b :: p0))) p.
Lemma compactify_Pmult_helper : ∀ (a1 a2 : C) (p1 p2 : Polynomial),
a1 ≠ C0 → a2 ≠ C0 →
compactify (p1 ++ [a1]) *, compactify (p2 ++ [a2]) = compactify ((p1 ++ [a1]) *, (p2 ++ [a2])).
Lemma C0_end_breakdown : ∀ (p : Polynomial),
(fun p0 ⇒ Peval p0 ≠ Peval [] →
(∃ n a p', a ≠ C0 ∧ p0 = (p' ++ [a]) ++ (repeat C0 n))) p.
Lemma compactify_breakdown : ∀ (p : Polynomial),
Peval p ≠ Peval [] →
(∃ a p', a ≠ C0 ∧ compactify p = (p' ++ [a])).
Lemma compactify_Pmult : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
compactify p1 *, compactify p2 = compactify (p1 *, p2).
Definition degree (p : Polynomial) : nat :=
length (compactify p) - 1.
Add Parametric Morphism : degree
with signature Peq ==> eq as degree_mor.
Lemma length_compactify1 : ∀ (p1 p2 : Polynomial),
length (compactify (p1 +, p2)) ≤ length (compactify p1 +, compactify p2).
Lemma length_compactify2 : ∀ (p1 p2 : Polynomial),
(fun p ⇒
length (compactify p1) < length (compactify p) →
length (compactify (p1 +, p)) = length (compactify p)) p2.
Lemma Pplus_degree1 : ∀ (p1 p2 : Polynomial),
degree (p1 +, p2) ≤ max (degree p1) (degree p2).
Lemma Pplus_degree2 : ∀ (p1 p2 : Polynomial),
degree p1 < degree p2 →
degree (p1 +, p2) = degree p2.
Lemma Pmult_degree : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
degree (p1 *, p2) = (degree p1) + (degree p2).
Lemma Psum_degree : ∀ (f : nat → Polynomial) (n deg : nat),
(∀ i, i < n → degree (f i) ≤ deg) → degree (big_sum f n) ≤ deg.
Lemma Pmult_neq_0 : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
Peval (p1 *, p2) ≠ Peval [].
Fixpoint Ppow (p : Polynomial) (n : nat) :=
match n with
| 0 ⇒ [C1]
| S n' ⇒ (Ppow p n') *, p
end.
Add Parametric Morphism : Ppow
with signature Peq ==> eq ==> Peq as Ppow_mor.
Lemma Ppow_eval : ∀ (p : Polynomial) (n : nat) (a : C),
(Ppow p n)[[a]] = ((p[[a]])^n)%C.
Lemma Ppow_neq_0 : ∀ (p : Polynomial) (n : nat),
Peval p ≠ Peval [] →
Peval (Ppow p n) ≠ Peval [].
Lemma Ppow_degree : ∀ (p : Polynomial) (n : nat),
degree (Ppow p n) = n × (degree p).
Definition poly_shift (p : Polynomial) (m : C) : Polynomial :=
big_sum (fun i ⇒ [nth i p C0] *, (Ppow [-m; C1] i)) (length p).
Lemma poly_shift_ver : ∀ (p : Polynomial) (m c : C),
p[[c - m]] = (poly_shift p m)[[c]].
Add Parametric Morphism : poly_shift
with signature Peq ==> eq ==> Peq as polyshift_mor.
Lemma poly_shift_const : ∀ (a m : C),
[a] ≅ (poly_shift [a] m).
Lemma poly_shift_degree : ∀ (p : Polynomial) (m : C),
degree p = degree (poly_shift p m).
Local Close Scope nat_scope.
Lemma discriminant_pos_Peval_pos : ∀ (a b c : R),
a > 0 →
(∀ t, 0 ≤ fst (Peval [(c,0); (b,0); (a,0)] (t, 0))) ↔ 0 ≤ 4×a×c - b^2.
Require Import String.
Require Export Complex.
Require Import List.
Require Import Setoid.
Declare Scope poly_scope.
Delimit Scope poly_scope with P.
Open Scope poly_scope.
Lemma diff_pow_n : ∀ (n : nat) (a b : C),
(a^(S n) - b^(S n)) = (a - b) × (big_sum (fun i ⇒ a^i × b^(n - i)) (S n)).
Lemma destruct_from_last : ∀ {X} (n : nat) (d : X) (l : list X),
length l = S n → l = (firstn n l) ++ [nth n l d].
Lemma ind_from_end_helper : ∀ {X} (p : list X → Prop) (n : nat),
p [] →
(∀ (x : X) (l : list X), p l → p (l ++ [x])) →
∀ l, length l = n → p l.
Lemma ind_from_end : ∀ {X} (p : list X → Prop),
p [] →
(∀ (x : X) (l : list X), p l → p (l ++ [x])) →
∀ l, p l.
Definition Polynomial := list C.
Definition Peval (p : Polynomial) (x : Complex.C):=
big_sum (fun i ⇒ (nth i p C0)* x^i) (length p).
Definition Peq (p1 p2 : Polynomial) :=
Peval p1 = Peval p2.
Fixpoint Pplus (p1 p2 : Polynomial) : Polynomial :=
match p1 with
| [] ⇒ p2
| (a1 :: p1') ⇒
match p2 with
| [] ⇒ p1
| (a2 :: p2') ⇒ (a1 + a2) :: (Pplus p1' p2')
end
end.
Fixpoint Pmult (p1 p2 : Polynomial) : Polynomial :=
match p1 with
| [] ⇒ []
| (a1 :: p1') ⇒ Pplus (map (Cmult a1) p2) (C0 :: (Pmult p1' p2))
end.
Definition Popp (p : Polynomial) : Polynomial :=
Pmult [-C1] p.
Program Instance P_is_monoid : Monoid Polynomial :=
{ Gzero := []
; Gplus := Pplus
}.
Solve All Obligations with program_simpl; try lca.
Infix "≅" := Peq (at level 70) : poly_scope.
Infix "+," := Pplus (at level 50, left associativity) : poly_scope.
Infix "*," := Pmult (at level 40, left associativity) : poly_scope.
Notation "-, P" := (Popp P) (at level 30) : poly_scope.
Notation "P [[ x ]]" := (Peval P x) (at level 0) : poly_scope.
Lemma cons_eval : ∀ (p1 : Polynomial) (a c : C),
(a :: p1)[[c]] = a + c × (p1[[c]]).
Lemma Pplus_eval : ∀ (p1 p2 : Polynomial) (c : C),
(p1 +, p2)[[c]] = p1[[c]] + p2[[c]].
Lemma Pmult_eval : ∀ (p1 p2 : Polynomial) (c : C),
(p1 *, p2)[[c]] = p1[[c]] × p2[[c]].
Lemma Psum_eval : ∀ (f : nat → Polynomial) (n : nat) (c : C),
(big_sum f n)[[c]] = big_sum (fun i ⇒ (f i)[[c]]) n.
Lemma app_eval : ∀ (f g : Polynomial),
Peval (f ++ g) = (fun c ⇒ f [[ c ]] + ((repeat C0 (length f)) ++ g) [[ c ]]).
Lemma nth_repeat : ∀ {X} (x : X) (i n : nat),
(nth i (repeat x n) x) = x.
Lemma mul_by_x_to_n : ∀ (f : Polynomial) (n : nat) (c : C),
((repeat C0 n) ++ f)[[c]] = f[[c]] × c^n.
Lemma app_eval_to_mul : ∀ (f g : Polynomial) (c : C),
(f ++ g)[[c]] = f[[c]] + c^(length f) × g[[c]].
Lemma Peq_refl : ∀ (p : Polynomial), p ≅ p.
Lemma Peq_symm : ∀ (p1 p2 : Polynomial), p1 ≅ p2 → p2 ≅ p1.
Lemma Peq_trans : ∀ (p1 p2 p3 : Polynomial),
p1 ≅ p2 → p2 ≅ p3 → p1 ≅ p3.
Lemma Pplus_eq_compat : ∀ (p1 p1' p2 p2' : Polynomial),
p1 ≅ p1' → p2 ≅ p2' → p1 +, p2 ≅ p1' +, p2'.
Lemma Pmult_eq_compat : ∀ (p1 p1' p2 p2' : Polynomial),
p1 ≅ p1' → p2 ≅ p2' → p1 *, p2 ≅ p1' *, p2'.
Add Parametric Relation : Polynomial Peq
reflexivity proved by Peq_refl
symmetry proved by Peq_symm
transitivity proved by Peq_trans
as Peq_equiv_rel.
Add Parametric Morphism : Pplus
with signature Peq ==> Peq ==> Peq as Pplus_mor.
Add Parametric Morphism : Pmult
with signature Peq ==> Peq ==> Peq as Pmult_mor.
Add Parametric Morphism : cons
with signature eq ==> Peq ==> Peq as cons_mor.
Lemma Pplus_comm : ∀ (p1 p2 : Polynomial),
p1 +, p2 = p2 +, p1.
Lemma Pplus_assoc : ∀ (p1 p2 p3 : Polynomial),
(p1 +, p2) +, p3 = p1 +, (p2 +, p3).
Lemma Pplus_0_r : ∀ (p : Polynomial),
p +, [] = p.
Lemma C0_Peq_nil : [C0] ≅ [].
Lemma Pmult_0_r : ∀ (p : Polynomial),
p *, [] ≅ [].
Lemma Pscale_comm_nempty : ∀ (a : C) (p : Polynomial),
p ≠ [] → [a] *, p = p *, [a].
Lemma Pmult_comm_helper : ∀ (n : nat) (p1 p2 : Polynomial),
(length p1 + length p2 ≤ n)%nat →
p1 *, p2 ≅ p2 *, p1.
Lemma Pmult_comm : ∀ (p1 p2 : Polynomial),
p1 *, p2 ≅ p2 *, p1.
Lemma map_comm_distr_l : ∀ (p1 p2 : Polynomial) (c : C),
map (Cmult c) (p1 +, p2) = map (Cmult c) p1 +, map (Cmult c) p2.
Lemma Pmult_plus_distr_l : ∀ (p1 p2 p3 : Polynomial),
p1 *, (p2 +, p3) ≅ p1 *, p2 +, p1 *, p3.
Lemma Pmult_plus_distr_r : ∀ (p1 p2 p3 : Polynomial),
(p2 +, p3) *, p1 ≅ p2 *, p1 +, p3 *, p1.
Lemma cons_simplify : ∀ (p : Polynomial) (a : C),
(a :: p) = [a] +, (C0 :: p).
Lemma cons_0_mult : ∀ (p1 p2 : Polynomial),
(C0 :: p1) *, p2 ≅ C0 :: (p1 *, p2).
Lemma cons_singleton_mult : ∀ (p : Polynomial) (a : C),
[a] *, p ≅ map (Cmult a) p.
Lemma Pmult_assoc_singleton : ∀ (a1 : C) (p2 p3 : Polynomial),
([a1] *, p2) *, p3 ≅ [a1] *, (p2 *, p3).
Lemma Pmult_assoc : ∀ (p1 p2 p3 : Polynomial),
(p1 *, p2) *, p3 ≅ p1 *, (p2 *, p3).
Lemma map_1_id : ∀ (p : Polynomial),
map (Cmult C1) p = p.
Lemma Pmult_1_l : ∀ (p : Polynomial),
[C1] *, p ≅ p.
Lemma Pmult_1_r : ∀ (p : Polynomial),
p *, [C1] ≅ p.
Lemma Pplus_opp_r : ∀ (p : Polynomial),
p +, -,p ≅ [].
Lemma Pplus_opp_l : ∀ (p : Polynomial),
-,p +, p ≅ [].
Lemma head_0_Pmult_x : ∀ (p : Polynomial),
(C0 :: p) ≅ [C0; C1] *, p.
Definition limit_at_point (f : C → C) (a L : C) : Prop :=
∀ ϵ : R, ϵ > 0 → ∃ δ, (δ > 0 ∧ ∀ x, x ≠ a → Cmod (x - a) < δ → Cmod (f(x) - L) < ϵ).
Definition continuous_at (f : C → C) (a : C) : Prop :=
limit_at_point f a (f a).
Lemma limit_unique : ∀ (f : C → C) (a L1 L2 : C),
limit_at_point f a L1 → limit_at_point f a L2 →
L1 = L2.
Lemma limit_const : ∀ (a x : C),
limit_at_point (fun c ⇒ a) x a.
Lemma limit_const_poly : ∀ (a x : C),
limit_at_point (Peval [a]) x a.
Lemma limit_linear_poly : ∀ (a x : C),
limit_at_point (Peval [C0;a]) x (a × x).
Lemma limit_scale : ∀ (f : C → C) (a c L : C),
limit_at_point f a L →
limit_at_point (fun x ⇒ c × f x) a (c × L).
Lemma limit_plus : ∀ (f1 f2 : C → C) (a L1 L2 : C),
limit_at_point f1 a L1 → limit_at_point f2 a L2 →
limit_at_point (fun c ⇒ f1 c + f2 c) a (L1 + L2).
Lemma limit_mult_0 : ∀ (f1 f2 : C → C) (a : C),
limit_at_point f1 a C0 → limit_at_point f2 a C0 →
limit_at_point (fun c ⇒ f1 c × f2 c) a C0.
Lemma limit_mult : ∀ (f1 f2 : C → C) (a L1 L2 : C),
limit_at_point f1 a L1 → limit_at_point f2 a L2 →
limit_at_point (fun c ⇒ f1 c × f2 c) a (L1 × L2).
Lemma continuous_plus : ∀ (f1 f2 : C → C) (a : C),
continuous_at f1 a → continuous_at f2 a →
continuous_at (fun c ⇒ f1 c + f2 c) a.
Lemma continuous_mult : ∀ (f1 f2 : C → C) (a : C),
continuous_at f1 a → continuous_at f2 a →
continuous_at (fun c ⇒ f1 c × f2 c) a.
Lemma constant_continuous_poly : ∀ (c a : C),
continuous_at (Peval [c]) a.
Lemma linear_continuous_poly : ∀ (c a : C),
continuous_at (Peval [C0; c]) a.
Lemma power_x_eval : ∀ (n : nat) (a x : C),
(repeat C0 n ++ [a]) [[x]] = a × x^n.
Lemma power_x_mul_x : ∀ (n : nat) (a : C),
(repeat C0 (S n) ++ [a]) ≅ [C0; C1] *, (repeat C0 n ++ [a]).
Lemma continuous_power_x : ∀ (n : nat) (a b : C),
continuous_at (Peval ((repeat C0 n) ++ [b])) a.
Lemma polynomial_continuous : ∀ (p : Polynomial) (a : C),
(fun p ⇒ continuous_at (Peval p) a) p.
Lemma constant_ae_continuous : ∀ (f : C → C) (a c : C),
continuous_at f c → (∀ x, x ≠ c → f x = a) →
f c = a.
Lemma almost_0_implies_0 : ∀ (p : Polynomial),
(∀ c, c ≠ C0 → p[[c]] = C0) → p ≅ [].
Lemma almost_Peq_implies_Peq : ∀ (p1 p2 : Polynomial),
(∀ c, c ≠ C0 → p1[[c]] = p2[[c]]) → p1 ≅ p2.
Lemma Peq_head_eq : ∀ (p1 p2 : Polynomial) (a1 a2 : C),
(a1 :: p1) ≅ (a2 :: p2) → a1 = a2.
Lemma Peq_tail_Peq_helper : ∀ (p1 p2 : Polynomial),
(C0 :: p1) ≅ (C0 :: p2) → p1 ≅ p2.
Lemma Peq_tail_Peq : ∀ (p1 p2 : Polynomial) (a1 a2 : C),
(a1 :: p1) ≅ (a2 :: p2) → p1 ≅ p2.
Lemma Peq_app_Peq : ∀ (p p1 p2 : Polynomial),
(p ++ p1) ≅ (p ++ p2) → p1 ≅ p2.
Lemma Peq_length_eq_helper : ∀ (n : nat) (p1 p2 : Polynomial),
p1 ≅ p2 →
length p1 = n → length p2 = n →
p1 = p2.
Lemma Peq_length_eq : ∀ (n : nat) (p1 p2 : Polynomial),
p1 ≅ p2 → length p1 = length p2 →
p1 = p2.
Lemma Peq_nil_reduce : ∀ (p : Polynomial) (a : C),
(a :: p) ≅ [] → a = C0 ∧ p ≅ [].
Lemma Peq_nil_contains_C0 : ∀ (p : Polynomial),
p ≅ [] → (∀ c, In c p → c = C0).
Lemma same_elem_same_rev : ∀ (p : Polynomial),
(∀ c, In c p → c = C0) → p = repeat C0 (length p).
Lemma Peq_0_eq_repeat_0 : ∀ (p : Polynomial),
p ≅ [] → p = repeat C0 (length p).
Lemma Peq_nil_rev_Peq_nil : ∀ (p : Polynomial),
p ≅ [] → rev p = p.
Lemma last_C0_Peq_front : ∀ (p : Polynomial),
p ++ [C0] ≅ p.
Lemma repeat_C0_Peq_front : ∀ (n : nat) (p : Polynomial),
p ++ (repeat C0 n) ≅ p.
Lemma Peq_firstn_eq : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → (length p1 ≤ length p2)%nat →
p1 = firstn (length p1) p2.
Lemma Peq_skipn_Peq_nil : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → (length p1 ≤ length p2)%nat →
skipn (length p1) p2 ≅ [].
Local Open Scope nat_scope.
Fixpoint prune (p : Polynomial) : Polynomial :=
match p with
| [] ⇒ []
| (a :: p') ⇒
match (Ceq_dec a C0) with
| left _ ⇒ prune p'
| right _ ⇒ p
end
end.
Definition compactify (p : Polynomial) : Polynomial :=
rev (prune (rev p)).
Lemma prune_idempotent : ∀ (p : Polynomial),
prune (prune p) = prune p.
Lemma prune_length : ∀ (p : Polynomial),
length (prune p) ≤ length p.
Lemma compactify_length : ∀ (p : Polynomial),
length (compactify p) ≤ length p.
Lemma compactify_idempotent : ∀ (p : Polynomial),
compactify (compactify p) = compactify p.
Lemma prune_0_reduce : ∀ (p : Polynomial),
prune p = [] → prune (p ++ [C0]) = [].
Lemma Peq_0_prune_0 : ∀ (p : Polynomial),
p ≅ [] → prune p = [].
Lemma Peq_0_compactify_0 : ∀ (p : Polynomial),
p ≅ [] → compactify p = [].
Lemma app_C0_compactify_reduce : ∀ (n : nat) (p : Polynomial),
compactify (p ++ (repeat C0 n)) = compactify p.
Lemma app_C0_compactify_reduce_1 : ∀ (p : Polynomial),
compactify (p ++ [C0]) = compactify p.
Lemma app_nonzero_compactify_reduce : ∀ (p : Polynomial) (a : C),
a ≠ C0 → compactify (p ++ [a]) = p ++ [a].
Lemma Peq_compactify_eq_helper : ∀ (p1 p2 : Polynomial),
length p1 ≤ length p2 →
p1 ≅ p2 → compactify p1 = compactify p2.
Lemma Peq_compactify_eq : ∀ (p1 p2 : Polynomial),
p1 ≅ p2 → compactify p1 = compactify p2.
Add Parametric Morphism : compactify
with signature Peq ==> eq as compactify_mor.
Lemma p_Peq_compactify_p : ∀ (p : Polynomial),
(fun p0 ⇒ p0 ≅ compactify p0) p.
Lemma compactify_eq_Peq : ∀ (p1 p2 : Polynomial),
compactify p1 = compactify p2 → p1 ≅ p2.
Lemma Peq_0_dec : ∀ (p : Polynomial),
{ p ≅ [] } + { ~( p ≅ [] ) }.
Lemma Peq_dec : ∀ (p1 p2 : Polynomial),
{ p1 ≅ p2 } + { ~(p1 ≅ p2) }.
Lemma Pplus_length1 : ∀ (p1 p2 : Polynomial),
length (p1 +, p2) = max (length p1) (length p2).
Lemma Pplus_length2 : ∀ (p1 p2 : Polynomial),
length p1 ≤ length p2 →
length (p1 +, p2) = length p2.
Lemma Pplus_lt_app : ∀ (a : C) (p1 p2 : Polynomial),
length p1 ≤ length p2 →
p1 +, (p2 ++ [a]) = (p1 +, p2) ++ [a].
Lemma Pmult_leading_terms : ∀ (a1 a2 : C) (p1 p2 : Polynomial),
∃ p : Polynomial, (p1 ++ [a1]) *, (p2 ++ [a2]) = p ++ [(a1 × a2)%C] ∧
length p2 ≤ length p.
Lemma Pmult_length_le : ∀ (p1 p2 : Polynomial),
p2 ≠ [] →
length p1 ≤ length (p2 *, p1).
Lemma Pmult_length_helper : ∀ (n : nat) (a1 a2 : C) (p1 p2 : Polynomial),
length p1 ≤ n →
length ((a1 :: p1) *, (a2 :: p2)) = (length (a1 :: p1)) + (length (a2 :: p2)) - 1.
Lemma Pmult_length : ∀ (p1 p2 : Polynomial),
p1 ≠ [] → p2 ≠ [] →
length (p1 *, p2) = length p1 + length p2 - 1.
Lemma compactify_neq_nil : ∀ (a : C) (p : Polynomial),
a ≠ C0 → (fun p0 ⇒ compactify (a :: p0) ≠ []) p.
Lemma compactify_Pscale : ∀ (a b : C) (p : Polynomial),
a ≠ C0 → b ≠ C0 → (fun p0 ⇒ [a] *, compactify (b :: p0) = compactify ([a] *, (b :: p0))) p.
Lemma compactify_Pmult_helper : ∀ (a1 a2 : C) (p1 p2 : Polynomial),
a1 ≠ C0 → a2 ≠ C0 →
compactify (p1 ++ [a1]) *, compactify (p2 ++ [a2]) = compactify ((p1 ++ [a1]) *, (p2 ++ [a2])).
Lemma C0_end_breakdown : ∀ (p : Polynomial),
(fun p0 ⇒ Peval p0 ≠ Peval [] →
(∃ n a p', a ≠ C0 ∧ p0 = (p' ++ [a]) ++ (repeat C0 n))) p.
Lemma compactify_breakdown : ∀ (p : Polynomial),
Peval p ≠ Peval [] →
(∃ a p', a ≠ C0 ∧ compactify p = (p' ++ [a])).
Lemma compactify_Pmult : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
compactify p1 *, compactify p2 = compactify (p1 *, p2).
Definition degree (p : Polynomial) : nat :=
length (compactify p) - 1.
Add Parametric Morphism : degree
with signature Peq ==> eq as degree_mor.
Lemma length_compactify1 : ∀ (p1 p2 : Polynomial),
length (compactify (p1 +, p2)) ≤ length (compactify p1 +, compactify p2).
Lemma length_compactify2 : ∀ (p1 p2 : Polynomial),
(fun p ⇒
length (compactify p1) < length (compactify p) →
length (compactify (p1 +, p)) = length (compactify p)) p2.
Lemma Pplus_degree1 : ∀ (p1 p2 : Polynomial),
degree (p1 +, p2) ≤ max (degree p1) (degree p2).
Lemma Pplus_degree2 : ∀ (p1 p2 : Polynomial),
degree p1 < degree p2 →
degree (p1 +, p2) = degree p2.
Lemma Pmult_degree : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
degree (p1 *, p2) = (degree p1) + (degree p2).
Lemma Psum_degree : ∀ (f : nat → Polynomial) (n deg : nat),
(∀ i, i < n → degree (f i) ≤ deg) → degree (big_sum f n) ≤ deg.
Lemma Pmult_neq_0 : ∀ (p1 p2 : Polynomial),
Peval p1 ≠ Peval [] → Peval p2 ≠ Peval [] →
Peval (p1 *, p2) ≠ Peval [].
Fixpoint Ppow (p : Polynomial) (n : nat) :=
match n with
| 0 ⇒ [C1]
| S n' ⇒ (Ppow p n') *, p
end.
Add Parametric Morphism : Ppow
with signature Peq ==> eq ==> Peq as Ppow_mor.
Lemma Ppow_eval : ∀ (p : Polynomial) (n : nat) (a : C),
(Ppow p n)[[a]] = ((p[[a]])^n)%C.
Lemma Ppow_neq_0 : ∀ (p : Polynomial) (n : nat),
Peval p ≠ Peval [] →
Peval (Ppow p n) ≠ Peval [].
Lemma Ppow_degree : ∀ (p : Polynomial) (n : nat),
degree (Ppow p n) = n × (degree p).
Definition poly_shift (p : Polynomial) (m : C) : Polynomial :=
big_sum (fun i ⇒ [nth i p C0] *, (Ppow [-m; C1] i)) (length p).
Lemma poly_shift_ver : ∀ (p : Polynomial) (m c : C),
p[[c - m]] = (poly_shift p m)[[c]].
Add Parametric Morphism : poly_shift
with signature Peq ==> eq ==> Peq as polyshift_mor.
Lemma poly_shift_const : ∀ (a m : C),
[a] ≅ (poly_shift [a] m).
Lemma poly_shift_degree : ∀ (p : Polynomial) (m : C),
degree p = degree (poly_shift p m).
Local Close Scope nat_scope.
Lemma discriminant_pos_Peval_pos : ∀ (a b c : R),
a > 0 →
(∀ t, 0 ≤ fst (Peval [(c,0); (b,0); (a,0)] (t, 0))) ↔ 0 ≤ 4×a×c - b^2.