RFC: simp control over recursive functions (or lemmas)

When dealing with recursive functions (in particular, but not exclusively, those defined by well-founded recursion), one often encounters the problem of equational theorems that will make simp loop. For example

def foo (n : Nat) : Nat :=
  if h : n = 0 then 0 else foo (n - 1)

theorem ex1 : foo 10 = 0 := by simp [foo]
theorem ex2 : foo n = foo (n + 1) := by simp [foo] -- maximum recursion depth has been reached

#check foo._eq_1 -- foo._eq_1 (n : Nat) : foo n = if h : n = 0 then 0 else foo (n - 1)

I’d argue that the user writing simp [foo] can have two distinct intentions:

1. Please unfold foo, once
2. Really do simplify with foo’s equations, possibly recursively.

A strawperson syntax could be

1. simp [foo] for rewriting with foo non-recursively, and
2. simp [*foo] for the rewriting with foo arbitrarily often.

If Lean would know which one the user actually wanted, it could be smarter about it. In the first case, the simplifier could presumably not simplify occurrences of foo that appear due to rewriting with foo’s equations. This way, simp [foo] would always work reliably without looping, and the extra power would be just one character away.

Variant: SimpTheorem counters

If recognizing recursive occurrences is hard, or if such a mechanism would be useful for simp [arbitrary_eq_theorem], then a variant of this idea would be a general “lemma counter” for simp, for example simp [3×some_equality] will apply some_equality at most 3 times, with simp [∞×some_equality] being the current behavior. With such annotations in place, maybe the default for simp [foo] where foo is a function definition (not a lemma) could be simp [1×foo]; not quite the same as “foo non-recursively”, but maybe a close enough approximation, easier to generalize to other lemmas, and maybe easier to implement.

But: Unclear how to get this behavior given simp's cache.

Community Feedback

None yet

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.

No implementation files or tests are identified. Start by locating the simp implementation and its cache, then compare the proposed one-use and bounded-counter semantics against the recursive foo example. Done would require an agreed design and corresponding behavior, but this RFC provides no concrete acceptance test.