proposition: Lemma wf_shorten_clauses : forall d l st (WFM: WMap.wf_watch_map l) (D : Annot.lift_deps (wf_pset (hconsmap st)) d) (ALL: WMap.Forall_watch_map (check_annot has_watched_clause (hconsmap st)) l) (WF: wf_state st), wf_result_state (shorten_clauses d l st).
proof: Proof. unfold shorten_clauses. intros. change (wf_result_state (Progress st)) in WF. set (Q := fun (st': dresult) => wf_result_state st' /\ Annot.lift_deps (wf_pset (hconsmap_result st')) d). assert (Q (WMap.fold_watch_map (fun (acc : dresult) (i : int) (k : Annot.t watched_clause) => update_watched_clause d i k acc) l (Progress st))). { assert (WF' : Q (Progress st)). { split; auto. } revert WF'. revert ALL. apply fold_up; auto. - intros. revert H0. eapply check_annot_mono;eauto. apply isMono_lift. apply has_watched_clause_mono. - intros. destruct H. simpl in *. tauto. - intros. split. apply hconsmap_update_watched_clause. destruct H. split; auto. apply wf_update_watched_clause; simpl; auto. destruct H0 ; auto. destruct H0; auto. rewrite hconsmap_update_watched_clause; auto. apply not_fail_update_watched_clause. } destruct H; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause