如何使用在给定库中验证的结果？例如,我想Lemma peano_ind从库中使用BinInt.我用CoqIDE写这个:
Require Import BinInt.
Check peano_ind.
并获得"在当前环境中找不到参考peano_ind".错误.我也无法apply在证明期间使用它.
但是,它应该在那里,因为Locate Library BinInt.我看到Coq可以找到文件BinInt.vo,当我打开文件BinInt.v时我可以看到Lemma peano_ind.
我在Debian 9.0 + CoqIDE 8.5pl2和Windows 10 + CoqIDE 8.6上都有这个问题.
所有这一切都是因为我想对整数进行归纳.对此的不同解决方案也很不错,但我仍然因为缺乏使用以前经过验证的结果的能力而感到沮丧.
假设我已经定义了floor(fromR到Z)。现在我想证明这n <= x意味着n <= floor(x)，哪里n : Z，x : R。
我试过：
Lemma l: forall (n:Z) (x:R), (IZR n) <= x -> n <= (floor x).
但我收到错误The term n has type Z while it is expected to have type R.
我该怎么写这个？有没有一种方法可以同时<=使用？ZR
coq ×2