Termination checking of structure with nested Array

Stream: new members

[Philip Zucker]

I was trying to translate some term combinators written in python to lean and would like to understand how I can get the termination checker to accept them

structure App where
  f : String
  args : List App -- Array App
deriving Repr, Inhabited

--- Termination checker fails for both Array and List
def App.mysizeOf (a : App) : Nat :=
  1 + (a.args.map mysizeOf).sum

-- termination check succeeds but only if List
def App.mysize (a : App) : Nat :=
  match a with
  | ⟨_, []⟩ => 1
  | ⟨_, args⟩ => 1 + (args.map mysize |> List.sum)

I know I could define it as partial and I suppose I could work with List, but I'd like to understand how I could prove these definitions terminate if I want them?

[David Thrane Christiansen]

It seems to me that the second one works with Array as well:

structure App where
  f : String
  args : Array App
deriving Repr, Inhabited

def App.mysize (a : App) : Nat :=
  match a with
  | ⟨_, args⟩ => 1 + (args.map mysize |> Array.sum)

This version goes through because the match on a replaces it in the proof goals with ⟨_, args⟩, which allows sizeOf a.argsto be replaced with sizeOf args. There's also a preprocessing step that rewrites args.map f to args.attach.map fun ⟨x, h⟩ => f x, so h becomes a proof that x is contained in args. This proof lets the automation conclude that sizeOf x < sizeOf args, which can be used to prove the overall goal that sizeOf x < sizeOf ⟨_, args⟩ (equivalent to sizeOf x < 1 + sizeOf f + sizeOf args, where f is the _ from the pattern).

To replicate this for a version without pattern matching, you can write this proof:

def App.mysizeOf (a : App) : Nat :=
  1 + (a.args.map mysizeOf).sum
termination_by a
decreasing_by
  let ⟨f, args⟩ := a
  decreasing_tactic

The case analysis on a using the let tactic results in this goal:

a x✝ : App
f : String
args : Array App
h✝ : x✝ ∈ { f := f, args := args }.args
⊢ sizeOf x✝ < sizeOf { f := f, args := args }

decreasing_tactic is what's used by the automation; it can prove this.

In case that's still too magical, here's a manual, pedantic proof that you should not write except to better understand what's going on:

def App.mysizeOf (a : App) : Nat :=
  1 + (a.args.map mysizeOf).sum
termination_by a
decreasing_by
  next h =>
    let ⟨f, args⟩ := a
    -- First conclude that sizeOf x < sizeOf args
    have := Array.sizeOf_lt_of_mem h
    -- Next rewrite the goal to be in terms of addition of sizes of arguments to App.mk
    rw [App.mk.sizeOf_spec]
    -- Goal is: `sizeOf x✝ < 1 + sizeOf f + sizeOf args`
    -- Lemma type is `{a b : Nat} (c : Nat) (h : a < b) : a < c + b`
    exact Nat.lt_add_left (1 + sizeOf f) this

[Philip Zucker]

Wow! Thank you! Fantastic response. Yes, I was mistaken about Array not working on the second version

[Philip Zucker]

Actually I take back what I said with it working both ways. Trying it again, I do have a difference. I did have a silly redundant match on #[], but that's what I wrote translating without thinking my code. The version with the redundant branch is automatically proved terminating with List but Array does not pass automatically

def App.mysize3 (a : App) : Nat :=
  match a with
  | ⟨_, #[]⟩ => 1
  | ⟨_, args⟩ => 1 + (args.map mysize3 |>.sum)
  decreasing_by
  next h =>
  have p := Array.sizeOf_lt_of_mem h
  simp

f✝ : String
args : Array App
x✝ : App
h : x✝ ∈ args
p : sizeOf x✝ < sizeOf args
⊢ sizeOf x✝ < 1 + sizeOf f✝ + sizeOf args

I am also confused why this goal isn't discharging via grind or descreasing_tactic

I know this is sort of a case of "if it hurts to poke yourself in the eye, don't do it" but I don't have a mental model why the redundant branch is bad for termination checking or why Array is worse (I think this is because for proof purposes array is translated to List?).

[Robin Arnez]

That's because of lean4#9846. You can try

def App.mysize (a : App) : Nat :=
  if a.args.isEmpty then
    1
  else
    match a with
    | ⟨_, args⟩ => 1 + (args.map mysize |> Array.sum)

instead if you want to keep the redundant case