Status quo

Currently (assuming #2921), the termination_by syntax expect a list, possibly empty, of identifiers (or _), then =>, and then the body.

The semantics is that the names in the list override any variable names from the back. Examples:

def foo (n : Nat) : Nat := foo (n-1)
termination_by n => n

works but equivalently

def foo (n : Nat) : Nat := foo (n-1)
termination_by => n

or

def foo (n : Nat) : Nat := foo (n-1)
termination_by m => m

This is a bit silly: Why would the user not want to use the variable name given in the header? Is there ever a compelling reason?

Of course, the list of variables do have their justification: When the function arguments are not in the header, but bound by a lambda or by match equations:

def foo : Nat → Nat := fun n => foo (n-1)
termination_by n => n

or

def foo : Nat → Nat
 | 0 => 0
 | n => foo (n-1)
termination_by n => n

If there are variables both in the header and in the lambda/matches, the list is applied from the right:

def foo (a b : Nat) : Nat → Nat → Nat
 | 0, 0 => 0
 | c, d => foo (a-1) (b - 1) (c - 1) (d-1)
termination_by _ x y z => x -- termination goal: b - 1 < b

and you can wildly mix overriding variable names and referring to the original name using _:

termination_by x _  _ y => x + b + y -- termination goal: (a - 1) + (b - 1) + (d - 1) < a + b + d

Oddities

This works, and knowing the implementation it’s not surprised it behaves like this, but it is a bit odd:

• When no variable needs to be introduced, the arrow in termination_by => n looks odd.
• The right-to-left rule is probably not intuitive.
• Usually it is easy to predict how many parameters “after the :” lean considers, but maybe not always.
• I find hard to justify why the user even can change a to x here.

Proposed change

I wonder if our users are not better served with a more rigid syntax:

• The number of variables mentioned must match the number of “unnamed” variables (lambda after the := or discriminants in matches equations). No fewer and not more.
• If there are no such variables, the => must be omitted.

So above the valid variants would be:

def foo (n : Nat) : Nat := foo (n-1)
termination_by n

def foo : Nat → Nat := fun n => foo (n-1)
termination_by n => n

def foo : Nat → Nat
 | 0 => 0
 | n => foo (n-1)
termination_by n => n

def foo (a b : Nat) : Nat → Nat → Nat
 | 0, 0 => 0
 | c, d => foo (a-1) (b - 1) (c - 1) (d-1)
termination_by _ y => a + b + y -- termination goal: (a - 1) + (b - 1) + (d - 1) < a + b + d

If the system requires the user to get the number of variables right, the effect will more likely match the user’s intention than the more liberal “override from left to right”.

Impact

As we are changing the syntax anyways in #3040, the pain of having to touch this code would be mostly alleviated.

The implementation would probably have to carry around a bit of extra book keeping to remember which variables were originally bound before the : and which were afterwards. (This is maybe the reason it’s not already like this). But maybe worth for the extra guard rails.

Maybe there is an good compelling reason to allow users to rename variables? I don't see one yet.

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.