proposition: Theorem RangeTreeBag_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv RangeTreeBag_RepInv RangeTreeBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, RangeTreeBag_RepInv, RangeTreeBag_bdelete. intros container key_searchterm containerCorrect key' bag' inv'. destruct key_searchterm as [ filter searchterm ]. pose proof (RangeTreeBag_btraverse_closed container filter) as Hc. remember (RangeTreeBag_btraverse container filter) as ls; clear Heqls. induction ls as [ | [ key bag ] ls' ]; intros; simpl in inv'. - eauto. - destruct (bdelete bag searchterm) as [ bdelete_del bdelete_bag ] eqn: bdelete_des; simpl in inv'. rewrite add_mapsto_iff in inv'. inversion inv' as [ [ inv'_eq inv'_next ] | [ inv'_neq inv'_ind ] ]; clear inv'; subst. + specialize (Hc key bag). assert (InA (eq_key_elt (elt:=BagType)) (key, bag) ((key, bag) :: ls')). repeat constructor; apply X.eq_refl. apply Hc in H. apply containerCorrect in H; destruct H as [ cont_rep cont_in ]. pose proof (bdelete_RepInv bag searchterm cont_rep) as bdel_rep. rewrite bdelete_des in bdel_rep. simpl in bdel_rep. intuition. pose proof (bdelete_correct bag searchterm cont_rep) as [ bdel_correct_snd _ ]. rewrite bdelete_des in bdel_correct_snd. simpl in bdel_correct_snd. pose proof (Permutation_in _ bdel_correct_snd H). pose proof (In_partition (bfind_matcher searchterm) (benumerate bag) item) as [ _ inp ]. eapply X.eq_trans; eauto. + eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts