proposition: Lemma fold_spec : forall {A}(m:t A){B}(i : B) (f : key -> A -> B -> B), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
proof: Proof. unfold fold, bindings. intros A m B i f. revert m i. set (f' := fun a p => f (fst p) (snd p) a). assert (H: forall m i j acc, fold_left f' acc (xfold f m i j) = fold_left f' (xbindings m j acc) i). { induction m as [|l IHl o r IHr]; intros; trivial. destruct o; simpl; now rewrite IHr, <- IHl. } intros. exact (H m i 1 nil). Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)