Superfluous parentheses can inhibit structural recursion

[kmill]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When additional parentheses are inserted around a function, this can prevent structural recursion from succeeding.

Simple example:

def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => (f) n

With the parentheses, "structural recursion cannot be used." Replacing (f) n with f n makes it succeed. Looking at the terms (f) n and f n, the difference is whether n is included within the recApp metadata expression.

This behavior indirectly appeared in a Zulip question when trying to make use of structural recursion within a theorem. This is a minified example:

theorem thm (N : Nat) :
    N * 0 = 0 :=
  match N with
  | Nat.zero => rfl
  | Nat.succ n => by
    rewrite [Nat.succ_mul, Nat.add_zero]
    rw [thm]

Replacing rw [thm] with rw [thm n] makes structural recursion succeed -- the terms are identical except for whether n is included within a recApp metadata expression. Replacing rw [thm] by simp only [thm] also makes it succeed -- in this case simp does not create an appRec metadata expression.

Context

Zulip discussion

Versions

leanprover/lean4:v4.3.0-rc1

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[nomeata]

I ran into this issues a few weeks ago as well, while helping some user.

Mostly a guess at this point, so jumping in here just for learning, but probably at this line:

https://github.com/leanprover/lean4/blob/e217ad3929ed1c6f3dc71d5d47e18458b2357e39/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean#L124

the withApp may need to be a variant looks through the recApp metadata?

[digama0]

I think that would work to recognize this application, but this is in the context of something that is transforming the expression, so you shouldn't throw away any mdata except the _recApp node; see the .mdata case of the same function. I think this will need another recursive function doing the equivalent of withApp.

[nomeata]

Yes, I’d expect a annoyingly special withAppIgnoringRecApp.

[nomeata]

Let me give this a shot. I am supposed to work on that code soon anyways, so it’s a good learning experience.