proposition: Lemma intro_state_correct : forall f st hf (EQ : hf.(elt) = f) (WF : has_form (hconsmap st) hf) (WFST : wf_state st) (EVAL : eval_state st) (EVALA : eval_annot_state st) , match intro_state st f hf with | Fail _ => False | Success _ => True | Progress (st',f') => eval_state st' -> eval_annot_state st' -> eval_ohformula f' end -> eval_formula f.
proof: Proof. unfold intro_state. intros. destruct (intro_impl nil f hf) eqn:I. assert (I':=I). apply wf_intro_impl with (m:= hconsmap st) in I ; auto. generalize (intro_impl_correct (hconsmap st) _ _ _ _ WF EQ I'). intros. rewrite <- H0. clear H0. assert (WFC : wf_result_state (cnf_hyps (is_classic o) l st)). { apply wf_cnf_hyps ; auto. tauto. } specialize (eval_cnf_hyps o l st). generalize (hconsmap_cnf_hyps o l st). unfold hconsmap_progress. specialize (eval_annot_cnf_hyps o l st). destruct (cnf_hyps (is_classic o) l st). - simpl in WFC. tauto. - simpl in *. tauto. - simpl. intros. destruct I as (HL & HH). destruct o. + simpl in H1. eapply has_oform_mono in HH ; eauto. generalize (eval_augment_cnf (Some h) (NEG h) st0 HH WFC). generalize (eval_annot_augment_cnf (Some h) (NEG h) st0 HH WFC). simpl. destruct ((augment_cnf false (NEG h) st0)). * simpl in *. intros. unfold eval_hformula in *. tauto. * simpl in *. tauto. * simpl in *; intros. intuition. * intuition congruence. + simpl in *. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause