1回答
我找不到一个重载的标准库==函数，它返回一个布尔值(或者一个求和值，或者我可以用来计算的值)。我希望能够做到和而不必指定参数的类型。如果Coq没有这个相等类型的特性，我会很惊讶；有人能告诉我在哪里可以找到它吗？我有一种感觉，这与ssreflect有关，但我搞不清楚。
谢谢。
浏览 13提问于2020-05-19得票数 3
回答已采纳
1回答
怎样才能让Coq让我证明句法类型的不等式？我读过的答案，它表明，如果假设是单价的，那么证明类型不等式的唯一方法就是通过基数参数。我的理解是-如果Coq的逻辑与单价一致，它也应该与单价的否定一致。虽然我知道单价的否定实际上是某些同构类型是不相等的，但我认为应该可以表示没有同构类型(不完全相同)是相等的。类型构造函数的不
浏览 5提问于2020-04-18得票数 3
回答已采纳
1回答
我想在Coq中考虑实数上的相等。 但是Coq.Reals.Reals.中的R不是归纳类型，所以我不能定义像Nat.eqb这样的函数。 如何在Coq中定义实数上的等式？
浏览 7提问于2020-10-11得票数 3
回答已采纳
所以在学习Coq的时候，我做了一个简单的例子:纸，剪刀，石头。我定义了一个数据类型。Definition compose {A B C} (g : B -> C) (f : A -> B) : (A -> C) :=Class Monoid {A : Type} (dot
浏览 0提问于2014-06-26得票数 0
1回答
F#中的间接多态性
、、、、
OCaml的印地语-Milner类型系统不允许非谓词多态(àla System-F)，除非通过对记录类型的最近扩展。这同样适用于F#。然而，有时需要将使用非谓词多态(例如Coq)编写的程序翻译成这些语言。Coq萃取器对OCaml的解决方案是使用Obj.magic，这是一种通用的不安全铸造。这起作用是因为
在OCaml的运行时系统中，所有值都有相同的大小，而不管它们的</
浏览 3提问于2013-03-28得票数 12
I和tt都是单例类型的成员。前者住在Prop，后者住在Set。这些都是非常简单的类型，所以我不期望它们在任何设置中都支持丰富的相等类型。在不借助身份证明公理的唯一性的情况下，这些目标在Coq中是可以证明的吗？
浏览 20提问于2020-06-27得票数 1
回答已采纳
1回答
. (* for example *) 这样X就是一个参数，而不是一个参数，所以我可以让构造函数使用X进行即席多态性 上下文 我正在尝试编码一个类型判断，我希望它是多态的，因为我有许多不同类型的术语(Coq类型)的类型规则，但所有规则都有相同的判断形式。这意味着，对于Coq类型A、B，我希望能够执行以下操作 Inductive typing_judgement : (X : Type) -> context -> X -> myTyp
浏览 26提问于2020-03-29得票数 2
回答已采纳
我正在努力提高我的Idris技能，通过查看一些练习 (最初是为Coq，但我希望翻译到Idris不太坏)。我在上遇到了麻烦，它写着：
plusIdExercise : (n : Nat) -> (o : Nat第一种情况：似乎很有效，但我想说的是，例如：
浏览 3提问于2018-05-26得票数 2
回答已采纳
Coq是一个证明助手，而Agda/Idris是编程语言(尽管它们可以被称为证明助手)。
我正在探索这些语言，我想知道Agda/Idris是否足以做Coq所能做的一切。那么，有没有一些证据/管理代码/IDE (Emacs)函数的方法/其他Coq可以做而Agda/Idris不能做的事情呢？
浏览 21提问于2017-12-16得票数 9
回答已采纳
2回答
经常在Coq中，我发现自己做了以下工作:我有一个证明目标，例如：我只需要证明a = b，因为其他的一切都是一样的但是，在我的证据的最下面，让那些人在我身边闲逛似乎是不必要的混乱。
Coq中是否有一种一般策略，用于获取构造函数的相等，并将其分解为构造函数参数的相等(类似
浏览 3提问于2016-05-27得票数 6
回答已采纳
2回答
我希望能够在Coq中比较两个类型为"list“的项目，并获得布尔值"true”或"false“来表示它们的等价性。我得到了表单的支持： :: (2 :: 3 :: nil) :: (3 :: nil) :: nil =
nil
浏览 5提问于2018-04-25得票数 3
如何使Category中定义的符号在HomCategory中可用
Parameter Object : Type.
浏览 3提问于2014-09-29得票数 4
回答已采纳
1回答
这是我的第一篇帖子，如果我犯了错，很抱歉。一个快速的谷歌和搜索通过堆栈交换并不显示任何确认。有人能证实这一点或纠正我吗？
浏览 2提问于2015-06-18得票数 5
回答已采纳
with end = exist (fun n' : nat => n' < n) x0 l 在我的上下文中我无法在H上进行析构，因为结果项可能是错误类型的，但看起来很明显等价性是成立的，因为match的唯一可能分支并不依赖于匹配的内容。
浏览 40提问于2020-01-14得票数 1
回答已采纳
1回答
在Coq标准库中，自然数(lt_dec)和整数(Z_lt_dec)的“小于”关系是可确定的。然而，当我搜索(Search ({ _ _ _ } + {~ _ _ _ }))时，我找不到Q_le_dec或Qle_dec来寻找有理数，只能找到Qeq_dec来寻找可判定的相等。这是不是因为“小于”关系对于Coq中的逻辑来说是不可确定的？或者它是可确定的，但决策过程只是没有在标准库中实现？
浏览 3提问于2021-11-03得票数 3
下面是一个更大的证明的简化片段，它捕获了有问题的行为。 Parameter t : Type.
Parameter x : t.当您用rewrite prop替换rewrite prop2时，coq失败并出现隐含错误。然而，在我的观点中，coq应该在重写步骤之后产生forall e : t, True。有人能帮我吗？
浏览 0提问于2011-11-17得票数 3
我试图将(1,2,3)定义为coq中的一组元素。我可以使用list将其定义为(1 :：(2 :：(3 :：nil)。有没有办法在coq中定义set而不使用list。
浏览 1提问于2016-04-13得票数 6
这是我在数学定理中使用的一种归纳型pc。另一种归纳类型是pc_tree，它基本上是包含一个或多个pcs的二叉树。pcts是包含单个pc的叶节点构造函数，pctm是包含多个pc的内部节点构造函数。引理的含义非常简单:如果一棵具有包含y : pc n的单叶节点的树包含一些x : pc n，那么这就是x = y。我想我应该能够用一个简单的inversion在contains上证明这一点。我本来希望把x = y作为上下文中的一种假设。我所关心
浏览 0提问于2014-07-13得票数 8
回答已采纳
1回答
如何将Coq中的nat转换为q (Rational)？Require Import Coq.QArith.QArith.Error: The term "2" has type "nat" while it is expected to have type "Q".
浏览 2提问于2015-09-22得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
