proposition: Lemma mergeL_find f l l' acc x : (forall k, f k None None = None) -> sort O.ltk (rev l) -> sort O.ltk (rev l') -> exists y, y == x /\ findL x (mergeL f l l' acc) = oelse (f y (findL x (rev l)) (findL x (rev l'))) (findL x acc).
proof: Proof. intros Hf. revert l' acc. induction l as [|(y,e) l IHl]. - simpl. intros l' acc _ Sl'. destruct (@mapoL_find _ _ (fun k v' => f k None (Some v')) l' acc x Sl') as (y & Hy & EQ). exists y; split; auto; rewrite EQ; clear EQ. destruct findL; simpl; rewrite ?Hf; auto. - induction l' as [|(y',e') l' IHl']. + intros acc Sl _. clear IHl. destruct (@mapoL_find _ _ (fun k v => f k (Some v) None) _ acc x Sl) as (z & Hz & EQ). exists z; split; auto. cbn - [mapoL]. rewrite EQ; clear EQ. simpl. destruct findL; simpl; rewrite ?Hf; auto. + intros acc Sl Sl'. simpl in Sl, Sl'. assert (Sl0 := Sl). assert (Sl0' := Sl'). rewrite sort_app_key in Sl, Sl'. destruct Sl as (Sl & _ & AP). destruct Sl' as (Sl' & _ & AP'). rewrite mergeL_eqn. destmatch; [intro EQ | intro LT | intro LT]; set (acc' := ocons _ _ _). * destruct (IHl l' acc') as (z & Hz & E); auto. rewrite E. apply merge_find_eq; auto. * destruct (IHl' acc') as (z & Hz & E); auto. setoid_rewrite E. apply merge_find_lt; auto. * destruct (IHl ((y',e')::l') acc') as (z & Hz & E); auto. setoid_rewrite E. apply merge_find_gt; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)