coq 相关问题

Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。

从不同类型的转换

coq

回答 1 投票 -1

Rel：反对称理解

逻辑基础中的相关章节。给了我要理解的最佳解决方案：定义反对称{X：类型}（R：关系X）：= forall ab：X，（R ab）->（R b ...

coq logical-foundations

回答 1 投票 0

如果参数匹配模式，则为额外的类型构造函数

让我们定义一个表示集合的类型：归纳mySet：= | funSet：mySet-> mySet-> mySet | prod：mySet-> mySet-> mySet。我们有两个类型构造函数：funSet A B-一组...

coq

回答 1 投票 0

从自动战术的角度看，符号和定义之间有什么区别？

在《 Programming Language Foundations的STLC》一章中，我们找到了以下内容：（** [idB = \ x：Bool。x] *）表示法idB：=（abs x Bool（var x））。（** [idBB = \ x：Bool-> Bool。x] *）表示法idBB：...

coq coq-tactic

回答 1 投票 0

coq中的链定义

我正在阅读有关与Coq合作的软件基础书籍。我目前在“战术”一章，但仍处于forall_exists_challenge上。我想否定测试谓词...

coq

回答 1 投票 0

自然数零检验的矛盾

我有一个不等于零的自然数。我想证明，如果它等于零，那么它将为假。引理非零：forall n，n <> 0-> n =？ 0 =错误。证明。 ...

coq

回答 2 投票 1

Coq / SSReflect：反映&&和/ \]时如何进行案例分析>

我具有以下反射谓词：要求导入mathcomp.ssreflect.all_ssreflect。感应反射（P：支撑）（b：布尔）：支撑：= | ReflectT（p：P）（e：b = true）| ReflectF（np：〜P）（e：...

coq coq-tactic ssreflect

回答 2 投票 1

检查自然数

我有不等于零的自然数。我想证明，如果它等于零，那么它就为假。引理非零n：n <> 0->（n =？0 =否）。证明。简介倒置H。

coq

回答 1 投票 0

为什么vm_compute在定义中比Coq中的证明更快？

我有一个Fixpoint函数f和以下形式的引理：引理L：forall x，f x = true-> P x。当我定义一个变量a且其f a = true时，我可以通过以下方式证明P a：引理：...

coq

回答 1 投票 0

如何将用户定义的枚举类型设为`finType`？

我想在Coq / SSReflect中创建归纳定义的枚举类型，就像归纳E：类型：= A | B | C.是finType，因为它显然是有限类型。我有三种解决方案，但是全部...

coq ssreflect

回答 1 投票 4

用假设替换假设而不添加其前提作为子目标

这是我为使用Is_true而尝试构建的一些自动化的一部分。我有引理Is_true_implb_impl：（Is_true x-> Is_true y）Is_true（implb x y）。我有一个假设...

coq

回答 1 投票 0

在Coq中将非A转换为A-> False

我想通过假设A并找到False来证明不是A。将目标不是A转换为A-> False的最短，最通用的方法是什么？我尝试了exfalso，但它并未在我的假设中添加A……

coq theorem-proving

回答 1 投票 1

Coq：要求导出问题

我的问题似乎很普遍，但是找不到任何答案可以解决。我正在遵循Coq的软件基础课程，因此我要执行以下命令：>从LF要求导出...

coq coqide

回答 1 投票 2

“非严格正发生......”

我尝试定义以下类型归纳T：类型 - >类型：= |我：T的NAT | F：FORALL A，（T NAT - > T A） - >牛逼A.我收到以下错误：非”严格正发生...

coq

回答 1 投票 2

证明（未完全）不相干破坏COQ平等时，当

我有一个依赖型该款机型在一个过渡系统有限路径。过渡系统有一个函数R能产生一个命题说法是否有状态S和S'与之间的边缘......

coq dependent-type

回答 1 投票 1

在COQ依赖记录破坏平等

给定从属记录类型：记录FinPath：类型：= {mkPath fp_head：S I; fp_tail：FinPathTail fp_head}。和两个对象...

coq dependent-type

回答 1 投票 2

coq基础知识：bin_to_nat函数

我通过了Logical Foundations课程，并停留在Basics的最后一个摘要上：用二进制数将转换器写入其一进制表示形式：归纳bin：类型：= | Z |一个（...

coq logical-foundations

回答 3 投票 2

少于功能

我正在通过coq课程“逻辑基础”。解决问题：功能少于或等于：Fixpoint leb（n m：nat）：bool：=与n匹配n O => true | S n'=>匹配m ...

coq logical-foundations

回答 1 投票 1

携带样张的感应式

在“软件基础”中有一个练习，我一直试图正确解决一段时间，但实际上我试图写下被问到的函数的问题......

coq logical-foundations

回答 1 投票 1

Coq战术是正确的联合还是左联合？

我正在通过软件基础并得到了一个例子：repeat（try（left; reflexivity）; right）。并且很困惑这意味着什么。例如，我们得到：尝试[（左;反身性）;对 ] ...

coq coq-tactic logical-foundations

回答 1 投票 1

coq 相关问题

最新问题