Coq:分离逻辑基础中的Int与Nat的比较

文章/答案/技术大牛

发布

1回答

coq、proof、theorem-proving

通过Separation Logic Foundations，我被Repr.v中的exercise triple_mlength卡住了。我认为我目前的问题是我不知道如何在Coq中处理int和nats。： eq (Z.add (length xs) (Zpos xH)) (length (cons x xs)) 我认为这是试图将(1:Z)添加到(length xs: nat)，然后将其与(length(cons X xs)：nat)进行

浏览 35提问于2021-07-04得票数 1

1回答

不带基数参数的类型不等式

coq

怎样才能让Coq让我证明句法类型的不等式？我读过的答案，它表明，如果假设是单价的，那么证明类型不等式的唯一方法就是通过基数参数。我的理解是-如果Coq的逻辑与单价一致，它也应该与单价的否定一致。虽然我知道单价的否定实际上是某些同构类型是不相等的，但我认为应该可以表示没有同构类型(不完全相同)是相等的。类型构造函数<e

浏览 5提问于2020-04-18得票数 3

回答已采纳

2回答

Coq中普遍量化的方法

coq

那么，现在我想知道:在具有普遍量化命题的Coq中，这种方法可以推断吗？在我的示例中，我允许变量范围在nat上，但这是一个任意的选择。任何Set (Set的任何组合？)(有Type吗？)就行了。Coq < Parameter FunctionAntecedent : nat -> Prop .Coq < Parameter FunctionConsequent : nat<

浏览 4提问于2014-05-06得票数 0

2回答

Coq:用归纳法证明两个阶乘函数的等式

functional-programming、coq、factorial

用归纳法证明了Coq中的两个阶乘函数是等价的。如何在Coq中证明这一点呢？Fixpoint fac_v1 (n : nat) : nat := | 0 => 1 end.Fixpo

浏览 6提问于2016-11-13得票数 2

回答已采纳

2回答

Coq核的证明技术

coq

伊莎贝尔将其核心证明能力建立在与高阶统一相结合的分辨率上。命题作为类型可能会占用过多的空间；什么将取代Huet的高阶逻辑统一程序？。

浏览 3提问于2020-08-12得票数 1

回答已采纳

3回答

coq基函数: bin_to_nat函数

coq、logical-foundations

我正在通过逻辑基础课程，在基础课程的最后一节课上被困住了：Inductive bin : Type := | A (n : bin) (* What to do here? *) 我用C中的递归函数解决了这个问题。唯一的问题是，我用"0“代替"A”和&q

浏览 0提问于2019-01-19得票数 2

回答已采纳

1回答

如何证明一阶语言的术语是有根据的？

coq

目前，我已经开始在Coq()中证明关于一阶逻辑的定理.我已经证明了推论定理，但是在正确性定理上，我被引理1所困住了。所以，我把引理中的一个优雅的部分简洁地写了出来，我邀请大家来看看它。这是一个不完整的证明，证明了这些术语的良好基础。如何正确地摆脱这对“承认”呢？Require Export Coq.Vectors.Vector.Require Import

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

回答已采纳

1回答

递减参数(程序修正点是什么)

coq、termination、totality

考虑以下定点：Import ListNotations.Coq拒绝下面的不动点，因为它无法猜测递减的不动点(有时left列表会松开它的头，有时它就是right的不动点)。我的问题是：是否可以在常规Fixpoint中明确表示递减参数？Next Obligation的目标是什么？

浏览 7提问于2017-12-14得票数 4

回答已采纳

1回答

如何理解Coq类型构造函数var (t: T)

functional-programming、logic、coq

我正在阅读Coq 和中的线性逻辑机械化，并且很难从理解归纳型term的类型构造函数。:= |cte (e:A) (* constants from the domain DT.A *) |fc2 (n:nat) (t1 t2: term). (* family

浏览 5提问于2018-04-08得票数 1

回答已采纳

2回答

两个命题之间的相等nat -> nat

coq、equality、computation-theory、find-occurrences、computability

我目前在coq的一个项目中工作，在那里我需要处理nat -> nat的列表。因此，基本上我将有一个以list (nat -> nat)和命题f : nat -> nat作为参数的定义，目标是检索给定列表中的f的索引。我所做的是实现了一个固定点，遍历列表，并使用相等的=将每个元素与f进行

浏览 21提问于2021-11-23得票数 1

1回答

我怎么能用coq来证明荒谬呢？

coq

我正在阅读软件基础系列中的逻辑基础，我看到了plus_id_example，即： n = m ->让我们荒谬地考虑一下，n+n <> m+m，所以我们有2n <> 2m，n <> m，这是一个矛盾，因为我们有n=m作为我们的</

浏览 1提问于2022-05-11得票数 0

回答已采纳

1回答

求和与直觉分离的区别

coq

根据Coq的文件那我们为什么需要sumbool

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

回答已采纳

1回答

Coq假设中的分裂分离(\/)

coq

我试图证明Coq中的一个简单引理，其中假设是一个分离的。当目标发生时，我知道如何分裂split，但当它们出现在假设中时，我无法将它们分开。以下是我的例子： ((n < 5) \/ (n > 8)) -> (split H1. (** this doesn't work ... *)

浏览 2提问于2019-03-24得票数 2

回答已采纳

1回答

Coq -覆盖相等的概念以添加要设置的元素。

coq

我试图使用Coq的listSet创建一个set of nats。但是，我在将成员添加到集合时遇到了问题。Require Import ListSet Nat.Axiom eq_dec : forall x y : nat, {x = y} + {x <> y}.运行时，输出为现在，我知道了为什么要在输出中获得if-else语句。这是因为我只告诉<

浏览 3提问于2017-09-07得票数 1

回答已采纳

2回答

Coq中实数的“小于”是如何定义的？

coq、real-number

我只是想知道实数的“小于”关系是如何定义的。特别是，我感兴趣的</em

浏览 5提问于2015-12-21得票数 7

回答已采纳

1回答

Coq中自然数的布尔等式

coq

是否可以比较Coq中的两个自然数x和y，并将等式作为布尔值返回？理想情况下，我希望能够做以下事情：Variable y : nat.

浏览 3提问于2014-01-17得票数 1

回答已采纳

2回答

两个等价函数应用的等价性证明

coq

我如何在Coq中证明以下内容？Hypothesis Hfg : forall x, f x = g x.Variable F : (nat->nat)->nat.我们有两个函数，f和g，它们不一定相等，但它们是等价的。例如，f x可以是0+x，g x可以是x+0。F返回一个nat，而且由于F不能查看它的函数参数，

浏览 0提问于2018-07-11得票数 3

2回答

我搞不懂为什么重写不起作用

coq、coq-tactic

我正在学习coq，不明白为什么重写不起作用。我的代码如下所示： Inductive nat : Type :=| succ (n : nat) match b with | succ b' => add (succ a) b' end.- 我目前的证明状态是： - a, b' : nat</em

浏览 51提问于2021-09-28得票数 0

回答已采纳

1回答

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

functional-programming、coq、verification

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

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

回答已采纳

1回答

如何让Coq接受以下Fixpoint？

coq

我正在尝试为lambda演算编写一个替换函数，在递归调用e上的替换之前，如果是lambda抽象(\x.e)，我必须在e中重命名变量。我如何在Coq中表示这种逻辑？下面是一个最小的例子，对于这个例子，Coq给出了它不能猜测递减参数的错误。在简化的替换中，为什么Coq不能得到相同感应大小的e余量？Fixpoint replace (x: nat) (y: nat) (

浏览 17提问于2017-12-23得票数 3

回答已采纳

点击加载更多