proposition: Lemma TrieBag_BagFindCorrect : BagFindCorrect TrieBagRepInv TrieBag_bfind TrieBag_bfind_matcher TrieBag_benumerate.
proof: Proof. intros container search_term. destruct search_term as [ [st |] search_term]. { unfold TrieBag_bfind. rewrite <- (app_nil_l st) at 1. unfold TrieBagRepInv; remember [] as l; clear Heql; revert l. eapply Trie_find_ind; intros; subst; simpl. - rewrite !app_nil_r, <- bfind_correct by eauto. destruct trie; simpl. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite Permutation_benumerate_fold_left, flatten_app; simpl; rewrite filter_app, app_nil_r; simpl. rewrite <- app_nil_r; f_equiv. + rewrite filter_Prefix; eauto; reflexivity. + match goal with | [ H : TrieOK _ _ |- _ ] => inversion H; subst; eapply TrieBag_enumerateOK'; intros; match goal with | [ H5 : _ |- _ ] => eapply H5; eapply (@XMap.elements_2 _ (XMap.Bst (SubTrieMapBST' H))); eauto end end. - rewrite <- H; eauto. destruct trie; simpl in *. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite Permutation_benumerate_fold_left, flatten_app; simpl; rewrite filter_app, app_nil_r; simpl; f_equiv. rewrite <- bfind_correct by eauto. + match goal with | [ H0 : TrieOK _ _ |- _ ] => inversion H0; subst end. rewrite filter_Prefix; eauto. + rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. match goal with | [ H : TrieOK _ _ |- _ ] => rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST H) end. simpl. apply find_2 in e0. match goal with | [ H0 : TrieOK _ _ |- _ ] => pose proof (KeyBasedPartition_fst_singleton key0 subtrie (XMap.Bst (SubTrieMapBST H0)) e0) as singleton end. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) singleton) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite !fold_add; eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey, empty_In. rewrite map_app, flatten_app, filter_app, <- app_nil_r. f_equiv. rewrite <- app_assoc; simpl; eauto. rewrite fold_empty, flatten_filter,map_map. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) (filter_negb_remove key0 _)) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). eapply filter_remove_key; eauto. - rewrite !app_nil_r, <- bfind_correct by eauto. destruct trie; simpl. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite Permutation_benumerate_fold_left, flatten_app; simpl; rewrite filter_app, app_nil_r; simpl. rewrite <- app_nil_r; f_equiv. + rewrite filter_Prefix; eauto. + rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. match goal with | [ H0 : TrieOK _ _ |- _ ] => rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST' H0) end. simpl in *. match goal with | [ H : TrieOK _ _ |- _ ] => rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' H)) key0) in e0 end. match goal with | [ H : TrieOK _ _ |- _ ] => pose proof (KeyBasedPartition_fst_singleton_None key0 (XMap.Bst (SubTrieMapBST H)) e0) as singleton end. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) singleton) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite fold_empty, flatten_filter, map_map. rewrite (fold_Equal_simpl (eqA := @Permutation BagType) (filter_negb_remove key0 _)) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). eapply filter_remove_key; eauto. } { simpl; unfold TrieBag_bfind_matcher; simpl. intros. generalize (Trie_enumerate_RepInv containerCorrect). unfold TrieBag_benumerate. induction (Trie_enumerate container); simpl. - eauto. - intros; rewrite <- bfind_correct by eauto. rewrite !filter_app; f_equiv; eauto. } 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