proposition: Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_bf (Reval_formula env) f.
proof: Proof. intros f w. unfold RTautoChecker. intros TC env. apply tauto_checker_sound with (eval:=QReval_formula) (eval':= Qeval_nformula) (env := env) in TC. - change (eval_f e_rtyp (QReval_formula env)) with (eval_bf (QReval_formula env)) in TC. rewrite eval_bf_map in TC. unfold eval_bf in TC. rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto. intros. apply Tauto.hold_eiff. rewrite QReval_formula_compat. unfold QReval_formula'. rewrite <- eval_formulaSC with (phiS := R_of_Rcst). + rewrite Reval_formula_compat. tauto. + intro. rewrite Q_of_RcstR. reflexivity. - apply Reval_nformula_dec. - destruct t. apply (check_inconsistent_sound Rsor QSORaddon) ; auto. - unfold rdeduce. intros. revert H. eapply (nformula_plus_nformula_correct Rsor QSORaddon); eauto. - intros. rewrite QReval_formula_compat. eapply (cnf_normalise_correct Rsor QSORaddon) ; eauto. - intros. rewrite Tauto.hold_eNOT. rewrite QReval_formula_compat. now eapply (cnf_negate_correct Rsor QSORaddon); eauto. - intros t w0. unfold eval_tt. intros. rewrite make_impl_map with (eval := Qeval_nformula env0). + eapply RWeakChecker_sound; eauto. + tauto. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing List Coq.micromega.Tauto