vectors in lean4

Stream: lean4

[Frederic Peschanski]

In the "Theorem proving with Lean4" book there is an inductive for Vectors in the section on "Inductive families". I looked at the standard library but no vectors there. Did someone tried to implement the basic operations on vectors : append, fromList, toList, etc. ? I must confess I am stuck with these basic things.

[Henrik Böving]

The area you are talking about are so called "length indexed lists" (indexed is a type theory, not a list term here), the standard library is however just a piece of code that the compiler requires in order to bootstrap itself right now so don't expect too fancy things from it. I have a few operations I translated from the coq code in CPDT (this book: http://adam.chlipala.net/cpdt/cpdt.pdf) here: https://github.com/hargoniX/cpdt-lean/blob/main/Cpdt/Chapter8/LengthIndexed.lean but nothing too fancy.

If you have more concrete questions just ask here, we're happy to help.

[Frederic Peschanski]

Thank you @Henrik Böving this gives me a starting point ... I see that subtypes could be useful ...

[Andrés Goens]

I've a follow-up question/kind of in the same spirit. If I wanted to express more complex properties in the type like this, say, for ordered lists, is there a way to encode it in the type, the same way? My naive attempt at this doesn't work

inductive OrderedList (α : Type) [LE α]
  | OrderedNil : OrderedList α
  | OrederedCons (a : α) (as : OrderedList α) (h : match as with | OrderedNil => True | OrderedCons b _ => a ≤ b)

I suppose that the construction isn't in scope yet in its own constraint. Is there a way to express a constraint like this? I suppose I can "split it up" like so

def OrderedList (α : Type) [LE α] : List α → Prop
  | a::b::rest => a ≤ b ∧ OrderedList α (b::rest)
  | _ => True

But that's somewhat unsatisfactory, as we don't get the same types of guarantees with the type as we do for length-indexed lists (i.e. correct by construction)

[Henrik Böving]

