All geek questions in one place

Use library verified results (Coq)

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

 Require Import BinInt. Check peano_ind.

and get "Peano_ind link not found in current environment". I also cannot use it with apply during the proof.

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

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

All this, because I wanted to do induction on integers. Another solution for this would be nice, but I'm still disappointed with the inability to use some previously proven results.

+5
source share
1 answer

The BinInt library has one of several peano_ind definitions in different submodules for different types. They can be found 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 allow the unqualified name peano_ind to be used.

+5
source

Source: https://habr.com/ru/post/1268034/

More articles:


All Articles