proposition: Lemma map2_0 : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m') (x:key), find x (map2 m m') = at_least_one_then_f (find x m) (find x m').
proof: Proof. intros. rewrite <- map2_alt_equiv. unfold map2_alt. assert (H:=combine_1 Hm Hm' x). assert (H2:=combine_sorted Hm Hm'). set (f':= fun p : oee' => f (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'. generalize H; clear H. match goal with |- ?m=?n -> ?p=?q => assert ((m=n->p=q)/\(m=None -> p=None)); [|intuition] end. induction m0; simpl in *; intuition. - destruct o; destruct o'; simpl in *; try discriminate; auto. - destruct a as (k,(oo,oo')); simpl in *. inversion_clear H2. destruct (X.compare x k) as [Hlt|Heq|Hlt]; simpl in *. + destruct (f' (oo,oo')); simpl. * elim_comp. destruct o; destruct o'; simpl in *; try discriminate; auto. * destruct (IHm0 H0) as (H2,_); apply H2; auto. 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 H4 H1)). exists p; apply find_2; auto. + assert (at_least_one_then_f o o' = f oo oo'). * destruct o; destruct o'; simpl in *; inversion_clear H; auto. * rewrite H2. unfold f'; simpl. destruct (f oo oo'); simpl. -- elim_comp; auto. -- 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'))). ++ red; auto with ordered_type. ++ destruct (Sort_Inf_NotIn H0 (Inf_eq (eqk_sym H5) H1)). exists p; apply find_2; auto. + unfold f'; simpl. destruct (f oo oo'); simpl. * elim_comp; auto. destruct (IHm0 H0) as (H3,_); apply H3; auto. * destruct (IHm0 H0) as (H3,_); apply H3; auto. - destruct a as (k,(oo,oo')). simpl. inversion_clear H2. destruct (X.compare x k) as [Hlt|Heq|Hlt]. + unfold f'; simpl. destruct (f oo oo'); simpl. * elim_comp; auto. * destruct (IHm0 H0) as (_,H4); apply H4; auto. 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_2; auto. + discriminate. + unfold f'; simpl. destruct (f oo oo'); simpl. * elim_comp; auto. destruct (IHm0 H0) as (_,H4); apply H4; auto. * destruct (IHm0 H0) as (_,H4); apply H4; auto. Qed.
imports: FMapInterface