proposition: Corollary TrieBag_enumerateOK''' : forall l st1 key' st' search_term, (forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) l -> TrieOK subtrie (st1 ++ [k])) -> ( forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) l -> ~X.eq k key') -> Permutation (List.filter (fun a => negb (TrieBag_bfind_matcher (Some (st1 ++ key' :: st'), search_term) a)) (flatten (List.map benumerate (fold_left (fun (a : list (BagType)) (p : key * Trie) => (Trie_enumerate (snd p)) ++ a) l [ ])))) (flatten (List.map benumerate (fold_left (fun (a : list (BagType)) (p : key * Trie) => (Trie_enumerate (snd p)) ++ a) l [ ]))).
proof: Proof. intros. remember (@nil BagType) as bags. remember (@nil (key * BagType)) as bags'. assert (forall (k0 : key) (bag0 : BagType), List.In (k0, bag0) bags' -> forall item : TItem, List.In item (benumerate bag0) -> Prefix (st1 ++ [k0]) (projection item)) by (rewrite Heqbags'; intuition). generalize (fun k bag => @TrieBag_enumerateOK l st1 bags' k bag H H1). clear H1. assert (bags = List.map (@snd _ _) bags') as H1 by (rewrite Heqbags', Heqbags; reflexivity); rewrite H1; clear H1. assert (forall (k : X.t) b, InA (PX.eqke (elt:=BagType)) (k, b) bags' -> ~X.eq k key') by (intros; rewrite Heqbags' in *; inversion H1). generalize bags' H H0 H1; clear; induction l; simpl; intros. - induction bags'; simpl; intros; eauto. rewrite filter_app, IHbags'; eauto; f_equiv. destruct a; simpl in *. assert (~ X.eq k key') by (intros; eapply H1; econstructor; eauto || typeclasses eauto). generalize (fun item => H2 k b (or_introl (refl_equal _)) item) H3; clear. induction (benumerate b); simpl; eauto; intros. pose proof (H _ (or_introl (refl_equal _))). rewrite <- IsPrefix_iff_Prefix in H0. unfold TrieBag_bfind_matcher, IsPrefix in *; simpl in *. case_eq (Prefix_dec F.eq_dec (projection a) (st1 ++ key' :: st')); eauto. intros. assert (Prefix (st1 ++ [k]) (st1 ++ key' :: st')) by (etransitivity; eauto). pose proof (Prefix_app_inv _ _ _ H2). destruct H4; inversion H4; subst. exfalso; eapply H3; eauto. simpl; intros; f_equiv. generalize (fun item In_item => H item (or_intror In_item)). generalize H3; clear; induction l; simpl; intros; eauto. pose proof (H _ (or_introl (refl_equal _))). destruct (Prefix_dec F.eq_dec (projection a) (st1 ++ key' :: st')); simpl in *; eauto. intros. assert (Prefix (st1 ++ [k]) (st1 ++ key' :: st')) by (etransitivity; eauto). apply Prefix_app_inv in H1. destruct H1; simpl in H1; inversion H1; subst. intuition. try rewrite IHl; eauto. intros; try eapply H2; eauto. constructor 2; eauto. - intros. pose proof (IHl ((List.map (fun a' => (fst a, a')) (Trie_enumerate (snd a))) ++ bags')) as H'. rewrite map_app, map_map, map_id in H'. rewrite <- H' at 2; clear H'; intros. rewrite !flatten_filter; eauto. destruct a; eapply H; econstructor 2; eauto. eapply H0; eauto. apply InA_app in H3; intuition eauto. assert (~X.eq k (fst a)) by (destruct a; intro; eapply H0; [ constructor; typeclasses eauto | simpl in *; repeat match goal with | [ H : X.eq ?k _ |- _ ] => rewrite H in *; clear H end; reflexivity ]). apply H3; revert H5; clear; induction (Trie_enumerate (snd a)); intros; inversion H5; subst; eauto. destruct H0; simpl in *; eauto. eapply H2; 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