proposition: Lemma hconsmap_fold : forall (F: int -> Annot.t watched_clause -> dresult -> dresult) cl st (FOK : forall i k st, hconsmap_progress_r (F i k) st) (NOTFAIL : forall i k st, ~ is_fail st -> ~ is_fail (F i k st)) , hconsmap_progress (fun (st : state) => WMap.fold_watch_map (fun (acc : dresult) (i : int) (k : Annot.t watched_clause) => F i k acc) cl (Progress st)) st.
proof: Proof. unfold hconsmap_progress. intros. assert (ACC: ~ is_fail ((Progress st):dresult) /\ hconsmap_result (Progress st : dresult) = (hconsmap st)). { simpl. tauto. } rewrite WMap.fold_elements in *. revert H ACC. generalize (Progress st : dresult). induction (WMap.elements cl nil). - simpl. tauto. - simpl in *; intros. eapply IHl ; eauto. specialize (FOK (fst a) (snd a) d). unfold hconsmap_progress_r in *. destruct ACC as (ACC1 & ACC2). apply (NOTFAIL (fst a) (snd a)) in ACC1; eauto. split ; auto. rewrite <- ACC2. apply FOK;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause