proposition: Lemma TrieBag_BagDeleteCorrect : BagDeleteCorrect TrieBagRepInv TrieBag_bfind TrieBag_bfind_matcher TrieBag_benumerate TrieBag_bdelete.
proof: Proof. intros container search_term. destruct search_term as [ [st | ] search_term]. { unfold TrieBag_bdelete. split. { rewrite <- (app_nil_l st) at 2. revert containerCorrect. unfold TrieBagRepInv; remember [] as l; clear Heql; revert l. eapply Trie_delete_ind; intros; subst; simpl. - destruct (bdelete_correct (TrieNode trie) search_term0); eauto. destruct trie; simpl. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite e0 in H. rewrite partition_filter_neq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite (Permutation_benumerate_fold_left _ [b]), flatten_app; simpl. rewrite filter_app. rewrite H, partition_filter_neq, !app_nil_r; simpl. f_equiv. + eapply filter_negb_Prefix; eauto; reflexivity. + inversion containerCorrect; subst. rewrite <- TrieBag_enumerateOK'' at 1. unfold TrieBag_bfind_matcher, IsPrefix; reflexivity. intros; eapply H7. eapply (@XMap.elements_2 _ (XMap.Bst H4)); eauto. - rewrite e2 in H; simpl in *. destruct trie; simpl in *. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite partition_filter_neq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite (Permutation_benumerate_fold_left _ [b]), flatten_app; simpl. rewrite !filter_app. rewrite app_nil_r, <- app_assoc. f_equiv. + replace (bag') with (snd (bdelete b search_term0)) by (rewrite e0; eauto). destruct (bdelete_correct b search_term0); eauto. rewrite H0. rewrite partition_filter_neq. eapply filter_negb_Prefix; eauto; reflexivity. + simpl. rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST containerCorrect). simpl in *. apply find_2 in e1. pose proof (KeyBasedPartition_fst_singleton key0 subtrie (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton. 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 flatten_filter. rewrite !map_app, fold_empty, !map_map. rewrite flatten_app. rewrite (Permutation_benumerate_add key0 bag'' (XMap.Bst (SubTrieMapBST containerCorrect))). rewrite map_app, flatten_app. f_equiv. * rewrite (H (l ++ [key0])), partition_filter_neq. unfold TrieBag_benumerate; rewrite flatten_filter, map_map. unfold TrieBag_bfind_matcher; rewrite <- app_assoc. repeat f_equiv. inversion containerCorrect; subst; eauto. * pose (@XMap.fold_1 _ (XMap.remove key0 (XMap.Bst (SubTrieMapBST containerCorrect))) _ nil (fun (_ : key) (trie : Trie) (a : list BagType) => Trie_enumerate trie ++ a)). simpl in e; unfold XMap.key, key in *; rewrite <- e. 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). unfold XMap.fold. rewrite !fold_1. rewrite <- TrieBag_enumerateOK'''. rewrite flatten_filter. rewrite map_map. unfold TrieBag_bfind_matcher, IsPrefix; simpl. f_equiv. intros; eapply TrieOK_subtrie_remove; simpl in *; eauto using Proper_negb_KeyBasedPartitioningFunction. intros; eapply TrieOK_distinct_subtries; eauto. exact (XMap.is_bst _). - destruct trie; simpl in *. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite partition_filter_neq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite (Permutation_benumerate_fold_left _ [b]), flatten_app; simpl. rewrite !filter_app. rewrite app_nil_r, <- app_assoc. f_equiv. + replace (bag') with (snd (bdelete b search_term0)) by (rewrite e0; eauto). destruct (bdelete_correct b search_term0); eauto. rewrite H. rewrite partition_filter_neq. eapply filter_negb_Prefix; eauto; reflexivity. + simpl. rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST containerCorrect). simpl. rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1. pose proof (KeyBasedPartition_fst_singleton_None key0 (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton. 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; eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey, empty_In. unfold XMap.fold; rewrite !fold_1. rewrite <- TrieBag_enumerateOK''' at 1. unfold TrieBag_bfind_matcher, IsPrefix. f_equiv. intros; eapply TrieOK_subtrie_filter; simpl in *; eauto using Proper_negb_KeyBasedPartitioningFunction. intros; eapply TrieOK_distinct_subtries'; eauto. exact (XMap.is_bst _). } { rewrite <- (app_nil_l st) at 2. revert containerCorrect. unfold TrieBagRepInv; remember [] as l; clear Heql; revert l. eapply Trie_delete_ind; intros; subst; simpl. - destruct (bdelete_correct (TrieNode trie) search_term0); eauto. destruct trie; simpl. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite e0 in H. rewrite partition_filter_eq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite filter_app. replace deletedItems with (fst (bdelete b search_term0)) by (simpl in *; rewrite e0; eauto). destruct (bdelete_correct b search_term0); eauto. rewrite H2, partition_filter_eq; simpl. rewrite <- app_nil_r at 1. f_equiv. + inversion containerCorrect; subst. revert H7; clear. induction (benumerate b); simpl; eauto. unfold TrieBag_bfind_matcher, IsPrefix. intros; case_eq (Prefix_dec F.eq_dec (projection a) l); simpl; intros. find_if_inside; simpl; rewrite IHl0; eauto. rewrite app_nil_r, H; simpl; eauto. rewrite andb_false_r; eauto. find_if_inside. simpl; rewrite app_nil_r, H; simpl. assert (Prefix (projection a) l) by (eexists nil; rewrite app_nil_r; eauto). rewrite <- IsPrefix_iff_Prefix in H0; simpl in *; rewrite H in H0; congruence. assert (Prefix (projection a) l) by (eexists nil; rewrite app_nil_r; eauto). rewrite <- IsPrefix_iff_Prefix in H0; simpl in *; rewrite H in H0; congruence. + inversion containerCorrect; subst. rewrite TrieBag_enumerateOK' at 1; eauto. rewrite app_nil_r. intros; eapply H9. eapply (@XMap.elements_2 _ (XMap.Bst H6)); eauto. - rewrite e2 in H; simpl in *. destruct trie; simpl in *. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite partition_filter_eq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite !filter_app; simpl. f_equiv. + replace deletedItems with (fst (bdelete b search_term0)) by (rewrite e0; eauto). destruct (bdelete_correct b search_term0); eauto. rewrite H1, partition_filter_eq, app_nil_r. inversion containerCorrect; subst. intros; eapply filter_Prefix; eauto; reflexivity. + rewrite (H (l ++ [key0])); simpl; eauto. rewrite partition_filter_eq. rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST containerCorrect). simpl. apply find_2 in e1. pose proof (KeyBasedPartition_fst_singleton key0 subtrie (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton. 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 flatten_filter. rewrite !map_app, fold_empty, !map_map. rewrite flatten_app. rewrite <- app_nil_r at 1. f_equiv. * unfold TrieBag_benumerate; rewrite flatten_filter, map_map, <- app_assoc; reflexivity. * rewrite <- filter_remove_key; eauto. 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). eauto. simpl; eauto. - destruct trie; simpl in *. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite partition_filter_eq. rewrite Permutation_benumerate_fold_left, flatten_app; simpl. rewrite !filter_app. rewrite <- app_nil_r at 1. f_equiv. + replace deletedItems with (fst (bdelete b search_term0)) by (rewrite e0; eauto). destruct (bdelete_correct b search_term0); eauto. rewrite H0, partition_filter_eq, app_nil_r. eapply filter_Prefix; eauto. + simpl. rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto. rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST containerCorrect). rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1. pose proof (KeyBasedPartition_fst_singleton_None key0 (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton. 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; eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey, empty_In. simpl. 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). rewrite <- filter_remove_key, flatten_filter, map_map; eauto. } } { unfold TrieBag_bfind_matcher; simpl. unfold TrieBagRepInv. pattern container, (@nil X.t) ; apply Trie_ind'; simpl; intros. unfold TrieBag_benumerate; simpl. intros; inversion containerCorrect; subst. case_eq (bdelete b search_term); simpl; intros. destruct (bdelete_correct b search_term); eauto. rewrite H0 in H1, H5; simpl in H1, H5. rewrite (Permute_XMapfold_cons m [b]), Permute_XMapfold_cons with (l := [b0]). rewrite !map_app, !flatten_app, !partition_app; simpl. rewrite !app_nil_r. split. - rewrite H1; f_equiv. rewrite !XMapfold_eq. setoid_rewrite (fold_pair (XMap.Bst H3)); simpl. rewrite fold_spec_right. pose fold_spec_right as e; unfold XMap.fold in e; rewrite (e _ (XMap.Bst H3)); clear e. assert (forall k trie, InA (@XMap.eq_key_elt _) (k, trie) (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |})) -> Permutation (TrieBag_benumerate (snd (Trie_delete' trie search_term))) (snd (List.partition (fun item : TItem => bfind_matcher search_term item) (TrieBag_benumerate trie)))). { intros; eapply H; eauto using elements_mapsto_iff. pose elements_mapsto_iff as e; unfold XMap.MapsTo in e; rewrite (e _ (XMap.Bst H3)); clear e. rewrite <- InA_rev; eauto with typeclass_instances. eapply H6. eapply (@elements_mapsto_iff _ (XMap.Bst H3)). eapply InA_rev; eauto with typeclass_instances. } generalize H7; clear. assert (NoDupA (@XMap.eq_key _) (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |}))) by (apply NoDupA_rev; eauto with typeclass_instances; eapply XMap.elements_3w). revert H. induction (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |})); simpl; intros; eauto. unfold uncurry. pose fold_add as e; unfold XMap.fold, XMap.add in e; simpl in e. rewrite e; clear e. rewrite !map_app, !flatten_app, !partition_app; simpl. unfold TrieBag_benumerate in H7. rewrite H7 with (k := fst a); f_equiv; eauto. rewrite <- IHl; eauto. inversion H; eauto; intros; eapply H7; simpl; econstructor 2; eauto. econstructor; destruct a; simpl; reflexivity. eauto with typeclass_instances. eauto with typeclass_instances. eauto using transpose_neqkey_Trie_enumerate_app. inversion H; subst; intro; apply H2. unfold XMap.In, In0 in H0. revert H0; clear; induction l; simpl. + intros; destruct H0; inversion H. + intros; destruct H0. pose add_mapsto_iff as e; unfold XMap.add, XMap.MapsTo in e; simpl in e; rewrite e in H; clear e. intuition. * econstructor 1; symmetry; apply H. * eauto. - rewrite H5, Permutation_app_swap; f_equiv. rewrite !XMapfold_eq. setoid_rewrite (fold_pair (XMap.Bst H3)); simpl. rewrite fold_spec_right. pose fold_spec_right as e; unfold XMap.fold in e; rewrite (e _ (XMap.Bst H3)); clear e. assert (forall k trie, InA (@XMap.eq_key_elt _) (k, trie) (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |})) -> Permutation ((fst (Trie_delete' trie search_term))) (fst (List.partition (fun item : TItem => bfind_matcher search_term item) (TrieBag_benumerate trie)))). { intros; eapply H; eauto using elements_mapsto_iff. pose elements_mapsto_iff as e; unfold XMap.MapsTo in e; rewrite (e _ (XMap.Bst H3)); clear e. rewrite <- InA_rev; eauto with typeclass_instances. eapply H6. eapply (@elements_mapsto_iff _ (XMap.Bst H3)). eapply InA_rev; eauto with typeclass_instances. } generalize H7; clear. assert (NoDupA (@XMap.eq_key _) (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |}))) by (apply NoDupA_rev; eauto with typeclass_instances; eapply XMap.elements_3w). revert H. induction (rev (XMap.elements (elt:=Trie) {| XMap.this := m; XMap.is_bst := H3 |})); simpl; intros; eauto. unfold uncurry. rewrite !map_app, !flatten_app, !partition_app; simpl. unfold TrieBag_benumerate in H7. rewrite H7 with (k := fst a); f_equiv; eauto. rewrite <- IHl; eauto. inversion H; eauto. econstructor; destruct a; simpl; reflexivity. } 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