proposition: Lemma case_split_correct : forall l g st m prf a d b (WF : wf_state st) (HASG : has_oform (hconsmap st) g) (HASAN : wf_pset (hconsmap st) a) (HASL : Forall (has_literal (hconsmap st)) l) (EQ: case_split l st g = Backjump b m prf d) , (eval_state st -> eval_annot_state st -> (if b then True else (eval_state st -> ( eval_or l -> eval_ohformula g) -> eval_ohformula g)) -> eval_ohformula g) /\ (eval_annot_state st -> if b then eval_pset m d -> eval_ohformula g else (eval_pset m a -> ((eval_or l -> eval_ohformula g) -> eval_ohformula g) -> eval_pset m (LitSet.union a d) -> eval_ohformula g)) /\ Forall eval_literal_list prf /\ hmap_order (hconsmap st) m /\ Forall (has_conflict_clause m) prf /\ wf_pset m d.
proof: Proof. induction l. - simpl. intros. inv EQ. split_and;auto with wf. + tauto. + intros AS EV F EU. apply eval_pset_union in EU; auto. tauto. destruct HASAN;auto. constructor. - intros. rewrite case_split_rew in EQ. unfold sound_prover in ProverTCorrect. inv HASL. rename H1 into HASA . rename H2 into HASL. assert (WFI:= wf_insert_unit (annot_hyp a) st WF (check_annot_hyp HASA)). assert (EI := eval_insert_unit (annot_hyp a) st WF). assert (EA := eval_annot_insert_unit (annot_hyp a) st WF). assert (ORD := hconsmap_insert_unit (annot_hyp a) st). unfold hconsmap_progress in ORD. assert (HASG' : has_oform (hconsmap (insert_unit (annot_hyp a) st)) g). { revert HASG. apply has_oform_mono; auto. rewrite hconsmap_insert_unit. apply hmap_order_refl. } set (st':= insert_unit (annot_hyp a) st) in *. clearbody st'. destruct (ProverT st' g) eqn:PRF; try congruence. destruct r as (p & ann'). destruct p as (m',prf'). destruct (negb (has_lit a ann') && annot_holds (units st) ann') eqn:CHECK. + rewrite andb_true_iff in CHECK. destruct CHECK as (C1 & HOLD). inv EQ. clear IHl. apply ProverTCorrect in PRF. destruct PRF as (PRF1 & PRF2 & PRF3 & PRF4 & PRF5 & PRF6). assert (HOLD' : eval_state st -> eval_pset m d). { intros. apply annot_holds_correct with (m:= m) in HOLD;auto. destruct H. revert ev_units0. apply eval_units_mono. rewrite ORD in *. auto. destruct WF ; auto. } simpl. unfold Annot.lift, annot_hyp in EI. simpl in *. assert (eval_annot eval_literal (hconsmap st) (annot_hyp a)). { apply eval_annot_hyp; auto. } split_and; try tauto; auto. * eapply hmap_order_trans;eauto. rewrite ORD. auto with wf. * auto. * auto. + generalize (ProverTCorrect st' g m' prf' ann' WFI HASG' PRF). intros (EVAL' & EVALA & EPRF & ORD' & HASC& WFP). assert (LE: hmap_order (hconsmap st) m'). { eapply hmap_order_trans ; eauto. rewrite ORD. apply hmap_order_refl. } generalize (set_hmap_correct m' st LE WF). set (st2 := set_hmap m' st) in *; clearbody st2. generalize (wf_augment_clauses st2 prf'). intros WFST2' (EVST2 &EVAST2 & WFST2 & HMST2). subst. assert (CST2 : (Forall (has_conflict_clause (hconsmap st2)) prf')). { revert HASC. apply Forall_Forall. intro. apply has_conflict_clause_mono; auto. intuition congruence. } generalize (eval_augment_clauses prf' st2). generalize (hconsmap_augment_clauses prf' st2 ). unfold hconsmap_progress. generalize (wf_augment_clauses st2 prf' CST2). generalize (eval_annot_augment_clauses prf' st2). destruct (augment_clauses prf' st2 ) ; try congruence. { simpl. intros. destruct r. inv EQ. simpl in *. rewrite H1 in * by tauto. split_and; try tauto. } { intros EVAST0 WFST0 HMST0 EVST0. simpl in HMST0. assert (HF : has_oform (hconsmap st0) g). { revert HASG'. apply has_oform_mono. eapply hmap_order_trans; eauto. intuition congruence. } assert (HASL' : Forall (has_literal (hconsmap st0)) l). { revert HASL. apply Forall_Forall. intro. apply has_literal_mono. eapply hmap_order_trans; eauto. intuition congruence. } assert (WFST0' : wf_state st0) by tauto. assert (WFA0 : wf_pset (hconsmap st0) a0). { eapply wf_pset_mono;eauto. rewrite ORD in *. rewrite HMST0 by tauto. tauto. } destruct (case_split l st0 g)eqn:DIS; try congruence. inv EQ. specialize (IHl g st0 m prf0 a0 deps b WFST0' HF WFA0 HASL' DIS). destruct IHl as (PRF1 & PRF2 & PRF3 & PRF4 & PRF5 & PRF6 ). simpl. rewrite HMST0 in * by tauto. assert (EA' :=eval_annot_hyp (hconsmap st) a). split_and. - destruct b. + intros. simpl in *. tauto. + tauto. - destruct b. tauto. intros ES EPS EOR EU. assert (WFA0' : LitSet.wf a0). { destruct WFA0 ; auto. } assert (WFD : LitSet.wf deps). { destruct PRF6; auto. } apply eval_pset_union in EU; auto. destruct EU as (EPSA0 & EPSD). apply eval_pset_union in EPSD; auto. destruct (has_lit a ann') eqn:HASLIT. { assert (eval_literal a -> eval_pset m (remove_lit a ann') -> eval_pset m ann'). { apply eval_pset_remove;auto. revert HASA. apply has_literal_mono. eapply hmap_order_trans; eauto. revert WFP. apply wf_pset_mono. tauto. } apply EOR. intros OR. destruct OR. * apply EVALA. tauto. destruct EPSD as (ED & ER). specialize (H H0 ER). revert H. apply eval_pset_mono. tauto. * apply PRF2; auto. apply EVAST0; auto. apply eval_pset_union; auto. tauto. } { apply EVALA. tauto. destruct EPSD as (ED & ER). revert ER. apply eval_pset_mono. tauto. } + destruct (has_lit a ann'). apply wf_remove_lit; auto. destruct WFP; auto. destruct WFP; auto. + destruct (has_lit a ann'). apply LitSet.wf_union; auto. apply wf_remove_lit; auto. destruct WFP; auto. apply LitSet.wf_union; auto. destruct WFP; auto. - rewrite Forall_app. tauto. - eapply hmap_order_trans; eauto. - rewrite Forall_app. split. revert HASC. eapply ForallMono. apply has_conflict_clause_mono. tauto. tauto. - destruct b ; try tauto. + destruct (has_lit a ann'). apply wf_pset_union;auto. unfold remove_lit. apply wf_pset_remove; auto. revert WFP. apply wf_pset_mono. tauto. apply wf_pset_union;auto. revert WFP. apply wf_pset_mono. tauto. } Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause