proposition: Theorem fold_rec : forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t), (forall s', Empty s' -> P s' i) -> (forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)) -> P s (fold f s i).
proof: Proof. intros A P f i s Pempty Pstep. rewrite fold_spec_right. set (l:=rev (elements s)). assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)). { intros; eapply Pstep; eauto. rewrite elements_iff, <- InA_rev; auto with *. } assert (Hdup : NoDup l) by (unfold l; eauto using elements_3w, NoDupA_rev with *). assert (Hsame : forall x, In x s <-> InA x l) by (unfold l; intros; rewrite elements_iff, InA_rev; intuition). clear Pstep; clearbody l; revert s Hsame; induction l. - intros s Hsame; simpl. apply Pempty. intro x. rewrite Hsame, InA_nil; intuition. - intros s Hsame; simpl. apply Pstep' with (of_list l); auto with relations. + inversion_clear Hdup; rewrite of_list_1; auto. + red. intros. rewrite Hsame, of_list_1, InA_cons; intuition. + apply IHl. * intros; eapply Pstep'; eauto. * inversion_clear Hdup; auto. * exact (of_list_1 l). Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide