2回答
假设我有一个花哨的策略来解决特定类型的引理： some_preparation;Lemma fancy3 := …. Proof. … Qed.现在，我可以简单地重新定义Ltac solveFancy ::= …并将important_step3添加到列表中，但这很快就过时了。
浏览 21提问于2018-02-19得票数 7
回答已采纳
我想知道simpl策略在COQ中是如何工作的。Parameter n:nat. S (n + 0) = S (n + 0)
我的理解是，simpl执行一系列cbv beta, delta, iota转换。我试过了，但没能得到和simpl一样的结果。基本问题是，在cbv delta扩展之后，plus术语保持扩展。如何解扩
浏览 8提问于2016-01-24得票数 5
直观地说，当两个函数g和h对于所有x都相等时，我们可以想象g = h，因此将所有出现的f g替换为f h。这就是我们所说的函数延伸性。但是，在Coq中，默认情况下没有添加函数的可扩展性，所以我们需要它，我们需要添加一个公理。然而，我想避免使用这个公理，并试图找到一个在实践中等价的定理，它看起来像“对于所有输出归纳类型的归纳函数，对于所有g和h，f g=f h”。具体地说，f不能是单位类型，因为单位函数不是归纳类型。现在，当我需要做这样
浏览 1提问于2017-11-27得票数 1
1回答
据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明助手中使用机器学习或其他启发
浏览 21提问于2019-05-15得票数 3
回答已采纳
我见过很多Coq战术，它们在功能上是相互重叠的。我的问题是：
是否有一个最小的基本策略集(不包括auto等)是完全的，在某种意义上，这个集合可以用来证明关于自然数函数的任何Coq-可证明定理？在这个最小的
浏览 1提问于2015-09-20得票数 8
回答已采纳
是否有可能以及如何在前向链接模式中将Coq用作计算器或规则引擎？Coq脚本通常需要声明可以找到证据的目标。但是，是否有可能在其他方向上进行，例如，计算由某些规则限定的一些结果的集合，例如，通过一些步骤。我对全一阶逻辑的序列演算特别感兴趣。我猜(但我不知道)有一些一阶逻辑的序列演算的实现或包，但它是用于定理证明的。我喜欢用这样的顺序演算来推导出一些有指导的顺序的结果。在Coq
浏览 1提问于2019-09-08得票数 0
Coq是一个证明助手，而Agda/Idris是编程语言(尽管它们可以被称为证明助手)。
我正在探索这些语言，我想知道Agda/Idris是否足以做Coq所能做的一切。那么，有没有一些证据/管理代码/IDE (Emacs)函数的方法/其他Coq可以做而Agda/Idris不能做的事情呢？
浏览 21提问于2017-12-16得票数 9
回答已采纳
1回答
我想在coq中制定一个Ltac策略，它可以接受1个或3个参数。我在模块中读过关于ltac_No_arg的文章，但如果我理解正确的话，我将不得不用以下命令调用我的策略：Coq < mytactic arg_1.
Coq < mytactic arg_1 arg_
浏览 8提问于2017-06-30得票数 6
回答已采纳
我试图将(1,2,3)定义为coq中的一组元素。我可以使用list将其定义为(1 :：(2 :：(3 :：nil)。有没有办法在coq中定义set而不使用list。
浏览 1提问于2016-04-13得票数 6
Coq 8.7集成了流行的Ssreflect库。因此，可以通过以下方式导入它的库：
From Coq Require Import ssreflect ssrfun ssrbool.但是，当我尝试导入时，它会报告它是Unable to locate library ssrnat with prefix Coq，并且我在磁盘上的Coq发行版中也找不到ssrnat。是否出于某种原因，ssrnat故意不包含在另一个模块中，或者是我的
浏览 14提问于2017-12-16得票数 2
回答已采纳
在COQ中添加公理通常会使证明更容易，但也会带来一些副作用。例如，通过使用经典公理，一个人离开了直观的领域，证明不再是可计算的。我的问题是，使用功能扩展公理的缺点是什么？
浏览 1提问于2016-09-01得票数 6
回答已采纳
1回答
我们有一个函数将元素插入到列表的特定索引中。上述函数的以下属性与该问题相关(在l上证明省略、直接的归纳而n没有固定)： n <我们有一个排列的计算定义，iota k是nats [0...k]的列表。我们试图证明的定理： length l =
浏览 3提问于2017-05-08得票数 6
回答已采纳
在研究其他作者的Coq证明时，我经常遇到一种策略，比如"inv eq Heq“或"intro_b”。我想了解这样的策略。我使用了SearchAbout，搜索，查找和打印，但找不到上述问题的答案。
浏览 1提问于2012-11-29得票数 6
我希望COQ在执行证明时记录其所有子目标。COQC的-verbose选项没有给出正确的结果。
其次，有没有一个选项可以让COQ记录自动、直觉等策略所使用的所有基本策略？
浏览 1提问于2015-11-10得票数 1
2回答
Coq的解析器是如何实现的，我对此感到非常惊讶。例如：
对于这种解析器在理论上是如何可行的，有什么建议吗？它应该如何工作？任何材料或知识都是有用的。我只是试着了解这类解析器的一般情况。谢谢。请不要让我自己读Coq的
浏览 2提问于2017-04-03得票数 10
回答已采纳
1回答
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
在coq中，策略有一个变体，它接受一种“连接分离引入模式”，允许用户为引入的变量指定名称，即使在解压复杂的归纳类型时也是如此。我希望我的自定义策略允许(或要求，无论哪个更容易)用户提供一个介绍模式，我的策略</e
浏览 3提问于2015-05-09得票数 8
回答已采纳
有时我发现coq进入了一种状态，当我应用一种策略时，新的目标和假设不会自动打印出来。如何将其设置为在每次策略调用后打印出来。
这是coq 8.7.2，使用coqtop
浏览 0提问于2018-11-13得票数 1
3回答
我正在使用Coq Proof Assistant实现一个(小型)编程语言的模型(扩展Bruno De Fraine，Erik Ernst，Mario Südholt的Featherweight Java在使用induction策略时，不断出现的一件事是如何保留类型构造函数中包装的信息。其中extends是在Java中看到的类扩展机制，而typ表示两种不同的可用类型。更糟糕的是，由于
浏览 2提问于2010-12-23得票数 16
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
