proposition: Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_bf (Qeval_formula env) f.
proof: Proof. intros f w. unfold QTautoChecker. apply tauto_checker_sound with (eval:= Qeval_formula) (eval':= Qeval_nformula). - apply Qeval_nformula_dec. - intros until env. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Qsor QSORaddon) ; auto. - unfold qdeduce. intros. revert H. apply (nformula_plus_nformula_correct Qsor QSORaddon);auto. - intros. rewrite Qeval_formula_compat. eapply (cnf_normalise_correct Qsor QSORaddon) ; eauto. - intros. rewrite Tauto.hold_eNOT. rewrite Qeval_formula_compat. now eapply (cnf_negate_correct Qsor QSORaddon);eauto. - intros t w0. unfold eval_tt. intros. rewrite make_impl_map with (eval := Qeval_nformula env). + eapply QWeakChecker_sound; eauto. + tauto. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing List Coq.micromega.Tauto