proposition: Lemma merge_find_lt f l l' acc x y y' z e e' : (forall k : key, f k None None = None) -> l < [(y, e)] -> l' < [(y', e')] -> y < y' -> z == x -> exists y0 : K.t, y0 == x /\ oelse (f z (findL x (l++[(y,e)])) (findL x l')) (findL x (ocons y' (f y' None (Some e')) acc)) = oelse (f y0 (findL x (l++[(y, e)])) (findL x (l'++[(y', e')]))) (findL x acc).
proof: Proof. intros Hf AP AP' Ey Ez. simpl. destruct findL eqn:INl. - exists z; split; auto. assert (x < y'). { apply findL_inA in INl. apply InA_alt in INl. destruct INl as ((x',e0') & (Hx',_) & INl). compute in Hx'. rewrite Hx'. rewrite in_app_iff in INl. destruct INl. - rewrite <- Ey. apply (AP (x',e0') (y,e)); simpl; auto. - simpl in H. destruct H as [[= <- _]|[ ]]; auto. } setoid_rewrite findL_app. destruct (findL x l'); simpl; breako. - clear INl. setoid_rewrite findL_app. destruct (findL x l') eqn:INl'; simpl. + exists z; split; auto. enough (x < y') by breako. { apply findL_inA in INl'. apply InA_alt in INl'. destruct INl' as ((x',e0') & (Hx',_) & INl'). compute in Hx'. rewrite Hx'. apply (AP' (x',e0') (y',e')); simpl; auto. } + clear INl'. rewrite Hf. simpl. destruct (f y' _ _) eqn:Fy'; simpl; destmatch; try setoid_rewrite Hf; firstorder; exists y'; now rewrite Fy'. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)