Structural recursion cannot be used

Stream: new members

[Bjarte M. Østvold]

I'm trying to do some programming in Lean 4, i.e., no proofs yet. Being a Haskell programmer I tried following :

inductive Term
| var : Nat → Term
| fn  : Nat → (List Term) → Term

def termfold { α : Type } : (Nat → α) → (Nat → List α → α ) → Term → α :=
  fun fv ff t =>
    match t with
    | Term.var v    => fv v
    | Term.fn f ts  => ff f $ List.map (termfold fv ff) ts

The error message include structural recursion cannot be used and well founded recursion has not been implemented yet.

Is there another way that I can write my definition of termfold? Or some additional information that I can provide to explain to Lean 4 that the recursion is well-founded?

I've looked here on Zulip and on GitHub for an answer since I assume this must be a well-known problem, but being ignorant about dependent types I may not have been able to understand the relevance of the material that I found.
(I did find a 6 month old issue that seems related, but no clues as how to address the problem.)

Any hints greatly appreciated! And apologies in advance for my ignorance.

[Mario Carneiro]

Use partial def

[Mario Carneiro]

Also use #lean4 stream

[Kevin Buzzard]

Bjarte M. Østvold said:

Any hints greatly appreciated! And apologies in advance for my ignorance.

Beginner questions are welcome both here in #new members (mostly Lean 3) and also in the #lean4 stream (all Lean 4), no need to apologise.

[Mario Carneiro]

partial def is basically the haskell button of lean

[Mario Carneiro]

Oh, you will run into an issue though: partial def doesn't want to compromise the soundness of the system, so it will require that the target type is inhabited, and here α isn't. You can fix that by adding a typeclass argument [Inhabited α]

[Mario Carneiro]

Alternatively, if you don't care about compromising soundness you can use unsafe def instead and then lean will stop complaining

[Horatiu Cheval]

What's the lean3 analogy here? From what you're saying I understand that unsafe is like meta, is that right? And then, is there a lean3 analogous to partial? (I've never used lean4)

[Bjarte M. Østvold]

Thanks for the rapid and kind answers! In case there is someone wondering here is the relevant line with the two required changes:

partial def termfold { α : Type } [Inhabited α] : (Nat → α) → (Nat → List α → α ) → Term → α :=

Having learned about partial def I do have some questions about how to prove results about such definitions, but I'll reserve that for a future posting in the #lean4 stream. Thanks again!

[Mario Carneiro]

Horatiu Cheval said:

What's the lean3 analogy here? From what you're saying I understand that unsafe is like meta, is that right? And then, is there a lean3 analogous to partial? (I've never used lean4)

In lean 3, meta plays the role of both unsafe and partial. unsafe lets you call external functions, do unsound things, and break the type system, while partial lets you do unguarded recursion