proposition: Lemma FTautoChecker_sound (ff : BFormula (RFormula F) isProp) (f : BFormula (Formula Q) isProp) (w : seq (Psatz Q)) (env : PolEnv F) : (forall F_of_Q opp add sub mul exp eqProp eqBool le lt, let norm_ff := Fnorm_formula F_of_Q opp add sub mul exp eqProp eqBool le lt in let eval_f := Feval_PFormula F_of_Q opp add sub mul exp eqProp eqBool le lt env in eval_bf norm_ff ff = eval_bf eval_f f) -> QTautoChecker f w -> eval_bf (Reval_formula eq eq_op <=%O <%O) ff.
proof: Proof. rewrite (Fnorm_bf_correct erefl erefl erefl erefl erefl erefl). move/(_ R_of_Q) => -> Hchecker. move: Hchecker env; apply: (tauto_checker_sound _ _ _ _ Feval_nformula). - exact: (eval_nformula_dec Rsor). - by move=> [? ?] ? ?; apply: (check_inconsistent_sound Rsor FSORaddon). - move=> t t' u deducett'u env evalt evalt'. exact: (nformula_plus_nformula_correct Rsor FSORaddon env t t'). - move=> env k t tg cnfff; rewrite Feval_formula_compat //. exact: (cnf_normalise_correct Rsor FSORaddon env t tg).1. - move=> env k t tg cnfff; rewrite hold_eNOT Feval_formula_compat //. exact: (cnf_negate_correct Rsor FSORaddon env t tg).1. - move=> t w0 checkw0 env; rewrite (Refl.make_impl_map (Feval_nformula env)) //. exact: (checker_nf_sound Rsor FSORaddon) 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)