我可以像这样在Coq中定义有限类型： Inductive fin : nat -> Set :=| FS : forall {n}, finDefinition void := fin 0.
Definition vunit : unit := FZ.Definition
浏览 20提问于2020-09-04得票数 4
回答已采纳
( 1)我认为在不进行模式匹配的情况下，可以使用归纳类型。(仅使用_rec、_rect、_ind )。它是不透明的，复杂的，但可能的。( 2)是否有可能使用具有模式匹配的共进类型？从共归纳型到同归纳型构造子域的结合都存在着一个函数。Coq是否显式地生成它？如果是，如何重写“hd”？ Variable A : Type.
浏览 2提问于2016-11-25得票数 1
回答已采纳
1回答
我注意到Coq对支持和类型的平等性综合了不同的归纳原则。有人对此有什么解释吗？平等被定义为相关的归纳原则有以下几种类型： : forall(A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -&
浏览 4提问于2016-09-25得票数 5
回答已采纳
1回答
这是的后续问题(尽管这个问题是自包含的)。
我有一个简单归纳类型的树(t)，它有一组固定的标签(arityCode)，每个标签都有固定数量的子树。我有一种类型(path)的路径到树中。这些都在代码中，但我要快速解释一下我遇到的问题:要构造一个there路径，我需要生成一个path (Vector.nth v i) (其中一个子节点中的路径)。但是唯一的path构造函数(here和t
浏览 2提问于2017-12-23得票数 1
2回答
我想考虑以下三个(相关的？)Coq定义。 | z1 : nat1 | z3 : nat3这三种类型都给出了证明命题成立的归纳原则。版本还包含set和
浏览 1提问于2015-03-29得票数 12
1回答
“`le`”的归纳原则
、、、
对于归纳类型nat，生成的归纳原则在其语句中使用构造函数O和S： : forallP : nat -> Prop, (forall n : nat, P n -> P (S n)) -> fo
浏览 0提问于2019-03-16得票数 1
回答已采纳
我已经通过使用函数作为fin n -> A在类型A上定义了向量类型。如果不经过归纳向量，我想不出连接向量的方法。我使用的有限集的定义是 match k with | S k => option (fin k)concat {A : Type} (n m : nat) (v1 : fin n -&g
浏览 20提问于2019-11-02得票数 3
回答已采纳
据我所知，它基本上允许对递归函数的所有参数“同时”执行归纳。将来，我怎样才能知道这种策略是干什么的呢？(有办法访问LTac吗？)
有更规范的方法来解决我下面提出的定理吗？Module Import OTF_Nat :=
浏览 0提问于2018-01-03得票数 3
回答已采纳
2回答
我已经开始学习Coq，并试图证明一些看起来相当简单的东西:如果一个列表包含x，那么该列表中x的实例数将> 0。我将包含函数和计数函数定义如下： match l with
| nil => FalseFixpoint count (n acc: nat) (l: list nat) : nat :=
浏览 6提问于2017-04-17得票数 0
回答已采纳
我试图在Agda中演示Coq提取机制和MAlonzo编译器在代码生成方面的区别。我在Agda中提出了一个简单的例子： zero : NatelemAt (cons _ xs) (finsucc n) = elemAt xs n
直接转换到Coq (使用)<em
浏览 2提问于2014-05-20得票数 1
回答已采纳
在Coq中，可以归纳地定义自然数如下：| zero : nat我想知道是否有可能以类似的方式归纳地定义整数？但是我想在int的定义中断言succ(pred x) = x和pred(succ x) = x，我不知道如何做到这一点。
浏览 2提问于2021-02-16得票数 0
回答已采纳
2回答
Coq推理行为
、、、
我试图用Coq编写以下Agda片段。(suc x) (suc y) = suc (thin x y)Inductive Fin : nat -> Type := | fs {n : nat} : Fin n -> Fin (S n).n) -> Fin n -> Fin (S n)
n : n
浏览 5提问于2016-05-03得票数 2
回答已采纳
和peano nats： | zewro : nawtTheorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n.可悲的是，下面的校对脚本的最后一行写着“错误:n是结论”。. - this is the culprit
官方文档中的错误并不多见，我有点困惑--为什么
浏览 0提问于2017-01-10得票数 3
回答已采纳
1回答
我是coq的初学者。我想证明一个关于自然数的布尔等式的对称性。我已经应用了归纳和析构命令，但它不起作用。请指导我证明这个定理。Fixpoint beqnat(n m : nat): bool:= |0=> match m with |S m'Theorem beq sys:
浏览 2提问于2018-08-11得票数 0
2回答
在coq中使用哪个向量库？
、、、、
我想知道，在coq中是否有一个常用的向量库，即按其类型的长度索引的列表。对于那些不想使用自己的库的人来说，什么是最好的或最常见的做法？标准库中的向量我错了吗？还是人们只是使用列表，并与其长度的</e
浏览 10提问于2017-02-17得票数 6
回答已采纳
2回答
当我在Agda中玩弄证明验证时，我意识到我对一些类型明确地使用了归纳原理，而在其他情况下使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文章：“在Agda中，依赖类型的模式匹配是语言的原语，核心语言没有模式匹配转换成的归纳/递归原则。”那么，Agda中的类型理论归纳和递归原
浏览 20提问于2015-06-02得票数 5
2回答
我的证明脚本给了我愚蠢的类型等式，比如nat = bool或nat = list unit，我需要用它们来解决矛盾的目标。
在正常的数学中，这是微不足道的。给定集合bool := { true, false }和nat := { 0, 1, 2, ... }，我知道true ∈ bool，但是true ∉ nat，因此是
浏览 2提问于2012-09-01得票数 7
回答已采纳
2回答
对于具有可判定顺序的类型，是否存在等价于同一性证明的唯一性？尤其是Peano自然数的类型？它是否在Coq的库中实现？(我找不到)
对于自然数，这似乎是正确的，因为n <= p看起来与n == p的证明相同:它迭代地破坏n和p，直到左边的数字达到0，然后结束。
浏览 0提问于2018-12-21得票数 3
回答已采纳
目前，我已经开始在Coq()中证明关于一阶逻辑的定理.我已经证明了推论定理，但是在正确性定理上，我被引理1所困住了。所以，我把引理中的一个优雅的部分简洁地写了出来，我邀请大家来看看它。这是一个不完整的证明，证明了这些术语的良好基础。如何正确地摆脱这对“承认”呢？Require Export Coq.Vectors.Vector.Require Export Coq.Lists
浏览 0提问于2018-08-29得票数 0
回答已采纳
2回答
考虑一下这个例子：| foo : T match t with | bar n x => evalBar x n match n with | S n' =>
浏览 1提问于2018-05-22得票数 2
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
