proposition: Theorem RangeTreeBag_BagCountCorrect : BagCountCorrect RangeTreeBag_RepInv RangeTreeBag_bcount RangeTreeBag_bfind.
proof: Proof. unfold BagCountCorrect, RangeTreeBag_RepInv, RangeTreeBag_bcount, RangeTreeBag_bfind. intros. destruct search_term as [ [ minkey maxkey ] searchterm ]. remember (RangeTreeBag_btraverse container (minkey, maxkey)) as bs. pose proof (RangeTreeBag_btraverse_closed container (minkey, maxkey)). rewrite <- Heqbs in H; clear Heqbs. rewrite length_flatten. setoid_rewrite Nat.add_comm at 1. replace (fun (y : TKey * BagType) (x : nat) => bcount (snd y) searchterm + x) with (compose plus (fun (y : TKey * BagType) => bcount (snd y) searchterm)) by reflexivity. rewrite !foldright_compose. symmetry; setoid_rewrite <- rev_involutive at 1. rewrite rev_involutive. pose proof bcount_correct; unfold BagCountCorrect in H0. induction bs as [ | [ key bag ] bs' ]; simpl. - reflexivity. - assert (forall k b, InA (eq_key_elt (elt:=BagType)) (k, b) bs' -> MapsTo k b container). intros; eapply H; eapply InA_cons_tl; eauto. specialize (IHbs' H1); clear H1. assert (InA (eq_key_elt (elt:=BagType)) (key, bag) ((key, bag) :: bs')) by (econstructor; econstructor; reflexivity). specialize (H _ _ H1); clear H1; specialize (containerCorrect _ _ H). destruct containerCorrect; specialize (H0 _ searchterm H1). rewrite H0. rewrite IHbs'. reflexivity. 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