proposition: Lemma TrieBag_enumerateOK1 : forall l st1 search_term bags, (forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) l -> TrieOK subtrie (st1 ++ [k])) -> (forall (k : X.t) (bag : BagType) item, List.In (k, bag) bags -> List.In item (benumerate (Bag := TBag) bag) -> Prefix (st1 ++ [k]) (projection item)) -> Permutation (List.filter (TrieBag_bfind_matcher (Some st1, search_term)) (flatten (List.map (fun p => benumerate (snd p)) (fold_left (fun (a : list (key * BagType)) (p : key * Trie) => (List.map (fun bag => (fst p, bag)) (Trie_enumerate (snd p)) ++ a)) l bags)))) [].
proof: Proof. induction l; simpl; eauto. - induction bags; simpl in *; intros; eauto. rewrite filter_app, IHbags; eauto. destruct a. rewrite app_nil_r. simpl. generalize (fun item => H0 _ _ item (or_introl (refl_equal _))) ; clear; simpl. induction (benumerate b); simpl; eauto. intros. unfold TrieBag_bfind_matcher, IsPrefix; simpl. destruct (Prefix_dec F.eq_dec (projection a) st1); simpl in *. find_if_inside; eauto. intros. pose proof (H _ (or_introl (refl_equal _))). exfalso. generalize st1 p H0; clear. induction (projection a); simpl. + destruct st1; simpl; intros; destruct H0; inversion H. + destruct st1; simpl; try congruence. intros; inversion p; inversion H. intros; eapply (IHl st1). destruct p; simpl in *; inversion H; subst; eexists; eauto. intros; destruct H0; inversion H; subst. eexists; eauto. + eauto. - intros; rewrite IHl; eauto. intros. apply in_app_or in H1; intuition eauto. destruct a. assert (InA (PX.eqke (elt:=Trie)) (t, t0) ((t, t0) :: l)) by (econstructor; eauto || typeclasses eauto). apply H in H1; simpl in *. assert (k = t). { revert H3; clear; induction (Trie_enumerate t0); simpl; intros; intuition; congruence. } subst. revert H2 H3 H1. clear. eapply (fun P H => @Trie_enumerate_ind P H t0 (st1 ++ [t])). simpl; intros. destruct trie; simpl in *. rewrite !XMapfold_eq, !fold_1 in H3; eauto. rewrite <- In_fold_left_split, map_app in H3. apply in_app_or in H3; intuition. + simpl in H0; intuition; injections; subst. inversion H1; subst. apply H6 in H2; revert H2; clear. * revert st; induction (projection item); simpl. intros; inversion H2; subst. eexists nil; rewrite app_nil_r. constructor; symmetry; eauto. eexists nil; simpl; rewrite app_nil_r; symmetry; eauto. + assert (forall (k : key) (trie' : Trie), InA (XMap.eq_key_elt (elt:=Trie)) (k,trie') (elements m) -> List.In item (benumerate bag) -> List.In (t, bag) (List.map (fun bag0 : BagType => (t, bag0)) (Trie_enumerate trie')) -> TrieOK trie' (st ++ [k]) -> Prefix (st ++ [k]) (projection item)). { intros; eapply H; eauto. eapply (@XMap.elements_2 _ (XMap.Bst (SubTrieMapBST H1))); eauto. } assert (forall k' trie, InA (XMap.eq_key_elt (elt:=Trie)) (k', trie) (elements m) -> TrieOK trie (st ++ [k'])). { revert H1; clear. intros; inversion H1; subst. apply (@XMap.elements_2 _ (XMap.Bst H4)) in H. apply H7 in H; simpl in H; eauto. } generalize st bag item b t H2 H3 H0 H4; clear. induction (elements m); simpl; intros. * intuition. * rewrite <- In_fold_left_split, map_app in H0. apply in_app_or in H0; intuition eauto. assert (forall a b c, Prefix (a ++ [b]) c -> Prefix a c). { clear; intros; destruct H. exists (b :: x); rewrite <- app_assoc in H; eauto. } destruct a; eapply H0; eapply H3. econstructor; reflexivity. eauto. rewrite app_nil_r in H. eauto. eapply H4; econstructor; eauto. reflexivity. eapply IHl; 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