proposition: Lemma RangeTreeBag_BagDeleteUpdateCorrect' : forall (container : RangeTreeBag) keys f, Permutation (List.map snd (Raw.elements (fold_right (fun (y : TKey * BagType) (x : RangeTreeBag) => add (fst y) (f (snd y)) x) container (RangeTreeBag_btraverse container keys)))) (List.map snd (List.map (fun (key_bag : TKey * BagType) => if Range_InRange keys (fst key_bag) then (fst key_bag, f (snd key_bag)) else key_bag) (RangeTreeBag_bcollect container))).
proof: Proof. intros; eapply Permutation_InA_cons; intros. { pose proof (RangeTreeBag_bcollect_nodup container). remember (RangeTreeBag_bcollect container) as ls. clear Heqls. induction ls. - constructor. - inversion H. subst. specialize (IHls H3). clear H3. simpl. constructor; eauto; intro. apply H2. clear H2 IHls H. destruct a. simpl in *. induction ls. inversion H0. simpl in *. inversion H0; subst. apply InA_cons_hd. unfold eq_key, Raw.Proofs.PX.eqk in *. clear H0 IHls. repeat find_if_inside; auto. apply InA_cons_tl. eauto. } { apply elements_3w. } rewrite (InA_map_perm _ _ _ (Permutation_partition (fun x => Range_InRange keys (fst x)) _)). rewrite InA_map_app. split; intro H. { rewrite map_if_filter_eq. assert (forall P Q R : Prop, (P -> R) -> P \/ Q -> R \/ Q) as E by tauto; eapply E; clear E. eapply @InA_map_forall with (eqA := eq_key_elt (elt:=BagType)) (ls := (List.filter (fun x : TKey * BagType => Range_InRange keys (fst x)) (RangeTreeBag_btraverse container keys))); try solve [ apply eqke_equiv ]. { unfold Proper, respectful, eq_key_elt, Raw.Proofs.PX.eqke; intros; destruct x; destruct y. unfold eq_key_elt, Raw.Proofs.PX.eqke in H0; destruct H0; simpl in *; subst. destruct (Range_InRange keys k0); tauto. } { pose proof (fun x => proj2 (InA_InRange_bcollect_btraverse (fst x) (snd x) keys container)). intro a. replace a with (fst a, snd a). generalize dependent a. exact H0. destruct a. reflexivity. } destruct (Range_InRange keys k) eqn: eq. - left. assert (InA (eq_key_elt (elt:=BagType)) (k, v) (Raw.elements (fold_right (fun (y : TKey * BagType) (x : RangeTreeBag) => add (fst y) (f (snd y)) x) RangeTreeBag_bempty (RangeTreeBag_btraverse container keys)))). { pose proof (fun k b => RangeTreeBag_btraverse_correct container keys k b) as Htraverse. pose proof (RangeTreeBag_btraverse_nodup container keys) as Htraverse_nodup. remember (RangeTreeBag_btraverse container keys) as ls. clear Heqls. generalize dependent container. induction ls; intros. - simpl in *. rewrite Raw.Proofs.elements_mapsto in H. specialize (proj2 (Htraverse k v) (conj H eq)). inversion 1. - destruct a. inversion Htraverse_nodup; subst. specialize (IHls H3 (remove t0 container)); clear H3. simpl in H. rewrite Raw.Proofs.elements_mapsto in *. pose proof (F.add_mapsto_iff). unfold MapsTo, add in H0. simpl in H0. apply H0 in H. clear H0. intuition. simpl. rewrite H1. apply Raw.Proofs.add_1. assumption. simpl. apply Raw.Proofs.add_2. intuition. rewrite <- Raw.Proofs.elements_mapsto. apply IHls. generalize H H1; clear. induction ls; intros; simpl in *. + destruct container. apply Raw.Proofs.remove_2; eauto. + pose proof (F.add_mapsto_iff). unfold MapsTo, add in H0. simpl in H0. apply H0 in H1. apply H0. clear H0. intuition. + setoid_rewrite remove_mapsto_iff. intuition. apply H2. symmetry in H3. eapply InA_eqke_eqk; eauto. eapply Htraverse. constructor 2. assumption. eapply Htraverse. constructor 2. eassumption. specialize (proj2 (Htraverse k0 b0) (conj H5 H4)). inversion 1; eauto; destruct H7; simpl in *; symmetry in H7; tauto. } clear H. rename H0 into H. pose proof (fun k b => proj1 (RangeTreeBag_btraverse_correct container keys k b)) as Htraverse. pose proof (RangeTreeBag_btraverse_nodup container keys) as Htraverse_nodup. remember (RangeTreeBag_btraverse container keys) as ls; clear Heqls. induction ls. + simpl in *. inversion H. + simpl in *. rewrite Raw.Proofs.elements_mapsto in H. pose proof (F.add_mapsto_iff). unfold MapsTo, add in H0. simpl in H0. apply H0 in H. clear H0. intuition. erewrite InRange_Proper; eauto 2. rewrite eq. simpl. apply InA_cons_hd. unfold eq_key_elt, Raw.Proofs.PX.eqke in *. intuition. find_if_inside; simpl. apply InA_cons_tl. apply IHls. rewrite Raw.Proofs.elements_mapsto. assumption. destruct a. apply InA_ind_helper in Htraverse. intuition. inversion Htraverse_nodup. auto. apply IHls. rewrite Raw.Proofs.elements_mapsto. assumption. destruct a. apply InA_ind_helper in Htraverse. intuition. inversion Htraverse_nodup. auto. - right. pose proof (fun k b => proj1 (RangeTreeBag_btraverse_correct container keys k b)) as Htraverse. remember (RangeTreeBag_btraverse container keys) as ls; clear Heqls. induction ls. + simpl in *. unfold RangeTreeBag_bcollect. induction (Raw.elements container). inversion H. simpl. inversion H; subst; clear H. destruct H1; simpl in *. symmetry in H. erewrite InRange_Proper; eauto 2. rewrite eq; simpl. erewrite InRange_Proper; eauto 2. rewrite eq; simpl. constructor. unfold eq_key_elt, Raw.Proofs.PX.eqke. intuition. find_if_inside. simpl. constructor 2. apply IHl. assumption. apply IHl. assumption. + simpl in H. apply IHls. rewrite Raw.Proofs.elements_mapsto in *. pose proof (F.add_mapsto_iff). unfold MapsTo, add in H0. simpl in H0. apply H0 in H. clear H0. intuition. specialize (Htraverse (fst a) (snd a)). destruct Htraverse. constructor. destruct a; reflexivity. erewrite InRange_Proper in H2; eauto 2. congruence. destruct a. apply InA_ind_helper in Htraverse. intuition. } { destruct H as [H | H]. { rewrite map_if_filter_eq in H. pose proof (fun x => proj1 (InA_InRange_bcollect_btraverse (fst x) (snd x) keys container)) as InA_ct. eapply @InA_map_forall with (eqA := eq_key_elt (elt:=BagType)) (ls' := (List.filter (fun x : TKey * BagType => Range_InRange keys (fst x)) (RangeTreeBag_btraverse container keys))) in H; try solve [ apply eqke_equiv ]. pose proof (ListFacts.filter_map (fun x => Range_InRange keys (fst x)) (fun x => (fst x, f (snd x))) (RangeTreeBag_btraverse container keys)); simpl in H0; fold TKey in *; rewrite <- H0 in H; clear H0. rewrite filter_InA in H; try solve [ apply eqke_equiv ]. - destruct H as [H_in H_range]. pose proof (fun k b => proj1 (RangeTreeBag_btraverse_correct container keys k b)) as Htraverse. pose proof (RangeTreeBag_btraverse_nodup container keys) as Htraverse_nodup. remember (RangeTreeBag_btraverse container keys) as ls; clear Heqls InA_ct. induction ls as [ | [k' v'] ls']. + inversion H_in. + simpl in *; inversion H_in; clear H_in; subst. * rewrite Raw.Proofs.elements_mapsto in *. unfold eq_key_elt, Raw.Proofs.PX.eqke in H0. destruct H0. simpl in *. subst. apply Raw.Proofs.add_1; auto; symmetry; auto. * inversion Htraverse_nodup; subst. apply InA_ind_helper in Htraverse. destruct Htraverse as [Htraverse_s Htraverse_c]. specialize (IHls' H0 Htraverse_c H3); clear Htraverse_c. destruct (X.eq_dec k k'). { rewrite InA_Map in H0. destruct H0. exfalso. apply H2. rewrite InA_alt. exists x. destruct H. unfold eq_key_elt, Raw.Proofs.PX.eqke in H. destruct H. simpl in *. split. unfold eq_key, Raw.Proofs.PX.eqk. simpl. etransitivity; eauto; try symmetry; assumption. assumption. } { rewrite Raw.Proofs.elements_mapsto in *. apply Raw.Proofs.add_2; auto; intuition. } - unfold Proper, respectful; intros; apply InRange_Proper. unfold eq_key_elt, Raw.Proofs.PX.eqke in *; intuition. - unfold Proper, respectful; intros. unfold eq_key_elt, Raw.Proofs.PX.eqke in *; intuition; simpl. f_equiv. assumption. - intro. replace a with ((fst a, snd a)). apply InA_ct. destruct a; auto. } { rewrite map_if_filter_neg, map_id, filter_InA in H; try solve [ apply eqke_equiv ]. - destruct H as [H_in H_range]. pose proof (fun k b => proj1 (RangeTreeBag_btraverse_correct container keys k b)) as Htraverse. remember (RangeTreeBag_btraverse container keys) as ls; clear Heqls. induction ls as [ | [k'' v''] ls']. + apply H_in. + apply RangeTreeBag_bcollect_correct in H_in. apply InA_ind_helper in Htraverse. destruct Htraverse as [Htraverse_s Htraverse_c]. specialize (IHls' Htraverse_c); clear Htraverse_c. simpl in *. rewrite negb_true_iff in H_range. rewrite Raw.Proofs.elements_mapsto in *. apply Raw.Proofs.add_2. intro. apply InRange_Proper with (keys := keys) in H. rewrite H_range in H. destruct Htraverse_s. rewrite H1 in H. discriminate. assumption. - unfold Proper, respectful; intros; f_equal; apply InRange_Proper. unfold eq_key_elt, Raw.Proofs.PX.eqke in *; intuition. } } Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts