Stream: Coq users

Topic: Scope priority


view this post on Zulip Ana de Almeida Borges (Mar 05 2021 at 16:49):

As far as I know, if the same notation has different meanings in different scopes, then the most-recently-opened scope has priority. For example:

Require Import ZArith Int63.

Local Open Scope int63_scope.
Local Open Scope Z_scope.

Locate "+". (* default interpretation is Z.add *)

Then I would expect that

Check (to_Z (2 << 1 + 1)).

would fail, because 2 << 1 is an int and ... + 1 would be interpreted in Z by default. However, Coq accepts this, interpreting the + as the int63 one.

But!

Check (2 << 1 + 1).

does fail with

Error:
The term "2 << 1" has type "int" while it is expected to have type "Z".

as I expected. What is going on?

view this post on Zulip Kazuhiko Sakaguchi (Mar 05 2021 at 17:23):

That's because the first argument of to_Z has the int63_scope. See About to_Z.

view this post on Zulip Ana de Almeida Borges (Mar 05 2021 at 17:28):

Nice, I wasn't aware that arguments could have assigned scopes. How would I set that up for a new definition? Is it just an automatic consequence of the argument's type? What if there are several scopes related with that type?

view this post on Zulip Kazuhiko Sakaguchi (Mar 05 2021 at 17:33):

The Arguments command allows assigning scopes to arguments manually. As you have guessed, one may associate a type (more precisely, a coercion class) to a scope using the Bind Scope command, and then it becomes automatic. https://github.com/coq/coq/blob/3915bc904fc16060c25baaf7d5626e3587ad2891/theories/Numbers/Cyclic/Int63/PrimInt63.v#L36

view this post on Zulip Kazuhiko Sakaguchi (Mar 05 2021 at 17:48):

IIUC, at most one scope can be associated with a coercion class. Setting these scopes of arguments automatically is done when one declares a constant (such as to_Z) or an inductive type.

view this post on Zulip Ana de Almeida Borges (Mar 05 2021 at 18:27):

Thank you, this has been very helpful!

view this post on Zulip Paolo Giarrusso (Mar 06 2021 at 12:16):

A gotcha: You’ll want to call Bind Scope for a type foo as soon as foo is defined, for things to work well.
If you don’t, when you do call Bind Scope, the scopes of existing functions will be updated retroactively, but the scopes of existing notations will not.


Last updated: Jan 27 2023 at 01:03 UTC