I'm trying to find the proof of Z.mul_comm in the standard libraries through Coqide. The following commands:

```
Require Import ZArith.
About Z.mul_comm.
```

returns:

```
Z.mul_comm : forall n m : Z, (n * m)%Z = (m * n)%Z
Z.mul_comm is not universe polymorphic
Arguments Z.mul_comm (_ _)%Z_scope
Z.mul_comm is opaque
Expands to: Constant Coq.ZArith.BinInt.Z.mul_comm
```

I can't find the definitions here (I'm using Coq-8.13). Any help locating definition and proof of this lemma would be appreciated (locating any Coq lemma from an imported library, in general). Thanks!

did a GitHub search. couldn't find it. looks like the situation is similar to mathlib on the lean side

p sure it's not explicitly defined but automatically generated through some sort of stuff I have yet to learn

that proof is specialized to `Z.mul_comm`

using modules and `Include`

. If you're familiar with inheritance, this is _vaguely_ similar to "you have class A, then class B extends A, then you're looking for `B.foo`

but only `A.foo`

is defined".

(some might object modules aren't objects — they aren't in Coq, but the commonalities are easier to see after studying Scala)

To expand @Gaëtan Gilbert's answer. The NZ part regroups things which are common to natural numbers and integers. The Numbers sublibrary factorizes lemmas shared by nat, N, Z. Then the ZArith part uses this to implement some modules there. That is why it appears as `ZArith.BinInt.Z.mul_comm`

, it comes for free in the Z module.

Nowadays, modules aren't used as much (the Numbers library goes back to 2007) for abstraction. A more modern library would probably use canonical structures or typeclasses. I still think modules are nice for refactoring though.

I agree it would be nice to trace the origin of this lemma though.

Maybe the command you are looking for is `Locate <id>.`

- it tells you in which module <id> is defined. You can also use Locate "<notation>" to find the definition of a notation. The mapping of module names to file names is not completely trivial (there can be various roots), but for standard library stuff the module path maps to /lib/coq/theories. Also note that files can have modules in them.

Michael Soegtrop said:

Maybe the command you are looking for is

`Locate <id>.`

- it tells you in which module <id> is defined. You can also use Locate "<notation>" to find the definition of a notation. The mapping of module names to file names is not completely trivial (there can be various roots), but for standard library stuff the module path maps to /lib/coq/theories. Also note that files can have modules in them.

This is very helpful, thanks!

Pierre Rousselin said:

To expand Gaëtan Gilbert's answer. The NZ part regroups things which are common to natural numbers and integers. The Numbers sublibrary factorizes lemmas shared by nat, N, Z. Then the ZArith part uses this to implement some modules there. That is why it appears as

`ZArith.BinInt.Z.mul_comm`

, it comes for free in the Z module.Nowadays, modules aren't used as much (the Numbers library goes back to 2007) for abstraction. A more modern library would probably use canonical structures or typeclasses. I still think modules are nice for refactoring though.

I agree it would be nice to trace the origin of this lemma though.

Makes sense, thanks for the explanation!

Last updated: Oct 13 2024 at 01:02 UTC