proposition: Lemma RangeTreeBag_btraverse_left_correct : forall container minkey key bag, InA (@eq_key_elt _) (key, bag) (RangeTreeBag_btraverse_left container.(this) minkey) <-> MapsTo key bag container /\ Range_Min_le_Value minkey key = true.
proof: Proof. intros [ ctn_raw ctn_proof ] minkey 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. + rewrite InA_app_iff in hyp; try apply eqke_equiv. rewrite InA_cons in hyp. destruct hyp as [ hyp_l | [ hyp_s | hyp_r ] ]. * apply IHctn_raw1 in hyp_l. split. apply Raw.MapsLeft. tauto. tauto. * inversion hyp_s. simpl in *. subst. split. econstructor. eauto. destruct minkey; intuition; unfold Range_Min_le_Value in *. apply X_le_sound in min_cmp; apply X_le_sound. destruct min_cmp. eauto. try (left; rewrite H; assumption). right; apply X.eq_sym in H; eapply Raw.Proofs.L.PX.MO.lt_eq; eauto. * inversion ctn_proof; subst. pose ({| this := ctn_raw2; is_bst := H9 |}). change (ctn_raw2) with (b.(this)) in hyp_r. rewrite RangeTreeBag_bcollect_correct in hyp_r. split. apply Raw.MapsRight. eauto. apply Raw.Proofs.MapsTo_In in hyp_r. specialize (H11 _ hyp_r). eapply Range_Min_le_Value_trans; eauto. rewrite X_le_sound; eauto. + apply IHctn_raw2 in hyp. split. apply Raw.MapsRight. tauto. tauto. } { 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. + apply InA_app_iff; try apply eqke_equiv; rewrite InA_cons. inversion hyp_m; subst. * right; left. econstructor; eauto. * left. apply IHctn_raw1. eauto. * right; right. change ctn_raw2 with {| this := ctn_raw2; is_bst := H5 |}.(this). rewrite RangeTreeBag_bcollect_correct. eauto. + apply IHctn_raw2. inversion hyp_m; subst; eauto; exfalso; destruct minkey; simpl in *; try discriminate. * rewrite <- not_true_iff_false in *. rewrite X_le_sound in *. intuition eauto; rewrite <- H0 in *; tauto. * apply Raw.Proofs.MapsTo_In in H0. specialize (H6 _ H0). rewrite <- not_true_iff_false in *. rewrite X_le_sound in *; intuition eauto; rewrite <- H in *; tauto. } 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