lean

Non-empty list examples from "Functional Programming in Lean" produce error: unsolved goals

I've been working through the "Functional Programming in Lean" document and the Non-Empty Lists examples don't work for me.

The code:

def xs := [1]
theorem xs_not_empty : xs.length > 0 := by simp

based on the "Arrays and Indexing" section, results in:

smol.lean:2:40: error: unsolved goals
⊢ 0 < xs.length

I suspect that something has changed between release 4.1 (which "Functional Programming..." says it has been tested with) and 4.12, which is my installed version, but I can't find it.

Solution

  • Maybe the relevant change is that definitions are now by default irreducible and I'm pretty sure that this change was between 4.1 and 4.12. So you have to tell simp explicitly to unfold the definition of xs now.

    def xs := [1]
theorem xs_not_empty : xs.length > 0 := by simp [xs]

    works fine.