RFC: Run decreasing_by tactic on all goals, not each goal

[nomeata]

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.

[nomeata]

An implementation seems to be rather simple: In mkFix, Just don’t apply the tactic to the MVar at each recursive call, and then use getMVarsNoDelayed after traversing the whole expression.

I have a POC at https://github.com/nomeata/lean-derec-lab/blob/master/Derec/SingleGoal.lean

It would be a breaking change requiring existing uses of decreasing_by foo with decreasing_by all_goals foo.

[leodemoura]

Like the idea, but what about mutual recursion? The actual order may not be clear to users. Recall that we compute SCCs.

[nomeata]

Hmm, yes, the order may be surprising.

We could sort the MVars by the syntax ref maybe to put them back into source code order? (If MVars remember the ref they were created at or if we pass it separately.)

I'll experiment with multiple SCCs and see.

[nomeata]

Hmm, indeed, I didn’t have it on the radar that the termination_by and decreasing_by annotations need to work in cases where they apply to independent recursions. I’ll have to think about that a bit more, also related to the idea of termination_by? etc.

This already causes corner case issues like: If some recursions in the block should be done structurally, and others require a decreasing_by annotation, then you can’t have both, as the presence of decreasing_by makes it always try well-founded recursion:

mutual
def foo : Nat → Nat
 | 0 => 0
 | .succ n => foo n

def bar : Nat → Nat
  | n => if  n = 0 then 0 else bar (n - 1)

end
decreasing_by sorry

Not a problem per se, just an example of the complications to keep in mind here.

[nomeata]

Together with Leo I we had an idea for a nice way that solves

• the problem of ordering the goals,
• the problem that not all functions in a mutual block end up being in the same SCC (and setting up the goal state so that all those unrelated goals are visible) and
• the problem of guessing whether the user wants to do interactive proof, or just specify a different default tactic.

We allow the user to specify the tactic/proof keyed by the function it should be used in; like we already do with terminating_by. This way, the internal order of functions does not leak, and it doesn't matter if only some functions are mutually recursive with some others etc.

What would be a good syntax?

One idea is to use | to indicate that we have multiple cases:

mutual
def foo : Nat → Nat
 | 0 => 0
 | .succ n => bar n + bar (n - 1)

def bar : Nat → Nat
  | n => if  n = 0 then 0 else foo (n - 1)
end
decreasing_by
 | foo => 
   · -- first recursive call in foo
   · -- second recursive call in foo
 | bar => 
   · -- first recursive call in bar

It’s a bit verbose and silly if there is only one recursive function, which is a common case. But at least it’s consistent with recursing_by.

[digama0]

By the way, this relates to a syntax nit that I have been meaning to bring up: Why does decreasing_by / termination_by have to handle all the declarations at once? Couldn't these be placed after the respective definition? And then you wouldn't need the foo => part. Like this:

mutual
def foo : Nat → Nat
 | 0 => 0
 | .succ n => bar n + bar (n - 1)
decreasing_by
 · -- first recursive call in foo
 · -- second recursive call in foo

def bar : Nat → Nat
  | n => if  n = 0 then 0 else foo (n - 1)
decreasing_by
 · -- first recursive call in bar
end

They would still be processed together in the same way as is done currently, this is just a syntactic change.

I can see some reasons for keeping all the termination_by clauses together, if for example it makes it easier to review the functions for the mutual block and see that they interleave appropriately. Perhaps both could be supported and you could mix and match this style with the current everything-at-the-end style if this is a stylistic preference.

[nomeata]

That’s a good idea as well. Makes it also much more natural where to place thigns in case of where or letrec. I wonder what the downsides are.

Perhaps both could be supported

I tend to lean towards less options, as having to decide between options itself is a UX cost, so preferrably only if there are strong reasons to have both.

Maybe decreasing_by … should be used for interactive use, and there ought to be another syntax, like a command (possibly scoped with in)
default_decreasing_tactic <tac> in
to locally change the default termination tactic. That could then be used before mutual.

Do we have precedence for “tactic-valued options”?

[nomeata]

