我在Linux(Ubuntu 17.04)中成功安装了Coq 8.6和CoqIDE.但是,我不知道为了将SSReflect和MathComp添加到此安装中而继续.我检查过的所有参考资料似乎都让我很困惑.有没有人有一个直接和简单的食谱？我确实安装了opam.
如何在Coq中证明以下陈述？
forall x: nat,
x >= 1 -> 2 * 2 ^ (x - 1) = 2 ^ x.
我pow_add_r在模块中找到了引理,NZPow但由于某种原因我无法使用它.
谢谢,马库斯.
当我运行以下脚本时:
Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.
我得到"错误:这个条款是多余的." 知道为什么会这样吗？
谢谢,马库斯.
我在Ubuntu 17.04中全新安装了Coq 8.6.当我尝试使用make编译我的项目时,它工作正常,直到我收到第一条错误消息.然后,我尝试使用CoqIDE来定位并更正错误,但是我收到了新的错误消息,例如:
"文件foo.vo包含库Top.foo而不是库foo"
我的猜测是CoqIDE的配置出了问题,但我不知道那可能是什么.任何提示？
提前谢谢,马库斯.
有人知道以下定理的Coq的任何标准库中的证明吗？如果有的话,我找不到它.
forall abc:nat,b> = c - > a + b - c = a +(b - c)
提前谢谢,马库斯.