Sect. 8.5: incorrect error messages and solutions in Lean 4.11

[mars0i]

Please quote the text that is incorrect:

From the "Definitional equality" subsection of section 8.5:

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => ys
  | n + 1, k, .cons x xs, ys => .cons x (_ : Vect α (n.plusL k))

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL n k)

In what way is this incorrect?

In Lean (version 4.11.0, x86_64-apple-darwin22.6.0, commit ec3042d94bd1, Release), the error on the last line of this version of appendL is:

▶ 74:3-74:65: error:
type mismatch
  Vect.cons x ?m.2363
has type
  Vect α (n.plusL k + 1) : Type ?u.2140
but is expected to have type
  Vect α ((n + 1).plusL k) : Type ?u.2140

This is not similar to the error reported in the text. The solved versions below that point have similar errors--i.e. the solution doesn't work. The first variant (with the recursive call, but retaining n and k parameters) has this error:

▶ 79:3-79:60: error:
type mismatch
  Vect.cons x (appendL n k xs ys)
has type
  Vect α (n.plusL k + 1) : Type ?u.2959
but is expected to have type
  Vect α ((n + 1).plusL k) : Type ?u.2959

The second solution--without the indexes as parameters--has essentially the same error, but with daggers.

(Is this a bug in Lean 4.11 rather than the book?)

[david-christiansen]

Thanks!

This is an artifact of the book using a slightly old version of Lean. I plan to update it to a new version later this year. All error messages in the book are machine-checked, so this will definitely get fixed then.

[mars0i]

OK! I understand. Sounds good. (And I probably learned more by finding the discrepancy. 😄 )

[mars0i]

I think I'm running this code with Lean 4.1.0 now, but the error messages is the same except for a syntactic variation.:

▶ expected type (59:34-59:35)
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL n k + 1)

▶ 59:3-59:61: error:
type mismatch
  ?m.14985
has type
  Vect α (Nat.plusL n k + 1) : Type ?u.14775
but is expected to have type
  Vect α (Nat.plusL (n + 1) k) : Type ?u.14775

My lean-toolchain in the root of the project contains

leanprover/lean4:v4.1.0

and lake --version, and lean --version both report Lean version 4.1.0 when run from the project root. The nvim :checkhealth lean also reports 4.1.0, fwiw. It's possible for all I know that neovim is mistakenly using a different version of Lean, but I thought I'd report this just in case it's helpful. Maybe it's water under the bridge since a new version of the book will come at some point.

[mars0i]

I now think I did something wrong in my code--I modified something from FPIL after I copied it, or typed it in by hand incorrectly. Just copying the bare minimum of definitions directly from the book produces no unexepcted errors in v. 4.13.0-rc3, nor in v. 4.1.0 (as you'd expect). Maybe there was something weird about 4.11, but I suspect that the problem was solely due to something in my code. Sorry to make a mess.