proposition: Lemma prover_arrows_correct : forall l st (ALL : Forall (has_literal (hconsmap st)) l), sound_prover (prover_arrows l) st.
proof: Proof. induction l. - repeat intro. simpl in PRF. inv PRF. - repeat intro. rewrite prover_arrows_rew in PRF. inv ALL. generalize (remove_arrow_correct a st WFS). intros (WFR & EVAL & EVALA & HC). set (st' := remove_arrow a st) in *; clearbody st'. set (f := form_of_literal a) in *. unfold f in PRF. destruct (prover_intro st' (Some (form_of_literal a))) eqn:P; try congruence. + destruct f0 ; try congruence. eapply IHl; eauto. eapply IHl; eauto. + destruct r as (p,a'). destruct p as (m',prf'). assert (HASA : has_oform (hconsmap st') (Some (form_of_literal a))). { simpl. rewrite HC. apply has_form_of_literal; auto. } apply prover_intro_correct in P; auto. simpl in P. assert (HASL : (Annot.lift (has_literal (hconsmap st)) (annot_lit (form_of_literal a)))). { simpl. unfold Annot.lift. rewrite has_form_of_literal;auto. simpl in HASA. unfold annot_lit. simpl. congruence. } simpl in HASA. rewrite HC in HASA. generalize (insert_unit_correct (annot_lit (form_of_literal a)) st WFS (check_annot_lit HASA) ). intros (WFS' & HCS' & EVS' & EVA'). set (la:= form_of_literal a) in * ; clearbody la. set (st1 := insert_unit (annot_lit la) st) in * ; clearbody st1. destruct P as (EP & EA & ALL & ORD & CFL &WFD ). assert (ORD1 : hmap_order (hconsmap st1) m'). { eapply hmap_order_trans ; eauto. congruence. } generalize (set_hmap_correct m' st1 ORD1 WFS'). intros (ESM & ASM & WSM & HCSM). set (sm := set_hmap m' st1) in * ; clearbody sm. assert (ACM := hconsmap_augment_clauses prf' sm). unfold hconsmap_progress in ACM. assert (ALL' : Forall (has_conflict_clause (hconsmap sm)) prf'). { revert CFL. apply Forall_Forall. intro. apply has_conflict_clause_mono. congruence. } assert (ACW := wf_augment_clauses sm prf' ALL' WSM). assert (ACE := eval_augment_clauses prf' sm WSM ALL' ALL). assert (ACA := eval_annot_augment_clauses prf' sm WSM ALL' ALL). destruct (augment_clauses prf' sm); simpl in *; try congruence. { destruct r as (h,d'). inv PRF. split_and ; try tauto. - intros. exfalso. apply ACA; auto. apply ASM. apply EVA' ; auto. apply eval_annot_lit; auto. - rewrite <- HC. eapply hmap_order_trans; eauto. intuition congruence. - revert ALL'. apply ForallMono. apply has_conflict_clause_mono. rewrite ACM in * by tauto. auto with wf. } { apply ProverTCorrect in PRF; auto. destruct PRF as (PRF1 & PRF2 & PRF3 & PRF4 & PRF5). unfold eval_hformula in *. assert (ELA := eval_annot_lit (hconsmap st) la). split_and; try tauto. - subst. rewrite HC in *. rewrite ACM in * by tauto. eapply hmap_order_trans; eauto. - revert HASF. apply has_oform_mono. subst. rewrite HC in *. rewrite ACM in * by tauto. tauto. } + eapply IHl; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause