proposition: Lemma correctness_classical : forall {n} (f1 f2 : @formula (Fin.t n)), reduce (poly_of_formula f1).2 = reduce (poly_of_formula f2).2 <-> forall v, eval_formula (Vector.nth v) f1 = eval_formula (Vector.nth v) f2.
proof: Proof. intros n f1 f2; split. - intros H v. assert (H1 := poly_of_formula_eval f1 v); assert (H2 := poly_of_formula_eval f2 v). rewrite reduce_eval in H1; rewrite reduce_eval in H2. remember (eval_formula (Vector.nth v) f1) as b1; remember (eval_formula (Vector.nth v) f2) as b2. rewrite H in H1; rewrite <- H1 in H2. destruct b1; destruct b2; simpl in *; (discriminate || auto). - intros. assert ((plus (reduce (poly_of_formula f1).2).2 (poly_neg (reduce (poly_of_formula f2).2).2)).1 = true). + apply red_ok with (p := (plus (reduce (poly_of_formula f1).2).2 (poly_neg (reduce (poly_of_formula f2).2).2)).2). * auto using is_reduced_compat_plus, is_reduced_ok, is_reduced_compat_neg. * intro; autorewrite with eval. assert (H1 := poly_of_formula_eval f1 v); assert (H2 := poly_of_formula_eval f2 v). rewrite <- !reduce_eval, <- H1, <- H2, (H v); nia. + apply poly_diff_z_eq in H0. remember (reduce (poly_of_formula f1).2) as P1; destruct P1 as [bP1 P1]. remember (reduce (poly_of_formula f2).2) as P2; destruct P2 as [bP2 P2]. destruct bP1; destruct bP2; auto; simpl in H0; depelim H0; auto. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef