coq 相关问题

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

在mathcompssreflect中是否有对古典逻辑的支持？

例如，coq的标准库里有一个古典逻辑的包，里面有古典逻辑中的词法，比如涉及forall和existence的词法(https:/coq.inria.frlibraryCoq.Logic.Classical_Pred_Type...)。

coq ssreflect

回答 1 投票 3

ev0: even 0

我通过以下格式定义了偶数。归纳偶数： nat -> Prop :=

coq theorem-proving

回答 1 投票 0

如何在Coq中证明以下内容？

如何在Coq中证明以下内容？(p->q)->(~q->~p)这是我开始的。Lemma工作：（forall p q : Prop，(p->q)->(~q->~p))。证明.Intros p q.Intros p_implies_q not_q......。

logic coq

回答 1 投票 1

如何用ssreflect反思：无法用 "n=n0 "统一?x==?y

EDIT：我找到了! 我都忘了还有个胁迫。请忽略这个:) 我正在学习ssreflect，在这里被卡住了，不知道该如何进行。我的证明状态如下：n，n0 : nat ======================================================================================================================......

coq ssreflect

回答 1 投票 0

在Coq中指定导出文件的路径？

我正在编写我自己的第一个Coq文件，但在导出另一个用户定义的文件（由《软件基础》一书定义）时遇到了麻烦。问题是我当前的Coq文件的路径是CoqNWA.v ...。

coq

回答 1 投票 0

如何在coq中反过来使用定理a=b？

假设我有一个定理L，说forall x，x + 1 + 1 = x + 2.如果我的目标是a + 1 + 1 = b的形式，我可以写一个命令重写L，得到a + 2 = b的形式的目标。如果我的目标是a+1+1=b的形式，我可以写一条命令重写L，得到a+2=b的目标，但是，如果我的目标是......。

logic coq proof

回答 1 投票 0

Coq的类型系统CiC和lambda立方体之间是什么关系？

我阅读了https://en.wikipedia.org/wiki/Lambda_cube#Formal_definition，并对CiC和lambda多维数据集之间的关系感到困惑。据我了解，CiC扩展了CoC，后者是lambda的一个角落...

coq type-systems

回答 1 投票 0

在Coq中如何对自然数使用mod算术（特别是Zplus_mod定理）？

我想应用库定理：定理Zplus_mod：总体a b n，（a + b）mod n =（a mod n + b mod n）mod n。其中a b n预期为Z类型。我在...

logic coq mod coq-tactic

回答 1 投票 0

引入假设的策略，然后立即对其进行另一种策略

[当我的证明状态为H->目标时，我经常使用模式introsH。*某些策略* H.其中某些策略可以是“ inversion”或“ apply _ in”，等等。如果有一些...