Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
如何证明由coq中相同归纳的两个不同构造函数产生的项的不等式？
考虑一下我有一个归纳式：归纳DirectSum {L R：类型}：类型：= |左：L-> DirectSum L R |右：R-> DirectSum L R。我如何证明forall L R：类型，forall l：L，forall r：...
（（A-> B）/ \（B-> C）->（A-> C）in Coq？
[我正在通过本书的软件基础来学习Coq，并且难以证明以下引理（我需要证明其他定理。）引理if_trans：forall（PQR：Prop），（P-> Q）/ ...] >
我不确定如何措辞我的问题，因为我不熟悉coq。我想对包含双向蕴涵的一个定理使用优化。示例代码：参数A B C：Prop。theorem t1：A-> B-> C ....
我目前在Software Foundations – Logical Foundation。简而言之，我得到了错误错误：找不到与后缀<>和前缀LF匹配的逻辑路径的物理路径。我有Coq ...
我正在使用索引功能在列表nat中任何位置查找element的值。请Plz指导我证明引理的第二部分，如下所示。Fixpoint index（n：nat）（m：...
我正在尝试在coq中编译文件hw5.v，该文件位于软件基础的plf文件夹中。我想解决绑定问题，因此我使用了以下命令：coqc -Q.PLF hw5.v但它不能编译...
[很抱歉问一个简单的问题，但我一直在寻找答案，而且我还没有找到对我来说足够简单的解释（我不太了解Coq的模块系统）。 。
对于一个项目，我正在通过Coq编码组理论，显然已经给出了3个元素的关联性，但是我努力证明它对于长度为n的字符串成立。也就是说，（x1 * ... * xn）是...
我想证明Coq中两个nat数相等：a，b：nat Heq：一些a =一些b ======================= ==== a = b
假设我们有一个具有等价关系（===）的类型A：A-> A->对它的支持。最重要的是，有一个函数f：A->选项A。碰巧这个函数f是“几乎” ...
我试图证明自反-传递闭合的各种定义是等效的。这是有效的代码：需要导入Coq.Relations.Relation_Definitions。需要导入费用...
我已经在coq中创建了BST树，然后创建了有关BST正确性的定义。现在，我必须证明在正确的BST中插入会创建正确的BST，但是我无法关闭此......>
在Ltac中，上下文模式可用于构建Ltac级函数，该函数接受Gallina项并通过填充孔来构建Gallina项。我想验证此功能并使用它...
归纳ty0：类型：= |布尔：ty0 |整数：ty0 | Dyn：ty0 |箭头0：ty0-> ty0-> ty0。归纳ty1：类型：= | ty：ty0-> ty1 |间隔：ty1-> ty1-> ty1。归纳ty2：类型：= ...
我正在尝试在Coq中使用飞弹。我发现la库完全可以满足我的需求，但是对于Coq来说，它是一个新手，我想不出一种方法来证明有意义的属性。该库是SQIRE，并且它是...
我不能将Ssreflect的重写与setoids一起使用。尽管我认为此信息与解决问题无关，但我在Coq中使用了类别理论的表述：https：//github.com / ...