proposition: Lemma filter_remove_key : forall key' m l st' search_term, (forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) (elements (remove key' (XMap.this m))) -> TrieOK subtrie (l ++ [k])) -> Permutation (flatten (List.map (fun x : BagType => List.filter (TrieBag_bfind_matcher (Some (l ++ key' :: st'), search_term)) (benumerate x)) (XMap.fold (fun (_ : key) (trie : Trie) (a : list BagType) => Trie_enumerate trie ++ a) (XMap.remove (elt:=Trie) key' m ) []))) [].
proof: Proof. intros; unfold XMap.fold; rewrite fold_1; simpl; eauto. 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 (l ++ [k0]) (projection item)) by (rewrite Heqbags'; intuition). generalize (fun k bag => @TrieBag_enumerateOK (elements (remove key' (XMap.this m))) l bags' k bag H H0). clear H0. assert (bags = List.map (@snd _ _) bags') as H0 by (rewrite Heqbags', Heqbags; reflexivity); rewrite H0; clear H0. assert (forall (k : X.t) (subtrie : Trie), InA (PX.eqke (elt:=Trie)) (k, subtrie) (elements (remove key' (XMap.this m))) -> ~X.eq k key') by (intros; rewrite <- (@elements_mapsto_iff _ (XMap.Bst (remove_bst key' (XMap.is_bst m)))) in H0; apply remove_mapsto_iff in H0; intuition). 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 (elements (remove key' (XMap.this m))); simpl. - induction bags'; simpl; intros; eauto. rewrite IHbags'; eauto. 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) (l ++ key' :: st')); eauto. intros. assert (Prefix (l ++ [k]) (l ++ key' :: st')). etransitivity; eauto. pose proof (Prefix_app_inv _ _ _ H2). destruct H4; inversion H4; subst. exfalso; eapply H3; eauto. - intros. rewrite <- (IHl0 ((List.map (fun a' => (fst a, a')) (Trie_enumerate (snd a))) ++ bags')); eauto. rewrite map_app, map_map, map_id; reflexivity. intros. 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 (remove_bst _ (XMap.is_bst m)). 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