If you define a notion of membership for a list like mathlib (docs4#List.Mem) you can (in the cons case) say something like (h : ∀ y, y ∈ as → a ≤ y)

[Evgeniy Kuznetsov]

inductive OrderedList' (α : Type) [LE α]: Option α → Type
| nil: OrderedList' α .none
| cons_nil  (a: α) (as: OrderedList' α $ .none  )           : OrderedList' α (.some a)
| cons_cons (a: α) (as: OrderedList' α $ .some b) (_: a ≤ b): OrderedList' α (.some a)

def OrderedList (α : Type) [LE α] := (head: Option α) × OrderedList' α head

[Andrés Goens]

ahh, you're "remembering" the item at the head with the type, that's a really cool solution!

[Tomas Skrivan]

What is the problem with defining inductively a Prop that the list is ordered and then OrderedList is just a Subtype of List?

The only complicated thing is how to write a match statements with this type. You definitely want to match on the List and the Prop at the same time.

[François G. Dorais]

You can try using @[matchPattern] to define your own patterns:

def List.precede {α} [LE α] (x : α) : List α → Prop
| [] => True
| y::_ => x ≤ y

inductive IsOrdered {α} [LE α] : List α → Type
| nil : IsOrdered []
| cons {x xs} : List.precede x xs → IsOrdered xs → IsOrdered (x :: xs)

def OrderedList (α) [LE α] := (xs : List α) × IsOrdered xs

@[matchPattern]
def OrderedList.nil {α} [LE α] : OrderedList α := ⟨[], IsOrdered.nil⟩

@[matchPattern]
def OrderedList.cons {α} [LE α] (x : α) (xs : List α) (h : List.precede x xs) (hs : IsOrdered xs) : OrderedList α := ⟨x :: xs, IsOrdered.cons h hs⟩

def matchTest {α} [LE α] : OrderedList α → Nat
| OrderedList.nil => 0
| OrderedList.cons _ _ _ _ => 0

[Mac]

Tomas Skrivan said:

What is the problem with defining inductively a Prop that the list is ordered and then OrderedList is just a Subtype of List?

The only complicated thing is how to write a match statements with this type.

This is the big problem with subtypes (and propositions in general) when it comes to programming. Most natural pattern matching, structural recursion, type class deriving (e.g., Inhabited), namespacing, etc. is broken and thus requires lots of proving and other manual work to fix (instead of things "just working").

Don't get me wrong the tools (subtypes and proofs) are powerful, they are just often best reserved for when they are needed and use other, more convenient, approaches when possible (in the programming context at least).

[Frederic Peschanski]

I played a little bit more with vectors, still based on the following definition :

inductive Vector (A : Type) : Nat → Type u where
  | vnil  : Vector A 0
  | vcons : A → {n : Nat} → Vector A n → Vector A (n+1)
   deriving Repr

... I have something I don't undestand perfectly below:

def vindex {A : Type} {n : Nat} (fin : Fin n) (v : Vector A n) : A :=
  match (fin, v) with
  | (⟨0,_⟩ , vcons e _) => e
  | (⟨m+1,hk⟩, vcons _ v') => vindex ⟨m,by apply Nat.lt_of_succ_lt_succ ; exact hk⟩ v'

Seems fine (from my naive point of view)...

def v : Vector Nat 4 := vcons 1 (vcons 2 (vcons 3 (vcons 4 vnil)))
#eval vindex 2 v4 -- => 3
#eval vindex 3 v4 -- => 4

But ... oops

#eval vindex 4 v4 -- => 1
#eval vindex 5 v4 -- => 2

... not exactly what I intended :smiling_face:
Could someone explain me what happens here (probably this is not the Fin I imagined) ?
Also if you have a better proposition for vindex I would be interested

[Jannis Limperg]

Literals for Fin n are interpreted modulo n. So 4 : Fin 4 is 0, 5 : Fin 4is 1. Arguably Lean should throw an error instead, but that doesn't play well with how these literals are implemented.

[Frederic Peschanski]

Thank you @Jannis Limperg I understand now the issue. Probably I will play a little bit with a variant, such as Bound n with the behavior I'm expecting (a type error). However then I don't really understand when one would like to use Fin (at least in my understanding on why and when it's useful...).

[Henrik Böving]

When you want to make mathematical arguments about numbers mod n of course.

[Eric Wieser]

There are two potentially separate problems at play here:

1. What should 5 : fin 4 parse as?
2. What is the value of (3 : fin 4) + (2 : fin 4)?

I think there are technical limitations which make it hard to emit an error for 1, while 2 is chosen because it's as good an option as any

[Frederic Peschanski]

... and then maybe (Mod n) would be a better name ? (Fin is already quite connoted in dependent type theory, no ?)

[Yakov Pechersky]

We should have a glossary or faq entry for the nuances of fin, vs bounded (unallowed) finite numbers, vs ones with saturated ops, etc.

[Mac]

It should also be noted that Fin is used to implemented native fixed-sized (finite) unsigned integers -- UInt8, UInt16, UInt32, UInt64. Mathematically, though, that is also just modular arithmetic (assuming wrapping under/overflow as opposed to trapping under/overflow), so the name Mod n would still fit there too.

[Tomas Skrivan]

Also when indexing arrays shouldn't we use some variant of Fin n that is based on USize instead of Nat. Why pay for arbitrary large integers if they can be a meaningful memory address?

[Mac]

@Tomas Skrivan Nat only uses arbitrary-sized integers if the value is over a certain threshold (e.g., word-size - 1 bits) otherwise it only consumes one word. Also, many of the Array functions do take advantage of the fact that Arrays are at max USize. There is even a variant of Array.get that does just that (Array.uget).

[Tomas Skrivan]

Sure, but if you look at the generated C code then Nat gets passed through a pointer but USize is passed by value.

[Mac]

One of the advantages of the Conditional approach @Sebastian Ullrich suggested for getOp is that it could use USize instead of Fin for Array indexing.

[Mac]

Tomas Skrivan said:

Sure, but if you look at the generated C code then Nat gets passed through a pointer but USize is passed by value.

The lean_object* is not actually always a pointer. It can actually be either lean_object* OR a raw Nat (if the lower order bit is 1).

[Mac]

Such a pointer trick is actually a familiar idea in language design (e.g., Ruby's C implementation does a similar trick for Fixnum, True, False, and Nil).

[Tomas Skrivan]

Ohh I was not aware of that. I saw the pointer and updates on the reference counter in the C code. Assumed that it is not ideal and should use USize instead.

[Joe Hendrix]

I have a simple vector datatype used for a Lean crypto library that I am working on in my spare time. Polymorphic vectors are in this file, and are a subtype of Array. There's also byte vectors and bitvectors (which use Fin).

[Joe Hendrix]

It'd be nice to have a rich set of linear algebra operations and transforms such as scans for array-oriented programming.

[Frederic Peschanski]

Here's an ugly version ...

def vindex {A : Type} : {n : Nat} → (k : Nat) → (p : k < n) → (v : Vector A n) → A
  | .(_), 0, .(_), vcons e _ => e
  | n+1, m+1, .(_), vcons _ v' => let p' : m < n := by apply Nat.lt_of_succ_lt_succ ; assumption
                                  @vindex _ _ m p' v'

def v : Vector Nat 4 := vcons 1 (vcons 2 (vcons 3 (vcons 4 vnil)))
#eval vindex 2 (by simp) v -- => 3
#eval vindex 3 (by simp) v -- => 4

#check vindex 4 _ v -- crash !

[Error - 14:55:12] Request textDocument/foldingRange failed.
  Message: Server process for file:///<...>/Vectors.lean crashed, likely due to a stack overflow in user code.
  Code: -32603

[Frederic Peschanski]

(no need to say that I navigate by sight :sweat_smile: )

[Leonardo de Moura]

@Frederic Peschanski Could you please try the Lean latest nightly build? If it does not fix the problem, could you please create a #mwe?
I tried the following using the code fragments above, and it works in the latest nightly build

inductive Vector (A : Type) : Nat → Type u where
  | vnil  : Vector A 0
  | vcons : A → {n : Nat} → Vector A n → Vector A (n+1)
   deriving Repr

namespace Vector

def vindex {A : Type} : {n : Nat} → (k : Nat) → (p : k < n) → (v : Vector A n) → A
  | .(_), 0, .(_), vcons e _ => e
  | n+1, m+1, .(_), vcons _ v' => let p' : m < n := by apply Nat.lt_of_succ_lt_succ ; assumption
                                  @vindex _ _ m p' v'

def v : Vector Nat 4 := vcons 1 (vcons 2 (vcons 3 (vcons 4 vnil)))
#eval vindex 2 (by simp) v -- => 3
#eval vindex 3 (by simp) v -- => 4

#check vindex 4 _ v -- vindex 4 ?m v : Nat

[Frederic Peschanski]

@Leonardo de Moura I've just elan update'd and I can confirm it does not crash anymore with 4.0.0-nightly-2022-07-01, sorry for the false alarm.

[cognivore]

(deleted)

[Locria Cyber]

Vector isn't in Lean 4 yet

[Locria Cyber]

Is contribution welcome or not (adding Vector to Init.Data.Vector)?

[Henrik Böving]

Contributions to the Core libraries are in general not welcome unless the additions are required for something in the compilers since the todo list of the compiler team is overhelming already. You can contribute it to mathlib4 though

[Locria Cyber]

mathlib still don't have Vector? I was suprised

[Locria Cyber]

oh I think Github added a "clone master branch only" (option) when forking

[Arthur Paulino]

Mathlib4 is still very rudimentary at this point.

Such PRs are also welcome here: https://github.com/yatima-inc/YatimaStdLib.lean. We're focusing on algorithms and data structures, mostly

[Locria Cyber]

What's Yamata Inc?

[Locria Cyber]

https://github.blog/changelog/2022-07-27-you-can-now-fork-a-repo-and-copy-only-the-default-branch/

[Locria Cyber]

I have a bad feeling about this

[Henrik Böving]

Why? Big projects tend to have 100s of branches and if you need any of them you can still fetch them from the other remote regardless

[Arthur Paulino]

@Locria Cyber Yatima Inc is an R&D company lead by @John Burnham that develops open source technology, currently using Lean 4 in its stack

[Locria Cyber]

Henrik Böving said:

Why? Big projects tend to have 100s of branches and if you need any of them you can still fetch them from the other remote regardless

It's on github clone, not github to local.

Maybe Github is paving the way for its clound-based "workspace".

[Locria Cyber]

Also, I had some trouble here. Seems like :: and [term*]must be a typeclass in core for this to work

inductive Vector (α : Type u) : Nat → Type u
  | nil : Vector α 0
  | cons : α → Vector α n → Vector α (n+1)

infix:67 " :: " => Vector.cons

def a := 1 :: Vector.nil

ambiguous, possible interpretations
  1 :: Vector.nil : Vector ?m.1893 (?m.1894 + 1)

  1 :: ?m.1958 : List ?m.1914

[Locria Cyber]

def a : Vector Nat _ := 1 :: Vector.nil

error:

don't know how to synthesize placeholder
context:
⊢ Nat
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

[Locria Cyber]

I do need to unify a's type with declaration though.

[Henrik Böving]

Locria Cyber said:

def a : Vector Nat _ := 1 :: Vector.nil

error:

don't know how to synthesize placeholder
context:
⊢ Nat
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

This is the way it is supposed to work, the idea is that if you explicitly denote the type of a you are supposed to provide all arguments to that type explicitly which is a good thing IMO, if you are doing an explicit type you should go through with it

[Locria Cyber]

what if I do want to get the length from compiler?

[Henrik Böving]

def a := (1 :: Vector.nil : Vector Nat _)

this would work as long as :: isn't TC

[Locria Cyber]

thanks

[Locria Cyber]

h: a :: as = b :: bs
habs': a = b
⊢ as = bs

[Locria Cyber]

question: how do I prove this?

[Locria Cyber]

:: is the constructor for Vect

[Henrik Böving]

by injectivity of constructor applications:

example (a b : α) (as bs : List α) (h1 : a :: as = b :: bs) (h2 : a = b) : as = bs := by
  injection h1
  assumption

[Locria Cyber]

thanks!

[Locria Cyber]

instance : SizeOf (Vect α n) where
  sizeOf _ := n

Is this a correct use of SizeOf?

[Henrik Böving]

Lean should have already synthesized a SizeOf instance for you automatically that does at least yield the same result though via structural recursion instead of directly getting the n argument.

[Locria Cyber]

ok

[Henrik Böving]

Ah actually no it didnt

[Locria Cyber]

I think by default it's all 0

[Locria Cyber]

Also, why is Fin so complicated?

[Locria Cyber]

In Idris2, all the data types are their own type, and it's easier to reason about.

[Locria Cyber]

don't know how to synthesize placeholder for argument 'isLt'
context:
α : Type u_1
n✝ : Nat
x : α
xs : Vect α n✝
n : Nat
prf : Nat.succ n < n✝ + 1
value : α
⊢ n < n✝

[Henrik Böving]

Locria Cyber said:

I think by default it's all 0

That is not correct, yes the default SizeOf instance is 0 but lean generate an additional SizeOf instance for all inductive and structure declarations automatically while elaborating them, in the case of your Vector this is:

Vector.rec 1 (fun {n} a a_1 a_ih => 1 + sizeOf n + sizeOf a + a_ih) t

[Locria Cyber]

ok

[Locria Cyber]

Maybe I should make Nat literal its own type class, and make a new simpler Fin.

[Henrik Böving]

Locria Cyber said:

Also, why is Fin so complicated?

Fin isn't complicated its definition is:

structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n

which is pretty printed more like

structure Fin (n : Nat) where
  val  : Nat
  isLt : val < n

It's just that arguing about Fin while doing recursion on the n argument is icky

[Henrik Böving]

Locria Cyber said:

Maybe I should make Nat literal its own type class, and make a new simpler Fin.

Nat literals are already managed by the OfNat typeclass

[Locria Cyber]

interesting

[Mario Carneiro]

your goal earlier should be something like Nat.lt_of_succ_lt_succ prf

[Locria Cyber]

Here's Fin in Idris2:

data Data.Fin.Fin : Nat -> Type
  Numbers strictly less than some bound. The name comes from "finite sets".

  It's probably not a good idea to use `Fin` for arithmetic, and they will be
  exceedingly inefficient at run time.
  @ n the upper bound
  Totality: total
  Visibility: public export
  Constructors:
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

[Locria Cyber]

This is much easier to reason about

[Locria Cyber]

Because I only need to get from Fin (S k) to Fin k (in recursion).

[Mario Carneiro]

It's a lot harder to work with equalities in the index with that representation

[Mario Carneiro]

in mathlib there are API lemmas for the FZ and FS constructors

[Mario Carneiro]

it's pretty easy to define them

[Locria Cyber]

equalitiies in the index?

[Henrik Böving]

I imagine you could even build a custom induction principle that reflects them, there is no reason to build a new type really

[Mario Carneiro]

stuff like Fin (m + n) -> Fin (n + m)

[Locria Cyber]

I'm newbie to Lean though

[Locria Cyber]

Mario Carneiro said:

stuff like Fin (m + n) -> Fin (n + m)

You just need to prove that m + n = n + m, and they are the same type.

[Mario Carneiro]

you have to be advanced type tetris master to actually come up with a proof of that using FZ and FS

[Locria Cyber]

not really

[Henrik Böving]

Advanced type tetris master is going in my type theory urban dictionary

[Locria Cyber]

Idris has this cast : (a: A) -> (A = B) -> B

[Mario Carneiro]

You can prove it using cast but then you don't know e.g. how the value computes on successor

[Locria Cyber]

It's literally the same type though

[Mario Carneiro]

you won't be able to apply equation lemmas for other recursive definitions

[Locria Cyber]

what's equation lemma

[Mario Carneiro]

we usually call this DTT hell

[Mario Carneiro]

equation lemmas are the definitional equalities that follow from a definition by pattern matching

[Locria Cyber]

I've been avoiding using tactics because I don't quite understand the magic.

[Locria Cyber]

You can say that I'm a type tetris master

[Mario Carneiro]

The advantage of the structure definition of Fin is that you can do all the "real" reasoning on a non-dependent type, namely Nat

[Mario Carneiro]

Yes, this style of programming you are using is seen mostly in idris and agda

[Henrik Böving]

Locria Cyber said:

I've been avoiding using tactics because I don't quite understand the magic.

I'm afraid that won't really get you too far in the Lean eco system, we are pretty focused on tactics for non trivial term level proofs

[Mario Carneiro]

The situation with vectors is pretty similar BTW. In lean 4 they aren't defined, but the lean 3 definition of Vector A n is {l : List A // l.length = n}

[Mario Carneiro]

so all the vector operations are just list operations tupled with a proof that they preserve lengths

[Mario Carneiro]

and you don't have any problems with e.g. associativity of vector append

[Henrik Böving]

This also makes the runtime representation nicer right? With the indexed variant each node is also carrying the rest of the length around

[Mario Carneiro]

Indeed

[Mario Carneiro]

I think agda has a mechanism to avoid this using ghost arguments

[Mario Carneiro]

not sure about idris

[Locria Cyber]

Idris has beta reduction for Nat-like and (i forgot the name) for List-like

[Locria Cyber]

(runtime representation)

[Locria Cyber]

It doesn't have the Array type in Lean, because its List is just as fast

[Mario Carneiro]

in lean 4 the improvement of runtime representation for Fin is even more stark. the FZ/FS representation is a unary linked list, while the structure over Nat is a zero-cost wrapper around a GMP bignum with a direct numeral representation for numbers less than I think 2^63

[Locria Cyber]

Idris compile to scheme, so it's different

[Henrik Böving]

Locria Cyber said:

It doesn't have the Array type in Lean, because its List is just as fast

How can a linked list be just as fast as a slice of memory?

[Locria Cyber]

scheme magic?

[Mario Carneiro]

does it have O(1) push?

[Mario Carneiro]

push to the end

[Locria Cyber]

never tried

[Locria Cyber]

need to check Chez Scheme's source code to know

[Mario Carneiro]

a google search turns up https://www.idris-lang.org/docs/idris2/current/contrib_docs/docs/Data.Linear.Array.html

[Locria Cyber]

that's a type class

[Locria Cyber]

interface

[Mario Carneiro]

there's a data right after

[Locria Cyber]

that's in contrib (akin to mathlib4)

[Mario Carneiro]

okay, is that a disqualification?

[Henrik Böving]

They seem to have a lot of array thingies below

[Mario Carneiro]

there's no push though

[Locria Cyber]

it's probably incomplete (again, things in contrib are like that)

[Locria Cyber]

https://idris2-quickdocs.surge.sh/

[Locria Cyber]

Even third-party packages are better than contrib. contrib is the historical artifact before Idris2 core team decided it's a bad idea to let anything in the main repo.

[Mario Carneiro]

I would be generally doubtful that a fully functional List type is going to get array performance "by magic"

[Locria Cyber]

idk
I assume that list operation in LISP is fast enough

[Mario Carneiro]

It's a linked list

[Henrik Böving]

But that's not how memory works, as soon as you have a linked list cache performance sucks

[Locria Cyber]

probably not in memory

[Mario Carneiro]

no, it really is

[Locria Cyber]

Do you think that popular scheme implementations would only use linked list (in C)?

[Mario Carneiro]

you can sometimes optimize it to be a linked list of arrays but there are lots of operations that will break up the arrays

[Mario Carneiro]

(I know because I've written an optimized lisp interpreter)

[Locria Cyber]

Idris can't compile to C good enough yet.

[Locria Cyber]

The mature backends are Scheme/Racket/Javascript

[Mario Carneiro]

Scheme has an actual vector type though

[Mario Carneiro]

lists are lists and arrays are arrays in scheme

[Locria Cyber]

yes

[Mario Carneiro]

pretty sure racket does too

[Mario Carneiro]

and javascript has a whole zoo

[Mario Carneiro]

so I don't see how a language with only one List type is going to be able to lower this to both lists and arrays

[Locria Cyber]

not both

[Locria Cyber]

it's mapped to Scheme's list

[Mario Carneiro]

which is why I don't think you will get O(1) push with idris List

[Locria Cyber]

Maybe not

[Locria Cyber]

Locria Cyber said:

Idris has this cast : (a: A) -> (A = B) -> B

How do you do something like this (in Lean)?

[Henrik Böving]

You just do it: docs4#cast