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?

```
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]].
```

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.

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

Thanks a lot!

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

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?

As @Yannick Forster was saying, the `[[`

notation uses `@cons (option nat)`

to force Coq to construct a list of `option nat`

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

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

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?

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

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

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

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

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

Yeah that's what I feared

Last updated: Oct 04 2023 at 19:01 UTC