Zulip Chat Archive

Stream: new members

Topic: convert list to vector


Alfredo Garcia (Jun 29 2022 at 23:34):

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 (Jun 30 2022 at 00:21):

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 (Jun 30 2022 at 00:26):

import data.bitvec.core

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

Matt Diamond (Jun 30 2022 at 00:28):

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 (Jun 30 2022 at 00:42):

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 (Jun 30 2022 at 03:13):

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

Last updated: Dec 20 2023 at 11:08 UTC