proposition: Lemma eval_annot_intro_state : forall f st hf (EQ : hf.(elt) = f) (WF : has_form (hconsmap st) hf) (WFST : wf_state st) (EVAL : eval_annot_state st), match intro_state st f hf with | Fail _ => False | Success (hm',d) => eval_pset hm' d | Progress (st',f') => 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'). intro IFF. rewrite <- IFF. revert EVAL. apply eval_annot_cnf_hyps;auto. tauto. intro EA. destruct I as (HL & HH). generalize (wf_cnf_hyps (is_classic o) l st HL WFST). generalize (hconsmap_cnf_hyps o l st). unfold hconsmap_progress. destruct (cnf_hyps (is_classic o) l st). - simpl in EQ. tauto. - simpl in *. destruct r. tauto. - simpl. intros HM WFS0. destruct o. + rewrite <- HM in HH by tauto. simpl in *. generalize (eval_annot_augment_cnf (Some h) (NEG h) st0 HH WFS0). simpl. destruct ((augment_cnf false (NEG h) st0)). * simpl in *. intros. unfold eval_hformula in *. tauto. * simpl in *. destruct r. tauto. * simpl in *. tauto. + simpl in *. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause