## Stream: Coq users

### Topic: Locating Lemmas

#### Arjun Viswanathan (Nov 20 2023 at 14:50):

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

``````Require Import ZArith.
``````

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!

#### Huỳnh Trần Khanh (Nov 20 2023 at 17:06):

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

#### Huỳnh Trần Khanh (Nov 20 2023 at 17:07):

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

#### Gaëtan Gilbert (Nov 20 2023 at 17:22):

https://github.com/coq/coq/blob/0c40866dc1b2f0c54c0f9bba4d965d961e6655cb/theories/Numbers/NatInt/NZMul.v#L33

#### Paolo Giarrusso (Nov 20 2023 at 17:38):

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".

#### Paolo Giarrusso (Nov 20 2023 at 17:45):

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

#### Pierre Rousselin (Nov 20 2023 at 17:46):

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.

#### Michael Soegtrop (Nov 20 2023 at 18:43):

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.

#### Arjun Viswanathan (Nov 22 2023 at 15:10):

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.

#### Arjun Viswanathan (Nov 22 2023 at 15:11):

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: Jun 23 2024 at 05:02 UTC