[Coq-Club] overloading natural number notations for user types

[Jonathan Leivent]

Is there a way in Coq to overload the natural number notations? There
seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a
BigZ.t_. However, in neither case is the Notation "42" itself defined.
At least in the case of bigZ_scope, the only notations defined are "0",
"1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local. So,
what magic makes it work for all other natural number notations as
well? And can it be used for user-defined types?

-- Jonathan

[Robbert Krebbers]

Hi Jonathan,

The parsers for numerals are implemented in OCaml. See for example
plugins/syntax/nat_syntax.ml in the Coq source tree.

Best,

Robbert

Post by Jonathan Leivent
Is there a way in Coq to overload the natural number notations? There
seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a
BigZ.t_. However, in neither case is the Notation "42" itself defined.
At least in the case of bigZ_scope, the only notations defined are "0",
"1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local. So,
what magic makes it work for all other natural number notations as
well? And can it be used for user-defined types?
-- Jonathan

[Jonathan Leivent]

Thanks, Robbert. Unfortunately, I guess this means "not without a
plugin". Instead, I'll just define hopefully enough numbers via
Notations...

-- Jonathan

Post by Robbert Krebbers
Hi Jonathan,
The parsers for numerals are implemented in OCaml. See for example
plugins/syntax/nat_syntax.ml in the Coq source tree.
Best,
Robbert

Post by Jonathan Leivent
Is there a way in Coq to overload the natural number notations? There
seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a
BigZ.t_. However, in neither case is the Notation "42" itself defined.
At least in the case of bigZ_scope, the only notations defined are "0",
"1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local. So,
what magic makes it work for all other natural number notations as
well? And can it be used for user-defined types?
-- Jonathan

[Pierre-Marie Pédrot]

Post by Jonathan Leivent
Thanks, Robbert. Unfortunately, I guess this means "not without a
plugin". Instead, I'll just define hopefully enough numbers via
Notations...

Out of curiosity, what prevents you from writing / using a plugin?

PMP

[Jonathan Leivent]

Post by Pierre-Marie Pédrot

Post by Jonathan Leivent
Thanks, Robbert. Unfortunately, I guess this means "not without a
plugin". Instead, I'll just define hopefully enough numbers via
Notations...

Out of curiosity, what prevents you from writing / using a plugin?
PMP

1. I don't have all of the necessary instructions.

2. I want my project to be usable by Coq novices who know even less
about plugins than I do. One goal of my project is to try to make Coq
(and dependent-type language-based proof assistants in general) more
appealing as a tool to software developers who otherwise wouldn't
consider using a proof assistant, because they might believe the costs
outweigh the benefits. Hence, keeping the bar as low as possible is ideal.

3. Writing plugins does not appear to me to be as safe or maintainable
as directly using the existing UI.

4. Stressing the UI (Ltac, commands, etc.) allows me to find more bugs,
more opportunities for UI enhancement, and so forth - and in this way,
perhaps contribute ever so slightly to nudging the UI towards a future
less in continuous need of plugins. After all, not all Coq users should
have to become Coq developers.

These are subject to change...

-- Jonathan

[Clément Pit--Claudel]

Post by Pierre-Marie Pédrot

Post by Jonathan Leivent
Thanks, Robbert. Unfortunately, I guess this means "not without a
plugin". Instead, I'll just define hopefully enough numbers via
Notations...

Out of curiosity, what prevents you from writing / using a plugin?

