proposition: Lemma InvertedIndex_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv InvertedIndex_RepInv InvertedIndex_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, InvertedIndex_bdelete, InvertedIndex_RepInv; simpl. intros; destruct search_term; intuition. - rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff in H0; destruct H0; intuition; subst; apply filter_In in H3; intuition. case_In_dec; try discriminate. destruct (H _ _ H5 _ H0); intuition. eexists x0; split; eauto. apply filter_iff; intros; eauto with typeclass_instances. split; eauto. rewrite <- MValues_elements_in_iff in n. unfold InvertedIndex_bfind_matcher; simpl. destruct (IncludedInA_dec i (projection x0)); simpl; eauto. case_eq (i0 x0); intros; simpl; auto. destruct n; exists x0; rewrite filter_iff; eauto with typeclass_instances. intuition. unfold InvertedIndex_bfind_matcher; simpl. rewrite H3; destruct (IncludedInA_dec i (projection x0)); simpl; eauto. - rewrite filter_iff in H0; eauto with typeclass_instances; intuition. destruct (H1 _ _ H4 _ H3); intuition. eexists _; split. rewrite MoreMKeysFacts.BasicFacts.map_mapsto_iff. eexists _; split; eauto. apply filter_In; split; eauto. case_In_dec; eauto. rewrite <- MValues_elements_in_iff in i1; destruct i1. rewrite filter_iff in H0; eauto with typeclass_instances; intuition. rewrite (MoreMValuesFacts.BasicFacts.MapsTo_fun H8 H4) in *; rewrite H9 in H5; discriminate. - destruct H3. rewrite filter_iff in H3; eauto with typeclass_instances; intuition. eapply H2; eauto. eexists; 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