Stream: Coq users

Topic: Locating Lemmas


view this post on Zulip 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.
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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 20 2023 at 17:22):

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

view this post on Zulip 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".

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

This is very helpful, thanks!

view this post on Zulip 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