Here's my take on that question:
* It requires knowledge of a second programming language beyond Ltac and Gallina, and of some Coq internals
* It's harder to audit for people reviewing my code, due to the point above; it's also harder to maintain or extend for others
* It won't work with all Coq interfaces; for example, it won't work with jsCoq IIUC
* It will make it harder to ensure backwards compatibility (now I need to care about Coq's internal interfaces). Maybe it'll break or become outdated, and there won't be as much documentation about ways to update it (there's not much about internals in CHANGES)
* I don't know how to do it, and I'm not sure where to learn (quick searches didn't turn up documentation, just tutorials), or whether it would be a good investment to learn
* Coq's notations are pretty good already

Cheers,
Clément.

[Assia Mahboubi]

Hello,

Post by Pierre-Marie Pédrot
Out of curiosity, what prevents you from writing / using a plugin?

My 5 cents: it is nice to see plugins as user-defined facilities that increase
the proof *assistant* code base of Coq.

But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.

That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?

Anyway, for what it's worth, I wrote such a plugin during last year's Coding
Sprint, with the help of Pierre Boutillier. I just cleaned it up a bit and
made it independent from its original context so that it can serve as a
documentation stub: https://github.com/amahboubi/coq-num-notations

Best,

assia

[Beta Ziliani]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hello,

Post by Pierre-Marie Pédrot
Out of curiosity, what prevents you from writing / using a plugin?

My 5 cents: it is nice to see plugins as user-defined facilities that increase
the proof *assistant* code base of Coq.
But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.
That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?

You mean to incorporate parsing primitives to (e.g.) Mtac? This can be an
interesting project indeed!

Anyway, for what it's worth, I wrote such a plugin during last year's Coding
Sprint, with the help of Pierre Boutillier. I just cleaned it up a bit and
made it independent from its original context so that it can serve as a
documentation stub: https://github.com/amahboubi/coq-num-notations
Best,
assia
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)
iQIcBAEBAgAGBQJWydPkAAoJEFY7bbrolXGxYRoP/j1//TFFdYVPRA23mfyPuAsz
g74XI1++tqE8BPPxtuBDgm+aOGMfng1ii8/EXNSTxoJaL6N0fz9ACPCB2y//mwmU
AF0TPUJfekYb5Fu2yWaaJ3yh7IOH/4Jytxuofr9biGpWdmf+OaiZe3f9BiRoOlJc
JxMSlqVlWvTnFaiwUKtx8YcccD6XfPXS+grsX3aVK1nhyEyMYNjYkD8Ox+gnbK9d
qbDbybA9U2hzh6jbYBDjTbR99SA7XlVUndLbhXBoF6JfYJL9aIZ0wPfE4CppONNP
W+mXPz1lwQY6glvYkXmHQ5M4rHLRUCJjdtiKosTnT2iTd9dhv1v/OWcLP5ID/V0j
UPWUMEUWs0k6HMHTFROQKJzlyBG0HdZ0rqRyDYTJfEUuNgNqI8ieyfWNHeLTNIIe
z3KtqWaLj44PRp73A7f39igxeNaJJGOKPLJo4g0PmwYOEyzPWyltiOzXDlHOM70N
wiJoR2SildFUJ1T+Va2T1jWiLuKMwNtzQZS5HzB6HYkqGt9tO1UyNsuKaXLNKKfK
yV2cHPNuaPPNgC+TTA4aDP+MjBLuY8adIvXP/6vW/3GUJP7pg9y7djTZlvLM6boQ
Di2Wa3O9/jIHZ5/t5q0IiayRlYUIYuXH2nKa6pVT8oZqfKdOalw4MYVe/rRpTfPE
e7mNpbHRXVKxEARYXvbl
=t5PH
-----END PGP SIGNATURE-----

[Beta Ziliani]

Post by Assia Mahboubi
[...]
But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.
That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?

You mean to incorporate parsing primitives to (e.g.) Mtac? This can be an
interesting project indeed!

[Jason Gross]

How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in nat_scope
[O S].] and similarly for notations for negative numbers, ascii, strings,
etc?

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hello,

Post by Pierre-Marie Pédrot
Out of curiosity, what prevents you from writing / using a plugin?

