Hi. I was trying something like:

```
Inductive exp : Type :=
| Lst : forall (A:Type), list A -> exp.
Definition expDenote {A:Type} (e: exp) : list A :=
match e with
| Lst _ ls => ls
end.
```

But got error saying

```
In environment
A : Type
e : exp
T : Type
ls : list T
The term "ls" has type "list T" while it is expected to have type "list A".
```

So I guess what I expressed doesn't convey the idea that the `A`

in `exp`

and `expDenote`

can be taken to be the same (is that bad?) variable .

Is there a way to communicate to coq that the `A`

mentioned in `exp`

and the one in `expDenote`

can be taken to be the same type?

Here you are saying from *any* `exp`

I can obtain a list of `A`

for *any* `A`

.

I think what you want to do is to introduce a type *variable* like so:

```
Section foo.
Variable A : Type.
Inductive exp : Type :=
| Lst : list A -> exp.
Definition expDenote (e: exp) : list A :=
match e with
| Lst ls => ls
end.
End foo.
```

This is equivalent to directly doing

```
Inductive exp (A : Type) : Type :=
| Lst : list A -> exp A.
Definition expDenote {A : Type} (e : exp A) : list A :=
match e with
| Lst _ ls => ls
end.
```

The difference with what you did is that the whole inductive type `exp`

takes the type `A`

as a parameter, rather than it appearing in the constructor `Lst`

. That way when you define `expDenote`

you can track the fact that the `A`

used in `exp`

is the same as that in the output by saying so.

The type is part of the data in `exp`

. So you can extract it the same as the list:

```
Definition expType (e : exp) : Type :=
match e with
| Lst A _ => A
end.
```

Thanks! I had thought having `Variable`

in sections was just for easier typing.

I did

```
Section foo.
Variable A : Type.
Inductive exp : Type :=
| Lst : list A -> exp.
Definition expDenote (e: exp) : list A :=
match e with
| Lst ls => ls
end.
End foo.
Arguments Lst {A} _.
Arguments expDenote {A} _.
Require Import List.
Import ListNotations.
Compute Lst [1;2;3].
Compute (expDenote (Lst [1;2;3])).
```

and it worked.

Julin S has marked this topic as resolved.

Indeed variables are only sugar coating, the second bit of code I gave does not use them and achieves the same result once the section is closed. But I think it is generally considered good practice to use section variables to do this kind of factoring for variables that recur over and over again in subsequent definitions/proofs.

I mean this is really not the same thing. The thing @Julin S wrote was that `exp`

could encode any list of any type. While with variables you parameterise `exp`

with the type of thing it can store.

Note that the second option is just a convoluted way of writing `exp A := list A`

.

Julin S said:

Is there a way to communicate to coq that the

`A`

mentioned in`exp`

and the one in`expDenote`

can be taken to be the same type?

What I gathered from this sentence was exactly that the goal was to keep a relation between the type appearing in `exp`

and the return one of `expDenote`

:) But indeed your solution has quite a different meaning!

Yeah I guess what I wrote first was different from what I wanted to right...:grimacing:

Last updated: Jun 17 2024 at 22:01 UTC