Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我正在Coq中实现一些领域理论和表义语义，但是被一些技术问题卡住了。首先，我定义了流，定义为CoInductive Stream (D : Type) := ...
我对l'进行归纳。当第一次进行归纳时，在第二次归纳n::[],n::n0::t后，我遇到了[]和n::l''两种情况。我想简化一下，在执行两次归纳后 ...
如何在Coq中实现开放公式？我觉得Coq的Prop就是封闭式的意思，但是我也想用开放式，比如x=0，如果说x在R中，检查x=0，（*没有找到引用x ....
我请求您的帮助，因为我想知道是否可以允许在Coq中定义潜在的无限fixpoints，只是为了检查当前的定义是否最终产生......
如果有人能给我解释一下证明函数在下面这个简单的例子中是如何使用的，那将有助于我对'programsproofs'并行的理解。定理ex1: forall n:nat, 7*5 < ....
关于coq的非常基本的问题。如何定义以下两种归纳类型？类型1包含：o fo, ffo, fffo......k, sk, ssk, sssk......。请注意，这里的f也可以用表征......。
我在小于或等于的情况下使用destruct命令，在小于的情况下使用同样的命令。我在应用(ltb_correct)命令时遇到了问题，错误信息是 "this command is not found."。...
我想写一个函数，其类型是forall n, option (n = 1)。我选择option作为altertnative来反射，避免给出否定情况的证明。所以，Some扮演了ReflectT的角色......。
我试图证明eqb_neq：定理eqb_neq : forall x y : nat, x =?y = false x <> y.这是我目前的证明状态。在证明过程中，我到了最后一步，我只需要... ...
我怎样才能让Coq识别两个类型，这两个类型分别从一个模块中导入，而这个模块是由一个模块漏子创建的，使用相同的参数，但却出现在不同的模块中，它们实际上是......
经过一番练习，我达到了以下证明状态。tail1是nat列表模式生成器，lng是泛化的）1子目标n'：nat IH_n'：forall lng：nat，lng > n'-> nth ... ...
我在证明一个我定义的函数时遇到了很大的困难，甚至是非常简单的外延。这是我的定义。要求导入列表 要求导出 Omega。要求导出 FunInd。要求 ...
我想在Coq中编写和调试代码，类似于我在Python、R等中编写代码的方式。具体来说。我有一个终端窗口，在那里显示我的code.v文件，例如： Definition double (x:nat) : nat := ...
在mathcompssreflect中是否有对古典逻辑的支持？
例如，coq的标准库里有一个古典逻辑的包，里面有古典逻辑中的词法，比如涉及forall和existence的词法(https:/coq.inria.frlibraryCoq.Logic.Classical_Pred_Type...)。
如何在Coq中证明以下内容？(p->q)->(~q->~p)这是我开始的。Lemma工作：（forall p q : Prop，(p->q)->(~q->~p))。证明.Intros p q.Intros p_implies_q not_q......。
如何用ssreflect反思：无法用 "n=n0 "统一?x==?y
EDIT：我找到了! 我都忘了还有个胁迫。请忽略这个:) 我正在学习ssreflect，在这里被卡住了，不知道该如何进行。我的证明状态如下：n，n0 : nat ======================================================================================================================......
我正在编写我自己的第一个Coq文件，但在导出另一个用户定义的文件（由《软件基础》一书定义）时遇到了麻烦。问题是我当前的Coq文件的路径是CoqNWA.v ...。