proposition: Lemma FMap_Insert_fold_add {Value} : forall (f : Value -> Value) (bag : t Value) bag', (forall (k : key), InA E.eq k (List.map fst (elements bag)) -> ~ In k bag') -> Permutation (List.map snd (elements (fold (fun k bag'' r' => add k (f bag'') r') bag bag'))) (List.map snd ((List.map (fun kv => (fst kv, f (snd kv))) (elements bag)) ++ elements bag')).
proof: Proof. intros. intros; rewrite fold_1. generalize (elements_3w bag) as NoDupl. revert bag' H; induction (elements bag); simpl; intros. reflexivity. rewrite IHl, Permutation_cons_app; try (rewrite List.map_app; reflexivity). rewrite List.map_app, List.map_map. apply Permutation_app; try reflexivity. apply (Permutation_InA_cons ((fst a, f (snd a)) :: elements bag')); eauto using elements_3w. econstructor; eauto using elements_3w. unfold not; intros; eapply (H (fst a)); [ constructor; reflexivity | eapply elements_in_iff; revert H0; clear; intro; induction H0]. repeat econstructor; eauto. destruct IHInA; econstructor; econstructor 2; eauto. split; intros. apply InA_mapsto_add in H0; intuition. inversion H0; subst; eapply InA_mapsto_add'; intuition. right; intuition. eapply H; simpl. econstructor; reflexivity. eapply elements_in_iff; revert H2 H1; clear; intros; induction H2. destruct H; repeat econstructor; eauto. destruct IHInA; econstructor; econstructor 2; eauto. unfold not; intros. apply add_in_iff in H1; destruct H1. inversion NoDupl; subst; rewrite <- H1 in H0; eapply H4. revert H0; clear; induction l; intros; inversion H0; subst. constructor; eauto. econstructor 2; eauto. eapply H; eauto. inversion NoDupl; eauto. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances