问题标签 [coq-tactic]

我有目标

，但我不记得“四边形”的定义，也不想开始搜索它的定义。

有没有一种策略可以让我用它的定义快速替换 quad？

或者我必须记住并使用

?

我如何证明简单的事实

?

我的逻辑是

1. 对于任何 nat n，n > 0 或 n = 0。

2. S x = 0 导致矛盾。

我的主要问题是我无法记住所有这些关于 nat 的琐碎定理/引理，而且我对搜索命令的了解不够。

我试图“破坏 gt”或“>”构造函数，或者对“gt”进行一些反转。但我无法弄清楚语法或这是否是正确的方向。

任何帮助（除了像欧米茄这样的重物）都非常感谢。

我正在测试 Coq 重写策略模关联性和交换性 ( aac_tactics)。以下示例适用于整数 ( Z)，但当整数替换为有理数 ( Q) 时会生成错误。

Require Import ZArith.用etc替换Require Import QArith.的时候报错：

错误：策略失败：未找到模数 AC 的匹配发生。

在aac_rewrite H.

Z和之间也存在类似的不一致问题Q，这与Z/Q范围是否开放有关。

但我不明白为什么 aac rewrite 在这里不起作用。不一致的原因是什么，如何使它对Z和表现相同Q？

我无法理解相等和本地定义之间的区别。例如，在阅读有关该set策略的文档时：

记住术语作为身份

这表现为 * 中的 set ( ident := term ) 并 使用逻辑（莱布尼茨）相等而不是局部定义

的确，

1. set (ca := c + a) in *.例如ca := c + a : Z在上下文中生成，而

2. remember (c + a ) as ca.Heqca : ca = c + a在上下文中生成。

在案例 2 中，我可以使用生成的假设，如rewrite Heqca.，而在案例 1 中，我不能使用rewrite ca。

案例1的目的是什么？在实际使用方面它与案例2有什么不同？

另外，如果两者之间的区别是根本的，为什么在文档（8.5p1）中被remember描述为的变体？set

从 Coq 参考手册（8.5p1）中，我的印象是revert的倒数intro，但generalize在一定程度上也是如此。例如，revert和generalize dependent下面似乎是一样的。

只是generalize比 更强大revert吗？

此外，文档在解释有关以下内容时有点循环generalize：

这种策略适用于任何目标。它概括了关于某个术语的结论。

generalize类似于 lambda 演算中的抽象运算符？

我想知道 Coq 中是否存在一种类似倒置的策略，它适用于目标而不是其中一个假设？也就是说，如果有某种策略可以在目标上反转相同的构造函数。

举个愚蠢的例子，

， 这使

我想反转前两个 S，所以剩下要证明的是

我的问题是

1. 构造函数的这种“反转”是否合理？

2. 如果逻辑是合理的，那么 Coq 中是否有这样做的策略？

我正在阅读 Coq 参考手册 (8.5p1) 关于

战术的局部应用

可以使用以下形式将不同的策略应用于不同的目标：

[ > expr1 | ::: | 解释]

表达式expri被计算为 vi，因为 i = 0；...; n 一切都必须是战术。vi 应用于第 i 个目标，对于 = 1；...; n. 如果重点目标的数量不完全是 n，它就会失败。

所以我做了一个小测试，有两个目标，试图对idtac每个目标应用两种微不足道的策略，如下所示：

但是，我收到一条错误消息，告诉我只需要一种策略：

错误：进球数不正确（预期为 1 个战术）。

我很困惑。有人可以解释我做错了什么，正确的用法是什么？

我无法理解multiple successesCoq (8.5p1, ch9.2) 中的分支和回溯行为的概念。例如，从文档中：

回溯分支

我们可以使用以下结构进行分支：

expr1 + expr2

战术可以被看作是有几个成功的。当一个策略失败时，它要求先前策略的更多成功。expr1 + expr2 具有 v1 的所有成功，然后是 v2 的所有成功。

我不明白的是，为什么我们首先需要多次成功？一次成功还不足以完成证明吗？

同样从文档中，似乎有一些成本较低的分支规则以某种方式“有偏见”，包括

和

为什么我们需要更昂贵的选择+而不总是使用后者更有效的战术？

我试图展开Fixpoint定义并获得定义的主体。但是 Coq 不会从字面上给出定义的主体。相反，它给了我一些以 开头的东西(fix ...)，我无法使用。

例如，从Coq.Init.Wf证明以下内容

状态是：

现在，Fix_F在 RHS 上的定义与 LHS 完全相同：

我试图通过以下方式使其trivial平等：

然而，我(fix Fix_F ... )在 RHS 上得到了类似的东西，我不能再沿着这条线继续前进：

问题是：

有没有办法将上面的内容展开Fixpoint到它的功能体上？

注意：我知道有一种解决方法可以证明这个例子。

但如果它是有效的，我对unfold-ing 方法更感兴趣。

给定 Coq 中的任意归纳命题定义，在对归纳命题调用归纳策略时，是否有一个通用公式可以推导出合理的 disj_conj_intro_pattern 使用？

通常，对于任何一个归纳定义的构造函数，完整的 intro_pattern 可能需要（命名）多个假设和多个归纳假设，在这种情况下，模式中提供的名称顺序可能包括所有参数，然后一个假设和一个相应的归纳假设，然后是一个或多个由假设和归纳假设组成的附加对。例如，软件基础包括以下内容：

在这个例子中，MApp 和 MStarApp 的 intro_patterns 各有两对假设和归纳假设——大​​概是因为这两个构造函数都包含以下形式的表达式

x -> y -> z

关于这一点，当前的参考手册似乎只说

归纳术语为 disj_conj_intro_pattern

这表现为归纳术语，但使用 disj_conj_intro_pattern 中的名称来命名上下文中引入的变量。disj_conj_intro_pattern 通常必须是 [ p11 … p1n1 | … | pm1 ... pmnm ] 其中 m 是术语类型的构造函数的数量。在第 i 个目标的上下文中通过归纳引入的每个变量都从列表 pi1 ... pini 中按顺序获取其名称。如果没有足够的名称，则归纳为要引入的剩余变量发明名称。更一般地说，pij 可以是任何分离式/连接式引入模式（参见第 8.3.2 节）。例如，对于具有一个构造函数的归纳类型，可以使用模式表示法 (p1 , ... , pn) 代替 [ p1 ... pn ]。

这似乎没有指定如何为给定的归纳定义确定完整的 disj_conj_intro_pattern 的正确形式。

我上面的经验观察是1）每个构造函数的形式参数首先出现，然后是构造函数的假设与相应的归纳假设配对；2）假设和归纳假设对的数量来自构造函数中假设的数量，事情的总和？或者还有更多吗？

除了参考手册的战术章节和第 1 章中关于 Gallina 语法模式的一般性讨论之外，还有其他相关文档吗？