((_ %/ _) %/ _)%Z does not typecheck if polydiv is imported

[pi8027]

From mathcomp Require Import all_ssreflect all_algebra.

Fail Check ((_ %/ _) %/ _)%Z.

The command has indeed failed with message:
The term "(?p %/ ?q)%R" has type "GRing.Lmodule.sort (poly_lmodType ?R)" while it is expected to have type
 "int".

Arguments divz _%int_scope _%int_scope does not fix this. I guess we have to wait until Coq 8.14: coq/coq#13965. This one is for abbreviations so unrelated...

[pi8027]

I thought there would be an intermediate structure between integral domains and fields (such as Euclidean domains) that subsumes these concepts of division operators. However, divp is not a Euclidean division in general but is a pseudo-Euclidean division.

[CohenCyril]

@pi8027 in CoqEAL there are euclidean domains.

[pi8027]

Now I think %/ in int_scope should be redefined to let its arguments inherit int_scope, i.e.,

Notation "m %/ d" := (divz m%Z d%Z) : int_scope.

BTW, the following doesn't have the same effect and doesn't work. What is the difference? @proux01

Notation "m %/ d" := (divz m d)
  (m in scope int_scope, d in scope int_scope) : int_scope.

[pi8027]

I'm also a bit surprised since m and d in (m %/ d)%Z do not seem to use int_scope to interpret notations. I'm taking a look at the reference manual but cannot find the explanation.

[proux01]

I guess the difference is between deep scope opening (with m%Z the entire term m gets interpreted in scope int_scope) versus shallow (in the second case, only the topmost notation in m is interpreted in int_scope). But I haven't checked.

[proux01]

About the initial issue, maybe %/ in polydiv shouldn't be put in ring_scope (it's not a generic ring thing after all) but in some specific poly_scope?

[pi8027]

I guess the difference is between deep scope opening (with m%Z the entire term m gets interpreted in scope int_scope) versus shallow (in the second case, only the topmost notation in m is interpreted in int_scope). But I haven't checked.

If %Z is the deep scope opening, the inner %/ in ((_ %/ _) %/ _)%Z should be interpreted in int_scope, but the initial issue shows that it is not.

[proux01]

Apparently because it's overriden by

Arguments divz (m d)%ring_scope

[pi8027]

Thanks. That explains the issue! What we need is probably:

Arguments divz (m d)%int_scope%ring_scope

where my intention is to give priority to int_scope (placing int_scope on top of the notation scope stack).

[pi8027]

Also, always opening ring_scope when opening int_scope in this order is probably what I mean by int_scope is a subscope of ring_scope.

[proux01]

Yes, we should probably add something like #[add_top] Bind Scope int_scope with int in ssrint.v (c.f. https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#binding-types-or-coercion-classes-to-notation-scopes )