structural recursion fails in the equation compiler

[b-mehta]

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

variable {α : Type}
variable (r : α → α → Prop)

/-- `SymmGen r` is the symmetric relation generated by `r`. -/
inductive SymmGen : α → α → Prop
  | rel : ∀ x y, r x y → SymmGen x y
  | symm : ∀ x y, SymmGen x y → SymmGen y x

def MyRel : Nat → Nat → Prop := SymmGen fun x y => y = x + 2

theorem preserve_add' {a : Nat} : ∀ {x y : Nat}, MyRel x y → MyRel (x + a) (y + a)
| _, _, SymmGen.rel _ _ h => SymmGen.rel _ _ (by rw [h, Nat.add_right_comm])
| _, _, SymmGen.symm _ _ h => SymmGen.symm _ _ (preserve_add' h)
termination_by structural _ _ x => x

The second case errors, despite being applied to a structurally smaller term.

Context

Discussion thread

Steps to Reproduce

1. Code as above.

Expected behavior:
Code compiles with no error.

Actual behavior:
Code errors, with error message

failed to infer structural recursion:
Cannot use parameter #4:
  could not add below discriminan

Versions

Same behaviour on:
live.lean-lang.org current (4.9.0-rc2)
live.lean-lang.org nightly (4.10.0-nightly-2024-06-23, 4.12.0-nightly-2024-08-22)
MacOS Monterey 4.9.0-rc1

Impact

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

[nomeata]

Thanks! Does the former example depend on the def MyRel definition to trigger the issue?

[b-mehta]

I think so, in the sense that I don't know how to modify the example to avoid that definition.

[nomeata]

I'm on the phone so I can't try, but can you not unfold it in the type of preserve_add'?

[nomeata]

Ah, I must have looked at it before in April and found:

Based on the available trace options, the issue is somewhere in

def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
  xs.findSomeM? fun x => do
  let xTy ← inferType x
  xTy.withApp fun f _ =>
  match f.constName?, xs.indexOf? x with
  | some name, some idx => do                                                                       if (← isInductivePredicate name) then
      let (_, belowTy) ← belowType motive xs idx                                                      let below ← mkFreshExprSyntheticOpaqueMVar belowTy
      try
        trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
        if (← backwardsChaining below.mvarId! 10) then
          trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)                      else
          trace[Meta.IndPredBelow.match] "could not find below term in the local context"
          pure none
      catch _ => pure none
    else pure none
  | _, _ => pure none

(Adding this here just for future reference)

[b-mehta]

Woah, I see! The former example does depend on the definition to trigger the issue: unfolding it manually as you say makes the error disappear.

Marking the def @[inline, reducible] does not make the error disappear.

[nomeata]

Thanks for checking, this will certainly help whenever someone gets around debugging this :-)

[nomeata]

It also makes me wonder if the second example has the same cause, as no def is involved there.

[leodemoura]

@nomeata Yes, both examples are hitting bugs in the structural predicate recursion module: IndPred.lean.
@DanielFabian Any ideas on what might be the problem?

@b-mehta Possible workaround: define SymmGen and Steps in Type. It is not great, but it will work around the problem.

variable {α : Type}
variable (r : α → α → Prop)

/-- `SymmGen r` is the symmetric relation generated by `r`. -/
inductive SymmGen : α → α → Type where
  | rel : ∀ x y, r x y → SymmGen x y
  | symm : ∀ x y, SymmGen x y → SymmGen y x

def MyRel : Nat → Nat → Type := SymmGen fun x y => y = x + 2

