proposition: Lemma poly_of_formula_eval_compat : forall var f, eval var (poly_of_formula f) = formula_eval var f.
proof: Proof. intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. - now simpl; match goal with [ |- ?t = ?u ] => destruct u; reflexivity end. - rewrite poly_mul_compat, IHf1, IHf2; ring. - repeat rewrite poly_add_compat. rewrite poly_mul_compat; try_rewrite. now match goal with [ |- ?t = ?x || ?y ] => destruct x; destruct y; reflexivity end. - rewrite poly_add_compat; try_rewrite. now match goal with [ |- ?t = negb ?x ] => destruct x; reflexivity end. - rewrite poly_add_compat; congruence. - rewrite ?poly_add_compat, ?poly_mul_compat; try_rewrite. match goal with [ |- ?t = if ?b1 then ?b2 else ?b3 ] => destruct b1; destruct b2; destruct b3; reflexivity end. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia