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
[] 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.
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 "" 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
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
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
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
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