proposition: Theorem poly_of_formula_eval : forall {n} (f : @formula (Fin.t n)) (v : Vector.t bool n), (if eval_formula (Vector.nth v) f then 1%Z else 0%Z) = eval (poly_of_formula f).2 (Vector.map (fun x : bool => if x then 1%Z else 0%Z) v).
proof: Proof. intros. funelim (poly_of_formula f); intros; autorewrite with eval_formula poly_of_formula eval in *; trivial. - erewrite Vector.nth_map; auto. - rewrite <- H, <- H0; destruct (eval_formula (Vector.nth v) a); destruct (eval_formula (Vector.nth v) b); auto. - rewrite <- H, <- H0; destruct (eval_formula (Vector.nth v) a); destruct (eval_formula (Vector.nth v) b); auto. - rewrite <- H; destruct (eval_formula (Vector.nth v) a); auto. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef