proposition: Lemma fold_union : forall A `{Inhab B} C (m:monoid_op C) (f:A->B->C) (M N : map A B), Comm_monoid m -> finite M -> finite N -> M \# N -> fold m f (M \u N) = monoid_oper m (fold m f M) (fold m f N).
proof: Proof. Proof using. introv IB Hm FM FN HD. do 3 rewrite fold_eq_fold_pairs. match goal with |- context [ set_st ?X] => cuts_rewrite (set_st X = \set{ p | exists k x, p = (k, x) /\ binds_impl M k x} \u \set{ p | exists k x, p = (k, x) /\ binds_impl N k x}) end. rewrite~ fold_union. apply~ finite_to_finite_fold_support. apply~ finite_to_finite_fold_support. rewrite disjoint_eq. intros (k,x). rew_set. intros (k1&x1&E1&R1) (k2&x2&E2&R2). inverts E1. forwards~: binds_impl_dom_impl R1. inverts E2. forwards~: binds_impl_dom_impl R2. applys* @disjoint_inv HD. typeclass. rew_set. intros (k',x'). rew_set. iff (k&x&E&F) H. inverts E. simpl in F. unfolds union_impl, binds_impl. cases (N k). right. exists k x. inverts~ F. left. exists k x. auto. simpl. destruct H as [(k&x&E&R)|(k&x&E&R)]. inverts E. exists k x. split~. forwards~: binds_impl_dom_impl R. cases (N k) as EN. false. applys~ @disjoint_inv k HD. typeclass. unfold dom_impl. rew_set. congruence. unfolds union_impl, binds_impl. rewrite~ EN. inverts E. exists k x. split~. forwards~: binds_impl_dom_impl R. unfolds union_impl, binds_impl. rewrite~ R. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)