My 5 cents: it is nice to see plugins as user-defined facilities that increase
the proof *assistant* code base of Coq.
But parsers are definitely part of the trusted code base. And I agree with the
other contributors to this thread that in the current state of affairs, it is
not so easy to assess the reliability of third-party plugins.
That being said, I have no concrete suggestion on how to improve the situation
concretely. Is there any hope that one day tools like Cybele/Mtac could come
at the rescue?
Anyway, for what it's worth, I wrote such a plugin during last year's Coding
Sprint, with the help of Pierre Boutillier. I just cleaned it up a bit and
made it independent from its original context so that it can serve as a
documentation stub: https://github.com/amahboubi/coq-num-notations
Best,
assia
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)
iQIcBAEBAgAGBQJWydPkAAoJEFY7bbrolXGxYRoP/j1//TFFdYVPRA23mfyPuAsz
g74XI1++tqE8BPPxtuBDgm+aOGMfng1ii8/EXNSTxoJaL6N0fz9ACPCB2y//mwmU
AF0TPUJfekYb5Fu2yWaaJ3yh7IOH/4Jytxuofr9biGpWdmf+OaiZe3f9BiRoOlJc
JxMSlqVlWvTnFaiwUKtx8YcccD6XfPXS+grsX3aVK1nhyEyMYNjYkD8Ox+gnbK9d
qbDbybA9U2hzh6jbYBDjTbR99SA7XlVUndLbhXBoF6JfYJL9aIZ0wPfE4CppONNP
W+mXPz1lwQY6glvYkXmHQ5M4rHLRUCJjdtiKosTnT2iTd9dhv1v/OWcLP5ID/V0j
UPWUMEUWs0k6HMHTFROQKJzlyBG0HdZ0rqRyDYTJfEUuNgNqI8ieyfWNHeLTNIIe
z3KtqWaLj44PRp73A7f39igxeNaJJGOKPLJo4g0PmwYOEyzPWyltiOzXDlHOM70N
wiJoR2SildFUJ1T+Va2T1jWiLuKMwNtzQZS5HzB6HYkqGt9tO1UyNsuKaXLNKKfK
yV2cHPNuaPPNgC+TTA4aDP+MjBLuY8adIvXP/6vW/3GUJP7pg9y7djTZlvLM6boQ
Di2Wa3O9/jIHZ5/t5q0IiayRlYUIYuXH2nKa6pVT8oZqfKdOalw4MYVe/rRpTfPE
e7mNpbHRXVKxEARYXvbl
=t5PH
-----END PGP SIGNATURE-----

[Jason Gross]

I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.

I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.

On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <

Post by Jason Gross
How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP

[Jonathan Leivent]

I was thinking something even stupider than that! The user gives two
functions that map between nats and the user type they want to represent
with number notations:

Inductive mynat : Set := ...

Definition nat2mynat(n : nat) : mynat := ...

Definition mynat2nat(m: mynat) : nat := ...

Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.

The parser would, whenever it sees a number in the scope M_scope, call
nat2mynat and use the result. The printer would, whenever it sees a
mynat in the scope M_scope, call mynat2nat, and print the resulting number.

-- Jonathan

Post by Jason Gross
I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <

Post by Jason Gross
How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP

[Jason Gross]

Jonathan, how does that work on open terms? It'll work fine for parsing,
probably (though I don't really want to be able to do arbitrary computation
in the parsing of my numerals, that's perhaps a bit scary, but perhaps
useful), but seems kind-of sketchy for printing.

Post by Jonathan Leivent
I was thinking something even stupider than that! The user gives two
functions that map between nats and the user type they want to represent
Inductive mynat : Set := ...
Definition nat2mynat(n : nat) : mynat := ...
Definition mynat2nat(m: mynat) : nat := ...
Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.
The parser would, whenever it sees a number in the scope M_scope, call
nat2mynat and use the result. The printer would, whenever it sees a mynat
in the scope M_scope, call mynat2nat, and print the resulting number.
-- Jonathan

Post by Jason Gross
I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <

Post by Jason Gross
How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP

[Gregory Malecha]

Would Coercions fit the bill for the nat2mynat idea? Or are they not
expressive enough.

Post by Jason Gross
Jonathan, how does that work on open terms? It'll work fine for parsing,
probably (though I don't really want to be able to do arbitrary computation
in the parsing of my numerals, that's perhaps a bit scary, but perhaps
useful), but seems kind-of sketchy for printing.

Post by Jonathan Leivent
I was thinking something even stupider than that! The user gives two
functions that map between nats and the user type they want to represent
Inductive mynat : Set := ...
Definition nat2mynat(n : nat) : mynat := ...
Definition mynat2nat(m: mynat) : nat := ...
Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.
The parser would, whenever it sees a number in the scope M_scope, call
nat2mynat and use the result. The printer would, whenever it sees a mynat
in the scope M_scope, call mynat2nat, and print the resulting number.
-- Jonathan

Post by Jason Gross
I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <

Post by Jason Gross
How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP

[Jonathan Leivent]

In this particular case, I did manage to use coercions. I did have to
change a few tactics to accommodate the appearance of the coercion
function, but it worked. It does feel a bit fragile, though. In
particular, the user type that I want numerals to work for is also
declared to be a ring, and I need ring-simplify to work properly even in
other cases I haven't tried yet. Maybe I can rig the Add Ring
declaration with the necessary preprocess/postprocess tactics to
unfold/fold the coercion function?

