proposition: Lemma prover_formula_correct : forall thy (THY: Thy thy) up m m' prf d n f , prover_formula thy up m n f = Success (m',prf, d) -> eval_hformula f.
proof: Proof. unfold prover_formula. intros. destruct (wfb m && chkHc m (elt f) (id f) (is_dec f)) eqn:EQ ; try congruence. rewrite andb_true_iff in EQ. destruct EQ as (WFM & CHK). apply wfb_correct in WFM. apply chkHc_has_form in CHK; auto. assert (WE := wf_empty m WFM). assert (EE := eval_empty m). assert (EA := eval_annot_empty m). assert (M : hconsmap (empty_state m) = m) by reflexivity. set (s0 := empty_state m) in *. clearbody s0. assert (HL : has_literal (hconsmap s0) (POS hTT)). { simpl. unfold hTT. unfold TT. apply wf_OP with (l':= nil). constructor. apply wf_true ; auto. congruence. reflexivity. reflexivity. } assert (HL' : check_annot has_literal (hconsmap s0) (annot_lit hTT)). { apply check_annot_lit. apply HL. } generalize (insert_unit_correct _ _ WE HL'). intros (WF & HM & EV). simpl in EV. set (s1 := (insert_unit (annot_lit hTT) s0)) in * ; clearbody s1. destruct (prover_intro (prover_opt thy up n) s1 (Some f)) eqn:PI ; try congruence. destruct r. destruct p. inv H. apply prover_intro_correct in PI; auto. - simpl in *. unfold annot_lit, Annot.lift in EV. simpl in EV. assert (ETT := eval_annot_hyp _ (POS hTT) HL) . tauto. - apply eq_sound_prover with (P:= prover thy up n). apply prover_op_eq. eapply prover_correct; eauto. - simpl. destruct f ; simpl in *. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause