proposition: Lemma wf_intro_state : forall f st hf (EQ: elt hf = f) (WF : has_form (hconsmap st) hf) (WFST : wf_state st), match intro_state st f hf with | Progress (st', f') => wf_state st' /\ has_oform (hconsmap st') f' | Success (h,d) => wf_pset h d | Fail _ => False end.
proof: Proof. unfold intro_state. intros. destruct (intro_impl nil f hf) eqn:WFI. apply wf_intro_impl with (m:=hconsmap st) in WFI ; auto. destruct WFI. generalize (wf_cnf_hyps (is_classic o) l st). generalize (hconsmap_cnf_hyps o l st). unfold hconsmap_progress. intros. destruct (cnf_hyps (is_classic o) l st); try congruence. - simpl in H2. tauto. - simpl in H1. destruct r. simpl in H2; tauto. - assert (HF : has_oform (hconsmap st0) o). { eapply has_oform_mono; eauto. simpl in H1. intuition congruence. } destruct o; try congruence. + assert (AM := hconsmap_augment_cnf false (NEG h) st0). unfold hconsmap_progress in AM. generalize (wf_augment_cnf false (NEG h) st0). destruct ((augment_cnf false (NEG h) st0)); try congruence. * simpl. tauto. * intros. destruct r ; simpl in H3. tauto. * simpl in *. intuition. eapply has_form_mono ; eauto. 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