proposition: Theorem RangeTreeBag_BagFindCorrect : BagFindCorrect RangeTreeBag_RepInv RangeTreeBag_bfind RangeTreeBag_bfind_matcher RangeTreeBag_benumerate.
proof: Proof. hnf; intros. unfold RangeTreeBag_bfind, 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 ]. rewrite filter_and. rewrite !flatten_filter; simpl. pose proof (fun c k b => proj1 (RangeTreeBag_bcollect_correct c k b)) as rc_c. rewrite <- map_map with (l := (RangeTreeBag_btraverse container keys)) (f := snd) (g := fun bag => bfind bag searchterm). rewrite RangeTreeBag_btraverse_bcollect. remember (RangeTreeBag_bcollect container) as ls. specialize (rc_c container). rewrite <- Heqls in rc_c; clear Heqls. induction ls as [ | [ key bag ] ls' ]; simpl in *. reflexivity. assert (InA (eq_key_elt (elt:=BagType)) (key, bag) ((key, bag) :: ls')) as sc_c by (repeat constructor; apply X.eq_refl); apply rc_c in sc_c. assert (forall k b, InA (eq_key_elt (elt:=BagType)) (k, b) ls' -> MapsTo k b container) by (intros; eapply rc_c; eapply InA_cons_tl; eauto); specialize (IHls' H); clear H rc_c. specialize (containerCorrect key bag sc_c); destruct containerCorrect as [ cc_rev cc_eq ]; clear sc_c. pose proof (bfind_correct bag searchterm cc_rev) as bf_c; clear cc_rev. rewrite IHls'; clear IHls'. remember (benumerate bag) as xs; clear Heqxs. destruct (Range_InRange keys key) eqn: eqk; simpl. - f_equiv. rewrite <- bf_c; clear bf_c. induction xs as [ | item xs' ]; simpl. + constructor. + pose proof (InList_ind_helper _ cc_eq) as [ cc_eq_h cc_eq_t ]; clear cc_eq. specialize (IHxs' cc_eq_t); clear cc_eq_t. erewrite InRange_Proper; eauto. rewrite eqk. simpl. destruct (bfind_matcher searchterm item). apply Permutation_cons; try reflexivity. apply IHxs'. apply IHxs'. - assert (List.filter (bfind_matcher searchterm) (List.filter (fun a : TItem => Range_InRange keys (projection a)) xs) = nil). rewrite filter_commute. apply filter_all_false; intros. rewrite InRange_Proper with (v' := key); auto. apply cc_eq. 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