Structure eta doesn't work for nested inductives

[nomeata]

It is unclear if this is really a bug, or should be like this, but I’ll open an issue anyways to record this and ensuing discussion.

Lean’s type theory eta-expands structure like values when reducing, but only when using the type’s “native” recursor, not when reducing derived recursers over that type that are generated as part of nested inductives.

Small reporducer:

inductive StructLike α where
  | mk : α → StructLike α 

inductive Nested where
  | nest : StructLike Nested → Nested
  | other

theorem works (x : StructLike Nested) : StructLike.rec
  (motive := fun _ => Bool)
  (mk := fun _ => true)
  x = true 
  := rfl

/--
error: type mismatch
  rfl
has type
  Nested.rec_1 (fun x x => true) true (fun x x => true) x =
    Nested.rec_1 (fun x x => true) true (fun x x => true) x : Prop
but is expected to have type
  Nested.rec_1 (fun x x => true) true (fun x x => true) x = true : Prop
-/
#guard_msgs in
theorem fails (x : StructLike Nested) : Nested.rec_1
  (motive_1 := fun _ => Bool) (motive_2 := fun _ => Bool)
  (nest := fun _ _ => true)
  (other := true)
  (mk := fun _ _ => true)
  x = true 
  := rfl

One could argue that Nested.rec_1 should also eta-expand the argument if needed, on the grounds that it’s really just a renamed StructureLike.rec.

Incidentially, #4749 would fix this.

Versions

"4.12.0-nightly-2024-10-09"

Impact

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

[digama0]

Properly recursive inductive types and eta for structures don't mix. It makes defeq checking very undecidable, and there are many open research questions about the properties of the resulting type theory. Please no.

[kmill]

Arthur Adjedj points this out this undecidability problem in #4182 as well.

[nomeata]

Right, but note that I'm not proposing to add recursive structures here; this is for nesting through (itself non-recursive) structures, so the eta cannot go on forever.

Or put differently: in the example above analyzing a StructLike would be consistently eta'ed, no matter of whether it's StructLike Nat or StructLike Nested>

[digama0]

Well, Nested.rec_1 is not the structure constructor and so does not participate in the structure eta rule. That said, it occurs to me that you can still prove that it is a defeq as a derived rule:

theorem fails (x : StructLike Nested) : Nested.rec_1
  (motive_1 := fun _ => Bool) (motive_2 := fun _ => Bool)
  (nest := fun _ _ => true)
  (other := true)
  (mk := fun _ _ => true)
  x = true
  :=
congrArg (Nested.rec_1
  (motive_1 := fun _ => Bool) (motive_2 := fun _ => Bool)
  (nest := fun _ _ => true)
  (other := true)
  (mk := fun _ _ => true)) (show x = ⟨x.1⟩ from rfl)

[nomeata]

Well, Nested.rec_1 is not the structure constructor and so does not participate in the structure eta rule.

Do you mean recursor, do you?

Right, that's why it doesn't work at the moment. But could one argue that Nested.rec_1, given that it's analyzing a value of type StrutLike _, should behave like StructLike.rec in that respect, couldn't one?

(One could go one step further and consider defining Nested.rec_1 in terms of StructLike.rec, that would be #4749.)

[digama0]

It is neither the constructor nor the projections. The recursor does not participate in the structure eta rule either (which is a relation between the constructor and the primitive projections), although I think there might be special handling to do the same eta expansion I just showed above for stuck structure recursors, and I'm observing that the exact same argument also justifies making Nested.rec_1 unfold on neutral terms.

I'm mildly negative on #4749, it adds a lot of complexity to the analysis of nested inductives and makes it hard for users and programs to be able to guess what the recursor looks like.

[nomeata]

I think there might be special handling to do the same eta expansion I just showed above for stuck structure recursors

I think that’s what I am referring to, maybe I shouldn't have called it “structure eta rule” then. My understanding is that the kernel replaces x : S with S.mk x.1 x.2… when x occurs in specific situations, namely

• in defeq-checking when x =?= t where x and t are in whnf, but not both already constructor applications (try_eta_struct)
• when reducing S.rec … x (to_cnstr_when_structure via inductive_reduce_rec)

and I wonder here if that should happen for any recursor that has a major argument of type S, not just S.rec.

I'm observing that the exact same argument also justifies making Nested.rec_1 unfold on neutral terms.

Only 80% sure I parse this correctly; does this mean you agree?

[nomeata]

Maybe the fix is actually code simplification: Instead of

private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr := do
  unless (← useEtaStruct inductName) do
    return major
  let env ← getEnv
  if !isStructureLike env inductName then
    return major
  else if let some _ ← isConstructorApp? major then
    return major
  else
    let majorType ← inferType major
    let majorType ← instantiateMVars (← whnf majorType)
    let majorTypeI := majorType.getAppFn
    if !majorTypeI.isConstOf inductName then
      return major
  …

do not pass inductName and instead use the type of the given major:

private def toCtorWhenStructure (major : Expr) : MetaM Expr := do
  if let some _ ← isConstructorApp? major then
    return major
  let majorType ← inferType major
  let majorType ← instantiateMVars (← whnf majorType)
  let majorTypeI := majorType.getAppFn
  unless majorTypeI.isConst do
   return major
  let inductName := majorTypeI.constName!
  unless (← useEtaStruct inductName) do
    return major
  let env ← getEnv
  if !isStructureLike env inductName then
    return major
  …

(The kernel code is equivalent)

[digama0]

This is a performance issue. I don't think you want to call inferType on every subterm, which is what I think this will do. Maybe useEtaStruct can fire also on nested inductives which contain a structure-like, and/or nested inductive recursors taking structures should have a mark indicating that they take a structure type. That way you can do the check by just looking up constants instead of doing a full typecheck.

[nomeata]

Thanks, I take it as a “yes” on the overall analysis that these recursors from nested inductives should trigger the structure eta.

(It wouldn't be every subterm, but only every major argument of a recursor that didn't reduce to a constructor, and the kernel runs type inference rather often, so I wouldn't jump to conclusions about performance yet. But a flag or a field that stores the IndName of the major argument in the recinfo would of course also work.)

[nomeata]

I dived a bit into the code. The core problem is that

def RecursorVal.getInduct (v : RecursorVal) : Name :=
  v.name.getPrefix

returns “the name of the first inductive name in the mutual group”, but where it’s used it looks like the expectation is that it's “the inductive type of the major argument”.

So a less intrusive fix than the one suggested above would be to rename this to RecursorVal.getMajorInduct (to avoid this confusion), and either

• make this an explicit field of RecursorVal or
• calculate it from the v.type (should just be a matter of looking at the v.getMajorIdx’s parameter)

(Incidentially, it seems that one of the few uses of this functions is in mkRecursorInfoForKernelRec which I wonder if this is even used, since it seems to be only used by Lean.MVarId.induction, which despite the name seems to be only be used by the cases tactic with a recursorName name that is always some .casesOn and not a kernel recursor, so there maybe some cleanup that could be done here.)

[nomeata]

Here is a another symptom of this bug:

Before:

/--
info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
fun a => congrArg (Nat.add 1) (Nested._sizeOf_2_eq a)
-/
#guard_msgs in
#print Nested.nest.sizeOf_spec

After #5679:

/--
info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
fun a => Eq.refl (1 + sizeOf a)
-/
#guard_msgs in
#print Nested.nest.sizeOf_spec