Stream: Coq users

Topic: [Newbie] Creating a boolean vector type

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.

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.

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.

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.

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.

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.

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.

Théo Winterhalter (Jul 11 2021 at 11:22):

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

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: Oct 04 2023 at 23:01 UTC