proposition: Lemma filter_negb_remove : forall key m, XMap.Equal (filter (fun (k : XMap.key) (e : Trie) => negb (KeyBasedPartitioningFunction Trie key k e)) m) (XMap.remove key m).
proof: Proof. unfold XMap.Equal; intros. destruct (X.eq_dec key0 y). - rewrite remove_eq_o; eauto. rewrite <- e; unfold filter; clear y e. destruct m; unfold XMap.fold; rewrite fold_1; simpl; eauto. assert (XMap.find (elt:=Trie) key0 (XMap.empty Trie) = None). { rewrite <- not_find_in_iff. intro H; destruct H; simpl in *; eapply empty_1; eauto. } revert H. remember (XMap.empty Trie); generalize t; clear Heqt. induction (elements this); intros; simpl. + eauto. + eapply IHl. case_eq (negb (KeyBasedPartitioningFunction Trie key0 (fst a) (snd a))); intros; eauto. rewrite add_neq_o; eauto. intro; unfold KeyBasedPartitioningFunction in *. case_eq (F.eq_dec (fst a) key0); intros; rewrite H2 in H0; simpl in *; try congruence. - rewrite remove_neq_o by eauto. destruct m; unfold filter, XMap.fold; rewrite fold_1; simpl; eauto. case_eq (XMap.find (elt:=Trie) y {| XMap.this := this; XMap.is_bst := is_bst |}). + intros; apply find_2 in H. pose (@elements_mapsto_iff _ (XMap.Bst is_bst)) as H2; simpl in H2; unfold XMap.MapsTo in H2; simpl in H2; rewrite H2 in H; unfold XMap.elements in H; simpl in H; clear H2. assert (InA (XMap.eq_key_elt (elt:=Trie)) (y, t) (elements this) \/ InA (XMap.eq_key_elt (elt:=Trie)) (y, t) (XMap.elements (XMap.empty Trie))) by eauto. assert (forall key' v, XMap.MapsTo key' v (XMap.empty Trie) -> ~ X.eq key' key0) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (forall key' v, XMap.MapsTo key' v (XMap.empty Trie) -> ~ InA X.eq key' (List.map fst (elements this))) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (forall key' v, InA X.eq key' (List.map fst (elements this)) -> ~ XMap.MapsTo key' v (XMap.empty Trie)) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (NoDupA X.eq (List.map fst (XMap.elements (elt:=_) (XMap.Bst is_bst)))). { pose proof (@XMap.elements_3w _ (XMap.Bst is_bst)). unfold XMap.eq_key, PX.eqk in H4. revert H4; clear; induction (XMap.elements (XMap.Bst is_bst)); intros; constructor; eauto; inversion H4; subst; [ | apply IHl; eauto]. intro; apply H1; revert H; clear; induction l; intros; inversion H; subst. constructor; eauto. constructor 2; eauto. } unfold XMap.elements in H4; simpl in H4. revert H1 H0 H2 H3 H4. remember (XMap.empty Trie) as t'; generalize t'; clear Heqt' H. induction (elements this); intros; simpl. destruct t'0; apply find_1; eauto. apply elements_mapsto_iff; simpl in H0; intuition. inversion H. eapply IHl; simpl in *; intuition. * unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. destruct a; simpl in *. eapply XMap.add_3 in H0; eauto; match goal with | [ H : X.eq _ _ |- _ ] => rewrite H; auto end. * unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. eapply XMap.add_3 in H0; eauto; match goal with | [ H : X.eq _ _ |- _ ] => rewrite H; auto end. * inversion H; subst. destruct H5; destruct a; simpl in *; subst. right; rewrite <- elements_mapsto_iff; simpl. unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec k key0); simpl in *; eauto; try congruence. rewrite e in H0; symmetry in H0; intuition. apply add_1; eauto; try symmetry; eauto. eauto; match goal with | [ H : X.eq _ _ |- _ ] => rewrite H; auto end. * right; rewrite <- elements_mapsto_iff; simpl. unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. rewrite <- elements_mapsto_iff in *; simpl; eauto. rewrite <- elements_mapsto_iff in *; simpl; eauto. apply add_2; eauto; intuition; eapply H2; [ eassumption | left; symmetry; auto ]. * unfold KeyBasedPartitioningFunction in *. destruct (F.eq_dec (fst a) key0); simpl in *; eauto. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H0); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H3; eauto. * unfold KeyBasedPartitioningFunction in *. destruct (F.eq_dec (fst a) key0); simpl in *; eauto. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H0); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H3; eauto. * unfold KeyBasedPartitioningFunction in *. destruct (F.eq_dec (fst a) key0); simpl in *; eauto. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H5); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H3; eauto. * unfold KeyBasedPartitioningFunction in *. destruct (F.eq_dec (fst a) key0); simpl in *; eauto. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H5); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H3; eauto. * inversion H4; eauto. * inversion H4; eauto. + intros; apply not_find_in_iff in H. assert (forall v, ~ InA (XMap.eq_key_elt (elt:=Trie)) (y, v) (XMap.elements (XMap.Bst is_bst)) /\ ~ InA (XMap.eq_key_elt (elt:=Trie)) (y, v) (XMap.elements (XMap.empty Trie))). { unfold not in*; split; intros. rewrite <- elements_mapsto_iff in H0. apply H; eexists v; simpl in *; apply H0. rewrite <- elements_mapsto_iff in H0. eapply XMap.empty_1; eauto. } assert (forall key' v, XMap.MapsTo key' v (XMap.empty Trie) -> ~ X.eq key' key0) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (forall key' v, XMap.MapsTo key' v (XMap.empty Trie) -> ~ InA X.eq key' (List.map fst (elements this))) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (forall key' v, InA X.eq key' (List.map fst (elements this)) -> ~ XMap.MapsTo key' v (XMap.empty Trie)) by (unfold not; intros; eapply XMap.empty_1; eauto). assert (NoDupA X.eq (List.map fst (XMap.elements (elt:=_) (XMap.Bst is_bst)))). { pose proof (@XMap.elements_3w _ (XMap.Bst is_bst)). unfold XMap.eq_key, PX.eqk in H4. revert H4; clear; induction (XMap.elements (XMap.Bst is_bst)); intros; constructor; eauto; inversion H4; subst; [ | apply IHl; eauto]. intro; apply H1; revert H; clear; induction l; intros; inversion H; subst. constructor; eauto. constructor 2; eauto. } unfold XMap.elements in H4; simpl in H4, H0. unfold XMap.elements at 1 in H0; simpl in H0. rewrite <- not_find_in_iff. revert H1 H0 H2 H3 H4. remember (XMap.empty Trie) as t'; generalize t'; clear Heqt' H. induction (elements this); intros; simpl. unfold not; intros; destruct H as [x H]. apply (proj2 (H0 x)). rewrite <- elements_mapsto_iff; eassumption. eapply IHl; simpl in *; intuition. * unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. destruct a; simpl in *. eapply XMap.add_3 in H; eauto; try match goal with | [ H : X.eq _ _ |- _ ] => rewrite H; solve [ eauto ] end. * apply (proj1 (H0 v)); eauto. * unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. apply (proj2 (H0 v)); eauto. rewrite <- elements_mapsto_iff in H. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H); intuition; subst. apply (proj1 (H0 (snd a))); econstructor. constructor; eauto; simpl; symmetry; assumption. apply (proj2 (H0 v)); rewrite <- elements_mapsto_iff; eauto. * unfold KeyBasedPartitioningFunction in *. destruct (X.eq_dec (fst a) key0); simpl in *; eauto; try congruence. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H2; eauto. * unfold KeyBasedPartitioningFunction in *. destruct (F.eq_dec (fst a) key0); simpl in *; eauto. pose proof (proj1 (add_mapsto_iff _ _ _ _ _) H5); intuition; subst. inversion H4; subst; eauto. rewrite H6 in H9; eauto. eapply H3; eauto. * inversion H4; 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