Problem: Interactive termination proofs

Consider the (of course non-terminating) definition:

def foo (n : Nat) : Nat :=  foo (n - 1) + foo n + foo (n + 1)
decreasing_by …

The tactic passed to decreasing_by is currently executed on each recursive call separately, with one goal present. This makes it harder to write these termination tactics individually, for example when different recursive calls need widely different approaches, because whatever you write has to work with all goals at the same time.

As a user I would have expected to be able to focus individual calls with \., like so

def foo (n : Nat) : Nat := foo (n - 1) + foo n + foo (n + 1)
decreasing_by
  · trace_state; sorry
  · trace_state; sorry
  · trace_state; sorry

but here the second \. says “no goals to be solved”.

Solution: One subgoal for each recursive goal

To solve this, the proof following decreasing_by should have the proof obligations for each recursive call as a separate subgoal.

This has a few knock-on effects:

Problem: Mutual recursion and SCCs

If we have a mutual block (or local where, letrec), then Lean will look at all involved definitions, build strongly connected components (SCCs), and derecursify each SCC individually.

It seems technically hard to get all subgoals from these independent definitions into a single TacticM state. Furthremore, the user experience would be bad if the order of subgoals would change, and sorting the subgoals afterwards is tricky.

Solution: Per-function decreasing_by.

A good solution to this problem seems to be to attach the decreasing_by to each function definition, e.g.

mutual
def even : Nat → Nat := …
decreasing_by …

def odd : Nat → Nat := …
decreasing_by …
end

This naturally associates the proofs with the subgoals of that function. It is arguably also more intuitive in cases of letrec or where.

Problem: What happens to terminating_by?

Now that decreasing_by is attached to each function, it would be strange to not do the same for terminating_by.

Solution: Per-function terminating_by

So let’s also move it to per-function. This has the additional effect that we can simplify the syntax and not require the function name as part of the termination hint.

So instead of

mutual
def even : Nat → Nat := …

def odd : Nat → Nat := …
end
terminating_by
  even n => n
  odd n => n

we would write

mutual
def even : Nat → Nat := …
terminating_by n => n

def odd : Nat → Nat := …
terminating_by n => n
end

Problem: Changing the default tactic

At the moment, decreasing_by is used for two similar, but distinct use-cases:

1. Interactive long termination proofs
2. Using a tactic for automatic proofs that’s different than decreasing_tactic.

For example, if there is no termination_by clause, and Lean wants to guess the right measure. It’d be silly to apply the interactive proof when Lean is trying out various measures. But if the user has configured a different automatic tactic, then guessing the measure is sensible.

Also, for interactive proofs, red squiggly lines should be placed in the interactive proof, while for automatic proofs, the recursive call that cannot be proven should be highlighted.

Solution: Command to change default decrasing_tactic tactic

This calls for different command/syntax for the two use cases. The proposal is to use decreasing_by for interactive proofs. This means

• Applied once to all goals
• Error highlighted in the proof
• Requires a terminating_by clause, as we cannot guess the order. (Maybe allow to omit if there is exactly one changing parameter).

For temporarily using a different automatic tactic, introduce a command

default_decreasing_by <tac>

that effectively works like termination_by now:

• Applied to each goal separately
• Errors highlight the recursive call
• If not specified, default_decreasing_by is used.

Typical use might be

default_decreasing_by <tac> in
def ackerman …

or

default_decreasing_by <tac> in
mutual
def even …
def odd
end

which should feel familiar to the users (similar to set_option).

This seems to be a serious papercut: Users should have a nice environment to write these proofs interactively. So ideally, the following should hold

1. When writing decreasing_by proofs interactively, there should be recursive calls for each subgoal.
2. The grouping-by-SCC done internally by lean should not affect the user (predictable order of subgoals etc.)
3. When using the default termination tactic.

Open questions

• This is a breaking change: Some terminating_by need to be moved, some decreasing_by may become default_decreasing_by … in. Is this worth it? Should we try to find a backward compat way of achieving the goals (at the expense of a possibly worse UX)?

• Is there a good way to name each recursive call, either automatically or manually, so that case <name> => can be used? Such names will also come in handy when deriving an induction principle from a recursive definition.

  We could say that whenever the recursive call is let-bound, we use the name as case name:

  def foo (n : Nat) : Nat :=
    let n1 := foo (n - 1)
    let n2 := foo (n - 2)
    n1 + n2
  

  Too ad-hoc?

Community Feedback

Initial discussion on Zulip (but not much activity).

Impact

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