proposition: Theorem RangeTreeBag_BagDeleteCorrect : BagDeleteCorrect RangeTreeBag_RepInv RangeTreeBag_bfind RangeTreeBag_bfind_matcher RangeTreeBag_benumerate RangeTreeBag_bdelete.
proof: Proof. hnf; intros. unfold RangeTreeBag_bdelete, RangeTreeBag_benumerate, RangeTreeBag_bfind_matcher. unfold Values, elements. change (Raw.elements container) with (RangeTreeBag_bcollect container.(this)). unfold RangeTreeBag_RepInv in containerCorrect. destruct search_term as [ keys searchterm ]. simpl. split. { rewrite partition_filter_neq. rewrite !flatten_filter. remember (RangeTreeBag_btraverse container keys) as ls. pose proof (snd_fold_right (fun (y : TKey * BagType) (x : list TItem * RangeTreeBag) => (fst x) ++ (fst (bdelete (snd y) searchterm))) (fun (y : TKey * BagType) (x : RangeTreeBag) => add (fst y) (snd (bdelete (snd y) searchterm)) x) [] container ls) as snd_foldr. fold RangeTreeBag in *; rewrite snd_foldr; clear snd_foldr; subst. rewrite RangeTreeBag_BagDeleteUpdateCorrect' with (f := fun x => snd (bdelete x searchterm)). pose proof (fun k b => proj1 (RangeTreeBag_bcollect_correct container k b)) as bcol_correct. remember (RangeTreeBag_bcollect container) as ls; clear Heqls. induction ls as [ | [ key bag ] ls' ]. reflexivity. apply InA_ind_helper in bcol_correct; destruct bcol_correct as [ bcol_hd bcol_tl ]. simpl; rewrite (IHls' bcol_tl); clear bcol_tl IHls'. destruct (containerCorrect key bag bcol_hd) as [ cc_rep cc_eq ]; clear bcol_hd containerCorrect. f_equiv. pose proof (bdelete_correct bag searchterm cc_rep) as [ bdel_c _ ]. remember (benumerate bag) as xs. destruct (Range_InRange keys key) eqn: eqk; simpl. { rewrite bdel_c, partition_filter_neq; clear bdel_c. clear Heqxs. induction xs. reflexivity. simpl. apply InList_ind_helper in cc_eq; destruct cc_eq as [ cc_eq_hd cc_eq_tl ]. specialize (IHxs cc_eq_tl); clear cc_eq_tl. erewrite InRange_Proper; eauto; clear cc_eq_hd. rewrite eqk; simpl. destruct (negb (bfind_matcher searchterm a)); simpl. apply Permutation_cons; eauto. eauto. } { rewrite <- Heqxs; clear Heqxs. clear bdel_c. induction xs. reflexivity. simpl. apply InList_ind_helper in cc_eq; destruct cc_eq as [ cc_eq_hd cc_eq_tl ]. specialize (IHxs cc_eq_tl); clear cc_eq_tl. erewrite InRange_Proper; eauto; clear cc_eq_hd. rewrite eqk; simpl. eauto. } } { rewrite partition_filter_eq. rewrite filter_and. rewrite !flatten_filter. remember (RangeTreeBag_btraverse container keys) as ls. pose proof (fst_fold_right (fun (y : TKey * BagType) (x : list TItem) => x ++ (fst (bdelete (snd y) searchterm))) (fun (y : TKey * BagType) (x : list TItem * RangeTreeBag) => add (fst y) (snd (bdelete (snd y) searchterm)) (snd x)) [] container ls) as fst_foldr. fold RangeTreeBag in *. rewrite fst_foldr. clear fst_foldr. pose proof (Common.fold_right_map snd (fun (y : BagType) (x : list TItem) => x ++ fst (bdelete y searchterm)) [] ls) as map_foldr; unfold compose in map_foldr. rewrite <- map_foldr; clear map_foldr. subst. rewrite RangeTreeBag_btraverse_bcollect. pose proof bdelete_correct as bdel_correct; unfold BagDeleteCorrect in bdel_correct. pose proof (fun key bag => proj1 (RangeTreeBag_bcollect_correct container key bag)) as bcol_correct. remember (RangeTreeBag_bcollect container) as ls; clear Heqls. induction ls as [ | [ key bag ] ls' ]. constructor. apply InA_ind_helper in bcol_correct; destruct bcol_correct as [ bcol_hd bcol_tl ]. specialize (IHls' bcol_tl); clear bcol_tl. specialize (containerCorrect _ _ bcol_hd); destruct containerCorrect as [ rep xeq ]; clear bcol_hd. simpl. rewrite <- IHls'. clear IHls'. specialize (bdel_correct bag searchterm rep); destruct bdel_correct as [ _ bdel_correct ]. remember (benumerate bag) as xs. clear Heqxs. destruct (Range_InRange keys key) eqn: eqk; simpl. - rewrite Permutation_app_comm. f_equiv. rewrite bdel_correct. clear bdel_correct. rewrite partition_filter_eq. induction xs. reflexivity. simpl. pose proof (InList_ind_helper _ xeq) as [ xeq_h xeq_t ]; clear xeq. specialize (IHxs xeq_t); clear xeq_t. erewrite InRange_Proper; eauto. rewrite eqk. simpl. destruct (bfind_matcher searchterm a). constructor. assumption. assumption. - assert (List.filter (bfind_matcher searchterm) (List.filter (fun a : TItem => Range_InRange keys (projection a)) xs) = []). rewrite filter_commute. apply filter_all_false; intros. rewrite InRange_Proper with (v' := key); auto. apply xeq. rewrite filter_In in H. tauto. rewrite H. reflexivity. } 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