structural recursion fails when matching on `f x` where `f ` is argument’s subterm

arthur-adjedj commented 2 days ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Mutual/Nested structural recursion seems to fail on large inductive types. Consider the following example:

inductive Foo where
  | foo : (String → Option Foo) → Foo

def Foo.map (m : Foo → Foo) : Foo → Foo
  | .foo f => .foo fun s => match f s with
    | none => none
    | some x => map m x
termination_by structural x => x

Despite structural recursion being supported on both large inductive types and nested inductives, mixing the two leads to a failure. In a similar manner, the following function recursing over a large mutual inductive fails with the same error:

mutual
inductive Bar where
  | none
  | some (x : Foo)

inductive Foo where
  | foo : (String → Bar) → Foo
end

def Foo.map (m : Foo → Foo) : Foo → Foo
  | .foo f => .foo fun s => match f s with
    | .none => .none
    | .some x => .some (map m x)
termination_by structural x => x

Expected behavior: No error, these functions get accepted

Actual behavior: Structural recursion fails with the following error:

failed to infer structural recursion:
Cannot use parameter #2:
  failed to eliminate recursive application
    map m x

Versions

Lean 4.12.0-nightly-2024-10-24 Target: x86_64-unknown-linux-gnu

Impact

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

nomeata commented 2 days ago

I briefly investigated, and it seems that this is out of reach with the current architecture.

The problem is at match f s with. At this point we have this “below” value

[Elab.definition.structural] below before matcherApp.addArg: x✝ : (Foo.foo f).below

If we’d match f now, then matcherApp.addArg? would notice that we are refining the type of this value, and add it, and we’d get a “better” below value in the branches.

But matching on f s does not refine the type of the below value, so addArg? fails, and we lost the game.

For this to work I could imagine a different approach: Instead of passing down one below value that we (try to) refine through each match, but only at recursive calls try to take apart and find the actual entry, we keep track of a mapping from fvar to corresponding below value, initially from the function parameter of interest. Before a match we see if any of the match targets are in the mapping (or are applications of such fvars, to support the large inductives case), and if so, add the corresponding below value to the match. In each alt, look at the newly bound variables and search among in the below values for a corresponding entry (like we do for recursive calls now).

Unfortunately this would make the FunInd transformation a bit more complicated, with multiple “below values” to rewrite.

There exists a work-around:


mutual
def Foo.bar (m : Foo → Foo) : Foo → Foo
  | .foo f => .foo fun s => Foo.bar_aux m (f s)
termination_by structural x => x

def Foo.bar_aux (m : Foo → Foo) : Option Foo → Option Foo
    | none => none
    | some x => bar m x
termination_by structural x => x
end

So since it’s hard to fix, and there is a work-around, I’m demoting this to low, until someone makes a point that I am underestimating the severity.

nomeata commented 2 days ago

Oh, and it’s not actually related to nested or mutual inductive:

inductive Foo where
  | none
  | foo : (String → Foo) → Foo

/--
error: failed to infer structural recursion:
Cannot use parameter #2:
  failed to eliminate recursive application
    map m (f₂ s)
-/
#guard_msgs in
def Foo.map (m : Foo → Foo) : Foo → Foo
  | none => none
  | .foo f => .foo fun s => match f s with
    | none => none
    | foo f₂ => .foo fun s => map m (f₂ s)
termination_by structural x => x

nomeata commented 1 day ago

There is also a comment in the code about this not working, which would work with the alternative implementation above:

             def g (xs : List Nat) : Nat :=
             match xs with
             | [] => 0
             | y::ys =>
               match ys with
               | []       => 1
               | _::_::zs => g zs + 1
               | zs       => g ys + 2

I know I demoted it to low, but it’s weekend, and it’s itching under my fingernails, so maybe I’ll give it a shot.

nomeata commented 1 day ago

Hmm, I hit a roadblock in that search in in below (x :: xs) for the below xs value therein is tricky. Would work if either below had smart unfolding, or if from xs we would construct the below xs value (with the right motive, and even with mutual recursions around). Shelving at https://github.com/leanprover/lean4/pull/5849.

leanprover / lean4