proposition: Lemma InvertedIndex_BagUpdateCorrect : BagUpdateCorrect InvertedIndex_RepInv InvertedIndex_ValidUpdate InvertedIndex_bfind InvertedIndex_bfind_matcher InvertedIndex_benumerate bupdate_transform InvertedIndex_bupdate.
proof: Proof. unfold BagUpdateCorrect, InvertedIndex_bupdate, InvertedIndex_benumerate; simpl in *; intros; split. - rewrite Permutation_elements_update, Permutation_elements_filter, Permutation_filter_map_snd with (f := fun v => negb (_ v)). rewrite Permutation_app_swap. f_equiv. + 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_map, Permutation_map_snd_swap, 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. + intros; destruct x. intro; rewrite InA_eq_key_eq_key_elt in *; destruct_ex. rewrite <- !elements_mapsto_iff in *. rewrite !map_mapsto_iff in *; destruct_ex; intuition; subst. rewrite filter_iff in *; intuition eauto with typeclass_instances. rewrite <- (MoreMValuesFacts.BasicFacts.MapsTo_fun H H0) in H3. rewrite H3 in H1; discriminate. - 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