Julin S (Jan 18 2022 at 07:18): 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]].
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.
Gaëtan Gilbert (Jan 18 2022 at 09:52):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).
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