structural recursion over inductive predicates struggle with reflexive inductives

[mik-jozef]

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] 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”)
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.

Description

The following code

inductive F: Prop where
  | base
  | step (fn: Nat → F)

def F.asdf: F → True
  | base => trivial
  | step f => F.asdf (f 0)

results in the following error

fail to show termination for
  F.asdf
with errors
structural recursion cannot be used:

Context

This is a variation of a very similar previous issue. Just like previously, making F a Type rather than a Prop makes the error disappear

Steps to Reproduce

Expected behavior: There are no errors, the recursion is recognized as structural recursion.

Actual behavior: The error is present.

Versions

4.11.0-nightly-2024-07-12

Impact

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

[nomeata]

So here is what’s happening. I generalized this a bit to make it clearer

def TTrue (_f : F) := True

def F.asdf : (f : F) → TTrue f
  | base => trivial
  | step f => F.asdf (f 0)
termination_by structural f => f

This gives

Cannot use parameter #1:
  could not solve using backwards chaining 
x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : ∀ (a : Nat), TTrue (f a)
⊢ TTrue (f 0)

Now it seems strange that this cannot be solved, we have a✝ right there! And indeed it is tried, and the current goal is unified with a✝ ?a, and this unification succeeds. The problem is that the new metavariable ?a : Nat is not assigned during this unification, because f a is a Prop and thus this is solved by proof irrelevance.

Unfortunately, wrapping the search operation in withoutProofIrrelevance does not seem to help.

Anyways, even if we could make lean unify a with 0 here, it wouldn’t help us in your case

failed to infer structural recursion:
Cannot use parameter #1:
  could not solve using backwards chaining 
x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True

where the 0 has disappeared, so a simple backwards chaining search has little hope of finding the right argument to a✝.

TL;DR: With the current architecture, I doubt whether reflexive data types can be supported reliably by the IndPred construction.

@DanielFabian, does this sound about right?

[DanielFabian]

this latter proof state is a bit different from what I would've expected. Why is the def unfolded? I believe in my initial implementation, the algorithm would've simply done an apply a✝. Which should constrain the bound a to be 0 and thus require a proof that 0 : Nat which the metavar would do automatically?

I don't remember seeing definitions being unfolded. Also, what does withoutProofIrrelevance do?

[DanielFabian]

in my original case, the metavar ?a : Nat would've blocked the backwards chaining because there were multiple objects of the correct type, and picking one by assumption could pick the wrong one, thus leading to unprovable goals. Here, the ?a completely disappeared.

[DanielFabian]

here's the detailed state that was the issue with backwards chaining that we thought to be related: https://github.com/leanprover/lean4/issues/1672#issuecomment-1264617056

[nomeata]

Hmm, that seems to be about mkBelow, not about about the equation compiler.

this latter proof state is a bit different from what I would've expected. Why is the def unfolded?

sorry for being unclear; this is from the original example

inductive F: Prop where
  | base
  | step (fn: Nat → F)

def F.asdf: F → True
  | base => trivial
  | step f => F.asdf (f 0)

where the type of the function does not depend on the parameter. So not def being unfolded, the return type of the recursive call simply is True, and thus leads to

x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True

---

I wonder if it might help to let-bind the type of the recursive function as a local variable, say C, so that one gets

C : F → Prop := fun _ => True
x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : (a : Nat) → C (f a)
⊢ C (f 0)

at least if one is careful not to reduce C. Then at least the information about the arguments isn't lost, although one still can’t just use apply, and would have to use some other way to match to actually instantiate the Nat parameter:

example (f : Nat → True) : True := by
    let C := fun (_ : Nat) => True
    replace f : (n : Nat) → C n := f
    change C 0
    apply f
    -- still unsolved goal of type Nat here
    done

[nomeata]

Oh, I like that last idea: perform termination checking and compilation with an abstract motive for the function (in all three variants of termination checking). After all, termination checking is completely independent of the return type and only cares about the arguments. This way, when calculating the functional induction principles, I (hope I) don't have to do so much complicated surgery on the terms (MatcherApp.transform), and maybe a fair amount of complex code can go. We just™ have to be careful not to unfold the let-bound motive unnecessarily. I'll play with that idea some time maybe. And maybe it can help with the present issue as well.

[DanielFabian]

sounds promising, keep me posted, please.