Termination-checking of one-field structures

Stream: lean4

[Eric Wieser]

Is this something that could be supported by the equation compiler?

structure WrappedFunc where
  func : Nat → Nat

def factorial : WrappedFunc where
  func
  | 0 => 1
  | n + 1 => n * factorial.func n

[Eric Wieser]

I can cheat with

def factorial : WrappedFunc where func where
  func
  | 0 => 1
  | n + 1 => n * factorial.func n

but then the equation lemma is WrappedFunc.func factorial (n + 1) = n * factorial.func n, where the RHS is not dot notation

[Eric Wieser]

(probably a question for @Joachim Breitner)

[Eric Wieser]

The context is #mathlib4 > Changing `Stream.Seq` to use `GetElem` @ 💬

[Joachim Breitner]

Hmm, that reminds me of an issue I looked at recently. I think it was related to type classes… ah, no, that was about nested induction.

I’m not sure how to support it easily. There must be some kind of etwa-expansion happening, to expose the function parameter for the function inside factorial : WrappedFunc. So not completely impossible, but not a quick feature to add.