But, I would like to avoid this by having everything handled in the
parse/print layers.

As for Jason's question of how my "stupider" suggestion should handle
open terms and printing, well, I did say it was stupider.

If there were concerns about the functions not providing an isomorphism
(hence being able to appear to prove "2 = 3", for example) - then I
guess it could require a Class with proofs that the two conversion
functions provide an isomorphism.

-- Jonathan

Post by Gregory Malecha
Would Coercions fit the bill for the nat2mynat idea? Or are they not
expressive enough.

Post by Jason Gross
Jonathan, how does that work on open terms? It'll work fine for parsing,
probably (though I don't really want to be able to do arbitrary computation
in the parsing of my numerals, that's perhaps a bit scary, but perhaps
useful), but seems kind-of sketchy for printing.

Post by Jonathan Leivent
I was thinking something even stupider than that! The user gives two
functions that map between nats and the user type they want to represent
Inductive mynat : Set := ...
Definition nat2mynat(n : nat) : mynat := ...
Definition mynat2nat(m: mynat) : nat := ...
Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.
The parser would, whenever it sees a number in the scope M_scope, call
nat2mynat and use the result. The printer would, whenever it sees a mynat
in the scope M_scope, call mynat2nat, and print the resulting number.
-- Jonathan

Post by Jason Gross
I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <

Post by Jason Gross
How hard would it be to set up the syntax plugins already in Coq so that
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP

[Jonathan Leivent]

Post by Jonathan Leivent
In this particular case, I did manage to use coercions. I did have to
change a few tactics to accommodate the appearance of the coercion
function, but it worked. It does feel a bit fragile, though. In
particular, the user type that I want numerals to work for is also
declared to be a ring, and I need ring-simplify to work properly even
in other cases I haven't tried yet. Maybe I can rig the Add Ring
declaration with the necessary preprocess/postprocess tactics to
unfold/fold the coercion function?
But, I would like to avoid this by having everything handled in the
parse/print layers.

Another issue: with the coercions in place, some proofs are much
slower. I don't know what is causing the slowdown. Of course, one
suspect would be that the coercion function - being in the actual terms
as opposed to merely being something called and desugared by the parser
- is somehow messing with my tactics.

-- Jonathan

[Jonathan Leivent]

This is a follow-up to the "overloading natural number notations for
user types" thread.
Suppose one has a generic inductive type, such as:

Inductive foo(S : Set) : Set :=
| Foo(x : S).

And then wishes to declare coercions from various Sets, for example nat,
to the corresponding foo. Coq does not allow the following:

Coercion (Foo nat) : nat >-> foo.

as it requires that the Coercion command's first arg is a name. It also
doesn't allow using implicits, as in:

Arguments Foo {S} x.
Coercion Foo : nat >-> foo.

Instead, one must use an intermediate function for the coercion, such as:

Definition nat2foo := Foo nat.
Coercion nat2foo : nat >-> foo.

Why is there this restriction? Why doesn't Coq allow partially
parameterized functions as coercions?

Note that this restriction would not be so bad if there was a way to
declare nat2foo as "always unfolding". Meaning, not just something like
"Strategy expand [nat2foo].", but that nat2foo is always immediately
unfolded - that it behaves almost like a notation. Otherwise, consider a
rewrite rule such as:

Variables F G : (foo nat) -> nat.
Axiom rw : F 1 = G 2.

Because rw was defined using the nat2foo coercion, it can't handle cases
where nat2foo doesn't appear:

Goal F 1 = G 2.
cbv. (*unfolds nat2foo*)
Fail rewrite rw.

-- Jonathan

[Jason Gross]

Much like the uniform inheritance condition, I believe the answer is
"hysterical raisins" and "lack of time or manpower to fix it" and "pull
requests are welcome".

You might be interested in [Set Keyed Unification] in Coq 8.5 (to handle
your rewriting issue), bug #3115
<https://coq.inria.fr/bugs/show_bug.cgi?id=3115> (identity coercion
limitations), bug #3389
<https://coq.inria.fr/bugs/show_bug.cgi?id=3389> (feature
request for your "always unfolding", which I called "expand_invisible"), bug
#2322 <https://coq.inria.fr/bugs/show_bug.cgi?id=2322> (terms as
coercions), and bug #4593 <https://coq.inria.fr/bugs/show_bug.cgi?id=4593> (one
I just reported about removing the uniform inheritance condition).

