proposition: Lemma Trie_add_Correct : forall trie item st1 st2, eqlistA X.eq (projection item) (st2 ++ st1) -> TrieOK trie st2 -> Permutation (TrieBag_benumerate (Trie_add trie st1 item)) (item :: TrieBag_benumerate trie).
proof: Proof. intros trie item st1; eapply Trie_add_ind; intros; subst. - destruct trie0; simpl. unfold TrieBag_benumerate; simpl. rewrite !XMapfold_eq, !fold_1 by eauto. rewrite Permutation_benumerate_fold_left. simpl; rewrite binsert_enumerate; eauto. simpl; constructor. symmetry. rewrite Permutation_benumerate_fold_left; simpl. reflexivity. - destruct trie0; simpl. unfold TrieBag_benumerate; simpl. replaceXMapfold. replaceXMapfold. unfold XMap.fold at 2. rewrite Permutation_KeyBasedPartition with (key := key0) (bst_m := SubTrieMapBST H1). pose proof (@partition_after_KeyBasedPartition_and_add _ key0 (Trie_add subtrie st' item0) (XMap.Bst (SubTrieMapBST H1))) as part_add. rewrite Partition_fold at 1; (eauto using part_add, Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). apply find_2 in e0. pose proof (KeyBasedPartition_fst_singleton key0 subtrie (XMap.Bst (SubTrieMapBST H1)) e0) as singleton. pose proof (add_Equal_simple singleton key0 (Trie_add subtrie st' item0)) 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_Equal_simpl (eqA := @Permutation BagType) singleton) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite (fold_Equal_simpl (multiple_adds _ _ _ _)) by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite !fold_add by (eauto using Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey, empty_In). rewrite fold_empty. rewrite !map_app. unfold TrieBag_benumerate in H. rewrite !flatten_app, (H (st2 ++ [key0])); eauto. rewrite <- app_assoc; simpl; eauto. inversion H1; subst; eauto. - destruct trie0; simpl. unfold TrieBag_benumerate; simpl. replaceXMapfold. replaceXMapfold. pose proof (@partition_after_KeyBasedPartition_and_add _ key0 (Trie_add TrieBag_bempty st' item0) (XMap.Bst (SubTrieMapBST H1))) as part_add. pose proof (partition_Partition_simple _ (KeyBasedPartitioningFunction Trie key0) (KeyBasedPartitioningFunction_Proper _ _) (XMap.Bst (SubTrieMapBST H1))) as part. rewrite Partition_fold at 1; (eauto using part_add, Permutation_Equivalence, Tries_enumerate_app_Proper, Tries_enumerate_app_transpose_neqkey). rewrite Partition_fold with (m := {| XMap.this := m; XMap.is_bst := H3 |} ); (eauto using part, 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. rewrite (H (st2 ++ [key0])); simpl. unfold TrieBag_benumerate; simpl. rewrite benumerate_bempty_nil; simpl. reflexivity. rewrite <- app_assoc; eauto. econstructor; eauto using bempty_RepInv. + rewrite benumerate_bempty_nil in *; simpl in *; intuition. + intros; exfalso; eapply empty_1; eauto. + intro H4. destruct H4. apply (@partition_iff_1 _ (KeyBasedPartitioningFunction Trie key0) (Proper_KeyBasedPartitioningFunction key0) {| XMap.this := m; XMap.is_bst := SubTrieMapBST H1 |} _ key0 x (refl_equal _)) in H4; intuition. apply find_1 in H5; eauto; simpl in *; congruence. 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