在Coq中重新排序假设的显示？
在Coq中重新排序假设的显示可以通过使用tactic来实现。Coq是一个交互式定理证明助手，它提供了一种称为tactic的方式来指导证明过程。在Coq中，假设的显示顺序是根据它们在上下文中的出现顺序确定的。如果你想重新排序假设的显示顺序，你可以使用tactic来重新安排它们。
一种常用的方法是使用"pose" tactic来引入一个新的命题，并将它放在所需的位置。例如，假设我们有以下上下文：
H1: P1
H2: P2
H3: P3如果我们想要将H3放在H1和H2之前，我们可以使用以下tactic：
pose proof H3 as H3_new.这将引入一个新的命题H3_new，并将其放在H1和H2之前的位置：
H3_new: P3
H1: P1
H2: P2通过这种方式，我们可以重新排序假设的显示顺序。
Coq中的其他一些有用的tactic包括"assert"、"cut"和"replace"。这些tactic可以帮助你在证明过程中引入新的命题，并控制它们的显示顺序。
希望这个答案对你有帮助！如果你对Coq或其他云计算相关的问题有更多疑问，请随时提问。
相关·内容
2回答
是否有策略来重新排序Coq证明中假设的显示。通常在使用归纳法时(假设很长)，我想在顶部打印所有定义和所有其他方程。
浏览 22提问于2020-08-30得票数 0
回答已采纳
1回答
我在定义一种在证明上下文中递归反转假设的策略时遇到了麻烦。例如，假设我有一个证明上下文，其中包含如下假设：并且希望重复地反转该假设以获得包含该假设的证明上下文然而，有时颠倒一个假设会将不同的假设放到不同的子目标中，是否颠倒每个
浏览 0提问于2011-12-31得票数 9
回答已采纳
3回答
我在做Coq证据。我把P -> Q作为假设，(P -> Q) -> (~Q -> ~P)作为引理。我怎样才能把假设转化为~Q -> ~P
当我尝试apply它时，我只是产生新的子目标，这是没有帮助的。
浏览 3提问于2017-11-27得票数 2
回答已采纳
2回答
在我的证明中销毁了n之后，我陷入了以下问题：n : nath : Xn' : natH' : lengthnth_error t n = Nonenth_error t n' = None
我想使用IHl重写，但这是不可能的。
浏览 0提问于2018-09-16得票数 0
我试图证明Coq中的一个简单引理，其中假设是一个分离的。当目标发生时，我知道如何分裂split，但当它们出现在假设中时，我无法将它们分开。以下是我的例子： ((n < 5) \/ (n > 8)) -> (split H1. (** this doesn't work ... *)
浏览 2提问于2019-03-24得票数 2
回答已采纳
2回答
在一个证明过程中，我遇到了一个假设H。我有柠檬：H -> A和H -> B。lemma l1: X -> A.H: XY
但是
浏览 3提问于2014-12-07得票数 13
回答已采纳
2回答
我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。
在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Major的证明。这样的证明就是带有参数Minor的Minor函数的应用。那么，现在我想知道:在具有普遍量化
浏览 4提问于2014-05-06得票数 0
1回答
我是Coq的初学者，我很快就学会了语言，去做校对等等。
但我不明白我们能用这个做什么。好的，我们证明了一些定义等等，但是我们可以用什么方法来使用它们呢？
浏览 6提问于2022-03-17得票数 3
3回答
我试图用Coq定义Ackermann函数，我得到了一个我不明白的错误消息。如您所见，我将Ackermann的参数a, b打包成一对ab；我提供了一个为参数定义排序函数的排序函数。然后，我使用Function表单来定义Ackermann本身，为ab参数提供排序函数。
错误:没有这样的区段变量或假设：ack。我不知道Coq的
浏览 4提问于2012-04-24得票数 13
回答已采纳
我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？没有上面的命题，我就无法证明下面的命题或它们的否定。
Le
浏览 0提问于2014-10-26得票数 8
回答已采纳
我正在阅读Coq 和中的线性逻辑机械化，并且很难从理解归纳型term的类型构造函数。. (* family of functions of 2 argument *)
主要问题-如何理解类型构造函数var (t: T)**?**. ()软件基础在其第一章中只提供了两种类型<
浏览 5提问于2018-04-08得票数 1
回答已采纳
1回答
我想将假设H从下面的形式更改mR : Map MapsTo k e (filterfilter (is_vis_cookie l) mR)Goal
我认为，它们可以解决相同的目标，但我需要后一种形式的假设。或者更具体地说，进一步将k分成它的元素，如下所示。如何将
浏览 2提问于2013-03-22得票数 0
1回答
我在COQ中是新的，我试图证明反例定理。Hypothesis R2: ~B.
所以我们试着：tauto. (fun H : ~ A => let H0 : B
浏览 1提问于2018-08-23得票数 5
回答已采纳
1回答
我试图在Coq中证明以下定理： forall s x, PPs s x -> exists t, PPs t x /\ s <> t.我目前的背景和目标是：s, x : EntitynFxs : ~ F x sPsSxx : Ps Sx xexists t : Entit
浏览 1提问于2022-06-01得票数 0
回答已采纳
我在mac上使用CoqIDE_8.4pl5。当CoqIDE转到这个命令时，会弹出这个错误消息:需要导入基础信息。错误:编译库Basics.vo对库Coq.Init.Notations做出了不一致的假设
当我使用CoqIDE_8.4pl5时，我在我的旧Macbook Air上没有遇到这个问题，但当我买了一个新的macbook但这次在macbook pro上，我使用了brew cask install coq来安装它……但它似乎不起作用，
浏览 2提问于2015-04-16得票数 9
我有一个Coq项目，它的库被组织成子目录，类似于：…/MyProj/Main/Main.v (imports Auxiliary/Aux.v)但在Coqtop中，Error: Cannot find library MyProj.Auxiliary.Aux in loadpath失败了。然后，这在Coqtop中
浏览 3提问于2015-08-05得票数 8
回答已采纳
我试图将(1,2,3)定义为coq中的一组元素。我可以使用list将其定义为(1 :：(2 :：(3 :：nil)。有没有办法在coq中定义set而不使用list。
浏览 1提问于2016-04-13得票数 6
1回答
我一直在寻找在Coq中讨论与记录相关的子类型的参考资料，但找不到。 我特别想知道Record _ : _ := { _ :> * }语法是什么意思，以及它是如何运行的。尤其是当一条记录有:>和:判断的混合时，我想所有的正常子类型关系(包括排列)都成立？请分享您认为相关的其他参考资料(键入规则、子类型在Coq中的实际用法等) 顺便说一句- Agda中有没
浏览 26提问于2020-12-16得票数 1
3回答
在Coq中，假设我有一个不动点函数f，它在(g x)上的匹配定义，我想在证明中使用形式的假设(g x = ...)。下面是一个最小的工作示例(在实际的f中，g会更复杂)：这条消息显示Coq卡在哪里： match g x0 with
浏览 5提问于2015-02-08得票数 7
回答已采纳
在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？
浏览 3提问于2018-03-30得票数 2
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