def preserve_add' {a : Nat} : ∀ {x y : Nat}, MyRel x y → MyRel (x + a) (y + a)
| _, _, SymmGen.rel _ _ h => SymmGen.rel _ _ (by rw [h, Nat.add_right_comm])
| _, _, SymmGen.symm _ _ h => SymmGen.symm _ _ (preserve_add' h)

variable {Tm : Type}

inductive Steps (Step : Tm → Tm → Prop): Tm → Tm → Type :=
  | trans {a b c} : Step a b → Steps Step b c → Steps Step a c

def stepsTrans {Step} {a b c : Tm} (r₁ : Steps Step a b) (r₂ : Steps Step b c) : Steps Step a c :=
  match r₁ with
  | Steps.trans r r₁ => Steps.trans r (stepsTrans r₁ r₂)

[b-mehta]

Thanks for the workaround! The one I went with was to use the induction tactic, which worked for me instead. But I still find the equation compiler more aesthetically pleasing, hence this report.

[DanielFabian]

Without debugging my first guess would be that it fails in backwards chaining. That's also the root cause of the other bug ypu tagged me on. Basically, backwards chaining is greedy and not exhaustive iirc. We wanted to use a more powerful tactic here, i believe. Would it be possible to print the proof state as its trying to do the backward chaining?

[DanielFabian]

adding #1672 as a reference. We may well have the same problem; I need to figure out how I got the proof state in the other case. But if my guess is right, we are again in a situation where the compiler picks the wrong one of a few possible objects and as that adjusts the goals they become unprovable.

The solution would be to try all applicable objects of the correct type and backtrack.

[DanielFabian]

Ok, I did find at least, that it's probably not a problem with backwards chaining, as the code doesn't even seem to get to the first trace line in the try block.

[DanielFabian]

@leodemoura I'd need a bit of a crash course in how to debug lean again if I'm to try and find what's going on. It doesn't seem to even get to the tricky bit of synthesizing a proof (unless somebody from your team can take a look with or without me).

[nomeata]

So this particular issue, the one that goes away when unfolding MyRel, clearly points to missing calls to whnf in the code. And indeed with this the example works:

diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index b9fc37fc53..641302b08d 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -377,7 +377,7 @@ where
       loop xs rest belowIndices xIdx (yIdx + 1)

 private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Name × Expr := do
-  (← inferType xs[idx]!).withApp fun type args => do
+  (← whnf (← inferType xs[idx]!)).withApp fun type args => do
     let indName := type.constName!
     let indInfo ← getConstInfoInduct indName
     let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]!]
@@ -554,8 +554,7 @@ where

 def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
   xs.findSomeM? fun x => do
-  let xTy ← inferType x
-  xTy.withApp fun f _ =>
+  (← whnf (← inferType x)).withApp fun f _ =>
   match f.constName?, xs.indexOf? x with
   | some name, some idx => do
     if (← isInductivePredicate name) then

@DanielFabian, does that look reasonably? Are you interested in PR’ing that one (presumably after going through the code and checking if there are other places where you infer a type and should whnf before looking for an inductive predicate?

(I pushed my code and the test case to joachim/test4540, this is on top of termination_by structurally which is quite useful in this test to really focus on this code path.)

While we are at it: I am wondering if the IndBelow code could be unified with the BRecOn code some more. For example it would greatly simplify things if instead of constructing a fresh matcher, we could use Lean.Meta.MatcherApp.addArg like we do in the BRecOn construction. Presumably this would refine the type of the below value just like there … maybe the only difference is that instead of using basic projection (and reduction) to get the value out of the below, we’d need to generate appropriately typed projections for each field in each constructor of the below inductive and use these.

Maybe this would even get rid some of the heuristics and tactics? (The BRecOn code doesn’t need those, after all.)

[DanielFabian]

Do you understand how the construction works? It weaves these smaller witnesses into each of the arguments of the constructors of the predicate. And we prove brecOn for that other predicate. It works really quite differently from the below construction for type valued objects. The idea is that we create a stronger match clause and therefore can read off a below witness.

When I was doing it a few years ago, there didn't seem to be a good way to treat prop and type similarly.

Ultimately it boils down to proof irrelevance that does not allow us to extract any values out of a prop. So instead I need to define a whole parallel structure that's richer than the original prop and carries witnesses in the construction.

Happy to hop on a call and chat about it, if you like.

[nomeata]

I have a cold right now, so not too keen on videocalls today 🤧. I’ll also familiarize myself with the code, and try any possible construction by hand first, more before making more such proposals :-)

[DanielFabian]

honestly no problem, it's a bit complicated and I don't currently remember the whole detail. But essentially it goes more or less like this:

inductive MyProp : Prop
| Nil : MyProp
| Cons : (a: MyProp) → MyProp

for this we'd define an auxiliary prop more or less like this:

inductive MyProp.below : Prop
| Nil : MyProp.below
| Cons : (a: MyProp) → (a_below: below a) → MyProp.below

