proposition: Lemma merge_spec0 m m' {Hm : Ok m}{Hm' : Ok m'} (x:key) : exists y, X.eq y x /\ find x (merge m m') = at_least_one_then_f y (find x m) (find x m').
proof: Proof. intros. rewrite <- merge_equiv. unfold merge'. assert (H:=combine_spec x). assert (H2:=@combine_ok m m' _ _). set (f':= fun k p => f k (fst p) (snd p)). set (m0 := combine m m') in *; clearbody m0. set (o:=find x m) in *; clearbody o. set (o':=find x m') in *; clearbody o'. clear Hm Hm' m m'. revert H. match goal with |- ?G => assert (G/\(find x m0 = None -> find x (fold_right_pair option_cons (mapi f' m0) nil) = None)); [|intuition] end. induction m0; simpl in *; intuition. - exists x; split; [easy|]. destruct o; destruct o'; simpl in *; try discriminate; auto. - destruct a as (k,(oo,oo')); simpl in *. inversion_clear H2. destruct (X.compare_spec x k) as [Heq|Hlt|Hlt]; simpl in *. + exists k; split; [easy|]. assert (at_least_one_then_f k o o' = f k oo oo'). { destruct o; destruct o'; simpl in *; inversion_clear H; auto. } rewrite H2. unfold f'; simpl. destruct (f k oo oo'); simpl. * elim X.compare_spec; trivial; try MX.order. * destruct (IHm0 H0) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))). now compute. symmetry in H5. destruct (Sort_Inf_NotIn H0 (Inf_eq H5 H1)). exists p; apply find_spec; auto. + destruct (f' k (oo,oo')); simpl. * elim X.compare_spec; trivial; try MX.order. destruct o; destruct o'; simpl in *; try discriminate; auto. now exists x. * apply IHm0; trivial. rewrite <- H. case_eq (find x m0); intros; auto. assert (ltk (elt:=oee') (x,(oo,oo')) (k,(oo,oo'))). red; auto. destruct (Sort_Inf_NotIn H0 (Inf_lt H3 H1)). exists p; apply find_spec; auto. + unfold f'; simpl. destruct (f k oo oo'); simpl. * elim X.compare_spec; trivial; try MX.order. intros. apply IHm0; auto. * apply IHm0; auto. - destruct a as (k,(oo,oo')). simpl. inversion_clear H2. destruct (X.compare_spec x k) as [Hlt|Heq|Hlt]; try discriminate. + unfold f'; simpl. destruct (f k oo oo'); simpl. elim X.compare_spec; trivial; try MX.order. intros. apply IHm0; auto. case_eq (find x m0); intros; auto. assert (ltk (elt:=oee') (x,(oo,oo')) (k,(oo,oo'))). now compute. destruct (Sort_Inf_NotIn H0 (Inf_lt H3 H1)). exists p; apply find_spec; auto. + unfold f'; simpl. destruct (f k oo oo'); simpl. elim X.compare_spec; trivial; try MX.order. intros. apply IHm0; auto. apply IHm0; auto. Qed.
imports: Coq(OrdersFacts OrdersLists)