RFC: simp control over recursive functions (or lemmas)

[nomeata]

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.

[nomeata]

This idea came up in a discussion right now, so writing it down here for reference.

[kmill]

I like the direction of the simp theorem counters idea, since sometimes you want to do something like simp only [1×add_comm] to do a single rewrite "under a binder".

My feeling is that in general one wants recursive definitions to be unfolded arbitrarily deeply, though there are some caveats here — my experience is with structural recursion, where there's no harm in doing this, unlike your foo example. I think I'd prefer simp [*foo] over simp [∞×foo] for being easier to type, even if it's less consistent. Or maybe simp [1*add_comm] is fine syntax? I can't think of an example where this would be ambiguous with multiplication (edit: it might be odd having * have a separate meaning in simp [*]).

[nomeata]

Leo pointed out that the counter variant doesn’t play very nicely with the simp cache. So maybe recursive-or-not is the more plausible way.

[nomeata]

For the non-counting variant (simp [foo] vs. simp [*foo]), I am wondering what the precise specification and possibly implementation should be.

The question will be: If simp encounters an occurrence of foo, should it rewrite it or not.
I see two variants.

1. For all functions not marked with a *, only rewrite those occurrences that were visible in the goal before simp ran. This way, every occurrence that arises as an result of a rewrite, in particular those on the RHS of foo’s equational lemmas, will not be rewritten.

2. Whenever we apply the equational lemma for foo (or it's mutually recursive siblings…), we somehow mark all ocurrences of foo in that lemma’s RHS as “should not be rewritten any further”. This marker needs to be preserved by other rewrite rules, though.

Variant 1 is more restrictive: If the goal is bar 42 then simp [bar_eq_foo, foo] will stop after rewriting to foo 42, whereas in the second case it would continue to rewrite foo (once).

But Variant 2 seems trickier; what if we have a rule P_foo : P (foo 42) = P (foo 23), and the goal is P (foo 42) where the foo is already such a recursive call that we do not want to unfold further. Should P_foo apply? Should the foo it rewrites to be considered a recursive call (no further unfolding), or should it be ok to unfold.

Given these complexities, leaning towards 1.

A possible implementation of variant 1 could be a preprocessing step that goes through the goal and wraps every mention of foo with a marker (.mdata or an id-like function, not sure). Then SimpTheorems.addDeclToUnfold in the non-recursive case could massage the eqns to match only on the function with the marker. (And other theorems matching on foo would have to look through it?). A postprocessing step would finally have to remove all these markers.

This is all pushing the complexity budget quite a bit; not sure what to make of that.