试图用MT1 (或MT1bis)来证明MT1A，但是Coq不能统一：(这不是家庭作业，只是一个业余爱好项目)
浏览 4提问于2018-01-01得票数 1
回答已采纳
2回答
考虑以下几行( Coq)：Variable f g : A -> A.但是，Coq无法单独找到t。战术refine (eq_trans (Hfg _) _)。对于<em
浏览 2提问于2015-02-12得票数 3
回答已采纳
1回答
我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道~~A -> A不是直觉逻辑的一部分，但我所选的课程是经典的，所以我不介意。我知道上述公理可以被Coq.Logic.Classical_Prop.NNPP访问，但是这个公理无助于从更复杂的句子中删除双重否定，比如例如最好我能在H
浏览 3提问于2018-10-29得票数 1
回答已采纳
1回答
表示归纳类型
、、、
我以本文的精神实现了依赖类型的lambda演算：微积分，工作，并对它进行了实验和扩展:许多宇宙，硬编码的归纳公理。然而，我想添加归纳类型来做更复杂的事情。生成归纳和递归公理。
我两种方式都不喜欢。第一个层次太低，从高级语言转换到核心语言需要付出很大的努力。这些类型是如何在现有系统中实现的，如Coq、Agda和Idris？
浏览 4提问于2014-03-12得票数 3
在精益手册“精益证明定理”中，我读到：“用经典公理，我们可以证明每一个命题都是可判定的”。我想要求澄清这一声明，我在问一个Coq论坛，因为这个问题同样适用于Coq，也适用于精益(但我觉得我更有可能在这里得到答案)。在阅读“用经典公理”时，我知道我们有一些等价于排除中间定律的东西：
Axiom LEM : forall (p:Prop), p \/ ~p.然而，根据我对Coq的了解，我无法实现decide，因为我不能销毁(LEM p) (排序为Prop)来返回Prop以外的其他内
浏览 0提问于2020-04-20得票数 3
回答已采纳
1回答
Lit : char -> Exp | Or : Exp -> Exp -> Exp从其中我归纳地定义了一个类型的家族通常，当试图用归纳类型(或谓词)证明(负)结果时，我会使用elim策略(确保所有相关假设都在我的目标(generalize)内，并且只有变量出现在类型构造函数中)。但在这种情况下，elim是不好的。
浏览 6提问于2016-05-21得票数 1
回答已采纳
它可以在没有的Coq中证明吗？它可以用谓词或函数的扩展性来显示，但是由于结论比通常的结论(f = g)更弱，我天真地认为可以在不使用附加公理的情况下产生一个证明。毕竟，平等的两个方面都只涉及f和g的应用；如何才能辨别出任何潜在的差异？
我是错过了一个简单的证明，还是这个引理无法证明？
浏览 0提问于2018-07-24得票数 3
回答已采纳
1回答
> {-# LANGUAGE RankNTypes #-}
现在的问题是，我们如何制造一种类型来代表选择的公理？选择的公理是关于集合集合的。这意味着我们需要类型或其他的东西。是否有可以编码的与选择公理等价的东西？注意:理想情况下，它应该是适用于的选择公理的版本
浏览 4提问于2015-12-06得票数 1
我正试图理解如何在过程语言或面向对象语言(如Ruby或JavaScript )中实现JavaScript。对于 (这是Coq)：
Axiom point : Type.它本质上说：“对于每一个用点p1和p2创建的公理，它必须满足在一条线上的特性，等等。”这做不到我想做的事。我希望它能完成定义一个实际公理的数学目标。想知道如何在Ruby或JavaScript这样的语言中完成这一任务，如果这不是直接的可能的话，就尽可能接近它。即使它只是一个DSL或定义一些
浏览 1提问于2019-03-01得票数 2
2回答
下面是一个人工的MRE，它使用适当的coq设计实践编译：02 Parameter CReal: Set.现在它抱怨O是CReal而不是CNat，因此，如果x被多态地解释为一个CReal，能够与其他CReals进行比较并以一种漂亮而非复杂的方式应用CReal定理和公理，那就太好了。编辑
为了更清楚地说
浏览 6提问于2020-03-18得票数 0
回答已采纳
2回答
有没有办法在Coq中恢复这些信息？
当然，如果这样的y存在，那么它不是2。如何在Coq中恢复此信息-我是否需要显式假设它(即，无法通过存在实例化以某种方式恢复它？)
浏览 0提问于2017-12-06得票数 5
1回答
我相信它是直接从推理规则应用中得到的，因为metis可以很小地证明它。apply (rule allI; rename_tac P; rule allI; rename_tac h; rule impI)留给我的目标是我比Isabelle/HOL更熟悉Coq，但即使在那里，我也无法证明它(即使假设P的参数类型是有人居住的，classic公理也是如此)。
任何线索都会很感激的。
浏览 7提问于2022-03-03得票数 1
回答已采纳
当我证明一些定理时，我的目标随着我应用越来越多的策略而变化。一般来说，目标倾向于分成多个子目标，子目标更简单。在最后一点，Coq决定目标是被证明的。这个“经过验证”的目标是什么样子的？这些目标看起来很好：
a = a. (* Any object is identical to itself (?)换句话说，当我最终应用reflexivity时，C
浏览 0提问于2014-02-07得票数 1
2回答
我试图证明内射函数在Coq中是可逆的。我已经在我的证明中达到了一个点，我的目标是一个“存在”命题。我想定义一个使用证明作用域(我之前介绍过的类型和函数)中的术语的函数，然后将该函数显示给"exists“目标。我是Coq的新手，所以欢迎其他的评论和指针。
浏览 19提问于2020-12-22得票数 1
回答已采纳
我想对我的ASP.NET MVC3应用程序使用服务层模式(如中所述)。
我的目标是在深入研究代码之前，通过为其设置适当的框架来设置解决方案结构，使我能够更容易地学习该模式。有人能向我展示在Visual Studio 2010解决方案中布局解决方案、项目和文件夹的常规方法吗？
浏览 0提问于2011-10-14得票数 1
回答已采纳
1回答
深入研究test_nostutter_1的摘录，我找到了一种解决方法，不再重复：do num expr
expr被求为v，这必须是一个策略值。此策略值v被应用于数值计算。假设num > 1，在第一次应用v之后，v至少被应用于生成的子目标，等等。如果v的应用程序
浏览 2提问于2019-06-27得票数 0
回答已采纳
cached: 1)我无法理解的是，如果我将大小更改为14 (甚至更少).Is，那么它将被成功地证明
浏览 10提问于2022-09-20得票数 2
回答已采纳
2回答
我试着从我正在读的一篇论文中证明一个定理(Bennett，有两个部分，2013年)，但我不知道如何解决一个子目标。Parameter Entity: Set.所以有两个子目标我无法证明。在每一种情况下，都有~ (exists s : Entity, F b s /\ Ps s a)作为一个假设，或者作为子目标。我被困在这一点上了。第一个未解决子目标的状态是b, a, c : EntityPscb : Ps c b
nPba : ~ (
浏览 4提问于2021-12-18得票数 0
回答已采纳
来自这里的建议是：这是个好问题。在阅读了关于TLA+的文章之后，我对在web应用程序中进行正式校对的想法非常感兴趣。同样地，通过绘图，我可以测试颜色是否是我期望的颜色，或者动画是否持续一定的长度，等等。还有很多视觉属性需要检查。
但我的问题是如何在证据方面做到这一点。回到那篇文章，问题是我们甚至可以在HTTP请求或呈现中精确地证明什么。考虑到这两个特性都是本机平台特性，而且它们都有我们无法控制的副作用，我不知道该怎么做。在链接文章中
浏览 0提问于2019-03-12得票数 -2
回答已采纳
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号