proposition: Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> In y m \/ In y m' -> find y (map2_opt m m') = f0 y (find y m) (find y m').
proof: Proof. intros m m'; functional induction (map2_opt m m'); intros; auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; try (generalize (split_in_1 x1 H0)(split_in_2 x1 H0) (split_in_3 x1 H0)(split_bst x1 H0)(split_find x1 y H0) (split_lt_tree (x:=x1) H0)(split_gt_tree (x:=x1) H0); rewrite e1; simpl in *; destruct 4; intros; inv bst; subst o2; rewrite H7, ?join_find, ?concat_find; auto). - simpl; destruct H1; [ inversion_clear H1 | ]. rewrite mapr_f0; auto. generalize (in_find H0 H1); destruct (find y m2); intuition. - factornode l1 x1 d1 r1 _x as m1. destruct H1; [ | inversion_clear H1 ]. rewrite mapl_f0; auto. generalize (in_find H H1); destruct (find y m1); intuition. - simpl; destruct X.compare; auto. + apply IHt1; auto; map2_aux. + rewrite (@f0_compat y x1), <- f0_f; auto. + apply IHt0; auto; map2_aux. - intros z Hz; destruct (@map2_opt_2 l1 l2' z); auto. - intros z Hz; destruct (@map2_opt_2 r1 r2' z); auto. - destruct X.compare. + nonify (find y (map2_opt r1 r2')). apply IHt1; auto; map2_aux. + nonify (find y (map2_opt r1 r2')). nonify (find y (map2_opt l1 l2')). rewrite (@f0_compat y x1), <- f0_f; auto. + nonify (find y (map2_opt l1 l2')). rewrite IHt0; auto; [ | map2_aux ]. destruct (f0 y (find y r1) (find y r2')); auto. - intros y1 y2 Hy1 Hy2; apply X.lt_trans with x1. + destruct (@map2_opt_2 l1 l2' y1); auto. + destruct (@map2_opt_2 r1 r2' y2); auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int