proposition: Lemma consist' : forall (container: IndexedBag) key (containerCorrect : IndexedBag_RepInv container), Permutation (Values (filter (fun (k : M.key) (e : list TItem) => negb (KeyBasedPartitioningFunction (list TItem) key k e)) (map benumerate container))) (Values (map benumerate (remove key container))).
proof: Proof. intros; eapply Permutation_InA_cons; eauto using elements_3w. intros. repeat rewrite <- elements_mapsto_iff. rewrite filter_iff. - intuition; intros. + rewrite map_mapsto_iff in H0; destruct H0 as [bag' [eq_bag' filter_k] ]; subst. rewrite map_mapsto_iff; eexists; split; eauto. rewrite remove_mapsto_iff; split; eauto. unfold not; intros. rewrite KeyBasedPartitioningFunction_eq_true in H; rewrite H in H1; discriminate. + rewrite map_mapsto_iff in H; destruct H as [bag' [eq_bag' filter_k] ]; subst. rewrite remove_mapsto_iff in filter_k; intuition. + rewrite map_mapsto_iff in H; destruct H as [bag' [eq_bag' filter_k] ]; subst. rewrite remove_mapsto_iff in filter_k; intuition. eapply KeyBasedPartitioningFunction_eq_false in H; rewrite H; reflexivity. - unfold Proper; compute; intros; subst; trivial. destruct (F.eq_dec x _), (F.eq_dec y _); rewrite H in *; intuition. 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