proposition: Lemma fold_left_fst_partition_update : forall search_term update_term (valid_update: ValidUpdate update_term) l l' l'', (forall (key0 : TKey) (bag : BagType), InA (@eq_key_elt _) (key0, bag) l -> RepInv bag /\ (forall item : TItem, List.In item (benumerate bag) -> E.eq (projection item) key0)) -> Permutation l'' (fst (List.partition (fun item : TItem => bfind_matcher search_term item) l')) -> Permutation (fold_left (fun (a : list TItem) (p : key * BagType) => fst (bupdate (snd p) search_term update_term) ++ a) l l'') (fst (List.partition (fun item : TItem => bfind_matcher search_term item) (l' ++ (flatten ((List.map benumerate (List.map snd l))))))).
proof: Proof. induction l; simpl; intros. rewrite app_nil_r; eauto. rewrite app_assoc. rewrite <- IHl; f_equiv. intros; eapply H; constructor 2; eauto. rewrite H0, partition_app; simpl. rewrite Permutation_app_comm; f_equiv. apply bupdate_correct. destruct a; eapply H; repeat constructor; eauto. assumption. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts