proposition: Lemma merge_find_gt 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) (findL x (l' ++ [(y',e')]))) (findL x (ocons y (f y (Some e) None) 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. setoid_rewrite (findL_app x l). 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'. apply (AP (x',e0') (y,e)); simpl; auto. } destruct (findL x (l' ++ _)); simpl; breako. - clear INl. 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'. rewrite in_app_iff in INl'. simpl in *. destruct INl'. - rewrite <- Ey. apply (AP' (x',e0') (y',e')); simpl; auto. - destruct H as [[= <- _]|[ ]]; 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)