coq 相关问题

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

Coq集继承

我已经从实数公理证明了许多定理，现在我想将自然定律定义为实数的子集，并重用所有已证明的定理。怎么做到呢？这是一个人工的MRE，它会...

inheritance coq

回答 2 投票 0

离开5-8年后返回Coq证明检查器：如何证明（总n，m：N，（n-（S m））= pred（n-m））？

coq

回答 1 投票 1

在Coq中设置继承

我已经从实数公理证明了许多定理，现在我想将自然定律定义为实数的子集，并重用所有已证明的定理。怎么做到呢？这是一个人工的MRE，它会...

inheritance coq

回答 2 投票 0

避免在带有普通证明的Coq中打印符号

在DeepSpec 2018的第6讲中，讲师检查string_dec的定义，以获得：string_dec：forall s1 s2：string，{s1 = s2} + {s1 <> s2}然后他继续观察...] >

coq proof-general

回答 1 投票 0

证明Coq中“小于”关系的证据

我正在研究软件基础（第1卷：逻辑基础）的IndProp.v中以下定理Sn_le_Sm__n_le_m的证明。定理Sn_le_Sm__n_le_m：nm，S n≤S m→n≤m。证明。 ...

coq theorem-proving coq-tactic induction

回答 1 投票 3

从头证明Coq具有较强的归纳性

我正在证明弱感应和强感应的等效性。我有一个类似的定义：definition strong_induct（nP：nat-> Prop）：Prop：= nP 0 / \（forall n：nat，（forall ...

coq induction

回答 1 投票 1

您如何在Coq中证明（e：p = p）= eq_refl？

我正试图证明这一点：引理eq_eq：全部（U：类型）（p：U）（eqv：p = p），eq_refl = eqv。但是似乎没有办法做到。问题是类型p = p是同一...上的等式...

coq

回答 1 投票 -1

与Coq中的bool和Prop有密切关系吗？

是否有将Prop转换为bool的方法？我知道forall a b：nat，a b-> a a b？如果没有，是否存在...

coq

回答 1 投票 2

[coq中的参数类型

我在此stackexchange帖子上找到了此代码，我对其工作原理感到困惑。特别地，归纳矢量{A：Type}：nat-> Type：= | nil：矢量0 |缺点：forall n，A->向量n ...

polymorphism coq dependent-type parametric-polymorphism

回答 1 投票 0

coq中的泛型相等性

是否有任何策略或事实或其他东西可以将相等性提升到归纳和反向的构造函数中，将归纳构造函数的相等性提升到构造函数参数的相等性，即：...

coq

回答 1 投票 0

如何证明由coq中相同归纳的两个不同构造函数产生的项的不等式？

考虑一下我有一个归纳式：归纳DirectSum {L R：类型}：类型：= |左：L-> DirectSum L R |右：R-> DirectSum L R。我如何证明forall L R：类型，forall l：L，forall r：...

coq

回答 1 投票 0

（（A-> B）/ \（B-> C）->（A-> C）in Coq？

[我正在通过本书的软件基础来学习Coq，并且难以证明以下引理（我需要证明其他定理。）引理if_trans：forall（PQR：Prop），（P-> Q）/ ...] >

coq coq-tactic

回答 1 投票 0

我如何描述向量矩阵的乘法？

我想计算巨大（特定）矩阵的乘积。从复杂性的角度来看，乘积应采用元素表达式的形式。我试图用...

coq ssreflect

回答 1 投票 1

Coq使用带二次蕴涵的精炼

我不确定如何措辞我的问题，因为我不熟悉coq。我想对包含双向蕴涵的一个定理使用优化。示例代码：参数A B C：Prop。theorem t1：A-> B-> C ....

coq coq-tactic

回答 1 投票 0

Coqtop无法加载文件

我目前在Software Foundations – Logical Foundation。简而言之，我得到了错误错误：找不到与后缀<>和前缀LF匹配的逻辑路径的物理路径。我有Coq ...

coq

回答 1 投票 0

列表中元素的位置

我正在使用索引功能在列表nat中任何位置查找element的值。请Plz指导我证明引理的第二部分，如下所示。Fixpoint index（n：nat）（m：...

coq

回答 1 投票 0

coqc：-Q.PLF：没有这样的文件或目录

我正在尝试在coq中编译文件hw5.v，该文件位于软件基础的plf文件夹中。我想解决绑定问题，因此我使用了以下命令：coqc -Q.PLF hw5.v但它不能编译...

coq coqide

回答 1 投票 0

如何使用具有“通常”相等性的MSets来创建有限集类型？

[很抱歉问一个简单的问题，但我一直在寻找答案，而且我还没有找到对我来说足够简单的解释（我不太了解Coq的模块系统）。。

set coq

回答 1 投票 0

证明组中的一般关联性

对于一个项目，我正在通过Coq编码组理论，显然已经给出了3个元素的关联性，但是我努力证明它对于长度为n的字符串成立。也就是说，（x1 * ... * xn）是...

coq associativity

回答 1 投票 0

如何证明某些人的平等

我想证明Coq中两个nat数相等：a，b：nat Heq：一些a =一些b ======================= ==== a = b

coq coq-tactic coqide

回答 2 投票 0

coq 相关问题

最新问题