Stream: Coq users

Topic: ✔ [Newbie] Coerce a list

Matthis Kruse (Sep 04 2021 at 12:56):

Hey,
I have an inductive type that looks like

Inductive A : Type :=
| Abase : A
| Alist : list A -> A
.

I'd like to use Alist as a coercion, how can I achieve that?

e.g.

Definition isA : A := (nil : list A).

Paolo Giarrusso (Sep 04 2021 at 13:45):

I don't know a way to do exactly that, but here is something close. Feel free to ask questions.

Inductive A : Type :=
| Abase : A
| Alist : list A -> A
.

Module Import test.
  Definition listA := list A.

  Identity Coercion Id_listA_list : listA >-> list.
  #[global] Arguments Id_listA_list /.

  Coercion Alist' := Alist : listA -> A.
  #[global] Arguments Alist' /.
End test.

Definition isA : A := (nil : listA).

Note the coercion applies to listA, not list A; coercions (like much else in Coq) distinguish between definitionally equal but syntactically different terms.

References: https://coq.inria.fr/refman/addendum/implicit-coercions.html

Gaëtan Gilbert (Sep 04 2021 at 14:02):

what's the identity coercion for?

Paolo Giarrusso (Sep 04 2021 at 18:05):

good point; I was trying to get bidirectional coercions between list A and listA, but then I remembered I never got that to work because of the uniform inheritance condition.

Paolo Giarrusso (Sep 04 2021 at 18:06):

That seems disappointing, since working around that restriction is a crucial use-case for identity coercions.

Paolo Giarrusso (Sep 04 2021 at 18:07):

Indeed, I rechecked https://coq.inria.fr/refman/addendum/implicit-coercions.html#identity-coercions and the same question applies.

Paolo Giarrusso (Sep 04 2021 at 18:08):

Maybe you’re supposed to replace all uses of list A with listA by hand in your development? That’s what I did other times.

Notification Bot (Sep 06 2021 at 07:53):

Matthis Kruse has marked this topic as resolved.

Last updated: Apr 20 2024 at 12:02 UTC