Unable to Apply List Lemma?

Stream: lean4

[David Pearce]

I am confused why the fails (Lean 4.7.0):

-- A set of zero or more bytes upto a given size.
structure FinVec {n:Nat} (T) where
  data : List T
  isLt : data.length <= n

def slice32(l:List Nat) : (FinVec (n:=32) Nat) :=
 let bytes := (l.take 32)
  -- Prove bytes has at most 32 elements.
  have q : bytes.length ≤ 32 := by rw [List.length_take]
  -- Construct FinVec
  {data:=bytes, isLt:=q}

Specifically, the error is that it List.length_take_le is an unknown constant. But, this is a real lemma I'm trying apply. I figure an import is required, but could not get the right incantation.

I should add, that I thought I understood that the standard library (now batteries) was included by default. So, I expected something like this to do it:

import Std.Data.List.Lemmas

Thoughts?

[David Pearce]

(deleted)

[David Pearce]

(deleted)

[David Pearce]

(deleted)

[Kim Morrison]

Seems to work fine with import Batteries.Data.List.Lemmas.

[Kim Morrison]

You may need to upgrade from v4.7.0 to v4.8.0-rc2, but I suspect it should work fine in v4.7.0

[Kim Morrison]

Batteries is not included by default, so you need to have a

[[require]]
name = "batteries"
git = "https://github.com/leanprover-community/batteries"
rev = "main"

in your lakefile.toml (or equivalent in lakefile.lean).

[David Pearce]

I managed to get this to work with 4.8.0-rc2:

import Batteries

-- A set of zero or more bytes upto a given size.
structure FinVec {n:Nat} (T) where
  data : List T
  isLt : data.length <= n

def slice32(l:List Nat) : (FinVec (n:=32) Nat) :=
 let bytes := (l.take 32)
  -- Prove bytes has at most 32 elements.
  have q : bytes.length ≤ 32 := by apply List.length_take_le
  -- Construct FinVec
  {data:=bytes, isLt:=q}

[David Pearce]

I thought import Std was a thing? It definitely worked for me at some point.

[Kim Morrison]

Std was renamed to Batteries. Sorry for the confusion!

[David Pearce]

So did you still need to require it when it was Std ?

[David Pearce]

Yeah, so the release notes for 4.7.0 say this:

Lean 4.7.0 has been released! While this release includes the usual collection of quality-of-life improvements and bug fixes, the most noticable change is that a large part of Std, the external standard library, is included with Lean.

[Kim Morrison]

Yes, it's true that many lemmas don't require any imports any more, but this was not a wholesale ingestion of Std. ("large part", not "all")

[David Pearce]

So how are you supposed to import stuff that is now included automatically with Lean? Or is it just automatically available?

[Kim Morrison]

It is just automatic.