proposition: Lemma fold_up : forall (P: hmap -> Annot.t watched_clause -> Prop) (Q: dresult -> Prop) (WPI : forall m m', hmap_order m m' -> forall x, P m x -> P m' x) (UP : int -> Annot.t watched_clause -> dresult -> dresult) (QOUT : forall f, Q (Fail f) -> False) (UPSuccess : forall i x d, UP i x (Success d) = Success d) (UPOK : forall i cl st , Q (Progress st) -> P (hconsmap st) cl -> hconsmap_progress_r (UP i cl) (Progress st) /\ Q (UP i cl (Progress st))) cl (st: state) (WF: WMap.wf_watch_map cl) (CL : WMap.Forall_watch_map (P (hconsmap st)) cl) (ES : Q (Progress st)), Q (WMap.fold_watch_map (fun acc k el => UP k el acc) cl (Progress st)).
proof: Proof. intros. set (P':= fun (o:dresult) cl => match o with Progress st => P (hconsmap st) cl | Success (h,_) => P h cl | _ => True end). apply (fold_lemma _ P'); eauto. unfold P'. intros. destruct acc ; auto. - apply QOUT in H1. tauto. - destruct r. rewrite UPSuccess. auto. - clear P'. specialize (UPOK i _ _ H1 H). unfold hconsmap_progress_r in UPOK. destruct (UP i e (Progress st0)) eqn:EQ; simpl in * ; auto. + destruct r. intuition congruence. + intuition congruence. - intros. destruct acc. apply QOUT in H. tauto. rewrite UPSuccess. auto. apply UPOK; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause