0回答
Coq索引关系
coq、dependent-type
我在Coq中定义了一个索引归纳类型： Inductive hz : Set :如何将我的Arrow / Sum索引约束为与maxHZ关系相同的形状(无需创建更多的构造函数，如ArrowHZ : t H -> t Z -> t Z)。
浏览 0提问于2017-11-30得票数 1
回答已采纳
然而，我没有看到一种方法来利用只出现在索引中的事件。如果在类型索引中允许非严格正的出现，有没有办法推导出类似的矛盾？
浏览 1提问于2018-01-10得票数 4
回答已采纳
1回答
在Coq中有一个类型层次结构，每个类型都表示前一个类型的类型，例如Type_0 : Type_1、Type_1 : Type_2等等。然而，在coqtop中，当我键入Check Type.时，我得到了Type : Type，这看起来像是一个矛盾，但并不是因为Type是隐式索引的。
问:如何启用类型宇宙的显式索引？
浏览 7提问于2017-07-24得票数 3
回答已采纳
2回答
如何将Ocaml升级到最新版本以支持Coq中的QuickChick？
ocaml、upgrade、coq、ubuntu-18.04、opam
当我时，我得到了：
此开关的基座(使用--unlock-base强制)
opam list
浏览 1提问于2019-05-02得票数 0
回答已采纳
1回答
考虑关系的自反传递闭包：| star_refl x : star如何在Coq中给出表示法，以便编写x ->* y，或者添加一个下标来表示关系->__r。这在伊莎贝尔身上是可能的。在Coq有干净的方法吗？
浏览 1提问于2020-04-02得票数 2
回答已采纳
1回答
我有一个术语重写系统( A，→)，其中A是一个集合，→是A上的一个嵌入二进制关系，给定A的x和y，x→y表示x降为y。为了实现一些属性，我只使用来自Coq.Relations.Relation_Definitions和Coq.Relations.Relation_Operators的定义。我怎样才能在Coq中实现这一点呢？
浏览 1提问于2017-05-14得票数 3
回答已采纳
1回答
在Coq中，有理数的“小于”是可判定的吗？
comparison、coq、rational-number、decidable
在Coq标准库中，自然数(lt_dec)和整数(Z_lt_dec)的“小于”关系是可确定的。这是不是因为“小于”关系对于Coq中的逻辑来说是不可确定的？或者它是可确定的，但决策过程只是没有在标准库中实现？
浏览 3提问于2021-11-03得票数 3
2回答
Coq中实数的“小于”是如何定义的？
coq、real-number
我只是想知道实数的“小于”关系是如何定义的。特别是，我感兴趣的是，是否可以在平等关系的基础上定义诸如<或<=之类的关系。但这是否符合<em
浏览 5提问于2015-12-21得票数 7
回答已采纳
1回答
Coq的类型系统CiC和lambda cube之间的关系是什么？
coq、type-systems
我读了https://en.wikipedia.org/wiki/Lambda_cube#Formal_definition，把CiC和lambda cube的关系搞糊涂了。据我所知，CiC扩展了CoC，它是lambda cube的一个角，所以lambda cube的规则也应该在Coq中得到满足。 例如，似乎coq接受(*，*)。但似乎Coq不接受(-，*)。如果是，则Set -> nat的类型必须是Set，而不是Type。但是Coq对Check (Set -
浏览 32提问于2020-06-14得票数 0
回答已采纳
3回答
使用Coq证明助手证明(p->q)->(~q->~p)
logic、coq、theorem-proving
我是Coq的新手，正在尝试Ruth和Ryan的样例引理。使用自然演绎的证明非常简单，这就是我想用Coq来证明的。 assume ~q.有没有人能告诉我自然演绎和Coq关键字之间是否存在一对一的映射关系？
浏览 3提问于2013-02-01得票数 2
2回答
我刚刚从CMU讲座中了解到，虽然Check Type以Coq格式返回Type : Type，但左、右的Types被不同的数字隐式索引，因为如果它们是相同的，就会导致类似Burali-Forti悖论的类型理论模拟如果您试图实现这样一个悖论，Coq将拒绝编译。
我很好奇Coq脚本中这个悖论是什么样子，但是找不到任何代码。一些讨论提到了B.Barras的“coq中的Burali-Forti悖论的形式化”，但是与它的联系被打破了。这一悖论是否有Coq实现？
浏览 2提问于2015-08-13得票数 2
回答已采纳
1回答
在Coq (受关系约束的归纳定义)中归纳定义整数
integer、coq、induction
在Coq中，可以归纳地定义自然数如下：| zero : nat我想知道是否有可能以类似的方式归纳地定义整数？
浏览 2提问于2021-02-16得票数 0
回答已采纳
1回答
我对Coq类型系统在下面h的定义中证明术语的匹配部分的行为感到困惑：
Set Implicit Arguments.
浏览 3提问于2017-07-27得票数 4
回答已采纳
1回答
问题：例如，在这个问题的公认答案中：Coq中的关系(在Relations：中)定义为：Definition relation := A -> A -> Prop.我的意图是表达对某种“较小的”B的关系的限制。如果这些类型是相互排斥的，那么它可能没有任何意义。
浏览 0提问于2018-06-22得票数 3
回答已采纳
3回答
我有一个Coq项目，它的库被组织成子目录，类似于：…/MyProj/Main/Main.v (imports Auxiliary/Aux.v)((coq-mode . ((coq-prog-args .
浏览 3提问于2015-08-05得票数 8
回答已采纳
1回答
由自己类型的项索引的依赖类型
types、coq、dependent-type
所以，我想知道依赖类型是否可以通过自己类型的项进行索引？我试过的是Parameter a: Obj.我试图用依赖类型理论做些什么，以及如何用Coq实现它呢？
浏览 0提问于2018-08-09得票数 2
1回答
证明一种关系是没有根据的
coq
回想一下Coq的库中对基础良好的关系的定义： Acc_intro : (这个Coq定义接受所有常见的数学基础良好的关系，例如自然数上的严格顺序<。我在什么地方弄错了吗？
浏览 4提问于2018-08-15得票数 3
回答已采纳
1回答
这是我在数学定理中使用的一种归纳型pc。 | pcs : forall ( m : nat ), m < n -> pc n另一种归纳类型是pc_tree，它基本上是包含一个或多个pcs的二叉树。pcts是包含单个pc的叶节点构造函数，pctm是包含多个pc的内部节点构造函数。 | pcts : forall ( n : nat ), pc n -> pc_tree
浏览 0提问于2014-07-13得票数 8
回答已采纳
人们会认为，这一建议同样适用于Coq。然而，我最近强迫自己使用same_relation谓词的Relation模块，我留下的感觉是更糟的。所以我肯定遗漏了什么，所以我的问题。为了说明我的意思，让我们考虑一下可能的关系：Require Import Setoids.SetoidInductive rel2 {A:Type} : A -> A -> Prop :=
| rel2_refl : forall x:A, rel2 x x. (*
浏览 6提问于2016-06-18得票数 3
回答已采纳
云服务器
ICP备案
对象存储
云点播
即时通信 IM
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号