eval_mul' vs : forall P Q, eval vs (mul P Q) = eval vs P * eval vs Q. Proof. induction P as [c | P1 IHP1 v P2 IHP2];[apply eval_mulC|]. destruct Q as [d | Q1 w Q2]. - change (mul (PX P1 v P2) (Pconst d)) with (mulC d (PX P1 v P2)). rewrite eval_mulC. apply mult_comm. - simpl. rewrite plus_mult_distr_r,!plus_mult_distr_l. repeat (rewrite eval_add || rewrite eval_mulX). rewrite plus_mult_distr_r,(plus_mult_distr_l (eval vs P2)). rewrite IHP1,IHP2. apply ap011;apply ap011. + rewrite <-!mult_assoc. apply ap. rewrite (mult_comm (vs v)). apply mult_assoc. + rewrite <-mult_assoc,(mult_comm (vs v)),mult_assoc. rewrite IHP1;reflexivity. + symmetry;apply mult_assoc. + auto. Qed.
Require Import Import Quoting.