Stream: Coq users

Topic: Declare variable


view this post on Zulip MMY MMY (Jul 23 2022 at 08:39):

How can I declare an array type variable defined as follows:
Inductive array (n : nat) : Type :=
tab : forall l : list Z, length l = n -> array n.

I want to declare as:
arrayConstant: array

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 10:24):

You could write arrayConstant : array 10 instead, for an array of length 10.

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 10:25):

In general, yoy want arrayConstant : array m for some term m of type nat; my last example used m = 10, but that's just an example.

view this post on Zulip MMY MMY (Jul 23 2022 at 10:34):

Thank you for your reply.
I tried to do something like this but got the error : The reference n was not found in the current environment.

With code :

Inductive array (n : nat) : Type :=
tab : forall l : list nat, length l = n -> array n.

Definition n : nat.

Inductive Const : Type :=
| arrayConstant : array n -> Const.

view this post on Zulip James Wood (Jul 23 2022 at 14:27):

Is it that you want Variable rather than Definition? A definition has to have a body, i.e, a specific natural number in this case.

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 15:06):

Indeed, n is not available after Definition n : nat. — that command just _starts_ a definition, but n is only available when you've _completed_ the definition — say, after Defined.

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 15:07):

eg n is available after

Definition n : nat.
  exact 42.
Defined.

but that is best written as

Definition n : nat := 42.

view this post on Zulip MMY MMY (Jul 23 2022 at 15:24):

I don't need to specify a value.
I'm looking to define an array type for some semantics.

view this post on Zulip James Wood (Jul 23 2022 at 15:40):

Can you say a bit more about what you're trying to do, and why neither Definition nor Variable is the right thing?

view this post on Zulip James Wood (Jul 23 2022 at 15:48):

Do you want to say something like “a Const can be an array of arbitrary length”? That'd look like:

Inductive Const : Type :=
| arrayConst {n} : array n -> Const.

(with no Definition or Variable or whatever). The idea is that the length is another piece of data packed into the constructor arrayConst (along with the actual array).

view this post on Zulip MMY MMY (Jul 23 2022 at 15:48):

I want to define an array type.
Then use this definition as a type.

How can I make this piece of code work:

Inductive array (n : nat) : Type :=
tab : forall l : list nat, length l = n -> array n.

Inductive Const : Type :=
| arrayConstant : array -> Const.

view this post on Zulip James Wood (Jul 23 2022 at 16:05):

In case it helps, you can also consider the type { n & array n } (using notation https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#e6a434cae860987d1c5f61b342cc9e57), which is what you might be thinking of when you want to use array as a type (the total space of arrays). By Currying, declaring arrayConstant : { n & array n } -> Const is equivalent (at the level of isomorphism) to what I gave before.

view this post on Zulip MMY MMY (Jul 23 2022 at 16:11):

Thanks a lot.


Last updated: Feb 08 2023 at 22:03 UTC