proposition: Lemma Permutation_benumerate_add : forall k v m, Permutation (flatten (List.map benumerate (fold_left (fun (a : list BagType) (p : XMap.key * Trie) => Trie_enumerate (snd p) ++ a) (XMap.elements (XMap.add k v m)) []))) (flatten (List.map benumerate (Trie_enumerate v ++ (fold_left (fun (a : list BagType) (p : key * Trie) => Trie_enumerate (snd p) ++ a) (XMap.elements (XMap.remove k m)) [])))).
proof: Proof. intros; pose (@XMap.fold_1 _ (XMap.add k v m) _ nil (fun _ (p : Trie) (a : list BagType) => Trie_enumerate p ++ a)). simpl in e. rewrite <- !e. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) (elements_add_eq k v m)) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite !fold_add; eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey, empty_In. rewrite XMap.fold_1; simpl. f_equiv. eapply XMap.remove_1; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix