Defining a terminating `ripple`, with arguments swapping places

Question

In Agda, I can make the following definition, and Agda believes that the recursion terminates. Notice that the arguments “swap places” in the recursive call, so neither of the arguments individually gets obviously smaller.

open import Data.List

ripple : ∀ {a} {A : Set a} → List A → List A → List A
ripple [] ys = ys
ripple (x ∷ xs) ys = x ∷ ripple ys xs

I am interested in how other proof assistants deal with this recursion pattern. I have tried calquing this definition into Coq using Fixpoint, but predictably it can't find a decreasing argument. Answers to this question should establish that ripple terminates (either because all functions in the language terminate, or because an explicit termination proof is given), and preferably be as idiomatic and lightweight as possible.

---

I think I first heard of this exercise, in some form or another, from Conor McBride.

Answer 1

Idris is also happy with this definition:

module Ripple

%default total

ripple : List a -> List a -> List a
ripple [] ys = ys
ripple (x :: xs) ys = x :: ripple ys xs

The computation of the size change graph is fairly clean in the compiler in case you are interested in the implementation: Core.Termination.SizeChange

Answer 2

In Lean 4, this is done using well-founded recursion by specifying a termination measure:

def ripple : List α → List α → List α
  | [], ys => ys
  | x :: xs, ys => x :: ripple ys xs
termination_by ripple xs ys => xs.length + ys.length

The resulting elaborated code is quite horrible:

#print ripple
def ripple.{u_1} : {α : Type u_1} → List α → List α → List α :=
 fun {α} x x_1 => ripple._unary { fst := x, snd := x_1 }

and

#print ripple._unary
def ripple._unary.{u_1} : {α : Type u_1} → (_ : List α) ×' List α → List α :=
fun {α} =>
  WellFounded.fix
    (_ :
      WellFounded
        (invImage (fun a => PSigma.casesOn a fun xs snd => List.length xs + List.length snd) instWellFoundedRelation).1)
    fun _x a =>
    PSigma.casesOn (motive := fun x =>
      ((y : (_ : List α) ×' List α) →
          (invImage (fun a => PSigma.casesOn a fun xs snd => List.length xs + List.length snd)
                  instWellFoundedRelation).1
              y x →
            List α) →
        List α)
      _x
      (fun x x_1 a =>
        (match (motive :=
            (x x_2 : List α) →
              ((y : (_ : List α) ×' List α) →
                  (invImage (fun a => PSigma.casesOn a fun xs snd => List.length xs + List.length snd)
                          instWellFoundedRelation).1
                      y { fst := x, snd := x_2 } →
                    List α) →
                List α)
            x, x_1 with
          | [], ys => fun x => ys
          | x :: xs, ys => fun x_2 =>
            x ::
              x_2 { fst := ys, snd := xs }
                (_ :
                  (invImage (fun a => PSigma.casesOn a fun xs snd => List.length xs + List.length snd)
                        instWellFoundedRelation).1
                    { fst := ys, snd := xs } { fst := x :: xs, snd := ys }))
          a)
      a

On the other hand, not having the termination checker as part of the trusted code base and instead elaborating to eliminators is nice.

Answer 3

In Coq, using Equations, the program is pretty much as simple as in Agda:

Require Import List Lia.
From Equations Require Import Equations.

Import ListNotations.

Equations ripple {A : Type} (xs ys : list A) : list A by wf (length xs + length ys) :=
  ripple [] ys := ys ;
  ripple (x :: xs) ys := x :: (ripple ys xs).
Next Obligation.
  lia.
Qed.

The main difference is the explicit termination argument, using the combined length of the lists. Thanks to tactics, the inequality proof is a one-liner.

You probably do not want to look at the generated term, which is not very good looking, and has not the best computational behaviour. However, you get the unfolding equations propositionally, which for most purposes is good enough.

About ripple_equation_1.
(* ripple_equation_1 : forall (A : Type) (ys : list A), ripple [] ys = ys *)
About ripple_equation_2.
(* ripple_equation_2 : forall (A : Type) (x : A) (xs ys : list A), ripple (x :: xs) ys = x :: ripple ys xs *)

Accordingly, the definition is by default opaque, but you can make it transparent and compute on closed lists, which gives you the right values, albeit not very efficiently because it computes accessibility proofs:

Transparent ripple.

Eval vm_compute in ripple [0;2;4] [1;3].
(* = [0; 1; 2; 3; 4] : list nat *)

Accordingly, extracting the definition should result in code that has the right computational behaviour, but removes the slow-down coming from computing proofs.

Answer 4

HOL4's automatic search for a well-founded termination relation succeeds in this case, so you need only write:

Definition ripple_def:
  ripple [] ys = ys ∧
  ripple (x::xs) ys = x::ripple ys xs
End

I assume it's finding the sum of argument sizes measure, but haven't dug into its internals to find out.