coq 相关问题

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

Coq - 如何证明eqb_neq?

我试图证明eqb_neq：定理eqb_neq : forall x y : nat, x =?y = false x <> y.这是我目前的证明状态。在证明过程中，我到了最后一步，我只需要... ...

coq proof coqide

回答 1 投票 0

Coq - 统一来自具有相同参数的模块漏斗的类型？

我怎样才能让Coq识别两个类型，这两个类型分别从一个模块中导入，而这个模块是由一个模块漏子创建的，使用相同的参数，但却出现在不同的模块中，它们实际上是......

module coq

回答 1 投票 1

为什么Coq不能统一目标和假设？

经过一番练习，我达到了以下证明状态。tail1是nat列表模式生成器，lng是泛化的）1子目标n'：nat IH_n'：forall lng：nat，lng > n'-> nth ... ...

coq

回答 2 投票 1

不能证明关于非标准递归函数的琐碎定理。

我在证明一个我定义的函数时遇到了很大的困难，甚至是非常简单的外延。这是我的定义。要求导入列表要求导出 Omega。要求导出 FunInd。要求 ...

coq coq-tactic

回答 1 投票 1

如何在Linux中使用交互式shell来编写Coq代码？

我想在Coq中编写和调试代码，类似于我在Python、R等中编写代码的方式。具体来说。我有一个终端窗口，在那里显示我的code.v文件，例如： Definition double (x:nat) : nat := ...

linux shell coq

回答 1 投票 0

在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”，等等。如果有一些...

coq ssreflect

回答 1 投票 0

如何证明（0 <> 2）->在Coq中为假？

[证明一个引理后，我最终达到了一个前提，我的前提是H：0 = 2，我必须证明是错误的。问题：如何推断前提H为假以得出结论？

logic coq

回答 1 投票 0

如何在coq中使用rewrite命令进行内部子表达式？

我有一个引理，告诉加法通勤：引理通勤：对于所有x y，加x y =加y x。现在，在我的目标中，我试图证明：加（加x（S y））z =加x（S（加y z））...

logic coq induction

回答 1 投票 0

在Coq中如何使`simpl`命令仅执行一步缩减？

我对add的定义如下：定点添加n m：=将n与|匹配。 0 => m | S p =>加p（S m）端。在文件的后面，我试图证明以下目标：加（S n）0 = S n I ...

logic coq induction

回答 1 投票 0

在Software Foundations Trie模块中，is_trie的良好实现是什么？

该模块在此处：https://softwarefoundations.cis.upenn.edu/vfa-current/Trie.html如果搜索“ Definition is_trie”，则可以找到以下定义以及我不确定的部分。 ..

coq

回答 1 投票 0

证明一个常数是偶数

鉴于偶数的归纳定义，如何最好地证明1024是偶数？重复将even_S减小到零肯定不是正确的方法。

coq

回答 1 投票 -1

如何在Coq中使用德摩根法律将“并非永远”替换为“存在”？

我正在学习Coq语言并尝试证明以下陈述：引理ex4：forall（X：Set）（P：X-> Prop），〜（forall x，〜（P x））->（存在x ，（P x））。在我的证明开始时：...

coq

回答 1 投票 1

coq 相关问题

最新问题