Stream: Coq users

Topic: ✔ Same type in multiple definitions

Julin S (Feb 01 2022 at 09:16):

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?

Théo Winterhalter (Feb 01 2022 at 09:19):

Here you are saying from any exp I can obtain a list of A for any A.

Meven Lennon-Bertrand (Feb 01 2022 at 09:20):

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.

Théo Winterhalter (Feb 01 2022 at 09:20):

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.

Julin S (Feb 01 2022 at 09:27):

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.

Notification Bot (Feb 01 2022 at 09:29):

Julin S has marked this topic as resolved.

Meven Lennon-Bertrand (Feb 01 2022 at 09:29):

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.

Théo Winterhalter (Feb 01 2022 at 09:40):

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.

Meven Lennon-Bertrand (Feb 01 2022 at 09:45):

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!

Julin S (Feb 01 2022 at 11:57):

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

Last updated: Sep 28 2023 at 10:01 UTC