proposition: Lemma prover_correct : forall thy (THY:Thy thy) b n st , sound_prover (prover thy b n) st /\ never_progress (prover thy b n) st.
proof: Proof. induction n. - unfold sound_prover. simpl ; auto. split ; try congruence. - rewrite prover_rew. remember (prover thy b n) as P. simpl. split. repeat apply sound_prover_seq. + unfold sound_prover. intros. unfold prover_unit_propagation in PRF. assert (UPC := unit_propagation_correct n _ _ WFS HASF). assert (UPA := eval_annot_unit_propagation n _ _ WFS HASF). assert (UPWF := wf_unit_propagation n _ _ WFS HASF). assert (UPM := hconsmap_unit_propagation n g st0). unfold hconsmap_progress in UPM. destruct (unit_propagation n g st0) ; try discriminate. simpl in UPM. destruct r. inv PRF. split_and; auto with wf. rewrite UPM by auto. apply hmap_order_refl. + unfold sound_prover_progress. intros. unfold prover_unit_propagation in PRF. assert (UPC := unit_propagation_correct n _ _ WFS HASF). assert (UPA := eval_annot_unit_propagation n _ _ WFS HASF). assert (UPWF := wf_unit_propagation n _ _ WFS HASF). assert (UPM := hconsmap_unit_propagation n g st0). unfold hconsmap_progress in UPM. destruct (unit_propagation n g st0) ; try discriminate. simpl in UPM. destruct r. inv PRF. inv PRF. split_and; auto with wf. simpl in UPM. rewrite UPM by auto. apply hmap_order_refl. + unfold sound_prover. intros. unfold prover_case_split in PRF. destruct (find_split (units st0) (is_classic g) (clauses st0)) eqn:FD ; try congruence. * assert (FDC : eval_state st0 -> (ohold (Annot.lift eval_or) (find_split (units st0) (is_classic g) (clauses st0)) -> eval_ohformula g) -> eval_ohformula g). { intro ES'. destruct ES' ; destruct WFS. apply eval_find_split with (m:=(hconsmap st0)); auto. } assert (FDC' : eval_annot_state st0 -> eval_pset (hconsmap st0) (Annot.deps t0) -> (eval_or (Annot.elt t0) -> eval_ohformula g) -> eval_ohformula g). { intro ES'. destruct ES' ; destruct WFS. intros. eapply eval_annot_find_split in ev_an_clauses0; eauto. rewrite FD. simpl. unfold eval_annot ; auto. } rewrite FD in FDC. simpl in FDC. assert (WFD : (ohold (check_annot has_conflict_clause (hconsmap st0)) (find_split (units st0) (is_classic g) (clauses st0)))). { destruct WFS. apply wf_find_split; auto. } rewrite FD in WFD. assert (HF0 : has_oform (hconsmap st0) g). { revert HASF. apply has_oform_mono; auto. simpl in *. intuition congruence. } simpl in WFD. destruct WFD as (AN & WFD). unfold Annot.lift in *. eapply case_split_ann_correct; eauto. apply IHn. + intros. unfold sound_prover_progress. unfold prover_case_split. intros. destruct_in_hyp PRF F; try discriminate. unfold case_split_ann in PRF. destruct_in_hyp PRF C; try discriminate. + unfold sound_prover; intros. unfold prover_impl_arrows in PRF. assert (Forall (has_literal (hconsmap st0)) (find_arrows st0 (arrows st0))). { apply has_find_arrows. destruct WFS ; auto. } set (l := (find_arrows st0 (arrows st0))) in *. clearbody l. apply prover_arrows_correct in PRF ; auto. apply IHn. + unfold sound_prover_progress. intros. unfold prover_impl_arrows in PRF. exfalso. induction ((find_arrows st0 (arrows st0))). discriminate. simpl in PRF. destruct (intro_state (remove_arrow a st0) (elt (form_of_literal a)) (form_of_literal a)). destruct f ; try congruence. destruct r. unfold augment_clauses in PRF. simpl in PRF. eapply IHn ; eauto. destruct st1. destruct (P s o) ; try discriminate. destruct f ; try discriminate. tauto. tauto. destruct r. destruct p. destruct_in_hyp PRF A; try discriminate. destruct r ; discriminate. eapply IHn; eauto. tauto. + intros. unfold sound_prover. unfold prover_thy. destruct b ; try congruence. apply run_thy_prover_correct. apply IHn ; auto. auto. + repeat apply never_progress_seq. unfold never_progress, prover_thy. destruct b ; try congruence. unfold run_thy_prover. intros. destruct (thy (hconsmap st0) (generate_conflict_clause st0 g)); try congruence. destruct p. destruct_in_hyp PRF H ; try congruence. destruct r ; try congruence. eapply IHn ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause