Sami Liedes (Oct 16 2021 at 21:09): 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?
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).
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.
Sami Liedes (Oct 16 2021 at 22:00):Ah, that makes sense. Thank you :)
Notification Bot (Oct 17 2021 at 08:18):Sami Liedes has marked this topic as resolved.
Last updated: Oct 05 2023 at 02:01 UTC