proposition: Lemma TrieBag_enumerateOK : forall l st1 (bags : list (key * BagType)) k bag, (forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) l -> TrieOK subtrie (st1 ++ [k])) -> (forall (k : key) (bag : BagType), List.In (k, bag) bags -> forall (item: TItem), List.In item (benumerate bag) -> Prefix (st1 ++ [k]) (projection item)) -> List.In (k, bag) (fold_left (fun (a : list (key * BagType)) (p : key * Trie) => (List.map (fun bag => (fst p, bag)) (Trie_enumerate (snd p)) ++ a)) l bags) -> forall (item: TItem), List.In item (benumerate bag) -> Prefix (st1 ++ [k]) (projection item).
proof: Proof. induction l; simpl; eauto. - intros. rewrite <- In_fold_left_map_split' in H1. rewrite <- app_assoc in H1. apply in_app_or in H1; intuition eauto. destruct a as [k' t]; simpl in *. assert (InA (PX.eqke (elt:=Trie)) (k', t) ((k', t) :: l)) by (econstructor; eauto || typeclasses eauto). generalize (H k' t H1). assert (k = k') by (revert H3; clear; induction (Trie_enumerate t); simpl; intro; intuition; injections; eauto). subst. apply in_map with (f := snd) in H3; rewrite map_map, map_id in H3. remember (st1 ++ [k']). setoid_rewrite <- Heql0. generalize bag H2 H3; clear. eapply (fun P H => @Trie_enumerate_ind P H t l0). simpl; intros. destruct trie; simpl in *. rewrite !XMapfold_eq, !fold_1 in H3; eauto. rewrite <- In_fold_left_split' in H3. apply in_app_or in H3; intuition. + simpl in H1; intuition; injections; subst. inversion H0; 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 H0))); eauto. apply in_map with (f := snd) in H5; rewrite map_map, map_id in H5; simpl in *; eauto. } assert (forall k' trie, InA (XMap.eq_key_elt (elt:=Trie)) (k', trie) (elements m) -> TrieOK trie (st ++ [k'])). { revert H0; clear. intros; inversion H0; 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 H1 H4; clear. induction (elements m); simpl; intros. * intuition. * rewrite <- In_fold_left_split' in H1. apply in_app_or in H1; 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. simpl in H. apply in_map_iff; eauto. eapply H4; econstructor; eauto. reflexivity. eapply IHl; eauto. + eapply IHl; eauto. apply In_fold_left_map_split'; 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