proposition: Lemma RangeTreeBag_btraverse_correct : forall container searchkey key bag, InA (@eq_key_elt _) (key, bag) (RangeTreeBag_btraverse container.(this) searchkey) <-> MapsTo key bag container /\ Range_InRange searchkey key = true.
proof: Proof. intros [ ctn_raw ctn_proof ] [ minkey maxkey ] key bag; split; intro hyp. { induction ctn_raw; intros; simpl in *. - inversion hyp. - inversion ctn_proof; subst. specialize (IHctn_raw1 H3); specialize (IHctn_raw2 H5). destruct (Range_Min_le_Value minkey k) eqn: min_cmp; destruct (Range_Value_le_Max k maxkey) eqn: max_cmp. + apply InA_app_iff in hyp; try apply eqke_equiv; rewrite InA_cons in hyp. inversion hyp as [ hyp_l | [ hyp_m | hyp_r ] ]. * change ctn_raw1 with {| this := ctn_raw1; is_bst := H3 |}.(this) in hyp_l. rewrite RangeTreeBag_btraverse_left_correct in hyp_l; destruct hyp_l; split. apply Raw.MapsLeft; assumption. unfold Range_InRange. simpl. rewrite H0. simpl. apply Raw.Proofs.MapsTo_In in H. specialize (H6 _ H). eapply Range_Value_le_Max_trans; try eapply X_le_sound; eauto. * inversion hyp_m. simpl in *. subst. split. econstructor; eauto. unfold Range_InRange. simpl. apply andb_true_intro. split. destruct minkey; auto; simpl in *; rewrite X_le_sound in *; inversion min_cmp; [ left | right; eapply Raw.Proofs.L.PX.MO.lt_eq ]; eauto; rewrite H; reflexivity || auto. destruct maxkey; auto; simpl in *; rewrite X_le_sound in *; inversion max_cmp; [ left | right; eapply Raw.Proofs.L.PX.MO.lt_eq ]; eauto; try rewrite H; eauto; reflexivity. * change ctn_raw2 with {| this := ctn_raw2; is_bst := H5 |}.(this) in hyp_r. rewrite RangeTreeBag_btraverse_right_correct in hyp_r; destruct hyp_r; split. apply Raw.MapsRight; assumption. unfold Range_InRange. simpl. rewrite H0. rewrite andb_true_r. apply Raw.Proofs.MapsTo_In in H. specialize (H7 _ H). eapply Range_Min_le_Value_trans; try eapply X_le_sound; eauto. + apply IHctn_raw1 in hyp; intuition; apply Raw.MapsLeft; eauto. + apply IHctn_raw2 in hyp; intuition; apply Raw.MapsRight; eauto. + apply IHctn_raw2 in hyp; intuition; apply Raw.MapsRight; eauto. } { destruct hyp as [ hyp_m hyp_r ]; induction ctn_raw; intros; simpl in *. - inversion hyp_m. - inversion ctn_proof; subst. specialize (IHctn_raw1 H3); specialize (IHctn_raw2 H5). destruct (Range_Min_le_Value minkey k) eqn: min_cmp; [ destruct (Range_Value_le_Max k maxkey) eqn: max_cmp | ]. + apply InA_app_iff; try apply eqke_equiv; rewrite InA_cons. inversion hyp_m as [ hyp_mm | hyp_ml | hyp_mr ]; subst. * right; left; econstructor; eauto. * left. change ctn_raw1 with {| this := ctn_raw1; is_bst := H3 |}.(this). rewrite RangeTreeBag_btraverse_left_correct; intuition. unfold Range_InRange in hyp_r. rewrite andb_true_iff in hyp_r. tauto. * right; right. change ctn_raw2 with {| this := ctn_raw2; is_bst := H5 |}.(this). rewrite RangeTreeBag_btraverse_right_correct; intuition. unfold Range_InRange in hyp_r. rewrite andb_true_iff in hyp_r. tauto. + apply IHctn_raw1; inversion hyp_m; subst; eauto; unfold Range_InRange in hyp_r; apply andb_prop in hyp_r; destruct hyp_r; simpl in *; [ apply X.eq_sym in H0; eapply or_introl in H0; eapply X_le_sound in H0 | apply Raw.Proofs.MapsTo_In in H0; specialize (H7 _ H0); eapply or_intror in H7; eapply X_le_sound in H7 ]; eapply Range_Value_le_Max_trans with (value' := k) in H1; auto; rewrite H1 in max_cmp; discriminate. + apply IHctn_raw2; inversion hyp_m; subst; eauto; unfold Range_InRange in hyp_r; apply andb_prop in hyp_r; destruct hyp_r; simpl in *; [ eapply or_introl in H0; eapply X_le_sound in H0 | apply Raw.Proofs.MapsTo_In in H0; specialize (H6 _ H0); eapply or_intror in H6; eapply X_le_sound in H6 ]; eapply Range_Min_le_Value_trans with (value' := k) in H; auto; rewrite H in min_cmp; discriminate. } 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