proposition: Lemma gmerge_find m m' x `{!Ok m, !Ok m'} : x ∈ m \/ x ∈ m' -> exists y, y == x /\ find x (gmerge m m') = f0 y (find x m) (find x m').
proof: Proof. functional induction (gmerge m m'); try factornode m2; invok; rewrite ?in_node, ?in_leaf. - intros [[ ]|H]. destruct (@mapr_f0 x m2) as (y,(Hy,E)); trivial. exists y; split; trivial. rewrite E. simpl. apply in_find in H; trivial. destruct (find x m2); simpl; intuition. - intros [H|[ ]]. destruct (@mapl_f0 x m2) as (y,(Hy,E)); trivial. exists y; split; trivial. rewrite E. simpl. apply in_find in H; trivial. destruct (find x m2); simpl; intuition. - generalize (@split_ok_l _ m2 x1 _) (@split_ok_r _ m2 x1 _). rewrite (@split_find _ m2 x1 x); autok. rewrite e1 in *; simpl in *. intros. rewrite join_find by (cleansplit; constructor; autok). simpl. case K.compare_spec; intros. + exists x1. split; autom. now rewrite <- e3, f0_f. + apply IHt2; autom. clear IHt2 IHt0. cleansplit; rewrite split_in_l; trivial. intuition_in; order. + apply IHt0; auto. clear IHt2 IHt0. cleansplit; rewrite split_in_r; trivial. intuition_in; order. - generalize (@split_ok_l _ m2 x1 _) (@split_ok_r _ m2 x1 _). rewrite (@split_find _ m2 x1 x); autok. pose proof (@split_lt_l _ m2 x1 _). pose proof (@split_gt_r _ m2 x1 _). rewrite e1 in *; simpl in *. intros. rewrite concat_find by (try apply between with x1; autok). case K.compare_spec; intros. + clear IHt0 IHt2. exists x1. split; autom. rewrite <- f0_f, e2. nonify (find x (gmerge r1 r2')). nonify (find x (gmerge l1 l2')). trivial. + nonify (find x (gmerge r1 r2')). simpl. apply IHt2; auto. clear IHt2 IHt0. intuition_in; try order. right. cleansplit. now apply split_in_l. + nonify (find x (gmerge l1 l2')). simpl. rewrite oelse_none_r. apply IHt0; auto. clear IHt2 IHt0. intuition_in; try order. right. cleansplit. now apply split_in_r. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)