proposition: Lemma fold_union_inter : forall i s s', eqA (fold f (union s s') (fold f (inter s s') i)) (fold f s (fold f s' i)).
proof: Proof. intros; pattern s; apply set_induction; clear s; intros. - transitivity (fold f s' (fold f (inter s s') i)). { apply fold_equal; auto with set. } transitivity (fold f s' i). { apply fold_init; auto. apply fold_1; auto with set. } symmetry; apply fold_1; auto. - rename s'0 into s''. destruct (In_dec x s'). + transitivity (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set. { apply fold_init; auto. apply fold_2 with (eqA:=eqA); auto with set. rewrite inter_iff; intuition. } transitivity (f x (fold f s (fold f s' i))). 1:transitivity (fold f (union s s') (f x (fold f (inter s s') i))). 2:transitivity (f x (fold f (union s s') (fold f (inter s s') i))). * apply fold_equal; auto. apply equal_sym; apply union_Equal with x; auto with set. * apply fold_commutes; auto. * apply Comp; auto with relations. * symmetry; apply fold_2 with (eqA:=eqA); auto. + transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))). { apply fold_2 with (eqA:=eqA); auto with set. } transitivity (f x (fold f (union s s') (fold f (inter s s') i))). { apply Comp;auto with relations. apply fold_init;auto. apply fold_equal;auto. apply equal_sym; apply inter_Add_2 with x; auto with set. } transitivity (f x (fold f s (fold f s' i))). * apply Comp; auto with relations. * symmetry; apply fold_2 with (eqA:=eqA); auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide