Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我想对Peano nats进行归纳，但我想证明属性P超过nats 1 ... n。 Coq是否提供了这样做的策略/工具？
我想证明自然数不包括0的东西。所以我的属性P的基本情况是P 1而不是P 0.我正在考虑使用n> = 0作为目标中的假设，但是有......
我有以下Coq实现的整数除法与余数。当我将它提取到Haskell时，一切正常。我将Coq版本与生成的Haskell版本进行了比较并试图...
引理In_map_iff：forall（A B：类型）（f：A - > B）（l：列表A）（y：B），in y（map f l）存在x，f x = y / \ In x l。证明。分裂。 - 概括依赖y。概括......
我正在尝试在Coq中编写一个简单的strchr函数，然后将其导出到Haskell。我面临的导入问题可能类似于这篇文章（？），但我似乎无法解决它们。这是我的coq代码：...
是否存在类型理论，其中相同形状的归纳数据类型的等价性是可表示的？
假设我有两个归纳定义的数据类型：归纳list1（A：类型）：类型：= | nil1：list1 A | cons1：A - > list1 A - > list1 A.和Inductive list2（A：Type）：类型：= | nil2：......
Coq初学者，我最近独自完成了“逻辑基础”的前7章。我试图通过感应在∀n> = 3,2n + 1 <2 ^ n的Coq中创建证明。我从...开始
在我的证明中破坏n后，我陷入以下困境：1 subgoal n：nat X：输入h：X t：list X n'：nat E：n = S n'H'：length t = n'IHl：长度t = n - > nth_error tn =无......
在Coq中，假设我有一个固定点函数f，其匹配定义在（g x）上，我想在证明中使用形式（g x = ...）的假设。以下是一个最小的工作示例（在...中
有没有办法使用Coq的类型类的递归？例如，在为列表定义show时，如果要递归调用list的show函数，那么你将不得不使用一个fixpoint ...
变量A B：Prop。定理proj1：A / \ B - > A.为了学习，我试图通过使用and_ind明确写下证明项来证明这个定理。我会假设正确的证据......
任何人都可以告诉我为什么当我试图证明以下涉及理性的目标时，战术“领域”不起作用？ nat_to_Q 3 * nat_to_Q n * nat_to_Q n + nat_to_Q 3 * nat_to_Q n + nat_to_Q 3 * ...
对于像自然数nat这样的简单归纳类型，很容易证明两个构造函数（零和后继）给出所有可能的自然数，引理nat_destruct（n：nat）：n = O \ / ...
我尝试使用Infix“⊂”实现S是Z的子集：=（包括Z）（在70级）。 （我们的教授提供了这个，但当我尝试写forall（S⊂Z），（插入定理）一个错误信息...
我正在尝试通过Software Foundations Coq书（http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html），但是当我编译Induction.v（看起来像http： //www.cs.uml.edu/~rhenniga / ...
使用Coq中的`Function`和`Program`来简化依赖类型编程的生活
我正在尝试使用Program Fixpoint在Coq中实现一个依赖类型的STLC评估器。由于语言没有定点运算符，我认为评估者应该终止，尽管......
我有一种情况，我定义了归纳数据类型t和它的部分顺序（c.f. le_refl，le_trans和le_antisym）。订单在le_C情况下具有这种特殊性，即......的顺序
对于任何A B：Prop，总和A B和sumbool A B是同构的，通过以下定义from_sumbool（A B：Prop）（x：sumbool A B）：sum A B：= match x with |左l => inl l |对r =＆...
我正在研究使用结构同余的证明，其定义与此示例非常相似：需要导入Nat。需要导入Omega。归纳expr：= | Const：nat - > expr |添加：...
鉴于这两种类型，归纳单位：Set：= tt。 Inductive otherUnit：Set：= ttt。 Coq可以证明它们是不同的，即unit <> otherUnit？两者都是排序集中的单例类型，所以它不是......