Stream: Coq users

Topic: Notation for `list (option nat)`


view this post on Zulip 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?

view this post on Zulip 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]].

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 18 2022 at 09:52):

bidi hints work

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Julin S (Jan 18 2022 at 11:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 18 2022 at 15:17):

Yeah that's what I feared


Last updated: Mar 28 2024 at 17:01 UTC