为什么Coq在归纳中重命名变量？

文章/答案/技术大牛

发布

1回答

rename、coq

在generalize dependent l1.之后的第3行中，我有以下上下文： l2, l3 : list nat H23 : subseq l2 l3 但是在第5行，在重命名之前，我有 l1, l2为什么会这样呢？我如何才能防止这种情况发生？我的Coq版本： The Coq Proof Assistant, version 8.8.2 (January 2019)

浏览 18提问于2019-02-27得票数 1

回答已采纳

1回答

为什么我可以用构造方法来证明自反性呢？

coq、coq-tactic

构造器策略允许您通过自动应用构造函数来完成一个目标，即归纳数据类型。然而，在Coq中，定义等式并不是一个归纳积。那为什么Coq会接受这个证据呢？

浏览 1提问于2021-01-29得票数 1

回答已采纳

3回答

如何在Coq中证明命题的可扩充性？

coq

下面的定理能在coq中被证明吗?如果不能，为什么不能。重点是，在逻辑上，证明是通过归纳的。据我所知，Prop不是归纳定义的。如何在Coq中证明这样的定理？

浏览 2提问于2012-06-17得票数 7

1回答

归纳命题的一致性

logic、coq

在coq中，定义归纳命题似乎类似于在逻辑中添加新的推理规则/公理。在定义归纳命题时，有哪些约束可以保证coq保持一致？

浏览 0提问于2018-03-24得票数 2

回答已采纳

3回答

如何在Coq中对列表的长度进行归纳？

coq、induction

在纸上推理的时候，我经常用归纳的方式对某些列表的长度进行论证。我想用Coq将这些参数正规化，但似乎没有任何方法可以对列表的长度进行归纳。更具体地说，我试图证明。在理论上，我通过对w长度的归纳法证明了这一点。我的目标是在Coq中把这个证明正式化。

浏览 7提问于2017-08-25得票数 7

回答已采纳

1回答

在一般的构造演算中，构造函数是不相交的和内射的吗？

functional-programming、coq、dependent-type

，它看起来像Coq中使用的归纳构造的演算，对于归纳类型有不相交的内射构造函数。。

浏览 3提问于2017-05-03得票数 3

回答已采纳

1回答

在具有非均匀类型参数的数据类型上进行归纳会产生错误类型的术语。

coq、theorem-proving

我正致力于在Coq中正式化，但是对于具有非均匀类型参数的归纳数据类型，我很难通过归纳法来证明。这里的关键是第二个数据构造函数中的存在类型变量b。不能构造抽象在类型变量上的谓词，因为从语句中提取的反向函数应用程序会变成错误类型。请参阅GitHub：上的完整示例更新：继中的讨论之后，我尝试通过<

浏览 0提问于2019-07-08得票数 5

回答已采纳

1回答

elim是如何在/\和\/的Coq中工作的？

coq、coq-tactic

在的1.3.1和1.3.2节中，有两个elim应用程序:第一个： B : Prop H : A /\ B B /\ ACoq < elim H. B : PropCoq < elim H.

浏览 7提问于2017-09-24得票数 3

回答已采纳

1回答

据我所知，Coq策略是在幕后编译成一些函数式程序的，但我真的不确定这是怎么回事。我非常确定这不是我想要做的。我想要做的是类似下面的Idris程序。在Coq中，两个证明卡在一个lambda中，我不确定这是怎么发生的。我看到Coq的induction策略并没有做我认为它应该做的事情。除了上面的解释之外，让我问一下，有没有比软件基础更多的Coq入门材料，以防我在某些策略上再次陷入这样的困境？请注意，我知道如何在Coq<e

浏览 15提问于2019-04-09得票数 1

回答已采纳

2回答

Coq需要什么才能为归纳类型生成淘汰组合器？

coq

Coq的Finite_sets库具有归纳类型，指定某些集合是有限的：| Empty_is_finite : Finite我试图证明有限集合中的成员是可决定的，如下所示： forall x:A,但是，Coq会生成以下错误消息： Cannot find the elimination combinator

