proposition: Lemma mult_eval : forall {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 n) v, (eval p1 v * eval p2 v)%Z = eval (mult p1 p2).2 v.
proof: Proof. Proof with (autorewrite with mult mult_l mult_s eval; auto with zarith). Ltac Y := (autorewrite with mult mult_l mult_s eval; auto with zarith). depind p1; try (depind p2; intros; depelim v; Y; simpl; Y; fail). depind p2; intros; depelim v; Y; simpl; Y; destruct (z * z0)%Z; simpl... - assert (mult_l_eval : forall {b2} (q : poly b2 (S n)) v h, eval (mult_l q (@mult _ _ p1)).2 (Vector.cons h v) = (eval q (Vector.cons h v) * eval p1 v)%Z). + depind q; intros; Y; rewrite <- IHp1... rewrite IHq2; auto; nia. + intros; depelim v; Y; simpl; Y; rewrite mult_l_eval... - assert (mult_s_eval : forall {b2} (q : poly b2 (S n)) v h, let mp := mult_s q (@mult _ _ p1_1) (@mult _ _ p1_2) in eval mp.2 (Vector.cons h v) = (eval q (Vector.cons h v) * (eval p1_1 v + h * eval p1_2 (Vector.cons h v)))%Z). + depind q; intros; Y; simpl; Y. rewrite <- IHp1_1, <- IHp1_2; Y; nia. rewrite <- IHp1_1. rewrite IHq2, <- IHp1_2; auto; Y; nia. + intros; depelim v; Y; simpl; Y; rewrite mult_s_eval... Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef