问题标签 [coq-tactic]

在 Coq 中，当试图证明记录的相等性时，是否有一种策略可以将其分解为所有字段的相等性？例如，

有没有一种策略可以减少这种情况a = c /\ b = d？请注意，一般来说，任何一个都a b c d可能是大而复杂的证明术语（然后我可以用证明无关公理来解除）。

我见过很多功能上相互重叠的 Coq 策略。

例如，当您在假设中有确切的结论时，您可以使用assumption, apply, exact, trivial, 或者其他。destruct其他示例包括induction非归纳类型（？？）。

我的问题是：

是否存在完整的最小基本策略集（不包括auto等），从某种意义上说，该集可用于证明任何 Coq 可证明的关于自然数函数的定理？

理想情况下，这个最小完整集合中的策略是基本的，因此每个人只执行一个（或两个）功能，并且可以很容易地理解它的作用。

我试图从一个在线课程中证明以下简单的定理，排除中间是无可辩驳的，但在第 1 步几乎被卡住了：

现在我得到：

如果 I apply H，那么目标将是P \/ ~P，它被排除在中间并且不能被建设性地证明。但除此之外apply，我不知道可以对假设做些什么P \/ (P -> False) -> False：暗示->是原始的，我不知道如何destruct分解或分解它。这是唯一的假设。

我的问题是，如何仅使用原始策略（如这里所描述的，即没有神秘auto的 s）来证明这一点？

谢谢。

在使用 Coqapply ... with策略时，我看到的所有示例都涉及显式指定要实例化的变量的名称。例如，给定一个关于等式传递性的定理。

apply对它：

请注意，在最后一行apply trans_eq with (m := 1).中，我必须记住要实例化的变量的名称是m，而不是o或n或其他一些名称y。

对我来说，是否在定理的原始陈述中使用m n o或x y z使用都无关紧要，因为它们就像虚拟变量或函数的形式参数。有时我不记得我在定义定理时使用的具体名称或其他人放在不同文件中的名称。

有没有一种方法可以让我引用变量，例如通过它们的位置并使用类似的东西：

在上面的例子中？

顺便说一句，我试过了：apply trans_eq with (1 := 1).得到了Error: No such binder.

谢谢。

我有一个关于如何在 Coq 中重新排列术语的一般性问题。例如，如果我们有一个 term m + p + n + p，人类可以快速将这些术语重新排列成类似的东西m + n + p + p（隐式使用 plus_comm 和 plus_assoc）。我们如何在 Coq 中有效地做到这一点？

举一个（愚蠢的）例子，

现在，我们有

我的问题是：

如何m + n + p + p有效地重写 LHS？

我尝试使用rewrite plus_comm at 2，但它给出了一个错误Nothing to rewrite.只需使用重写plus_comm将 LHS 更改为p + m + n + p.

也欢迎任何关于有效重写的建议。

谢谢。

destruct可用于拆分and，或在 Coq 中。不过好像也可以用含蓄？例如，我想证明~~(~~P -> P)

当destruct pff.它工作正常时，但我不知道为什么？谁能为我解释一下？

我想知道是否有办法在 Coq 中证明一个定理时引入一个全新的变量？

对于一个完整的示例，请考虑以下关于列表长度均匀性的属性。

现在我想证明对于任何列表l，如果它length是偶数，则ev_list l成立：

这使：

现在，我想“定义”一个新的自由变量n和一个假设n = length l。在手写数学中，我认为我们可以做到这一点，然后对n. 但是有没有办法在 Coq 中做同样的事情？

笔记。我问的原因是：

1. 我不想将其n人为地引入定理本身的陈述中，就像在前面链接的页面中所做的那样，恕我直言，这是不自然的。

2. 我试过了induction H.，但它似乎不起作用。Coq 无法对length l's ev-ness 进行案例分析，也没有生成归纳假设 (IH)。

谢谢。

假设我有以下策略来检查一个术语是否是文字零：

现在想象一下，我希望该策略接受更多；也许任何可以用零转换的术语。如果这是针对目标的策略，我会这样做

但这对于产生术语的策略来说是失败的：

如何检查战术产生条款中的可兑换性？在这个具体的例子中，减少或x计算它（let xx := eval compute in x

PS：作为参考，未简化的问题是我正在尝试有效地查找一个键，该键可能与FMap由调用序列构建的值匹配add，并且该策略看起来像

在这个实现中，如果不是valuemap 包含一个可转换为value但在语法上不等于它的术语，则该策略将错误地返回None.

在证明过程中，我遇到了一种情况，即当前目标/子目标在同一定理的后期阶段证明是有用的。

是否有一种策略可以将当前目标“保存”为引理，就好像当前目标已被assert编辑一样？

当然，我可以 assert明确地复制并粘贴到目标，或者在当前定理之前写一个单独的引理。但我只是好奇是否存在捷径。

谢谢。

据我了解，Coq 中的函数调用是不透明的。有时，我需要使用unfold它来应用它，然后fold将函数定义/主体转回其名称。这通常很乏味。我的问题是，有没有更简单的方法来应用函数调用的特定实例？

作为一个最小的例子，对于 list l，证明右附加[]不会改变l：

这留下：

现在，我需要应用一次++(ie app) 的定义（假设目标中还有其他++我不想应用/扩展的）。目前，我知道实现这个一次性应用程序的唯一方法是先展开++然后折叠它：

给予：

但这很不方便，因为我必须弄清楚要在fold. 我做了计算，而不是 Coq。我的问题归结为：

有没有更简单的方法来实现这个一次性功能应用程序达到同样的效果？