proposition: Lemma Trie_enumerate_RepInv : forall trie l, TrieOK trie l -> forall item, List.In item (Trie_enumerate trie) -> RepInv item.
proof: Proof. intros trie l; pattern trie, l; eapply Trie_ind'; simpl; intros. inversion H0; subst; clear H0. rewrite Permute_XMapfold_cons in H1; apply List.in_app_or in H1; intuition. - rewrite XMapfold_eq in H0. pose fold_spec_right as e; unfold XMap.fold in e; rewrite (e _ (XMap.Bst H5)) in H0; clear e. assert (exists k trie, List.In (k, trie) (XMap.elements (elt := Trie) {| XMap.this := m; XMap.is_bst := H5 |}) /\ List.In item (Trie_enumerate trie)). { revert H0; clear. induction (XMap.elements (elt := Trie) {| XMap.this := m; XMap.is_bst := H5 |}); simpl; intros; intuition. rewrite fold_right_app in H0; simpl in H0. rewrite fold_left_rev_right in H0; simpl in H0. unfold uncurry in *. rewrite Permutation_app_fold_left in H0; apply in_app_or in H0; intuition. apply in_app_or in H; intuition. destruct a; eauto. destruct IHl as [k [trie' [In_k In_trie] ] ]. rewrite fold_left_rev_right; eauto. eexists; eauto. } destruct H1 as [k [trie' [In_k In_trie'] ] ]. eapply (H k trie' l0); eauto. eapply elements_mapsto_iff with (m := XMap.Bst H5). eapply InA_In; eauto. econstructor; reflexivity. apply H8. eapply elements_mapsto_iff with (m := XMap.Bst H5). eapply InA_In; eauto. econstructor; reflexivity. - simpl in H0; intuition; subst; 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