proposition: Lemma xnnormalise_correct : forall env f, eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.
proof: Proof. intros env f. rewrite Zeval_formula_compat'. unfold xnnormalise. destruct f as [lhs o rhs]. destruct o eqn:O ; cbn ; rewrite ?eval_pol_sub; rewrite <- !eval_pol_norm ; simpl in *; unfold eval_expr; generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env lhs); generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0. - split ; intros. + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence. rewrite Z.add_0_r in H0. rewrite <- H0. ring. + subst. ring. - split ; intros H H0. + subst. apply H. ring. + apply H. assert (z0 + (z - z0) = z0 + 0) as H1 by congruence. rewrite Z.add_0_r in H1. rewrite <- H1. ring. - split ; intros. + apply Zle_0_minus_le; auto. + apply Zle_minus_le_0; auto. - split ; intros. + apply Zle_0_minus_le; auto. + apply Zle_minus_le_0; auto. - split ; intros H. + apply Zlt_0_minus_lt; auto. + apply Zlt_left_lt in H. apply H. - split ; intros H. + apply Zlt_0_minus_lt ; auto. + apply Zlt_left_lt in H. apply H. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing