proposition: Lemma wf_unit_propagation : forall n g st (WF : wf_state st) (WFG : has_oform (hconsmap st) g), wf_result_state' (unit_propagation n g st ).
proof: Proof. induction n. - simpl. tauto. - cbn. intros. destruct (extract_unit st) eqn:EQ ;[|auto with wf]. destruct p as (l,st'). assert (EQ':= EQ). apply wf_extract_unit in EQ; auto. apply hconsmap_extract_unit in EQ'. destruct EQ as (WFST' & WFA ). destruct (success g (units st') l) eqn:SUC. + simpl. eapply wf_success; eauto. destruct WFA ;auto. destruct WFST';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 (WFS : wf_result_state (shorten_clauses l L (insert_literal l st'))). { apply wf_shorten_clauses ; auto. destruct WFA;auto. apply wf_insert_literal; auto. } assert (MONO := hconsmap_shorten_clauses l L (insert_literal l st') ). unfold hconsmap_progress in MONO. destruct (shorten_clauses l L (insert_literal l st'))eqn:RES ; try tauto. simpl. auto. apply IHn;auto. { revert WFG. apply has_oform_mono. simpl in *. intuition congruence. } Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause