proposition: Lemma merge_spec1n (f:key->option elt->option elt'->option elt'') : (forall x, f x None None = None) -> forall (m: t elt)(m': t elt') x, exists y, K.eq y x /\ find x (merge f m m') = f y (find x m) (find x m').
proof: Proof. intros Hf m m' x. destruct (find x m) as [e|] eqn:Hm. - assert (H : In x m \/ In x m') by (left; exists e; now apply find_spec). destruct (merge_spec1 f H) as (y,(Hy,->)). exists y; split; trivial. now rewrite Hm. - destruct (find x m') as [e|] eqn:Hm'. + assert (H : In x m \/ In x m') by (right; exists e; now apply find_spec). destruct (merge_spec1 f H) as (y,(Hy,->)). exists y; split; trivial. now rewrite Hm, Hm'. + exists x. split. reflexivity. rewrite Hf. apply not_in_find. intro H. apply merge_spec2 in H. apply not_in_find in Hm. apply not_in_find in Hm'. intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)