proposition: Lemma InvertedIndex_BagFindCorrect : BagFindCorrect InvertedIndex_RepInv InvertedIndex_bfind InvertedIndex_bfind_matcher InvertedIndex_benumerate.
proof: Proof. unfold BagFindCorrect, InvertedIndex_bfind_matcher, InvertedIndex_bfind, InvertedIndex_benumerate; intros. unfold InvertedIndex_RepInv in *; intuition. rewrite !ListFacts.filter_map. rewrite <- Permutation_filter_elements with (f := fun (k : MValues.key) (item : TItem) => andb (if IncludedInA_dec (X_eq_dec := E.eq_dec) (fst search_term) (projection item) then true else false) (ItemSearchTermMatcher (snd search_term) item)); eauto using Proper_bfind_matcher. rewrite <- Permutation_filter_elements with (f := fun (k : MValues.key) (item : TItem) => ItemSearchTermMatcher (snd search_term) item); eauto using Proper_ItemSearchTermMatcher. eapply MoreMValuesFacts.Permutation_InA_cons; eauto using NoDupA_filter, MValues.elements_3w. intros; rewrite <- !elements_mapsto_iff. rewrite !filter_iff by (eauto using Proper_bfind_matcher, Proper_ItemSearchTermMatcher). intuition. - try find_if_inside; eauto. eapply Find_MatchingIndexesOK_Subset_iff; eauto. discriminate. - find_if_inside; eauto; discriminate. - eapply Find_MatchingIndexesOK_Subset_iff; eauto. - find_if_inside; eauto. apply Not_inclA_NIn in n; destruct n; split_and. eapply Find_MatchingIndexesOK_Subset_iff in H3; intuition eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion