proposition: Lemma unit_propagation_correct : forall n g st (WF : wf_state st) (WFG : has_oform (hconsmap st) g) (EST : eval_state st), match unit_propagation n g st with | Success _ => True | Fail _ => False | Progress st' => (eval_state st' -> eval_ohformula g) end -> eval_ohformula g.
proof: Proof. induction n. - simpl. tauto. - cbn. intros. destruct (extract_unit st) eqn:EQ ;[|auto]. destruct p as (l,st'). assert (EQ':= EQ). apply wf_extract_unit in EQ. destruct EQ as (WFST' & WFA). assert (HM:= hconsmap_extract_unit _ _ _ EQ'). apply extract_unit_eval_state in EQ'. destruct EQ' as (EL & EST'). destruct (success g (units st') l) eqn:SUC. + destruct WFST', EST'. apply success_correct with (m:=hconsmap st') in SUC; auto. eapply has_oform_mono;eauto. congruence. destruct WFA;auto. + set (L := WMap.find_clauses (Annot.elt l) (clauses st')) in *. assert (WFLL: WMap.Forall_watch_map (check_annot has_watched_clause (hconsmap st')) L /\ WMap.wf_watch_map L). { apply wf_find_clauses with (m:= hconsmap st') ; auto. destruct WFST';auto. destruct WFST';auto. } destruct WFLL as (WFL1 & WFL2). assert (EVALL : WMap.Forall_watch_map (Annot.lift eval_watched_clause) L). { apply eval_find_clauses. destruct EST' ; auto. } assert (eval_result_state (shorten_clauses l L (insert_literal l st'))). { apply eval_shorten_clauses; auto. split. apply wf_insert_literal; auto. apply eval_insert_literal ; auto. } assert (wf_result_state (shorten_clauses l L (insert_literal l st'))). { apply wf_shorten_clauses;auto. rewrite hconsmap_insert_literal. destruct WFA;auto. apply wf_insert_literal;auto. } assert (hconsmap_progress (shorten_clauses l L) (insert_literal l st')). { apply hconsmap_shorten_clauses. } unfold hconsmap_progress in *. destruct (shorten_clauses l L (insert_literal l st')) eqn:RES ; try tauto. simpl in H0. tauto. simpl in H2. revert H. apply IHn; auto. eapply has_oform_mono; eauto. rewrite H2 in * by tauto. congruence. + auto. + auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause