general recursion in Coq

generalrecursion.v

Require Import Arith_base.
Require Import List.

Import List Notations.

(*

Fixpoint merge (xs ys : list nat) : list nat :=
  match xs, ys with
  | nil , ys => ys
  | xs , nil => xs
  | (x :: xs) , (y :: ys) =>
    match le_gt_dec x y with 
    | left _ _ =>  x :: (merge xs (y :: ys))
    | right _ _ => y :: (merge (x :: xs) ys)
    end
  end.

Error: Cannot guess decreasing argument of fix.

 *)

(** Fuel based recursion *)


Fixpoint merge_fuel (xs ys : list nat)(fuel : nat) : option (list nat) :=
  match fuel with
  | O => None
  | S fuel' =>
    match xs, ys with
    | nil , ys => Some ys
    | xs , nil => Some xs
    | (x :: xs) , (y :: ys) =>
      match le_gt_dec x y with 
      | left _ _ =>
        match merge_fuel xs (y :: ys) fuel' with
        | Some r => Some (x :: r)
        | None   => None
        end
      | right _ _ =>
        match merge_fuel (x :: xs) ys fuel' with
        | Some r => Some (y :: r)
        | None   => None
        end
      end
    end
  end.

(** Well founded relations *)


Require Import Wellfounded Omega Relations.Relation_Operators Omega.

Definition merge_input := sigT (fun _ : list nat => list nat).

Definition mk_input (xs ys : list nat) : merge_input := existT _ xs ys.

Definition list1 (inp : merge_input) : list nat :=
  let (xs,_) := inp in xs.

Definition list2 (inp : merge_input) : list nat :=
  let (_,ys) := inp in ys.


Definition merge_input_lt : merge_input -> merge_input -> Prop
  := lexprod (list nat)
             (fun _ => list nat)
             (fun (xs xs' : list nat) => length xs < length xs')
             (fun _ (ys ys' : list nat) => length ys < length ys').


Definition merge_input_lt_wf : well_founded merge_input_lt
  := @wf_lexprod (list nat)
                 (fun _ => list nat)
                 (fun (xs xs' : list nat) => length xs < length xs')
                 (fun _ (ys ys' : list nat) => length ys < length ys')
                 (well_founded_ltof (list nat) (@length nat))
                 (fun _ => well_founded_ltof (list nat) (@length nat)).

Lemma mergeF_obligation1
  : forall x y xs ys, merge_input_lt (mk_input xs (y :: ys))
                                (existT _ (x :: xs) (y :: ys)).
Proof.
  intros ; apply left_lex ; simpl ; try omega.
Qed.

Lemma mergeF_obligation2
  : forall x y xs ys, merge_input_lt (mk_input (x :: xs) ys)
                                (existT _ (x :: xs) (y :: ys)).
Proof.
  intros ; apply right_lex ; simpl ; try omega.
Qed.

Hint Resolve  mergeF_obligation1 mergeF_obligation2.

Definition mergeF
  : forall inp : merge_input,
    (forall inp' : merge_input, merge_input_lt inp' inp -> list nat) -> list nat.
  refine (fun inp canRec =>
            match inp as inp' return inp = inp' -> list nat with
            | existT _ nil ys => fun _ => ys
            | existT _ xs nil => fun _ => xs
            | existT _ (x :: xs) (y :: ys) => fun _ => 
              if le_gt_dec x y then x :: canRec (mk_input xs (y :: ys)) _
                  else y :: canRec (mk_input (x :: xs) ys) _
            end (eq_refl inp)) ; subst ; auto.
Defined.

Definition merge_wf (xs ys : list nat) : list nat :=
  well_founded_induction merge_input_lt_wf (fun _ => list nat) mergeF (mk_input xs ys).

(** Bove-Capretta method *)

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 xxs yys,
        xxs = x :: xs -> yys = y :: ys ->
        merge_acc xxs yys ->
        x <= y ->
        merge_acc xs yys.
 Proof.
    intros xs ys x y xxs yys eqx eqy H Hle;
    subst; inv H ; eauto ; try omega.
 Defined.

 Lemma merge_acc_inv4
    : forall xs ys x y xxs yys,
      xxs = x :: xs -> yys = y :: ys ->
      merge_acc xxs yys ->
      x > y ->
     merge_acc xxs ys.
 Proof.
   intros xs ys x y xxs yys eqx eqy H Hxy ;
   subst ; inv H ; eauto ; try omega.
 Defined.

Fixpoint merge_bc1
     (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
   (match xs as us, ys as vs return xs = us -> ys = vs -> list nat with
     | nil, ys => fun _ _ => ys
     | xs , nil => fun _ _ => xs
     | (x :: xs) , (y :: ys) =>
        match le_gt_dec x y with
        | left _ h1 => fun eqx eqy =>
            let H' := merge_acc_inv3 _ _ x y _ _ eqx eqy H h1
            in x :: merge_bc1 _ _ H'
        | right _ h2 => fun eqx eqy =>
            let H' := merge_acc_inv4 _ _ x y _ _ eqx eqy H h2
            in y :: merge_bc1 _ _ H'
        end 
     end) eq_refl eq_refl.


Definition merge_acc_intro : forall xs ys, merge_acc xs ys.
  induction xs as [| x xs IHxs]; destruct ys as [| y ys] ;
    try solve [econstructor ; eauto].
  +
    destruct (le_gt_dec x y) ; eauto.
    induction ys as [| y' ys' IHys'].
    *
      apply Merge4 ; eauto.
    *
      apply Merge4.
      assumption.
      inv IHys'. try omega.
      destruct (le_gt_dec x y') ; try omega ; auto.
Defined.

Definition merge_bc (xs ys : list nat) : list nat.
  apply (merge_bc1 xs ys).
  apply merge_acc_intro.
Defined.