proposition: Theorem reduce_eval : forall {n} {b} (p : poly b n) (v : Vector.t bool n), eval p (Vector.map (fun x : bool => if x then 1%Z else 0%Z) v) = eval (reduce p).2 (Vector.map (fun x : bool => if x then 1%Z else 0%Z) v).
proof: Proof. Ltac YY := autorewrite with reduce reduce_aux eval; auto. depind p; intros; depelim v; YY. - rewrite IHp1, (IHp2 (Vector.cons h v)). remember (reduce p2) as P. destruct P as [bP P]. simpl. depelim P; simpl; YY. destruct h; nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef