Stream: Coq users

Topic: ✔ Getting Nat2Z to scope


view this post on Zulip Sami Liedes (Oct 16 2021 at 21:09):

I'm trying to understand the scoping of Coq. I'd need Nat2Z.inj_pow in a proof of mine, and https://coq.inria.fr/library/Coq.ZArith.Znat.html tells that such a module has such a lemma.

So, I've done

Require Import BinNums.
Require Import Coq.ZArith.BinInt.
Require Import Coq.ZArith.Znat.

For some reason, Coq doesn't find the lemma (or anything else) in Nat2Z, but does in a few other submodules there. Search "inj_pow". shows these lemmas named inj_pow:

Pos2Z.inj_pow:  p q : positive, Z.pos (p ^ q) = (Z.pos p ^ Z.pos q)%Z
N2Z.inj_pow:  n m : N, Z.of_N (BinNat.N.pow n m) = (Z.of_N n ^ Z.of_N m)%Z
Zabs2N.inj_pow:  n m : Z, (0 <= m)%Z  Z.abs_N (n ^ m) = BinNat.N.pow (Z.abs_N n) (Z.abs_N m)
Z2N.inj_pow:  n m : Z, (0 <= n)%Z  (0 <= m)%Z  Z.to_N (n ^ m) = BinNat.N.pow (Z.to_N n) (Z.to_N m)
Z2Pos.inj_pow:  x y : Z, (0 < x)%Z  (0 < y)%Z  Z.to_pos (x ^ y) = (Z.to_pos x ^ Z.to_pos y)%positive

What am I missing?

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 21:26):

It seems your link is about Coq 8.14, which has more inj_pow lemmas in that specific file than (say) Coq 8.13 (on which I can reproduce your symptoms).

view this post on Zulip Paolo Giarrusso (Oct 16 2021 at 21:48):

indeed, comparing https://coq.github.io/doc/v8.13/stdlib/Coq.ZArith.Znat.html vs https://coq.github.io/doc/v8.14/stdlib/Coq.ZArith.Znat.html seems to agree; the change seems to have happened as part of the lia improvements in https://github.com/coq/coq/pull/14037.

view this post on Zulip Sami Liedes (Oct 16 2021 at 22:00):

Ah, that makes sense. Thank you :)

view this post on Zulip Notification Bot (Oct 17 2021 at 08:18):

Sami Liedes has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC