对应用于Coq中nat列表的函数的推理

文章/答案/技术大牛

发布

1回答

list、coq、proof、reasoning

我们正在验证一个具有三个功能的系统，如下所示。然而，我们不知道如何进一步进行这样的证明。可以共享Coq函数的实际定义。请指导我们。Parameter weights : nat -> list nat -> nat -> nat.Parameter schedule: nat -> list nat -> list nat. Parameter co

浏览 29提问于2021-02-11得票数 0

1回答

如何用Coq表证明自然数定理

coq

我是新来的科克。为了实现对列表和对列表的练习，我使用Coq列表库证明了一个简单的自然数定理。我试图证明自然数的简单性质：((a0*multiplier)=d1)+((a1*multiplier)=d2)+((我使用对列表(将a存储在一个列表中，d存储在另一个列表中)在Co

浏览 0提问于2018-02-08得票数 0

回答已采纳

1回答

通过两种实现对阶乘程序的Coq验证

functional-programming、coq、verification

我是coq的新手，我正在尝试验证factorial程序的功能。这里是“一阶逻辑”中的FOL标准。然而，令我惊讶的是，在用factorial验证coq程序时，常见的方法是定义以下两个函数fact和fact_tr Fixpoint fact (

浏览 0提问于2018-03-25得票数 2

回答已采纳

1回答

在Coq中为共归纳类型流定义一个“head”(没有模式匹配)

coq、coinduction

( 1)我认为在不进行模式匹配的情况下，可以使用归纳类型。(仅使用_rec、_rect、_ind )。它是不透明的，复杂的，但可能的。( 2)是否有可能使用具有模式匹配的共进类型？从共归纳型到同归纳型构造子域的结合都存在着一个函数。Coq是否显式地生成它？如果是，如何重写“hd”？ Variable A : Type.

浏览 2提问于2016-11-25得票数 1

回答已采纳

1回答

处理表单{x: nat* x >= 13 /\ x <= 19 }的(子)类型的最佳方法？*

coq

Coq将允许我定义如下：问：，我应该怎么告诉Coq朱莉娅的支持类型是nat，这样我就可以写任何关于她的有用的东西了？Q':，我对青少年的定义似乎是一条死胡同；它更像是陈述性的，而不是

浏览 0提问于2016-06-18得票数 3

回答已采纳

3回答

Coq中的递归部分函数

recursion、coq

我想知道在Coq中定义部分递归函数的最佳方法是什么。Fixpoint MaxValueList (l : list nat | l <> []) : nat :=|[n] => n |n::l' =>但是，这是行不通

浏览 4提问于2016-02-29得票数 1

回答已采纳

1回答

作为Coq中的函数参数的依赖类型

function、coq、dependent-type

我是Coq的新手。我正在尝试使用Coq的依赖类型。我想要做的是，简单地将一个偶数输入到一个函数中。例如，在伪代码中：{}next_even(1) // Coq should show a

浏览 8提问于2019-11-14得票数 1

2回答

如何禁用Coq中的自定义符号？

coq

然而，在此之后，所有函数应用程序表达式都被表示为'>>‘样式。例如，在Coq Toplevel的证明模式中，我可以看到其实应该是为什么Coq会积极地将所有函数应用程序样式的表达式重写到我的自定义' >>‘表示中？如何将一切恢复正常，我的意

浏览 5提问于2015-05-18得票数 10

回答已采纳

1回答

如何为coq中的类型提供别名？

alias、typedef、coq

假设我想在coq中创建一个自然数矩阵。为了创建一个二维列表(即矩阵)，我需要编写list (list nat)。我的问题是:我不写list (list nat)，我该怎么做才能让coq完全理解matrix这个词，就好像它是list (list nat)一样。我试过Notation &qu

浏览 2提问于2018-11-04得票数 5

回答已采纳

1回答

在Coq中，如何定义A= {x | f(x) = 0}这样的集合？

coq

我是一个使用Coq的新手。我想问一下，如果我想定义一个像A = {x | f(x) = 0}这样的集合，我该怎么做呢？我写的内容类似于：非常感谢。

浏览 0提问于2017-09-05得票数 1

1回答

有限映射实例

dictionary、coq

在我的应用程序中，我需要使用Coq中的有限映射并进行推理。在谷歌上搜索，我发现FMapAVL似乎非常适合我的需求。问题是文档很少，我还没有弄清楚该如何使用它。作为一个简单的例子，请考虑以下使用成对列表的有限映射的愚蠢实现。Require Export List.Definition map_nat_nat: Type :

浏览 4提问于2013-01-23得票数 10

回答已采纳

2回答

偶数和奇数情况的模式匹配

coq

假设我在Coq中编写了一个固定点算法，它对一个数字的所有“二分之一”求和： match a with | 0如何让Coq识别a是偶数还是奇数，并将其与2 * k或S (2 * k)进行匹配

浏览 5提问于2017-09-24得票数 1

1回答

这个引理能在Coq中被证明吗？(f : nat -> nat), forall n:nat, P n (f n).简单的destruct不能编译，因为我们不能消除sort Prop中的对象exists p:nat, P n p，从而在sort Set中生成函数f。如果Coq不能证明这个引理，那么forall n:nat, exists p:nat, P n p的</e

浏览 17提问于2019-03-01得票数 1

回答已采纳

1回答

在coq中写入隐式证明对象时出现不可能的模式

coq

我尝试使用coq作为一种依赖类型的编程语言。我创建了以下小程序： | GoodNonEmpty : forall h t, Good (h :: t).Definition get_first(l : list nat)(good : Good l) : nat := | h :: t => h | nil我为非空列表定义了一个类型，并创建了一个<em

浏览 0提问于2012-09-22得票数 3

回答已采纳

2回答

COQ中两个递归函数展开的证明

coq、proof、coq-tactic

我已经开始学习Coq，并试图证明一些看起来相当简单的东西:如果一个列表包含x，那么该列表中x的实例数将> 0。我将包含函数和计数函数定义如下： match l with | nil => FalseFixpoint count (n acc: nat) (l: list

浏览 6提问于2017-04-17得票数 0

回答已采纳

2回答

将整数列表转换为自然数列表

coq

我想把list of integer转换成list of nat。下面是我在Coq中返回的函数。Fixpoint list_int_to_nat (l : list integer) : list nat := | nil => nil list_int_to_nat l

浏览 0提问于2013-06-06得票数 1

回答已采纳

1回答

证明在两个列表中找到相同元素的一个性质

coq

我是Coq的新手。我有一个函数findshare，它可以在两个列表中查找相同的元素。引理sameElements证明了函数findshare在两个列表的连接上的结果等于应用于每个列表的函数的结果的连接。我在证明引理sameElements时有点卡住了。Fixpoint findshare(s1 s2: list

浏览 18提问于2019-03-05得票数 1

回答已采纳

3回答

与类型族匹配时的Coq类型错误

coq

我正在尝试从内存中重新实现中的一个示例。我写道：b : myTypeThe term "twice" has type "nat -> nat" while it is expected to我认为，一旦Tw

浏览 5提问于2016-07-15得票数 2

回答已采纳

2回答

Coq证明中的匿名函数

coq

我正试图在Coq中证明一些涉及使用类型类的东西。(let (fmap0, _, _) := ListFunctor in fmap0) nat natCoq</e

浏览 2提问于2015-01-20得票数 2

回答已采纳

2回答

什么是Coq中的构造函数？

constructor、coq

我很难理解什么是构造函数以及它是如何工作的。例如，在Coq中，我们被教导这样定义自然数： | O : nat如果我这样做了：我知道它是nat类型的4。这是如何工作的，Coq

浏览 1提问于2011-02-23得票数 9

回答已采纳

点击加载更多