proposition: Theorem RangeTreeBag_binsert_Preserves_RepInv : binsert_Preserves_RepInv RangeTreeBag_RepInv RangeTreeBag_binsert.
proof: Proof. unfold binsert_Preserves_RepInv, RangeTreeBag_RepInv. intros ? item' ? k' bag' maps_to. unfold RangeTreeBag_binsert in maps_to. rewrite add_mapsto_iff in maps_to; destruct maps_to as [(is_eq & refreshed) | (neq & maps_to)]; subst; intuition; intros. - destruct (FindWithDefault_dec (projection item') bempty container) as [ [bag' (mapsto & equality)] | (not_found & equality) ]; rewrite equality in *; eauto using binsert_RepInv. eapply binsert_RepInv; eapply containerCorrect; eauto. eapply binsert_RepInv; eapply bempty_RepInv. - rewrite <- is_eq. rewrite binsert_enumerate_weak with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H; intuition; subst. destruct (FindWithDefault_dec (projection item') bempty container) as [ [bag' (mapsto & equality)] | (not_found & equality) ]; rewrite equality in *; clear equality. eapply containerCorrect; eauto. rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H0; simpl in H0; intuition. reflexivity. destruct (FindWithDefault_dec (projection item') bempty container) as [ [bag' (mapsto & equality)] | (not_found & equality) ]; rewrite equality in *; clear equality; eauto. + eapply containerCorrect; eauto. + apply bempty_RepInv. - eapply containerCorrect; eauto. - eapply containerCorrect; 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