Post by Jonathan Leivent
This is a follow-up to the "overloading natural number notations for
user types" thread.
Inductive foo(S : Set) : Set :=
| Foo(x : S).
And then wishes to declare coercions from various Sets, for example nat,
Coercion (Foo nat) : nat >-> foo.
as it requires that the Coercion command's first arg is a name. It also
Arguments Foo {S} x.
Coercion Foo : nat >-> foo.
Definition nat2foo := Foo nat.
Coercion nat2foo : nat >-> foo.
Why is there this restriction? Why doesn't Coq allow partially
parameterized functions as coercions?
Note that this restriction would not be so bad if there was a way to
declare nat2foo as "always unfolding". Meaning, not just something like
"Strategy expand [nat2foo].", but that nat2foo is always immediately
unfolded - that it behaves almost like a notation. Otherwise, consider a
Variables F G : (foo nat) -> nat.
Axiom rw : F 1 = G 2.
Because rw was defined using the nat2foo coercion, it can't handle cases
Goal F 1 = G 2.
cbv. (*unfolds nat2foo*)
Fail rewrite rw.
-- Jonathan

[Jonathan Leivent]

Another similar problem with coercions - the source and destination
types also have to be names, not terms. Hence, one cannot do:

Coercion f : (foo a) >-> (bar b).

I tried to fool this by using abbreviations, such as:

Notation fooa := (foo a).
Notation barb := (bar b).
Coercion f : fooa >-> barb.

Interestingly, the Coercion command in this case did not fail, but also
did not have any impact.

I think I will add this to bug #2322.

-- Jonathan

Post by Jason Gross
Much like the uniform inheritance condition, I believe the answer is
"hysterical raisins" and "lack of time or manpower to fix it" and "pull
requests are welcome".
You might be interested in [Set Keyed Unification] in Coq 8.5 (to handle
your rewriting issue), bug #3115
<https://coq.inria.fr/bugs/show_bug.cgi?id=3115> (identity coercion
limitations), bug #3389
<https://coq.inria.fr/bugs/show_bug.cgi?id=3389> (feature
request for your "always unfolding", which I called "expand_invisible"), bug
#2322 <https://coq.inria.fr/bugs/show_bug.cgi?id=2322> (terms as
coercions), and bug #4593 <https://coq.inria.fr/bugs/show_bug.cgi?id=4593> (one
I just reported about removing the uniform inheritance condition).

Post by Jonathan Leivent
This is a follow-up to the "overloading natural number notations for
user types" thread.
Inductive foo(S : Set) : Set :=
| Foo(x : S).
And then wishes to declare coercions from various Sets, for example nat,
Coercion (Foo nat) : nat >-> foo.
as it requires that the Coercion command's first arg is a name. It also
Arguments Foo {S} x.
Coercion Foo : nat >-> foo.
Definition nat2foo := Foo nat.
Coercion nat2foo : nat >-> foo.
Why is there this restriction? Why doesn't Coq allow partially
parameterized functions as coercions?
Note that this restriction would not be so bad if there was a way to
declare nat2foo as "always unfolding". Meaning, not just something like
"Strategy expand [nat2foo].", but that nat2foo is always immediately
unfolded - that it behaves almost like a notation. Otherwise, consider a
Variables F G : (foo nat) -> nat.
Axiom rw : F 1 = G 2.
Because rw was defined using the nat2foo coercion, it can't handle cases
Goal F 1 = G 2.
cbv. (*unfolds nat2foo*)
Fail rewrite rw.
-- Jonathan

[Daniel de Rauglaudre]

Hi all,

I am a volunteer to implement it, if nobody minds. I started looking
at it.

Post by Jonathan Leivent
Is there a way in Coq to overload the natural number notations?
There seems to be, because 42 in Z_scope is a Z, and 42 in
bigZ_scope is a BigZ.t_. However, in neither case is the Notation
"42" itself defined. At least in the case of bigZ_scope, the only
notations defined are "0", "1" and "2" (in
Numbers/Integer/BigZ/BigZ.v) - and those are Local. So, what magic
makes it work for all other natural number notations as well? And
can it be used for user-defined types?
-- Jonathan