Ah, one possible reason to have a common decreasing_by is that you probably start many proofs, even interactive ones, with all_goals simp_wf and similar preparation steps. They would have to repeated if we invoke the tactic on each function separately. (But my intuition is that that’s not too bad, and the syntactic clarity and simplicity of per-function decreasing_by still looks good.)

[nomeata]

I rewrote the proposal to include some of the ideas from this discussion, in particular

• Per-function termination_by and decreasing_by.
• Separate `default_decreasing_by for non-interactive proofs.

[Kha]

Is there a concrete syntax proposal in the case of let rec and where yet?

[nomeata]

I didn't spell it out yet, but my hope is that both termination_by and decreasing_by will just be attached to the individual function definitions, even if they are in a letrec or where. Do you expect problems with that?

[Kha]

I suppose it would have to be indentation sensitive at least. Indentation would determine whether a clause belongs to the last where or to the top-level function

[nomeata]

Ah, I see. I sometimes forget that Lean is less indentation sensitive than it looks like :-)

Do you think that’s feasible and reasonable?

[Kha]

Yes to both I think. At least it's where I, probably, would have tried to put them as a user.

[digama0]

I think it would also be okay to have the termination_by before where for clauses associated to the main declaration.

[nomeata]

I just had a discussion with Leo about this, and he’s generally supportive of this idea. I thus plan to work on this eventually.

[nomeata]

I made good progress here in #3040, and would like to have some feedback regarding the parsing of termination_by and decreasing_by, in particular after where.

I am currently experimenting with checkColGE before the keyword, see
https://github.com/leanprover/lean4/blob/1bf34f13cc/tests/lean/termination_by_where.lean
for the effect. As long as the user indents either the where or the function definition therein, this works fine: By choosing the right indentation, the use can make sure the termination_by is picked up by the right function.

The corner case that doesn't work if there is no indentation, like in

def Ex9.foo (n : Nat) : Nat := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt

Not sure how relevant that is in practice; if the rule otherwise works well and simple, maybe this is ok?

Or is there a better solution for this problem?

[digama0]

My suggestion would be to have the decreasing_by come before the where when applying it directly to the main function. That is:

def Ex9.foo (n : Nat) : Nat := foo (dec1 n) + bar n
decreasing_by apply dec1_lt -- this applies to foo
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt -- this applies to bar

For backward compatibility (and for convenience when using the same tactic in multiple places) we may wish to also have termination_by/decreasing_by at the top level of the SCC as is done currently, and in that case this example really would be ambiguous. I would suggest to interpret it as the decreasing_by block for bar, and you would have to indent bar if you want to write an overall decreasing_by.

(You should probably think about how migration is going to go here, because this will break every termination_by and most decreasing_by blocks in the wild. Will there be a code action or something?)

[nomeata]

I thought about putting it before the where as well, but it's also a bit odd in the sense that where is a term-level thing and can be attached to arbitrary terms, not just complete function RHSs.

As for migration: the current plan is to move fast and break things, knowing that this is an approach we can only do for so much longer, but can for now. It's basically impossible to support both syntaxes at the same time, because they unfortunately overlap and it's hard to know whether termination_by f g = f is old syntax (applicable to function f) or new syntax (binary fiction). Leo says that some time in the future we'll have to spend the effort here, but not yet.

What would make the migration easier without too much overhead is, I believe, if the keyword termination_by would change, because then at least there would be a clear parse error. So if there is a better keyword that we'll be happy to have switched to, now is a great time for that. Any hidden desires in that direction?

decreasing_on comes to mind; it's a bit more explicit, reads rather nicely as prose (“This function is decreasing on x, and decreasing by omega”), more obviously connected to decreasing_by and it means that stuff ending on by is more consistently a tactic.

[digama0]

I thought about putting it before the where as well, but it's also a bit odd in the sense that where is a term-level thing and can be attached to arbitrary terms, not just complete function RHSs.

It's not though? That would be nice, but that's not the current situation.

As for migration: the current plan is to move fast and break things, knowing that this is an approach we can only do for so much longer, but can for now. It's basically impossible to support both syntaxes at the same time, because they unfortunately overlap

I think it would be okay to have a simpler backup syntax like termination_by* (or even old_termination_by if you want to make it obviously placeholder-looking) for being able to get to the old syntax. Then it would be possible to do the migration by simply find/replacing termination_by to termination_by* and then use a code action to do the more involved syntax transformation. Without the intermediate termination_by* syntax, this migration becomes 10x harder because now you have hundreds of parse errors on your hands and none of lean's tools handle this well.

I would really like us to start thinking about how to do these things sooner rather than later, because the need for it is not ever going to go away and at least for this change it's worth putting in the effort to automate this to some degree just for the mathlib bump.

[nomeata]

It's not though? That would be nice, but that's not the current situation.

Ah, I got confused by the namespace of the Term.whereDecls parser. It seems that I’d have to insert it into various places; at least bothBut I guess you say that we can insert the termination hints into this parser

def declValSimple    := leading_parser
  " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls

and

def declValEqns      := leading_parser
  Term.matchAltsWhereDecls
…
@[run_builtin_parser_attribute_hooks]
def matchAltsWhereDecls := leading_parser
  matchAlts >> optional whereDecls

But that’s worth a try! Avoiding the ambiguities with where is certainly desirable; I just wrote an even longr test file for the various indentation combinations, and it would be nice to not have to think about it.

[nomeata]

I think it would be okay to have a simpler backup syntax like termination_by* (or even old_termination_by if you want to make it obviously placeholder-looking) for being able to get to the old syntax.

Do you propose that we keep the old (renamed) syntax, so that we don’t have an unhelpful parse error, but rather a helpful elaboration error, but still an error? Or do you want the old syntax to also to still work, which means the internal data strutures and logic have to support both variant at the same time?

Mathlib has 121 occurrences of termination_by, of which only one is a mutual block, and the rest should be fixable with a single sed script. For std I see 34 occurrences; there I sense more where blocks where the declaration has to be moved (if I end up implementing the suggestion above).

Yes, it’s more convenient if you can migrate parsing (or even fully working) code, but I’m not surprised it’s worth the detour at this point.

[digama0]

Do you propose that we keep the old (renamed) syntax, so that we don’t have an unhelpful parse error, but rather a helpful elaboration error, but still an error? Or do you want the old syntax to also to still work, which means the internal data strutures and logic have to support both variant at the same time?

I'd prefer if it still works. It should be relatively straightforward to normalize both syntaxes into one data structure and process them with the new code. My understanding is that this kind of syntactic normalization is a major reason for the DefView et al types in the first place.

Mathlib has 121 occurrences of termination_by, of which only one is a mutual block, and the rest should be fixable with a single sed script. For std I see 34 occurrences; there I sense more where blocks where the declaration has to be moved (if I end up implementing the suggestion above).

I'm also concerned about more than just std + mathlib here: Big CS projects doing formal verification tend to involve complex inductive types and termination measures, so I anticipate a fair amount of breakage in code we don't have much visibility into.

[nomeata]

It's certainly doable (although it'd be nicer if the syntaxes wouldn't overlap, and one would not have to rename to _old and then start migrate, e.g. with a different keyword. And it's not just syntax because of the changed semantics of decreasing_by running on all or each goal). It's just a question where to spend resources.

[emina]

I'm also concerned about more than just std + mathlib here: Big CS projects doing formal verification tend to involve complex inductive types and termination measures, so I anticipate a fair amount of breakage in code we don't have much visibility into.

For what it's worth, we're working on a fairly large CS verification project in Lean, and we'd be okay with adopting the new syntax: https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean

We do indeed have complex inductive types, but so far, Lean hasn't needed much help proving termination. We have just 5 occurrences of termination_by and no occurrences of decreasing_by.

If it helps, this is the entry point to our most complex proof so far: https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/Thm/Validation/Typechecker.lean

[nomeata]

While working on this, I noticed that there is another bit of termination_by syntax polishing that might be worth doing in one go. I’ve opened #3081 for that discussion, comments welcome.