proposition: Lemma eval_annot_unit_propagation : forall n g st (WF : wf_state st) (WFG : has_oform (hconsmap st) g) (EST : eval_annot_state st), match unit_propagation n g st with | Success (hm,d) => eval_pset hm d -> eval_ohformula g | Fail _ => True | Progress st' => eval_annot_state st' end.
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 eval_annot_extract_state in EQ'. destruct EQ' as (EL & EST'). destruct (success g (units st') l) eqn:SUC. + intro. apply eval_annot_success with (m:=hconsmap st') in SUC; auto. { eapply has_oform_mono;eauto. congruence. } { destruct WFST';auto. } { rewrite <- HM. tauto. } { destruct WFA; auto. } { destruct EST'; 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;auto. destruct WFST';auto. destruct WFST';auto. } destruct WFLL as (WFL1 & WFL2). assert (EVALL : WMap.Forall_watch_map (eval_annot eval_watched_clause (hconsmap st')) L). { apply eval_annot_find_clauses with (m:= hconsmap st') ; eauto. destruct EST' ; auto. } assert (eval_annot_result_state (shorten_clauses l L (insert_literal l st'))). { apply eval_annot_shorten_clauses; auto. rewrite hconsmap_insert_literal. rewrite <- HM. auto. split. apply wf_insert_literal; auto. apply eval_annot_insert_literal ; auto. rewrite <- HM. 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. * destruct r ; simpl in *. tauto. * simpl in H0. simpl in H1. revert H. apply IHn; auto. eapply has_oform_mono; eauto. rewrite H1 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