问题标签 [coq-tactic]

考虑以下部分证明：

执行到这一点会给我以下信息：

我想S从目标中删除 s ，获得目标n = m。有没有这样做的策略？

考虑以下玩具练习：

在这一点上，我有以下内容：

我想将目标分成两个子目标，m = n并且n = m. 有没有一种策略可以做到这一点？

我试图证明以下关于自然顺序的玩具定理：

在纸面上，这是对 的简单归纳Le (S n) m。特别是，基本情况le_n是微不足道的。

不过，在 Coq 中，以归纳法开始我的证明给了我以下信息：

...在这种情况下，我被阻止了。

我应该如何继续？

我想证明减法不会在 Coq 中通勤，但我被卡住了。我相信我想在 Coq 中证明的陈述会写成forall a b : nat, a <> b -> a - b <> b - a

到目前为止，这是我所拥有的证明。

我想我可以C : a <> b用来反驳目标a = b。

我正在尝试使用数学组件库来证明以下内容：

最初，我试图在orbigsum_aux的文档中找到一些等效的引理，但我找不到；所以这就是我到目前为止所能做的：ssralgbigop

欢迎任何有关相关引理的帮助或指示。

我有一个证明脚本，其部分如下所示：

似乎它将是用于;干净地解决的选择候选者，不幸的是，假设到处都是。如何将各种子证明折叠在一起？

如果我有以下情况：

我想抓住

无需将其硬编码到我的证明中（即，使用pose）

在 LTac 中有没有一种干净的方法可以做到这一点？

我有以下设置（对不起，如果它对 MCVE 来说有点长）并试图证明最后一个定理，但我遇到了困难，因为它无法统一态射的类型，因为它们依赖于理论上不同的对象类型，即使对象类型相同。

是否有分解具有依赖类型的构造函数的一般策略？injection并inversion产生似乎无用的结果ob_fn（我可以很容易地证明等价定理）而不是morph_fn.

我正在尝试编写一种用于柯里化函数的策略，包括普遍量化的函数。

如何扩展我的curry策略来处理普遍量化的函数？

我天真地期望checkForall H成功，但事实并非如此。

在他的书Certified Programming with Dependent Types中，Adam Chlipala讨论了模式匹配对依赖类型的限制：

问题是统一变量可能不包含本地绑定变量。

这是我在这里看到的行为的原因吗？