proposition: Lemma IndexedBag_BagCountCorrect : BagCountCorrect IndexedBag_RepInv IndexedBag_bcount IndexedBag_bfind .
proof: Proof. unfold IndexedBag_RepInv, IndexedBag_bcount, IndexedBag_bfind, BagCountCorrect; simpl in *; intros; destruct search_term as [ [ key | ] search_term ]; simpl in *. + case_eq (find key container); simpl; eauto. intros; rewrite <- find_mapsto_iff in *; rewrite bcount_correct; eauto; eapply containerCorrect; eauto. + rewrite length_flatten. rewrite (fold_over_Values _ _ (fun acc bag => acc + bcount bag search_term)) by eauto. rewrite <- fold_left_rev_right. setoid_rewrite Nat.add_comm at 1. replace (fun (y : BagType) (x : nat) => bcount y search_term + x) with (compose plus (fun bag => bcount bag search_term)) by reflexivity. rewrite !foldright_compose. symmetry; setoid_rewrite <- rev_involutive at 1. rewrite fold_left_rev_right, map_rev, rev_involutive. rewrite fold_plus_sym, <- !fold_map. unfold Values. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. remember 0; clear Heqn; revert TBagCorrect n containerCorrect'; clear; induction (elements container); simpl; intros; eauto. rewrite IHl; intuition. f_equal. rewrite bcount_correct; auto with arith. destruct a; eapply containerCorrect'; simpl; eauto; repeat constructor. simpl; reflexivity. eapply containerCorrect'; constructor 2; eauto. eapply containerCorrect'; eauto; constructor 2; eauto. Qed.
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