proposition: Lemma TrieBag_BagCountCorrect : BagCountCorrect TrieBagRepInv TrieBag_bcount TrieBag_bfind .
proof: Proof. unfold TrieBagRepInv, TrieBag_bcount, TrieBag_bfind, BagCountCorrect. simpl; intros; destruct search_term as [ [key | ] search_term ]. - rewrite length_flatten. rewrite !foldright_compose. rewrite <- !fold_left_rev_right. rewrite map_map. generalize (Trie_find_TreeOK key containerCorrect). remember 0 as n; clear Heqn; revert n. induction (Trie_find container key); simpl; eauto. intros. intros; rewrite IHl by eauto. rewrite fold_right_app; simpl. rewrite bcount_correct by eauto. rewrite !fold_left_rev_right; simpl. clear; revert n; induction l; simpl; eauto with arith. intros; rewrite IHl; f_equal; omega. - rewrite length_flatten. remember [] as l; replace 0 with (length l) by (subst; eauto). clear Heql; generalize (Trie_enumerate_RepInv containerCorrect). induction (Trie_enumerate container); simpl; eauto. rewrite !foldright_compose, <- !fold_left_rev_right, map_map. intros; unfold compose in *; rewrite bcount_correct by eauto. rewrite !fold_left_rev_right. rewrite <- map_map, <- foldright_compose. unfold compose; rewrite IHl0 by eauto. remember (length l) as n; clear Heqn; generalize n. clear; induction l0; simpl; eauto with arith; intros. rewrite IHl0; f_equal; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix