convert list to vector

Stream: new members

[Alfredo Garcia]

i think this might be easy so i was wondering if someone can have an example, i had been trying different approaches without luck for now. my goal is something as:

def list_to_bitvec (L : list bool) : bitvec h :=

the other way around is easy:

def bitvec_to_list (B : bitvec h) : list bool :=  vector.to_list B

i had been trying to do an inductive type for it but no luck yet, unsure if it will be the right way to go, any help is appreciated.

[Matt Diamond]

Someone more knowledgeable should jump in here, but it seems like the key hurdle is that you need to provide a proof that L.length = h.

[Matt Diamond]

import data.bitvec.core

def list_to_bitvec (L : list bool) (h : ℕ) (H : L.length = h) : bitvec h := ⟨L, H⟩

[Matt Diamond]

vector is a subtype of list, which means to construct a term of type vector you have to provide a term of the base type along with a proof that the term meets the predicate of the subtype

[Matt Diamond]

you could also do something like this:

def list_to_bitvec' (L : list bool) (h : ℕ) : option (bitvec h) :=
dite (L.length = h) (λ H, some ⟨L, H⟩) (λ _, none)

where you return a bitvec if the length matches, but none otherwise

[Matt Diamond]

This option will just cut the list off at n elements (or append additional falses if the list is too short):

def list_to_bitvec (L : list bool) (n : ℕ) : bitvec n := ⟨list.take' n L, list.take'_length n L⟩

and if you don't want to specify the length at all, you can do this:

def list_to_bitvec (L : list bool) : bitvec L.length := ⟨L, rfl⟩