浏览 0提问于2016-09-29得票数 3

1回答

Coq中术语的符号处理

coq

在我的Coq研究中经常会出现这样的证明状态：n : nat______________________________________(1/1)Coq抱怨说它不能把n和S n统一起来，S n和S (S n)不能统一。在纸和笔中，很容易在目标中引入象征性的操作，比如t = S n，甚至n = S n，那么

浏览 2提问于2022-04-27得票数 1

1回答

Coq的基础

coq

我假设Coq会在某一时刻转向LCF方法。在过去，我对感到好奇。我在一篇总结了现有文献的硕士论文中找到了对Isabelle/Pure的一些很好的描述。我想知道是否有关于Coq内核的描述，涵盖了它的逻辑和实现方面。

浏览 0提问于2020-03-06得票数 0

1回答

是否在任何同进式上都可以判定是否相等？

coq、decidable、coinduction

我怀疑，在Coq中，像Stream这样的协归纳类型没有可判定的相等性。也就是说，给定两个流s和t，不可能识别s=t还是~(s=t)。我怀疑Coq中的所有共归纳类型都是如此。

浏览 2提问于2015-06-18得票数 5

回答已采纳

2回答

什么是归纳谓词？

predicate、coq、induction

你如何解释归纳谓词？它们是用来干什么的？他们背后的理论是什么？它们只存在于依赖型系统中，还是在其他系统中？它们在某种程度上与GADT有关吗？在Coq中，为什么默认情况下它们是真的？这是Coq的一个例子：| even0 : even 0 | evens : forall p:nat, even p -> even (

浏览 7提问于2014-04-11得票数 5

回答已采纳

4回答

对带有产品类型参数的谓词的归纳

coq、induction、coq-tactic

然后我就可以用归纳来证明一些虚拟的引理： foo n n' -> n = n'. intros.对于几乎相同的引理，一个类似的证明被卡住了，因为所有关于变量的假设都消失了： bar (n, m) (n', m') -> ninduction H.为什么会发生这种情况？如果我将indu

浏览 4提问于2016-01-19得票数 2

回答已采纳

1回答

由自己类型的项索引的依赖类型

types、coq、dependent-type

我试图用依赖类型理论做些什么，以及如何用Coq实现它呢？

浏览 0提问于2018-08-09得票数 2

1回答

为什么删除假设会改变上岗策略的行为？

coq、coq-tactic

下面是工作的代码：Lemma clos_refl_trans_1n_right: forall {A: Type} {R: relation A} (x y: A),在</e

浏览 0提问于2020-02-13得票数 0

回答已采纳

1回答

我怎么写那些表现得像“毁灭.一样”的战术？

coq、ltac

在coq中，策略有一个变体，它接受一种“连接分离引入模式”，允许用户为引入的变量指定名称，即使在解压复杂的归纳类型时也是如此。我希望我的自定义策略允许(或要求，无论哪个更容易)用户提供一个介绍模式，我的策略可以交给destruct。

浏览 3提问于2015-05-09得票数 8

回答已采纳

1回答

为什么不能用Coq中的抽象值来计算固定定义的表达式？

coq

如果我在simpl之后使用intro x，什么都不会改变。Coq不尝试用抽象值x求固定函数。但是，如果我对x进行归纳分析，Coq将自动计算方程的左边，并将其简化为0和S x。为什么Coq禁止我用抽象值x计算修复函数？

浏览 1提问于2015-07-24得票数 3

回答已采纳

2回答

Coq中其他基例的归纳

coq、proof、coq-tactic

我在试图证明Coq中的鸽子洞问题。我认为可以用归纳来完成，就像在中一样。但是我想要基本的情况n=2。在Coq中是否有可能得到这样的结果，还是我走错了轨道？

浏览 0提问于2020-11-20得票数 0

回答已采纳

点击加载更多