recursion in list

Stream: new members

[Catarina Gamboa]

Hello, I am new to lean, and I am having difficulties in invoking a recursive function. I am trying to define a subtitution function with the following inductive type and definition:

inductive exp
| var     : string → exp
| app     : string → list exp → exp

def substitute: string → exp → exp → exp -- (substitute arg₀ by arg₁ in arg₂)
| v e (exp.var s)    := if v = s then e else (exp.var s)
| v e (exp.app s le) := exp.app s (le.map (λ x, substitute v e x))

However, the subtitution inside the map provokes the error message "failed to prove recursive application is decreasing, well founded relation". Do you have any suggestions to overcome this issue?

[Jannis Limperg]

Your exp is a nested inductive type because exp appears recursively as an argument to a different type (list). As you've discovered, such types are poorly supported by Lean's termination checker. There are two ways forward:

• Use well-founded induction. This is a technique that allows you to prove a function terminates even when Lean doesn't immediately see it. There should be a section in the mathlib docs about this.
• Restructure your type to avoid the nesting. If possible, this would be my preferred choice.

Coq supports nested inductives better btw, though afair the experience is not super great there either.

[Martin Dvořák]

Jannis Limperg said:

There should be a section in the mathlib docs about this.

Did you mean?
https://leanprover-community.github.io/extras/well_founded_recursion.html

[Floris van Doorn]

You'll have a much nicer time if you make the type app : ∀ {n}, string → (fin n → exp) → exp (which is one particular way to do choice (2) suggested by Jannis).