Automated termination proof on structural-ish recursion?

Stream: lean4

[Phil Nguyen]

Suppose we define a universe of tags, and their interpretation into Lean's Types:

inductive TAG where
| NAT : TAG
| LIST : TAG → TAG

abbrev TAG.interp : TAG → Type
| NAT => Nat
| LIST t => List t.interp

Now we define an addOne function. It looks structural recursion, but is unintuitively rejected by Lean, because the second argument doesn't have a fixed type:

def addOne : (t : TAG) → t.interp → t.interp
| .NAT, n => n + 1
| .LIST _, [] => []
| .LIST t, x :: xs => addOne t x :: addOne (.LIST t) xs
termination_by t x => (t, x) -- nope

The current workaround I'm trying is explicitly defining a measure:

def TAG.sizeOf : (t : TAG) → t.interp → Nat
| NAT, _ => 0
| LIST _, xs => xs.length

def addOne : (t : TAG) → t.interp → t.interp
/- above definition -/
termination_by t x => (t, TAG.sizeOf t x)
decreasing_by
. apply Prod.Lex.left; simp
. apply Prod.Lex.right; simp [TAG.sizeOf]

Is there a more automated way to have Lean accept that addOne terminates?

Many thanks!!

[Aaron Liu]

Use a sigma type?

[Phil Nguyen]

How does that work? Could you show me?

I tried the following, but it looks like there's no default working SizeOf instance for Sigma yet:

def addOne : (t : TAG) → t.interp → t.interp
| .NAT, n => n + 1
| .LIST _, [] => []
| .LIST t, x :: xs => addOne t x :: addOne (.LIST t) xs
termination_by t x => (t, (⟨_, x⟩ : (Σ (t : TAG), t.interp)))
/-
failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
t : TAG
x : t.interp
xs : List t.interp
⊢ sizeOf ⟨t.LIST, xs⟩ < sizeOf ⟨t.LIST, x :: xs⟩
-/

[Aaron Liu]

I think Sigma is missing a WellFoundedRelation instance?

[Robin Arnez]

Try this:

inductive Tag where
  | nat : Tag
  | list : Tag → Tag

abbrev Tag.interp : Tag → Type
  | nat => Nat
  | list t => List t.interp

protected noncomputable def Tag.interp.sizeOf : {t : Tag} → t.interp → Nat
  | .nat, x => x
  | .list t, x => (x : List t.interp).rec 1 (fun a _ ih => 1 + a.sizeOf + ih)

noncomputable instance : SizeOf (Tag.interp t) := ⟨Tag.interp.sizeOf⟩

@[simp] theorem Tag.interp.sizeOf_nat (x : Tag.nat.interp) : instSizeOfInterp.sizeOf x = x := rfl
@[simp] theorem Tag.interp.sizeOf_list {t : Tag} (x : t.list.interp) : instSizeOfInterp.sizeOf x = sizeOf (x : List t.interp) := rfl

def addOne (t : Tag) (x : t.interp) : t.interp :=
  match t, x with
  | .nat, n => n + 1
  | .list _, [] => []
  | .list t, x :: xs => addOne t x :: addOne (.list t) xs

It just needed the right sizeOf instance.