Coq:为什么重写定理中的引理会产生两个子目标？
Coq是一个交互式定理证明工具，用于形式化验证和证明数学定理。在Coq中，重写定理是一种用于改写表达式的规则，它允许我们在证明过程中使用等价关系来简化表达式。
当我们在Coq中使用重写定理时，如果引理（或等式）被应用到目标上，它会产生两个子目标。这是因为重写定理的应用通常会将目标中的某个子表达式替换为另一个等价的表达式，从而产生两个新的子目标。
具体来说，假设我们有一个重写定理或等式：A = B，我们想要将目标中的某个子表达式C替换为A。当我们应用重写定理时，Coq会将目标分解为两个子目标：
- 子目标1：C = B
- 子目标2：A = B
子目标1表示我们需要证明C与B相等，这是因为我们将C替换为A后，需要确保等式仍然成立。子目标2表示我们需要证明A与B相等，这是因为我们使用了重写定理的等式。
通过证明这两个子目标，我们可以最终证明整个目标。
需要注意的是，重写定理的应用可能会产生更多的子目标，具体取决于目标中需要替换的子表达式的数量。在Coq中，我们可以使用不同的策略和定理来处理这些子目标，以完成整个证明过程。
关于Coq和定理证明的更多信息，您可以参考腾讯云的产品介绍页面：Coq - 腾讯云
相关·内容
我试图证明我的函数非零的分布超过列表的拼接。我已经证明了这两个引理： Lemma nonzeros'_remove_0 : nonzeros' (0 :: b) = nonzeros' b.Coq创建2子目标： ______________________________________(1/2)
nonzeros' (concat t b) = concat (nonzeros&#
浏览 11提问于2019-12-11得票数 0
回答已采纳
我正在通过书中的软件基础学习Coq，并且很难证明下面的引理(我需要证明其他定理)。这就是我被困的地方。我不能对命题进行分解，虽然我可以apply E2 in E1，但它会生成两个子目标(我不明白为什么)，第二个子目标在逻辑上是不正确的。请帮帮忙。在，外，歧视，注入，分裂，左，右，介绍，展开，断言，重写。
Q2:另一个类似的问题。我需要利用上述证明引理来证明其他定理
浏览 3提问于2020-03-09得票数 0
回答已采纳
我在Coq里发现了一个奇怪的怪癖。当你有一个没有必要论证的定理时，它就发生了，我们用rewrite和这个定理。例如，考虑下面的代码片段。在本例中，foo有一个冗余参数x。然后，当我在bar的证明中使用bar时，它会生成一个只读"bool“的目标。
我的第一个问题是:为什么会产生这样一个目标？其次，我发现这个目标可以使用assumptio
浏览 4提问于2022-02-21得票数 1
回答已采纳
3回答
这似乎是一个非常简单的问题，但我找不到任何有用的东西。n - x = n(n - x) + x = n + x
我还没有找到什么定理允许这样做。
浏览 3提问于2016-05-03得票数 5
回答已采纳
2回答
我试图证明自然数上的下列简单定理：以下是我在Coq中的内容S (add i j) = S (add i k) -> j = k
所以我想我应该应用eq_add_S，它说明了S m = S n -> m = n。所以我想它无法理解我想要的是m = (add i j)和
浏览 0提问于2019-01-16得票数 0
回答已采纳
1回答
在最后一行之前，我的子目标是：我想把它转化为：然而，当我尝试通过rewrite -> neg_move时，它会产生以下错误：
错误:找不到变量y的实例。
浏览 6提问于2012-01-16得票数 10
回答已采纳
1回答
考虑以下定点：Import ListNotations.Coq拒绝下面的不动点，因为它无法猜测递减的不动点(有时left列表会松开它的头，有时它就是right的不动点)。我的问题是：
是否可以在常规Fixpoint中明确表示递减参数？Next Obligation的目标是什么？
浏览 7提问于2017-12-14得票数 4
回答已采纳
所以在学习Coq的时候，我做了一个简单的例子:纸，剪刀，石头。我定义了一个数据类型。Definition compose {A B C} (g : B -> C) (f : A -> B) : (A -> C) :=为什么仅仅通过应用intros和reflexivity就可以证明Instance MSP
浏览 0提问于2014-06-26得票数 0
2回答
在ACSL中定义的归纳谓词上可以使用归纳吗？请考虑中的以下示例 int value;}; @ \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);Alt在这里失败了，所以我求助于手动Coq但是，
浏览 4提问于2015-09-08得票数 1
回答已采纳
在的1.3.1和1.3.2节中，有两个elim应用程序:第一个： B : Prop H : A /\ B B /\ ACoq < elim H. B : Prop
C : Prop首先，在第二个示例中，我不明白将什么推理规则(或逻辑标识)应用于生成两</
浏览 7提问于2017-09-24得票数 3
回答已采纳
1回答
使用如下的sig类型定义：Lemma projection_injective : x : Ax0 : AH : x = x0
我尝试了一些重写，但没有成功。例如，<
浏览 29提问于2017-07-10得票数 3
回答已采纳
1回答
如果destruct H包含连接或分离，这是非常清楚的。但我不知道它在一般情况下会起什么作用。它做了一些奇怪的事情，特别是如果H: a -> b。现在我有两个分支：x, y : natx = 4x, y : nat这是不可证明的，但对我来说还是没有意义：
Lemma demo : forall (x y: nat), (x = 4 -> x = 4) -> x =
浏览 5提问于2021-08-18得票数 2
回答已采纳
假设我们有目标a, b, c, d: nat与Arith中的引理plus_comm : forall n m: nat, n + m = m + n
rewrite (plus_comm为什么会这样，我们如何在目标中将b + c重写为c + b？编辑.将
浏览 0提问于2019-03-03得票数 0
回答已采纳
我试图证明以下几点，我认为我有正确的解决方法，通过枚举b的所有情况和所有单参数布尔函数f (应该是4个函数除以2个布尔值)，通过彻底销毁所有东西来证明这一点。我以前对归纳类型使用过区分，它的工作效果与预期一样，所以我很惊讶它在这里不能用于布尔类型。你知道为什么吗？
浏览 3提问于2017-11-28得票数 1
我的问题是:为什么‘直觉’在我的例子中起作用？Lemma eqb_false : forall n m : nat, eqb n m = false -> n <> m.m) = false -> S n <> S m但为什么要起作用呢？Coq手册上说他们会做一些搜索工作。这是否意味着它可以用其他简单的策略
浏览 4提问于2015-05-19得票数 5
回答已采纳
为了说明我面临的问题，让我们假设我们有一个关于nat的谓词让我们进一步假设我们有一种封装数据的类型，以及封装的数据满足某种属性的证明。现在，我们希望将两个对象c n p和c m q视为与n = m相同的对象，而不管构建它们所涉及的证明是什么。因此，让我们介绍一个不相关的证明公理：
Axiom irrel : forall (P:Prop) (p q:P), p = q.
浏览 3提问于2017-12-17得票数 2
回答已采纳
1回答
Coq:证明时间等于重复
、、、
我刚开始学习Coq，学习形式语义学，我正在学习“软件基础”( Software )一书。目前，我在这一章：。其中，它为简单的命令式语言定义命令。作为练习，我尝试在定义如下的语言中添加一个重复命令： (* ...same as in the我将Coq中的定理定义如下：
浏览 6提问于2022-02-21得票数 0
回答已采纳
在定义Coq中的整数时，我遵循的回答，但当试图在其上定义加法时，总是会出现错误“无法猜测递减参数”。我尝试过多种不同的定义，似乎总是会发生这种情况。有办法证明Coq的论点正在减少吗？或者我错过了一些明显的方法来定义加法。| O
| S (n : nat).
浏览 2提问于2020-09-24得票数 1
回答已采纳
2回答
我试着从我正在读的一篇论文中证明一个定理(Bennett，有两个部分，2013年)，但我不知道如何解决一个子目标。Parameter Entity: Set.这是定理和我的不完全证明：Theorem T12 : forall y,
((exists x, PP x y) <->所以有两个子</
浏览 4提问于2021-12-18得票数 0
回答已采纳
我不能用Ssreflect用setoids重写。虽然我不认为这些信息与解决问题相关，但我在coq：中使用了这个范畴理论的公式。据我所知，如果能够解决合适的RewriteRelation Typeclass实例，defined的重写可以使用用户定义的等价关系。 (* Fails: not a rewritable relation: (a ≈ b) in rule __top_as
浏览 2提问于2020-02-02得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
