2回答
有没有办法一步一步地简化呢？假设您有f1 (f2 x)，这两个都可以通过单个simpl依次简化，是否可以将f2 x简化为第一步，检查中间结果，然后简化f1Theorem pred_length : forall nQed.Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --&g
浏览 0提问于2016-09-07得票数 11
回答已采纳
1回答
我从命令行对这个简单的输入文件调用Coq：Theorem plus_O_n : (forall n, O + n = n).当我看到0输出时，我知道一切正常，所以我尝试通过执行以下操作来检查Coq的输出：但是我得到了一些二进制的胡言乱语。我做错了什么？谢谢!
浏览 11提问于2018-08-09得票数 0
回答已采纳
1回答
我正在尝试()中的示例，这时我注意到要解决这个例子，请在链接中给出： andb b c = true → b = true然而，做下面的练习，在书中，即 andb b c = true → c = true.“反身性”并没有帮助，我认为这是因为'b‘在子目标中的位置。
浏览 2提问于2016-05-13得票数 0
所以在学习Coq的时候，我做了一个简单的例子:纸，剪刀，石头。我定义了一个数据类型。Definition compose {A B C} (g : B -> C) (f : A -> B) : (A -> C) :=Instance MSPR :
浏览 0提问于2014-06-26得票数 0
我的一般问题是:当我不熟悉我正在使用的类型时，有没有一种简单的方法来逐步在Coq中建立定义？考虑来自Coq.Narith.BinNat的Coq中的自然数的一个定义 Definition discr n : { p:positive | n = pos p } + { n = 0 }.我第一次尝试失败了： Require Import Coq.Narith.BinNat.
浏览 18提问于2020-07-02得票数 0
回答已采纳
1回答
我对Coq非常陌生，现在我只能用一个简单的定理来理解Coq的“理由”： andb b c = true ->
浏览 0提问于2018-04-30得票数 1
回答已采纳
1回答
我是Coq的初学者，我被Coq的一个问题困住了，我无法进一步简化这个问题。如果任何人有任何关于如何将问题分解为较小步骤的提示，那就太好了。
浏览 6提问于2021-10-28得票数 2
1回答
如果有人能很好地解释在以下简单情况下如何使用验证函数，这将有助于我理解“程序/校对”的并行性：ex1 = fun (n : nat) (H : 7 * 5 < n) => H在验证过程中是否执行了验证函数
浏览 1提问于2020-05-22得票数 1
回答已采纳
但问题是，我想要第一种工作方式，因为我有很多程序都是用这种方式编写的，而且似乎不符合逻辑地更改每个程序中的行。这是我的.emacs文件中的内容-(我想我可能需要添加类似于mathcomp/ssreflect的路径。'(coq-prog-name "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop")
'(package-selected-packages (quote
浏览 15提问于2020-03-11得票数 0
回答已采纳
如果我在simpl之后使用intro x，什么都不会改变。Coq不尝试用抽象值x求固定函数。但是，如果我对x进行归纳分析，Coq将自动计算方程的左边，并将其简化为0和S x。为什么Coq禁止我用抽象值x计算修复函数？
浏览 1提问于2015-07-24得票数 3
回答已采纳
1回答
问题是，如果我在公式中全面展开定义，简化将永远持续。相反，我想首先展开A * B，应用一些策略将其简化为普通形式的X，然后对X * C进行同样的处理等等。
知道我该怎么做吗？
浏览 4提问于2017-09-13得票数 5
回答已采纳
在证明中，我希望将(negb (negb true))简化为true (与false类似)。我知道Coq的negb_involutive过程，但由于我的教科书没有介绍它，我认为我应该设法只使用rewrite或apply来模仿它的功能。
浏览 1提问于2016-11-15得票数 2
在ocamltop中(加载我的文件之后)，我可以运行以下命令#directory "/afs/csail.mit.edu;;但是我不能跟踪未导出的函数，所以我想使用ocamldebug逐步执行函数。所以在ocamldebug
浏览 0提问于2013-09-27得票数 0
2回答
相同的Linux命令在一个环境中成功，而在另一个环境中失败：我正在遭受的失败是Debian拉伸和Coq v8.5LinuxOCaml 4.01.0Welcome to Coq 8.4pl4 (July 2014)因此，我正试图弄清楚到底是怎么回事，希望从那里得到一个答案，但没有结果。为了解决这个问题，我将源代码
浏览 3提问于2016-12-04得票数 2
回答已采纳
在中，有一个关于“隐式参数”的部分。在本节中，有一行：Error: No focused proof (No proof-editing in progress我已经将Poly.v文件简化为以下内容，这仍然会导致相同的错误： |
浏览 5提问于2013-11-18得票数 2
回答已采纳
我在Coq中定义了一个模块签名，它定义了几个符号。然而，当我试图在签名之外使用这些符号时，Coq失败了。下面给出了我的代码的简化版本。任何帮助都将不胜感激。
浏览 2提问于2013-03-31得票数 2
回答已采纳
1回答
关于排列的表示
、、、、
我希望有一个归纳类型来描述排列及其在一些容器上的操作。很明显，根据这种类型的描述，算法的定义复杂度(根据其长度)(计算合成或逆，分解为不相交的循环等)。会有所不同。或者，我们可以将置换表示为具有属性的有限映射。我找到的所有作品都处理命令式设置中的计算复杂性，而我对“推理复杂性”和函数式编程感兴趣。
浏览 1提问于2013-07-02得票数 26
回答已采纳
下面是一个更大的证明的简化片段，它捕获了有问题的行为。 Parameter t : Type.
Parameter x : t.当您用rewrite prop替换rewrite prop2时，coq失败并出现隐含错误。然而，在我的观点中，coq应该在重写步骤之后产生forall e : t, True。有人能帮我吗？
浏览 0提问于2011-11-17得票数 3
在下面的例子中，我可以使用哪些策略来执行rational表达式的简化并证明微不足道的rational等价性？
Require Import Coq.QArith.QArith.
浏览 2提问于2015-09-23得票数 0
回答已采纳
我读到，来自Ltac的策略集Ltac足以证明最小构造命题逻辑中的任何重言式。这意味着Ltac或另一种元语言可以反思这些策略的真正作用，并将它们作为变量加以操纵。
浏览 1提问于2017-02-11得票数 3
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
腾讯会议
云直播
对象存储活动推荐
腾讯云开发者
