我想证明一些关于自然数不包括0的东西。因此，我对属性P的基本情况是P1而不是P0。 我正在考虑在goal中使用n >= 0作为假设，但是在Coq中有其他方法可以做到这一点吗？
浏览 19提问于2019-04-30得票数 0
回答已采纳
自然数上的“强”(或“完全”)归纳法意味着，当证明n上的归纳步骤时，你可以假定这个性质对任何k都成立。> P n) ->
forall n : nat, P n.我设法证明了这个定理，没有太多困难。现在我想在一种新的策略中使用它，strong_induction，它应该类似于自然数上的</e
浏览 4提问于2014-01-02得票数 8
回答已采纳
2回答
我一直在学习Coq的策略，并通过修改自然数的基本事实来熟悉这个系统。
我一直在试图避免使用那些已经在图书馆中得到证明的定理，并对像乘法的相联性之类的东西进行批驳。然而，在一些情况下，我遇到了阻碍，我有一个n，m的性质:我想证明的是nat，但是当我试图同时对n
浏览 0提问于2018-11-16得票数 1
回答已采纳
我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，c
浏览 0提问于2014-10-26得票数 8
回答已采纳
1回答
为了理解一般的递归Function定义是如何工作的，以及它们如何符合Coq的结构递归约束，我尝试在Peano自然数上重新实现它。P n) : P n.我在nats上使用了一些没有粘贴在这里的自定义词条。它是有效的，我设法用它定义了欧几里得除法div a b，
浏览 7提问于2018-08-14得票数 3
回答已采纳
我有两个Fibonacci实现，如下所示，我想证明它们在功能上是等价的。<definition> ::= <keyword>
浏览 2提问于2016-11-13得票数 2
回答已采纳
3回答
我有一个自然数的列表，列表中的元素是降序的。我想写一个关于列表的引理，第一个元素h大于列表的所有元素。list是h;h1;t。0 h1？请指导我，如何写h大于列表尾部的所有元素。
浏览 3提问于2020-04-07得票数 1
1回答
我正在寻找OCaml中的用法示例，以演示简单的性质或定理。例如，给定二叉树的ocaml定义，可以证明节点的最大数目是2^(h+1)-1。
我为二叉树和图建立了这样的例子，但没有别的。
浏览 4提问于2012-10-17得票数 4
1回答
我在Coq中做了一个练习，试图证明如果一个列表等于它的相反，它是一个回文。下面是我如何定义回文的方法： | emptypal : pal []
| singlpal : forall根据我的定义，我需要进行归纳，提取前和尾元素，但是coq显然不允许我</
浏览 4提问于2017-03-25得票数 2
回答已采纳
5回答
认证计划的定义
、、、
在第5节中，有一个用于验证编译器的不同策略的列表，在某种意义上，它概述了创建经过认证的程序的不同策略。回到我最初的问题，什么是认证计划的定义，对我来说仍然有点不清楚。Wjedynak在某种程度上提供了一个答案，但实际上Leroy的工作涉及在Coq中创建编译器，然后在某种意义<
浏览 59提问于2014-01-24得票数 18
4回答
如果我有这样的谓词： | Foo : forall n, foo n n.然后我就可以用归纳来证明一些虚拟的引理： foo n n' -> n = n'. intros.对于几乎相同的引理，一个类似的证
浏览 4提问于2016-01-19得票数 2
回答已采纳
其中一个暗示了另一个。 ev n -> even n.induction E as [ | n' E' ].====================================================================== (1/1)但实际上我得到的</
浏览 4提问于2014-06-28得票数 4
回答已采纳
2回答
我正在学习命题逻辑和推理规则。析取三段论规则指出，如果我们有前提(P或Q)，也有(而不是P)，那么我们就可以达到Q。H : A \/ B______________________________________(1/1)H1 : B.另外，如果有人能和我分享
浏览 0提问于2018-10-20得票数 4
回答已采纳
3回答
证明助理的经证明的计算
、、、、
手工或由计算机代数系统进行的符号计算可能是错误的，或者只能在某些假设的前提下进行。一个经典的例子是sqrt(x^2) == x，它一般不是真的，但如果x是实的和非负的，它就成立了。是否有像Coq、Isabelle、HOL、Metamath等证明助手/检查人员被用来证明符号计算的正确性的例子？我特别感兴趣的是微积分和线性
浏览 2提问于2021-11-15得票数 2
回答已采纳
1回答
还有一个(递归)函数substitute，它将一个路径中的变量替换为另一个路径。有两个属性path-equivalence和instance-of (归纳地)是通过全量化断言定义的。下面是有关自然数的一个更具体的示例：
类是Zero、Succ和Nat，我们有一个变量a和一个字段p。我们向求解器提出的问题是:是否可能a是Succ，a.p</
浏览 8提问于2021-07-14得票数 0
2回答
我已经开始学习Coq，并试图证明一些看起来相当简单的东西:如果一个列表包含x，那么该列表中x的实例数将> 0。我将包含函数和计数函数定义如下： match l with match l with | h :: t => if beq
浏览 6提问于2017-04-17得票数 0
回答已采纳
4回答
我只是一个Coq的初学者，我一直试图证明一些关于自然数的基本定理。我已经做了一些，不是很优雅，但是完成得更少。然而，我完全坚持要完成这个定理：Proof.2 subgoalsH : A > 0
_
浏览 4提问于2016-02-18得票数 4
回答已采纳
1回答
在简单类型的lambda演算中，类型导子是唯一的证明在纸上是微不足道的。我熟悉的证据，通过完整的归纳，键入派生。但是，我很难证明类型派生(通过类型派生表示)是独一无二的。当证明类型派生项是唯一的时，我很难公开J类型项的结构。例如，我可以在下面的引理中在d1或d2上导入，但不能
浏览 3提问于2012-09-05得票数 2
回答已采纳
产率与产率
def nats(n): yield from nats(n+1)
n = next(s)next(p)在函数nats中，每次调用next()时，它都从n开始生成无限数，并生成n。series = nats(1)
next(series)
浏览 6提问于2020-11-11得票数 4
3回答
模上的协q归纳
、、
我是新来的coq，我真的很难运用归纳。只要我能使用图书馆的定理，或者像欧米茄这样的策略，所有这些都是“没有问题”。但一旦这些不起作用，我就被困住了。准确地说，现在我试图证明
Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m.情况
浏览 5提问于2015-03-21得票数 5
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
