proposition: Lemma IndexedBag_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv IndexedBag_RepInv IndexedBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, IndexedBag_RepInv, IndexedBag_bdelete. intros; destruct search_term; destruct o; simpl in *; unfold IndexedBag_RepInv; intros. - case_eq (find t0 container); intros; rewrite H0 in *. + case_eq (bdelete b s); intros; rewrite H1 in *; simpl in *. assert (RepInv b) as WF_b by (eapply containerCorrect; rewrite find_mapsto_iff; eassumption). rewrite add_mapsto_iff in H; intuition; subst. pose proof (bdelete_RepInv b s) as RepInv_H1; rewrite H1 in RepInv_H1; apply RepInv_H1; eauto. * pose proof (bdelete_correct b s WF_b); subst; rewrite H1 in *; simpl in *; intuition. apply find_2 in H0; rewrite <- H. eapply containerCorrect; eauto. eapply In_partition; eauto using Permutation_in, In_partition. * eapply containerCorrect; eauto. * eapply containerCorrect; eauto. + intuition; eapply containerCorrect; eauto. - rewrite fold_pair in H; simpl in H. rewrite FMap_Insert_fold_add_map_eq in H. rewrite map_mapsto_iff in H; destruct_ex; intuition; subst; assert (RepInv x) as WF_x by (eapply containerCorrect; eauto). eapply (bdelete_RepInv x s WF_x). destruct (bdelete_correct x s WF_x). eapply containerCorrect; eauto. eapply In_partition; right; eapply Permutation_in; eauto. Defined.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts