merge.v

Require Import List Omega.

Import ListNotations.

Inductive merge_acc : list nat -> list nat -> Prop :=
| Merge1 : forall xs, merge_acc xs nil
| Merge2 : forall ys, merge_acc nil ys 
| Merge3 : forall x y xs ys,
    x <= y -> merge_acc xs (y :: ys) -> merge_acc (x :: xs) (y :: ys)
| Merge4 : forall x y xs ys,
    x > y -> merge_acc (x :: xs) ys -> merge_acc (x :: xs) (y :: ys).

Hint Constructors merge_acc.

Ltac inv H := inversion H ; subst ; clear H.

Lemma merge_acc_inv3
  : forall xs ys x y,
    merge_acc (x :: xs) (y :: ys) -> x <= y -> merge_acc xs (y :: ys).
Proof.
  induction xs ; destruct ys ; intros x y H Hle ; inv H ; eauto ; try omega.
Defined.

Lemma merge_acc_inv4
  : forall xs ys x y, merge_acc (x :: xs) (y :: ys) -> x > y -> merge_acc (x :: xs) ys.
Proof.
  induction xs ; destruct ys ; intros x y H Hxy ; inv H ; eauto ; try omega.
Defined.

Hint Resolve merge_acc_inv3 merge_acc_inv4.


Fixpoint merge_bc (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
  match xs, ys with
  | nil, ys => ys
  | xs , nil => xs
  | (x :: xs) , (y :: ys) =>
    match le_gt_dec x y with
    | left _ h1 => x :: merge_bc (merge_acc_inv3 xs ys x y H h1) 
    | right _ h2 => y :: merge_bc (x :: xs) ys (merge_acc_inv4 _ _ _ _ H h2)
    end 
  end. 

Definition merge_bc : forall xs ys, merge_acc xs ys -> list nat.
  refine (fix merge_bc xs ys (H : merge_acc xs ys) {struct H}: list nat :=
            match xs as xs' return xs = xs' -> list nat with
            | nil => fun _ => ys
            | x :: xs => fun _ =>
              (match ys as ys' return ys = ys' -> list nat with
               | nil => fun _ => x :: xs
               | y :: ys => fun _ =>
                 match le_gt_dec x y with
                 | left _ Hle => x :: merge_bc xs (y :: ys) _
                 | right _ Hgt => y :: merge_bc (x :: xs) ys _
                 end
               end (eq_refl ys))
            end (eq_refl xs)).
  +
    subst.
    apply merge_acc_inv3 with (x := x).
    exact H. exact Hle.
  +
    subst.
    apply merge_acc_inv4 with (y := y).
    exact H.
    exact Hgt.
Defined.