Stream: Coq users

Topic: [Newbie] Creating a boolean vector type


view this post on Zulip Julin S (Jul 11 2021 at 10:52):

Hi. I was trying to make a 'custom' boolean vector type which uses the built-in Vector.t type.

A type boolvector that takes a length argument of type nat.

So I did:

Require Vector.
Import Vector.VectorNotations.

Inductive type : Type :=
| boolvector: nat -> type.

Definition typeDenote (t: type) : Type :=
  match t with
  | boolvector n => Vector.t bool n
  end.

But I couldn't figure how to make a definition which accepts arguments of this boolvector as argument.

I tried

Definition def1 (a: boolvector) : nat :=
  match a with
  | boolvector x => x
  end.

but got this error.

= Vector.t bool 2
     : Type

Can you help me find what I am doing wrong here?

EDIT: Sorry the error message above is not the real one. The actual error was

The term "boolvector" has type "nat -> type"
which should be Set, Prop or Type.

view this post on Zulip Gaëtan Gilbert (Jul 11 2021 at 10:58):

This is very confusing. For instance the "error" you showed is not an error (note how it doesn't say "error") and is not produced by any of the code you gave.
Please explain in more detail what your goal is and how you tried to reach it.

view this post on Zulip Théo Winterhalter (Jul 11 2021 at 10:58):

Inductive type : Type :=
| boolvector: nat -> type.

is creating a new type called type which is inhabited by boolvector n for each natural number n.
So you are essentially creating a copy of natural numbers except that they are boxed. I don't think that's what you want to do.

view this post on Zulip Théo Winterhalter (Jul 11 2021 at 10:59):

Wouldn't you rather want to have the following?

Definition boolvector n := Vector.t bool n.

view this post on Zulip Julin S (Jul 11 2021 at 11:02):

@Gaëtan Gilbert Oops.. Sorry that was a mistake. The real error message was:

The term "boolvector" has type "nat -> type"
which should be Set, Prop or Type.

view this post on Zulip Julin S (Jul 11 2021 at 11:09):

Théo Winterhalter said:

Inductive type : Type :=
| boolvector: nat -> type.

is creating a new type called type which is inhabited by boolvector n for each natural number n.
So you are essentially creating a copy of natural numbers except that they are boxed. I don't think that's what you want to do.

What I meant to do was to create a boolvector type for every natural number. Like boolvector 1 for a vector of size 1, boolvector 2 for a vector of size 2, etc.

And I also wanted to add more constructors for type later. That's why I made it like that.

view this post on Zulip Théo Winterhalter (Jul 11 2021 at 11:22):

Yes, but you're not creating a type that way. boolvector n is not a type with your definition. It is with mine.

view this post on Zulip Théo Winterhalter (Jul 11 2021 at 11:22):

And that's what the error message is telling you.

view this post on Zulip Julin S (Jul 11 2021 at 11:31):

Théo Winterhalter said:

Yes, but you're not creating a type that way. boolvector n is not a type with your definition. It is with mine.

Maybe I need to something with the typeDenote for that? To do some translation to Type?

(Was reading CDPT book by Adam Chlipala :-D )


Last updated: Feb 08 2023 at 22:03 UTC