proposition: Lemma consist4 : forall (container: IndexedBag) key (containerCorrect : IndexedBag_RepInv container), Permutation (flatten (Values (filter (KeyBasedPartitioningFunction (list TItem) key) (map benumerate container)))) match find key container with | Some bag => benumerate bag | None => nil end.
proof: Proof. intros; rewrite <- consist. rewrite <- Permutation_map_filter. rewrite <- Permutation_map_Values. rewrite Permutation_filter_Values; eauto using KeyBasedPartitioningFunction_Proper. unfold Values. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. induction (elements container); simpl. constructor. case_eq (KeyBasedPartitioningFunction BagType key0 (fst a) (snd a)); simpl; rewrite IHl; intros. - apply Permutation_app; try reflexivity. apply KeyBasedPartitioningFunction_eq_true in H. rewrite filter_all_true; eauto. intros; eapply KeyFilter_true; eapply containerCorrect'; eauto. repeat econstructor; eauto. - intuition; eapply containerCorrect'; eauto. - apply KeyBasedPartitioningFunction_eq_false in H. rewrite filter_all_false; eauto. intros; eapply KeyFilter_false. unfold not; intros; apply H; rewrite <- H1; eapply containerCorrect'; eauto; repeat econstructor; reflexivity. - intuition; eapply containerCorrect'; eauto. - eauto. 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