Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
根据某些定理，我们知道类型A等于类型B.如何在类型检查期间将其告知Coq编译器？我想实现一个非空树，使每个节点都知道它的大小：Inductive Struct：...
我正在尝试编写以下函数：Ltac restore_dims：=使用|重复匹配目标[| - context [@Mmult？m？n？o？A？B]] =>让Matrix m'n'：= A的类型...
如何在Prop中证明一些明显符合逻辑的 - list_get问题
问题是我不能在不跳过步骤的情况下在H上应用归纳法。我应该得到一些instr0来应用标准引理：Lemma get_Some {A}（l：list A）n x：list_get l n = Some x -...
引理rev_firstn：forall（x：list bool）（n：nat），rev（firstn n x）= firstn n（rev x）。我花了很多时间在这上面。我从一个明智的目标开始，但最终总是有一个目标......
如果我像这样定义乘法（drugi_c），我该如何证明，例如X * 0 = 0？ （如何通过定义证明某事？）Fixpoint drugi_c（x y：nat）：nat：=匹配x，y与| _，O => O | O，_ =＆...
对于归纳类型nat，生成的归纳原则在其语句中使用构造函数O和S：Inductive nat：Set：= O：nat | S：nat - > nat nat_ind：forall P：nat - > Prop，...
对于我的研究，我在Coq中为nat类型写了一堆函数，并证明它们是正确的。现在我需要为类型N编写相同的函数，但证明它们的正确性似乎很痛苦......
我正在寻找关于nats的这个引理。我希望它已经存在于其中一个Coq库中，所以我不必证明它。 forall m n：nat，（S m <n）％nat - >（n - （S m）<n）％nat请...
定理mult_comm：forall m n：nat，m * n = n * m。证明。前奏。感应 - 简单。重写（mult_0_r m）。反思。 - 简单。改写
目标forall（w x y z：string），w <> x - >（if（eqb_string w x）然后y else z）= z。证明。前奏。通过琐碎重写false_eqb_string。反思。 QED。 false_eqb_string是一个...
我有一对平凡不兼容的地图。我想知道什么是优雅/自动化的方式来获得它的证明。需要导入Coq.Strings.String。 （*前奏：total_map数据......
我有一个问题，关于证明函数nat - > QArith.Q（Coq的标准库中的有理数）是单调的（总是不减少的）作为关于在Coq中处理有理数的练习的一部分。 ...
基本上，我想证明以下引理，但我遇到麻烦，因为我似乎无法直接重写lambdas内部。但我觉得这应该是可能的，因为如果我是“......
我已经定义并证明了以下引理：NM.In k m - > {NM.In k m0} + {NM.In k m1}。我还可以证明一个对称引理：{NM.In k m0} + {NM.In k m1} - > NM.In k m但是当我...
我有以下目标：1 subgoal ______________________________________（1/1）（if（a =？a）％string || false然后#a :: nil else nil）= nil因为显然a = a，我想知道为什么这个策略“简化“......
如何在Coq中证明（p - > q） - >（~p \ / q）
我试图用公理证明（p - > q） - >（~p / q）使用Axiom：Axiom重言式：forall P：Prop，P \ / ~P。我试图将~p / q转换成〜 p / p应用p - > q。那样做......
我有一个类型为T的族，用自然数来计算。如果某种类型有人居住，那么下一种类型也有人居住。 （我可以说家庭是“向上居住的”吗？）让我们假设第n个......
我无法找到N选择k在Coq标准库中是不可或缺的证据。什么是这个引理的简短自足证明？引理事实除以N k：k <= N - > Nat.divide（...