structural recursion fails

Stream: lean4

[Bhavik Mehta]

Here's my example:

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)

I'd expect structural recursion to succeed in the final case, since I'm applying preserve_add' to a structurally smaller term. Using the induction tactic works, but why does the equation compiler fail to recognise this is structural recursion?

[Yaël Dillies]

cc @Joachim Breitner

[Joachim Breitner]

I haven't touched the code that compiles structural recursion over inductive predicates (which works differently than when recursing over inductive types) yet, so hard to tell before breakfast :-)

@Daniel Fabian, who authored that code, might be able to debug this better.

[Joachim Breitner]

Does inlining MyRel help?

[Bhavik Mehta]

Joachim Breitner said:

I haven't touched the code that compiles structural recursion over inductive predicates (which works differently than when recursing over inductive types) yet, so hard to tell before breakfast :-)

Ahh okay, then I don't feel as bad for thinking that structural recursion on inductive predicates didn't get better with your change!

[Bhavik Mehta]

Inlining MyRel doesn't make a difference

[Joachim Breitner]

My changes so far only affected well-founded recursion

[Joachim Breitner]

Anyways, this looks like a bug worth opening an issue for.

[Joachim Breitner]

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

[Jonathan Chan]

I also have a failing structural recursion on the following, it's the same issue right

variable {Tm : Type}

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

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

Was the issue ever opened? Is there a link to it?

[Kim Morrison]

I guess not.

[Bhavik Mehta]

Oops, sorry, I forgot about this. Here's an issue for it: https://github.com/leanprover/lean4/issues/4540