the a_below is a witness that a is smaller than the current one (sorry, don't remember the correct type at the moment). But crucially we rewrite your original pattern match into a pattern match on top of the MyProp.below type. That works, because it carries all the same information + additionally the below witnesses.

So when you are trying to eliminate the structural recursion and prove the below a property, it's just straight away available in the local ctx. The price we pay, is that we now need to prove the below a property, iirc. And for that we use the backwards chaining.

Again, sorry, if my memory is not 100% accurate, it's been a few years and it was a bit technical.

[nomeata]

Right, so far I could follow. And the MyProp.below has the same purpose as the MyType.below, they have very similar types and semantic content.

So my thought was: Can we leave the .brecOn and .below construction for MyProp as it is, but change the transformation from PreDefinition to a call to .brecOn to be as similar as the one for non-prop recursion.

So in Type we have

inductive N' : Nat → Type where
  | zero : N' 0
  | succ : N' n -> N' (n + 1)

def preserve_succ' : (n : Nat) → N' n → N' (n + 1)
  | .zero, .zero => .succ .zero
  | .succ n, .succ hn => .succ (preserve_pred' n hn)

and get this implementation under the hood

def preserve_succ'_impl : {n : Nat} → N' n → N' (n + 1) := fun {n} x =>
  N'.brecOn x fun {n} x f =>
    (match (motive := (n : Nat) → (x : N' n) → N'.below x → N' (n + 1)) n, x with
      | _, N'.zero => fun x => N'.zero.succ
      | _, N'.succ hn => fun x => N'.succ x.fst.fst)
      f

Note that (curcially!) this match is the original match from preserve_succ, there is no need to create a new match definition. Instead, the N'.below value is added as an “extra argument” and mentioned in the motive, so that it's type in the arms of the match is refined, and x.fst.fst picks out the motive stored in the below.

I have hopes that the same construction should work in the Prop case as well. Refining the index of the .below as we traverse into matches should work just the same. We only™ need to change x.fst.fst and replace these PProd projections with functions that project the values out of a N.below (with known index):

inductive N : Nat → Prop where
  | zero : N 0
  | succ : N n -> N (n + 1)

theorem N.below.succ_1 {n : Nat} {motive : (a : Nat) → N a → Prop} (hn1 : N (n + 1)) :
  @N.below motive (n + 1) hn1 → N n
  | @N.below.succ _ _ hn _ _ => hn

theorem N.below.succ_2 {n : Nat} {motive : (a : Nat) → N a → Prop} (hn1 : N (n + 1)) : 
  (nb : @N.below motive (n + 1) hn1) → @N.below motive n nb.succ_1
  | @N.below.succ _ _ _ hb _ => hb

theorem N.below.succ_3 {n : Nat} {motive : (a : Nat) → N a → Prop} (hn1 : N (n + 1)) : 
  (nb : @N.below motive (n + 1) hn1) → motive n nb.succ_1
  | @N.below.succ _ _ _ _ x => x


theorem preserve_succ_impl : (n : Nat) → N n → N (n + 1) := fun x x_1 =>
  N.brecOn x_1 fun x x_2 f =>
    (match (motive := (x : Nat) → (x_3 : N x) → N.below x_3 → N (x + 1)) x, x_2 with
      | Nat.zero, N.zero => fun x => N.zero.succ
      | Nat.succ n, N.succ hn => fun x => N.succ x.succ_3)
      f

Does this look reasonable?

[DanielFabian]

correct me if I'm wrong, but you can't project anything out of a prop due to proof irrelevance?

[nomeata]

You can as long as you project into Prop! But the motive and the N.below is in Prop, so that should be fine (the code above compiles :-))

[DanielFabian]

i wonder, then, why it didn't work when we were trying to do that a few years ago. Please do try your construction also on this one:

lean4/tests/lean/run/inductive_pred.lean

Line 38 in 18c9792

| ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor

It was one of the motivating examples, I think.

[DanielFabian]

(obviously if we find that your much simpler construction works, then let's ditch mine as it would be needlessly complicated - but let's please not regress what we can prove)

[nomeata]

Ah, thanks, that’s very helpful, and indeed I can’t make it work.

It seems it boils down to the fact that that Lean cannot tell that a value x : Power2.below (Power2.ind h) must have been constructed with the Power2.below.ind constructor, because of proof irrelevance of Power2.

My attempt

-- Status Quo

inductive Power2 : Nat → Prop
  | base : Power2 1
  | ind  : Power2 n → Power2 (2*n) -- Note that index here is not a constructor

theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) 
  | h1, base   => (Nat.mul_one n).symm ▸ h1
  | h1, ind h2 => (Nat.mul_left_comm ..) ▸ .ind (mul h1 h2)

-- Construction in Type

inductive Power2' : Nat → Type
  | base : Power2' 1
  | ind  : Power2' n → Power2' (2*n) -- Note that index here is not a constructor

def Power2'.mul : Power2' n → Power2' m → Power2' (n*m) 
  | h1, base   => (Nat.mul_one n).symm ▸ h1
  | h1, ind h2 => (Nat.mul_left_comm ..) ▸ .ind (mul h1 h2)

set_option pp.match false
set_option pp.proofs true

#print Power2'.mul

-- This is the construction used in Type

noncomputable
def Power2'.mul_impl : {n m : Nat} → Power2' n → Power2' m → Power2' (n * m) :=
fun {n m} x x_1 =>
  Power2'.brecOn (motive := fun {m} x => Power2' n → Power2' (n * m)) x_1
    (fun {m} x f x_2 =>
      Power2'.mul.match_1
        (fun m x x => Power2'.below (motive := fun {m} x => Power2' n → Power2' (n * m)) x → Power2' (n * m)) m x_2 x
        (fun h1 x => (Nat.mul_one n).symm ▸ h1)
        (fun h1 n_1 h2 x => (Nat.mul_left_comm ..) ▸ (x.fst.fst h1).ind) f)
    x

-- To replicate it in Prop, we need a replacement for x.fst.fst
-- If we had a function that can digest a value of type `Power2.below (Power2.ind h)` we could do it:

theorem Power2.below.ind_2_wish {n : Nat} {motive : (a : Nat) → Power2 a → Prop} {h : Power2 n} : 
  (nb : @Power2.below motive (2 * n) (.ind h)) → motive n h := sorry

-- Recall Power2.below
/--/
inductive Power2.below : {motive : (a : Nat) → Power2 a → Prop} → {a : Nat} → Power2 a → Prop
number of parameters: 1
constructors:
Power2.below.base : ∀ {motive : (a : Nat) → Power2 a → Prop}, Power2.base.below
Power2.below.ind : ∀ {motive : (a : Nat) → Power2 a → Prop} {n : Nat} {a : Power2 n},
  a.below → motive n a → (Power2.ind a).below
-/

theorem Power2.mul_impl : {n m : Nat} → Power2 n → Power2 m → Power2 (n * m) :=
fun {n m} x x_1 =>
  @Power2.brecOn (fun {m} x => Power2 n → Power2 (n * m)) _ x_1
    (fun {m} x f x_2 =>
      Power2.mul.match_1
        (fun m x x => @Power2.below (fun {m} x => Power2 n → Power2 (n * m)) _ x → Power2 (n * m)) m x_2 x
        (fun h1 x => (Nat.mul_one n).symm ▸ h1)
        (fun h1 n_1 h2 x => (Nat.mul_left_comm ..) ▸ (.ind (@below.ind_2_wish _ _ h2 x h1))) f)
    x

-- But, as Daniel rightfully expeted, we cannot write that function, due to prop irrelevance

-- tactic 'cases' failed, nested error:
-- dependent elimination failed, failed to solve equation
--   Nat.mul 2 n = 1
theorem Power2.below.ind_2 {n : Nat} {motive : (a : Nat) → Power2 a → Prop} {h : Power2 n} : 
  (nb : @Power2.below motive (2 * n) (.ind h)) → motive n h
  | @Power2.below.ind _ _ _ _ x => x

Thanks for bearing with me!

[DanielFabian]

It seems it boils down to the fact that that Lean cannot tell that a value x : Power2.below (Power2.ind h) must have been constructed with the Power2.below.ind constructor, because of proof irrelevance of Power2.

I don't think that's even true. Isn't it that due to proof irrelevance, the no-confusion rule is not applicable and you can in fact prove that Power2.below (Power2.ind h) = Power2.below (Power2.base)?

[nomeata]

I forgot where exactly we stand with the issue here.

Thanks to termination_by structural we can see that the two issues in the PR description are likely separate: The first gives

failed to infer structural recursion:
Cannot use parameter #4:
  could not add below discriminant

and the second

failed to infer structural recursion:
Cannot use parameter r₁:
  the type Steps Step does not have a `.brecOn` recursor

and with tracing

failed to prove brecOn for Steps.below
    couldn't solve by backwards chaining (Lean.Meta.IndPredBelow.maxBackwardChainingDepth = 10): 
α: Type
r: α → α → Prop
Tm✝Tm: Type
Step: Tm → Tm → Prop
motive✝: (a a_1 : Tm) → Steps Step a a_1 → Prop
a✝³a✝²: Tm
x✝: Steps Step a✝³ a✝²
ih✝: ∀ (a a_1 : Tm) (x : Steps Step a a_1), x.below → motive✝ a a_1 x
abc: Tm
a✝¹: Step a b
a✝: Steps Step b c
a_ih✝: a✝.below
⊢ Step a a✝³

In fact, the second example seems to be #1672, which has a possible (but to be refined) fix in #4840, so I’ll just remove that second example from the issue description here.

[nomeata]

Oh, and since in the example works if MyRel is inlined, as so

theorem preserve_add' {a : Nat} : ∀ {x y : Nat}, SymmGen (fun x y => y = x + 2) x y → MyRel (x + a) (y + a)
| _, _, SymmGen.rel _ _ h => SymmGen.rel _ _ (by rw [h, Nat.add_right_comm])
| _, _, SymmGen.symm _ _ h => SymmGen.symm _ _ (preserve_add' h)
termination_by structural _ _ x =>

maybe I should downgrade the severity to low.

Ah, but above, before the discussion goes off a tangent, I had a fix for this issue by adding whnf. Let’s get this in (#5136).