当使用rewrite策略时，Coq无法找到子项
我正在尝试修改Certified Programming with Dependent Types第一章中栈机器章节的compile_correct证明。在我的版本中，我试图利用progDenote是一个fold的事实，并在主引理的证明中使用更弱的归纳假设来证明compile_correct。...
Coqide出错：编译的库Basics.vo在库之间有不一致的假设。
我正在使用mac os X上的CoqIDE_8.4pl5。当CoqIDE转到此命令时，会弹出以下错误消息：Require Import Basics。 错误：编译的库Basics.vo对库Coq.Init.Notations做出了不一致的假设。 在我旧的Macbook Air上使用CoqI...
重写策略无法在模式匹配中找到项出现
在 Coq 中，我在以下情况下使用 rewrite 策略时遇到了问题： Section Test. Hypothesis s t : nat -> nat. Hypothesis s_ext_eq_t : forall (x : nat), s x = t x. De...
Coq：管理带有子目录的项目中的LoadPath
我有一个Coq项目，它的库被组织成子目录，类似于： …/MyProj/Auxiliary/Aux.v …/MyProj/Main/Main.v (imports Auxiliary/Aux.v) 当我编译文件时，我希望从工作目录MyProj（通过makefile）进行。但我也想使用Pr...
将Coq转换为Idris
如何将Coq源代码转换为Idris代码，有哪些有用的指导方针（例如它们的类型系统有多相似，如何翻译证明等）？据我所知，Idris的内置策略库很少但可扩展，因此我想这应该是可能的，只需进行一些额外的工作。
使用Coq能否编写C程序？
我知道可以将Coq程序提取成Haskell和OCaml程序。是否有办法用C语言做到这一点？ 我想象中有一个模拟C语言的库，该库可能包含有关C构造如何与进程内存交互的公理集，以及有关IEEE浮点数的公理和定理。然后它将能够在Coq中构建与程序有关的定理的C程序。 我会使用这样的库来构建一个对...
如何在Coq中表达“存在唯一的X”？
我想知道在Coq中是否有一种简洁的方法来表达存在唯一的某个东西（即写唯一存在量词）？ 例如，要说存在一个x使得2 + x = 4： Goal exists x, 2 + x = 4. 如何表达存在一个具有相同属性的x的唯一性？ 我知道可以像这样在s.t.部分复制谓词： Goal e...
我如何在Coq中证明命题等同性扩展性？
我正在尝试证明有关Prop的替换定理，但我失败了。以下定理是否可以在coq中证明，如果不能，为什么不能。 Theorem prop_subst: forall (f : Prop -> Prop) (P Q : Prop), (P <-> Q) -...
利用由良好定义归纳所定义的递归函数进行计算
当我在Coq中使用Function定义一个非结构递归函数时，当要求进行特定计算时，生成的对象表现得很奇怪。事实上，Eval compute in ...指令不直接给出结果，而是返回一个相当长的表达式（通常为170,000行）。看来Coq不能对所有内容进行求值，因此返回一个简化的（但很长）表达式...