Stream: Coq users

Topic: Declare variable

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

Paolo Giarrusso (Jul 23 2022 at 10:24):

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

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.

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.

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.

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.

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.

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.

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?

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).

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.

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.

MMY MMY (Jul 23 2022 at 16:11):

Thanks a lot.

Last updated: Sep 23 2023 at 13:01 UTC