proposition: Lemma combine_spec m m' {Hm : Ok m}{Hm' : Ok m'} (x:key) : find x (combine m m') = at_least_one (find x m) (find x m').
proof: Proof. revert m' Hm'. induction m. intros. simpl. induction m'. intros; simpl; auto. simpl; destruct a. simpl; destruct (X.compare x t0); simpl; auto. inversion_clear Hm'; auto. induction m'. intros; destruct a; simpl. destruct (X.compare_spec x t0) as [ |Hlt|Hlt]; simpl; auto. inversion_clear Hm; clear H0 Hlt Hm' IHm t0. induction m; simpl; auto. inversion_clear H. destruct a. simpl; destruct (X.compare x t0); simpl; auto. intros. destruct a as (k,e); destruct a0 as (k',e'); simpl. inversion Hm; inversion Hm'; subst. destruct (X.compare_spec k k'); simpl; destruct (X.compare_spec x k); MX.order || destruct (X.compare_spec x k'); simpl; try MX.order; auto. - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. - rewrite IHm; auto; simpl. elim X.compare_spec; auto; MX.order. - change (find x (combine ((k, e) :: m) m') = Some (Some e, find x m')). rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. - change (find x (combine ((k, e) :: m) m') = at_least_one None (find x m')). rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. - change (find x (combine ((k, e) :: m) m') = at_least_one (find x m) (find x m')). rewrite IHm'; auto; simpl. elim X.compare_spec; auto; MX.order. Qed.
imports: Coq(OrdersFacts OrdersLists)