proposition: Lemma consist : forall (container: IndexedBag) (containerCorrect : IndexedBag_RepInv container), forall k, flatten (List.map (List.filter (KeyFilter k)) (List.map benumerate (Values container))) = match find k container with | Some bag => benumerate bag | None => nil end.
proof: Proof. unfold IndexedBag_RepInv; intros. unfold Values. destruct (find k container) as [ bag | ] eqn:eqfind. rewrite <- find_mapsto_iff in eqfind. pose proof eqfind as maps_to. rewrite elements_mapsto_iff in eqfind. apply InA_split in eqfind. destruct eqfind as [ l1 [ y [ l2 (y_k_bag & decomp) ] ] ]. rewrite decomp. rewrite (map_map snd benumerate). rewrite ! map_app; simpl. pose proof (elements_3w container) as no_dup. rewrite decomp in no_dup; apply NoDupA_swap in no_dup; eauto using equiv_eq_key. inversion no_dup as [ | ? ? y_not_in no_dup' ]; subst. rewrite InA_app_iff in y_not_in by eauto using equiv_eq_key. unfold eq_key_elt in y_k_bag; simpl in y_k_bag. destruct y_k_bag as (y_k & y_bag). assert (forall k' bag', InA (@eq_key_elt _) (k', bag') (l1 ++ l2) -> forall item, List.In item (benumerate bag') -> ~ E.eq (projection item) k). { intros k' bag' in_app item in_bag'_items eq_k. rewrite InA_app_iff in in_app; eauto using equiv_eq_key_elt. pose proof in_app as in_app'. apply (InA_front_tail_InA _ _ y) in in_app. rewrite <- decomp, <- elements_mapsto_iff in in_app. pose proof (proj2 (containerCorrect _ _ in_app) _ in_bag'_items) as eq_k'. symmetry in eq_k. pose proof (E.eq_trans eq_k eq_k'). assert (eq_key y (k', bag')) as y_eq by (unfold eq_key; simpl; eauto). destruct in_app' as [ in_seq | in_seq ]; (apply (InA_eqke_eqk (k2 := fst y) (snd y)) in in_seq; eauto); rewrite <- surjective_pairing in in_seq; intuition. } rewrite ! map_filter_all_false; [ | intros subseq in_map item in_subseq; rewrite in_map_iff in in_map; destruct in_map as [ (k', bag') (benum_eq & in_seq) ]; rewrite KeyFilter_false; simpl in benum_eq; subst subseq; apply (H k' bag'); eauto; apply In_InA; eauto using equiv_eq_key_elt; rewrite in_app_iff; eauto .. ]. rewrite flatten_app, flatten_head, !flatten_nils, app_nil_l, app_nil_r, <- y_bag, filter_all_true; trivial. intros; rewrite KeyFilter_true; apply (containerCorrect _ bag); eauto. rewrite nil_in_false. intros [item item_in]. rewrite in_flatten_iff in item_in. do 2 setoid_rewrite in_map_iff in item_in. destruct item_in as [ subseq (in_subseq & [ subseq_prefilter ( pre_post_filter & [ bag (eq_bag_pre_filter & bag_in) ] ) ] ) ]. subst subseq. rewrite filter_In in in_subseq. destruct in_subseq as (in_subseq_prefilter & key_filter). rewrite KeyFilter_true in key_filter. rewrite <- MapsTo_snd in bag_in. destruct bag_in as [k' maps_to]. subst. rewrite <- key_filter in eqfind. rewrite <- (proj2 (containerCorrect k' bag maps_to) _ in_subseq_prefilter) in maps_to. rewrite find_mapsto_iff in maps_to. congruence. 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