证明在Coq抽取中的作用

文章/答案/技术大牛

发布

2回答

haskell、coq、coq-extraction

我试图理解在Coq提取中证明的作用是什么。下面是取自here的下层整数除以2的例子。在我的第一次尝试中，我使用了Admitted关键字： (*********************)(*********************) Definition当我检查生成的Haskell文件时，我发现它确实丢失了： div_2_even_n

浏览 16提问于2019-04-26得票数 7

回答已采纳

2回答

Coq中普遍量化的方法

coq

我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Major的证明。这样的证明就是带有参数Minor的Minor函数的应用。那么，现在我想知道:在具有普遍量化

浏览 4提问于2014-05-06得票数 0

2回答

为什么展开在Coq中不适用于lt(小于)？

coq

我想要证明lt n m -> le n m，因为它不存在于Coq的标准库中。虽然在Coq.Init.Peano中，lt m n被定义为S m <= n，但我无法在假设中使用这种定义。为什么展开不起作用？似乎只有inversion可以工作。

浏览 0提问于2015-07-21得票数 1

1回答

如何设置Coq作为一阶逻辑的定理证明器

logic、computer-science、coq、coq-tactic、coq-plugin

据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在</e

浏览 21提问于2019-05-15得票数 3

回答已采纳

2回答

Coq:证明‘P -> ~P -> Q’而不是‘矛盾’策略？

coq、coq-tactic

我正在学习Coq，我发现它是有建设性的。这是我可以证明“矛盾意味着一切”的一种方法，它起作用： Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.注意，没有Q是构造的，所以我假设contradiction是内置到Coq验证引擎中的。在我看来，如果不是这样，我们就得证明Q是如何构造的，而且不可能有

浏览 4提问于2021-07-27得票数 1

回答已采纳

1回答

余弦中Prop，Set和Type_i的基数

coq、cardinality

我们可以将Coq中的分配给Prop、Set和每个Type_i吗？我只在Coq的库中看到了的定义，所以也许我们首先需要大基数的定义。根据证明无关的语义，例如暴露的，Set和Type_i形成一个递增的序列。这可以在Coq中得到证明吗？由于不可预测性，Prop看起来更复杂。但是，对于任何两个证明p

浏览 13提问于2018-08-28得票数 4

回答已采纳

1回答

利用lia策略证明可判定性

coq

我对Presburger算法有一个抽象的语法，还有一个确定给定公式的命题表示的不动点函数(您可以在这里看到它：)。我该怎么做？谢谢!

浏览 3提问于2020-09-17得票数 0

回答已采纳

1回答

利用余弦证明有限集的幂集是有限的

math、coq、formal-verification、powerset

在试图证明一些事情时，我遇到了一个看起来很无辜的声明，但我在Coq中未能证明。我们的主张是，对于给定的有限集合，powerset也是有限的。该语句在下面的Coq代码中给出。我查阅了关于有限集的Coq文档以及关于有限集和幂集的事实，但我找不到可以将powerset解构为子集并集的东西(这样就可以使用Union_i

浏览 28提问于2019-05-21得票数 5

1回答

Z3与coq的区别

z3、coq、theorem-proving

我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？

浏览 1提问于2012-07-18得票数 44

回答已采纳

1回答

在Coq中使用自反性

coq

我正在尝试()中的示例，这时我注意到要解决这个例子，请在链接中给出： andb b c = true → b = true我们正在销毁出现在c左边的b表示"andb“。我发现同样的方法没有帮助。“反身性”并没有帮助，我认为这是因为'b‘在子目标中的位置。最后，我以下列方式完成了该证明： Theorem andb_true_elim2

浏览 2提问于2016-05-13得票数 0

1回答

为什么我的本地coq不与标准coq相同，例如JsCoq？

visual-studio-code、coq、coq-tactic、jscoq

我正在看这个问题中的小例子，但是这个证明在我的本地计算机上不起作用，尽管它在jscoq上工作。这就是我证明的地方： forall n:nat, Proof. induction n.Qed. *) 在此之后，反身性应该可以作为证明的结论，但在我的例子中，它只会进入一种奇怪的状

浏览 10提问于2022-03-08得票数 2

3回答

我是新来的科克，我想证明一些很基本的东西引理eq_if_eq : forall a1 a2，(if beq_nat a1 a2，a2 beq_nat a1) = a1。我在下面发布的解决方案中苦苦挣扎，但我认为一定有更好的方法。理想情况下，我希望在beq_nat a1 a2上清晰地使用大小写，同时将大小写值放在假设列表中。是否有一种策略t使使用t (beq_nat a1 a2)产生两个子情况，一个在beq_nat a1 a2 =

浏览 3提问于2013-05-15得票数 5

回答已采纳

1回答

在COQ中使用函数扩展性的缺点是什么？

coq

在COQ中添加公理通常会使证明更容易，但也会带来一些副作用。例如，通过使用经典公理，一个人离开了直观的领域，证明不再是可计算的。我的问题是，使用功能扩展公理的缺点是什么？

浏览 1提问于2016-09-01得票数 6

回答已采纳

1回答

没有特定目标的交互式定理证明

coq

在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？

浏览 3提问于2018-03-30得票数 2

3回答

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

coq

我试图证明一个关于Prop的替换定理，但我失败得很痛苦。下面的定理能在coq中被证明吗?如果不能，为什么不能。重点是，在逻辑上，证明是通过归纳的。据我所知，Prop不是归纳定义的。如何在Coq中证明这样的定理？

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

1回答

如何证明Coq中的“类型<>集”(即类型不等于集合)？

coq、dependent-type、theorem-proving、type-theory

在Coq中，Type和Set之间是否存在等式或不等式关系？我一开始 Lemma set_is_type : Type = Set.discriminate的战术不起作用</em

浏览 0提问于2019-05-31得票数 3

回答已采纳

1回答

如何证明或伪造“`forall (P，q:支柱)，(P -> Q) -> (Q -> P) -> P=q.”？

equality、coq、proof、dependent-type、curry-howard

我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？没有上面的命题，我就无

浏览 0提问于2014-10-26得票数 8

回答已采纳

1回答

理解在显示证明上的COQ证明。

coq、proof

我在COQ中是新的，我试图证明反例定理。Hypothesis R2: ~B. 所以我们试着：tauto. (fun H : ~ A => let H0 : B

浏览 1提问于2018-08-23得票数 5

回答已采纳

2回答

Coq核的证明技术

coq

伊莎贝尔将其核心证明能力建立在与高阶统一相结合的分辨率上。命题作为类型可能会占用过多的空间；什么将取代Huet的高阶逻辑统一程序？。

浏览 3提问于2020-08-12得票数 1

回答已采纳

1回答

Coq计算式双连通链

coq、proof

我正试图证明Coq中的一个二分派：我写下了一个有这种结构的证据：<-> <-><->thus: P <-> Q 如何在Coq中模拟这个计算证明结构？

浏览 2提问于2015-11-20得票数 2

回答已采纳

点击加载更多