proposition: Lemma InvertedIndex_BagDeleteCorrect : BagDeleteCorrect InvertedIndex_RepInv InvertedIndex_bfind InvertedIndex_bfind_matcher InvertedIndex_benumerate InvertedIndex_bdelete.
proof: Proof. unfold BagDeleteCorrect, InvertedIndex_bdelete, InvertedIndex_benumerate; simpl in *; intros; split. - rewrite Permutation_elements_filter. rewrite Permutation_filter_map_snd with (f := fun v => negb (_ v)). induction (MValues.elements (ValuesMap container)); simpl; eauto. rewrite <- partition_filter_neq. case_eq (InvertedIndex_bfind_matcher search_term (snd a)); intros; simpl in *. case_eq (List.partition (InvertedIndex_bfind_matcher search_term) (map snd l)); intros; simpl; eauto. case_eq (List.partition (InvertedIndex_bfind_matcher search_term) (map snd l)); intros; simpl; eauto. - rewrite Permutation_elements_filter, Permutation_filter_map_snd. induction (MValues.elements (ValuesMap container)); simpl; eauto. rewrite <- partition_filter_eq. case_eq (InvertedIndex_bfind_matcher search_term (snd a)); intros; simpl in *. case_eq (List.partition (InvertedIndex_bfind_matcher search_term) (map snd l)); intros; simpl; eauto. case_eq (List.partition (InvertedIndex_bfind_matcher search_term) (map snd l)); intros; simpl; 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