Stream: Coq users

Topic: ✔ [Newbie] What does % do in coq?

Julin S (Apr 22 2021 at 01:55):

Hi. I came across something like

Require Import Coq.PArith.BinPos.
Check 1%positive.

and couldn't figure out what "%" meant here. At first I thought it would be a modulus operation. But

Check positive. said positive is a Set.

I couldn't find anything on searching online (possibly due to % being a special character or something).

What does % mean in this context?

Jasper Hugunin (Apr 22 2021 at 03:01):

Here positive is the name of a notation scope, and the % opens that scope locally. Some documentation here Opening a notation scope locally.

Jasper Hugunin (Apr 22 2021 at 03:02):

The use of digits to represent numbers is something you can do in different ways, and Coq lets you customize it. Notation scopes then let you choose which interpretation you want to use.

Jasper Hugunin (Apr 22 2021 at 03:04):

Here, this just means "Interpret 1 as a term in the type positive", which as you found is a Set. The scope name and type name are often chosen to coincide, or at least be suggestive.

Julin S (Apr 22 2021 at 03:09):

Okay. So it's like asking coq to consider 1 as a positive. Something like type casts in programming languages like C.
Thanks!

Théo Winterhalter (Apr 22 2021 at 06:17):

No it's not a type-cast. If you do

Definition foo := 1%nat.

Definition bar := foo%positive.

Then bar will still be a natural number and not be cast to positive.
As Jasper was saying, numerals like 1 are only notations, and depending on the context they might have different interpretations. If you just write 1 it will give a different result depending on which scope is open. Using 1%positive, you tell Coq that the most important scope here is positive.

Julin S (Apr 24 2021 at 09:02):

So the notation will be interpreted based on the present environment?

Théo Winterhalter (Apr 24 2021 at 09:04):

Yes. Notations live in scope, and you can open them inside a module or section with

Open Scope nat_scope.

or locally inside a term with

expression%nat

you could add parentheses to make it clear which part is to be interpreted in which scope:

(0 + 1)%nat

Julin S (Apr 24 2021 at 09:05):

Thanks! Got a better idea now.

Notification Bot (Jul 16 2021 at 07:36):

Ju-sh has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC