## Stream: Coq users

### Topic: Notation for `list (option nat)`

#### Julin S (Jan 18 2022 at 07:18):

I was trying to have a coq notation for a shorter way to express a `list (option nat)`. Something like:

`[[ 1, N, 2, 3, N, 4]]` leading to `[Some 1, None, Some 2, Some 3, None, Some 4]`

where we just got to mention the numbers for it to be expanded to `Some` values, yet there is a way to express `None` values as well.

Is such a thing possible?

Can custom entries be of help here if it is possible to have a custom entry within a custom entry or something?

Like a notation for an outer custom entry like `[[ ... ]]` and then an inner notation that can expand the `nat` values to `option nat` values?

#### Yannick Forster (Jan 18 2022 at 08:19):

``````Module OListNotations.
Notation "[[ ]]" := (@nil (option nat)) (format "[[ ]]") : olist_scope.
Notation "[[ x ]]" := (@cons (option nat) x nil) : olist_scope.
Notation "[[ x ,  y , .. , z ]]" :=  (@cons (option nat) x (@cons (option nat) y .. (@cons (option nat) z nil) ..)) : olist_scope.
Notation N := (@None nat).
Coercion Some_nat := (@Some nat).
Open Scope olist_scope.
End OListNotations.

Import OListNotations.
Compute [[ 1, N, 2, 3, N, 4]].
``````

#### Yannick Forster (Jan 18 2022 at 08:22):

Two central tricks: First, I added the coercion `Some_nat` so no notation for Some is needed. Second, I adapted the notations for lists from `Coq.Lists.List.ListNotations` to only apply to `option nat` - without that, the coercion from the first would not be triggered, because `[[4]]` is interpreted as `list nat`. Putting everything in a module and using a scope is good practice, but not necessary to make the example work.

#### Julin S (Jan 18 2022 at 09:04):

Cool! Didn't know much about coercions in Coq. Read the docs and got some idea.
Thanks a lot!

#### Julin S (Jan 18 2022 at 09:09):

Also thanks for telling about the use of modules to have better organized code. That's something I need to start using.

#### Julin S (Jan 18 2022 at 09:10):

The `Some_nat` coercion allows values of `nat` to be made into `Some` values of `option nat`, right?

After having that coercion declared, I tried

``````Notation N := (@None nat).
Coercion Some_nat := (@Some nat).

Require Import List.
Import ListNotations.
Definition foo : list (option nat) := [ 1; N; 2; 3; N; 4].
(*
The term "[4]" has type "list nat" while it is expected to have type
"list (option nat)".
*)
``````

but that didn't work.

So I guess the effect of the coercion is somehow limited to `[[ ... ]]`. How is it so?

#### Paolo Giarrusso (Jan 18 2022 at 09:41):

As @Yannick Forster was saying, the `[[` notation uses `@cons (option nat)` to force Coq to construct a list of `option nat`

#### Paolo Giarrusso (Jan 18 2022 at 09:44):

You're writing a return type annotation, but that information is not propagated to the right spot... I wonder if `Program Definition` would fix that (thanks to its different type inference algorithm), tho Program also changes a few other things.

bidi hints work

#### Yannick Forster (Jan 18 2022 at 10:06):

Oh, I didn't know that! Here's the elaborated example of what Gaëtan probably had in mind:

``````Require Import List.
Import ListNotations.

Arguments cons _ & _ _.

Coercion Some_nat := (@Some nat).
Compute [ 1; None; 2; 3; None; 4] : list (option nat).
``````

#### Julin S (Jan 18 2022 at 10:51):

Is there a way to generalise over the type in `option T`? Not just for a specific type as with `nat`?

Something like `Coercion Some_t := forall t:Type, @Some t`?

Is that possible?

#### Kenji Maillard (Jan 18 2022 at 10:57):

I would be surprised it were possible: with such a generic coercion, you would have two coercion paths from `A` to `option (option A)` (depending whether the second coercion happens inside or outside) so Coq wouldn't know which it should apply

#### Julin S (Jan 18 2022 at 11:03):

Okay, I guess that's the limit then. Thanks everyone!

#### Paolo Giarrusso (Jan 18 2022 at 12:18):

polymorphic coercions do exist, fwiw, but have restrictions. For instance, a coercion from option t to list t should work fine

#### Paolo Giarrusso (Jan 18 2022 at 12:22):

t -> list t is probably impossible, but I don't understand @Kenji Maillard's reasoning: the only coercion is Some_t (Some_t n) it seems, but I don't know what would be the class of the generic t... Can one write a coercion from Sortclass? I guess not

#### Meven Lennon-Bertrand (Jan 18 2022 at 12:42):

AFAIK `Sortclass` and `Funclass` exist because in some situations you only know that something has to be a type/function but not more (ie the complete type something is checked against), so it makes sense to have those only as target classes but not sources

#### Paolo Giarrusso (Jan 18 2022 at 15:17):

Yeah that's what I feared

Last updated: Oct 04 2023 at 19:01 UTC