proposition: Theorem RangeTreeBag_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv RangeTreeBag_RepInv RangeTreeBag_ValidUpdate RangeTreeBag_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, RangeTreeBag_RepInv, RangeTreeBag_bupdate. intros container key_searchterm updateterm containerCorrect [ validupdate_rep validupdate_rt ] 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. - induction (bupdate bag searchterm updateterm) as [ bupdate_upd bupdate_bag ] eqn: bupdate_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 (bupdate_RepInv bag searchterm updateterm cont_rep) as bupdate_rep. rewrite bupdate_des in bupdate_rep. simpl in bupdate_rep. intuition. pose proof (bupdate_correct bag searchterm updateterm cont_rep validupdate_rep) as [ bupdate_correct_snd _ ]. rewrite bupdate_des in bupdate_correct_snd. simpl in bupdate_correct_snd. pose proof (Permutation_in _ bupdate_correct_snd H0) as E; apply in_app_or in E; destruct E as [ E | E ]. * pose proof (In_partition (bfind_matcher searchterm) (benumerate bag) item) as [ _ inp ]. eapply X.eq_trans; eauto. * rewrite in_map_iff in E. destruct E as [ item' [ item'_eq In_item' ] ]. subst. apply validupdate_rt. eapply X.eq_trans with key; auto. apply cont_in. pose proof (In_partition (bfind_matcher searchterm) (benumerate bag) item') as [ _ inp ]; 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