proposition: Lemma InvertedIndex_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv InvertedIndex_RepInv InvertedIndex_ValidUpdate InvertedIndex_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, InvertedIndex_bupdate, InvertedIndex_RepInv; simpl. intros; destruct search_term; intuition. - destruct (H _ _ H0 _ H3); intuition. setoid_rewrite MValuesProperties.update_mapsto_iff. setoid_rewrite MoreMValuesFacts.BasicFacts.map_mapsto_iff. case_eq (InvertedIndex_bfind_matcher (i, i0) x); intros. + eexists _; split. right; split. eexists x; split; eauto. rewrite MValuesProperties.filter_iff; intuition; eauto. intro H'; destruct H' as [? H']; rewrite MValuesProperties.filter_iff in H'; intuition. rewrite (MoreMValuesFacts.BasicFacts.MapsTo_fun H7 H5) in *; rewrite H4 in H8; discriminate. unfold InvertedIndex_ValidUpdate in *. rewrite <- valid_update; eauto. + exists x; split; eauto. left; rewrite MValuesProperties.filter_iff; intuition. rewrite H4; reflexivity. - setoid_rewrite MValuesProperties.update_mapsto_iff in H0; intuition. + rewrite MValuesProperties.filter_iff in H4; intuition. destruct (H1 _ _ H0 _ H3); intuition; eauto. + setoid_rewrite MoreMValuesFacts.BasicFacts.map_mapsto_iff in H0; destruct_ex; intuition; subst. rewrite MValuesProperties.filter_iff in H6; intuition. rewrite <- valid_update in H3. destruct (H1 _ _ H0 _ H3); intuition; eauto. - destruct H3. setoid_rewrite MValuesProperties.update_mapsto_iff in H3; eauto with typeclass_instances; intuition. rewrite MValuesProperties.filter_iff in H4; intuition. eapply H2; unfold MValues.In; eauto. setoid_rewrite MoreMValuesFacts.BasicFacts.map_mapsto_iff in H3; destruct_ex; intuition; subst. rewrite MValuesProperties.filter_iff in H6; intuition. eapply H2; unfold MValues.In; 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