proposition: Lemma RTautoChecker_sound (ff : BFormula (RFormula R) isProp) (f : BFormula (Formula Z) isProp) (w : seq (Psatz Z)) (env : PolEnv R) : (forall R_of_Z opp add sub mul exp eqProp eqBool le lt, let norm_ff := Rnorm_formula R_of_Z opp add sub mul exp eqProp eqBool le lt in let eval_f := Reval_PFormula R_of_Z opp add sub mul exp eqProp eqBool le lt env in eval_bf norm_ff ff = eval_bf eval_f f) -> ZTautoChecker f w -> eval_bf (Reval_formula eq eq_op <=%O <%O) ff.
proof: Proof. rewrite (Rnorm_bf_correct erefl erefl erefl erefl erefl erefl). move=> /(_ _ _ _ (fun x y => x - y)) -> Hchecker. move: Hchecker env; apply: (tauto_checker_sound _ _ _ _ Reval_nformula). - exact: (eval_nformula_dec Rsor). - by move=> [? ?] ? ?; apply: (check_inconsistent_sound Rsor RSORaddon). - move=> t t' u deducett'u env evalt evalt'. exact: (nformula_plus_nformula_correct Rsor RSORaddon env t t'). - move=> env k t tg cnfff; rewrite Reval_formula_compat //. exact: (cnf_normalise_correct Rsor RSORaddon env t tg).1. - move=> env k t tg cnfff; rewrite hold_eNOT Reval_formula_compat //. exact: (cnf_negate_correct Rsor RSORaddon env t tg).1. - move=> t w0 checkw0 env; rewrite (Refl.make_impl_map (Reval_nformula env)) //. exact: (checker_nf_sound Rsor RSORaddon) checkw0 env. Qed.
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)