Use results proven in a library (Coq)

Question

How do I use results proven in a given library? For example, I want to use Lemma peano_ind from the library BinInt. I write this in CoqIDE:

Require Import BinInt.
Check peano_ind.

and get a "The reference peano_ind was not found in the current environment." error. I am also not able to use it with apply during a proof.

However, it should be there, because with a Locate Library BinInt. I see that Coq can find the file BinInt.vo, and when I open the file BinInt.v I can see Lemma peano_ind.

I have this exact problem both on a Debian 9.0 + CoqIDE 8.5pl2 and on a Windows 10 + CoqIDE 8.6.

---

All of this because I wanted to do induction over the integers. A different solution for that would also be nice, but I'm still frustrated by my lack of ability to use some previously proven results.

Answer 1

The BinInt library has one of several peano_ind definitions in different submodules for different types. You can find these using Locate peano_ind:

Constant Coq.NArith.BinNat.N.peano_ind
  (shorter name to refer to it in current context is BinNat.N.peano_ind)
Constant Coq.PArith.BinPos.Pos.peano_ind
  (shorter name to refer to it in current context is Pos.peano_ind)
Constant Coq.ZArith.BinInt.Z.peano_ind
  (shorter name to refer to it in current context is Z.peano_ind)

Then you can use these qualified names, for example:

Check Z.peano_ind.
Z.peano_ind
     : forall P : Z -> Prop,
       P 0%Z ->
       (forall x : Z, P x -> P (Z.succ x)) ->
       (forall x : Z, P x -> P (Z.pred x)) -> forall z : Z, P z

You can also Import Z to allow to use the unqualified name peano_ind.