proposition: Lemma fold_spec: forall s (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i.
proof: Proof. unfold fold, elements. intros s A i f. revert s i. set (f' := fun a e => f e a). assert (H: forall s i j acc, fold_left f' acc (xfold f s i j) = fold_left f' (xelements s j acc) i). - induction s as [|l IHl o r IHr]; intros; trivial. destruct o; simpl xelements; simpl xfold. + rewrite IHr, <- IHl. reflexivity. + rewrite IHr. apply IHl. - intros. exact (H s i 1 nil). Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface