问题标签 [ltac]

在 Ltac 中，上下文模式可用于构建Ltac 级函数，该函数接受 Gallina 项并通过填充孔来构造 Gallina 项。我想具体化这个功能并在 Gallina 的级别上使用它，而不是 Ltac。

例如，以下代码使用元变量而不是上下文模式工作。

但是以下代码不起作用，因为x在填充模式之前我无法将变量带入范围：

以下内容也不起作用，因为我无法在 Gallina 中使用 Ltac：

但是下面的代码表明我的上下文模式像我认为的那样工作：

虽然这个示例很简单，因为目标是单个应用程序，但总的来说，我想使用上下文模式来匹配更复杂的目标，然后使用这些模式来构建 Gallina 函数。这可以做到吗？

这个问题是关于我正在做的一个项目，即在 Coq中编写Principia Mathematica代码。Principia导出了推理规则，其中之一是 Syll：

∀ PQR : 道具, P→Q, Q→R : P→R

我正在尝试创建一个对 Syll 推理形式进行编码的 Ltac 脚本。以下来自（Chlipala 2019）的 MP 策略非常有效：

这里我认为“=>”右边的策略专门将H1应用于H2。现在相关的 Syll 策略不起作用：

我在应用它时遇到的错误（在下面的示例中）是：

没有匹配的匹配子句。

我不确定为什么这是由此产生的错误。引入经典逻辑，证明为定理Syll2_06，即(P→Q)→((Q→R)→(P→R))。事实上，基本上是 Syll Ltac 被应用于定理 Trans2_16 的证明（见下文）。所以我不确定为什么将代码转换为 Ltac 脚本不起作用。

也许我误解了 Ltac 匹配在做什么，以及“=>”右侧的策略应该是什么。但是根据查看Coq 手册，可能是策略的左侧是问题所在，可能是因为 H1 不适用于 H2。

进一步的建议，特别是解释 Ltac 和/或我的思考方式错误的建议，将不胜感激。

这是我正在尝试做的一个简短示例。

假设我有关系

我也有以下ltac Ltac simplify := autorewrite with blah

我想定义一个 ltac，它确实简化为“可分割”目标中的第一项。就像是

当我在下面尝试上述内容时，

我得到一个

是否可以将 ltacs（即使是仅涉及自动展开和自动重写的简单方法）限制在目标的子表达式中？

谢谢你。

我是 Coq 的新手，目前在Software FoundationsIndProp章节。我很想学习编写自己的简单策略来自动化某些类型的推理，但不幸的是，作为初学者，官方文档对我来说有点难以理解。

我想写一个适用于以下场景的策略：

• 目前的目标是False
• 有一个形式的假设P \/ False

基于以下引理，我们应该能够~P在这种情况下将当前目标替换为：

我们可以手动使用引理来达到预期的效果：

我想自动化这个，所以我写了一个简单的策略来在目标和上下文匹配这个场景时应用引理：

它按预期工作。但是，当有多个假设与模式匹配时，我们无法在它们之间进行选择：

我假设解决这个问题就像将所需的假设orfalse作为参数传递给策略一样简单：

但是，在证明中使用它失败了：

?P如果我用 just和 return替换嵌套匹配的第一种情况idtac ?P，它只会打印我传入的假设的名称（例如H1or H2），所以我的猜测是匹配发生在标识符本身而不是假设上。

所以，我的问题是： 如果我将假设的名称传递给策略，我如何正确匹配该假设的结构？ 谢谢！

这很清楚destruct HifH包含合取或析取。但我无法弄清楚它在一般情况下的作用。它做了一些奇怪的事情，尤其是如果H: a -> b.

一些例子：

假设刚刚被破坏：

另一个：

现在我有两个分支：

第三个例子。这无法证明，但对我来说仍然没有意义：

x = x现在我必须在第二个分支中证明！

所以，我显然不明白是什么destruct H。

我是 Coq 和编写策略的新手，我一直无法弄清楚你是否可以定义更复杂的策略，比如内置策略。例如，假设我有一个tac1采用两个参数的策略，我定义tac2为

然后这就像我所期望的那样工作，但我真的很想能够tac2提出一个假设，比如tac2 arg in H. 我可以看到我可以将假设作为额外的参数给出，但是我不能在目标中使用它，我也希望能够像tac2 arg in *.

这样的事情是否可能，如何实现？

我找到了这个关于如何将介绍模式添加到你定义的策略的答案，它引导我到这个页面，Tactic Notation但我无法从中弄清楚我想要的是否可能。

我对 Coq 的策略symmetry和transitivity实际工作方式很感兴趣。我已经阅读了 Coq 手册，但这仅描述了它们的工作，而不是它们如何对证明进行操作并更改证明状态。作为我正在寻找的示例，在Interactive Theorem Proving and Program Development中，作者指出“反身策略实际上是apply refl_equal”（第 124 页）的同义词。但是，作者请读者参考symmetry和的参考手册transitivity。我还没有找到对这两种策略以相同方式同义的事物的良好描述。

为了澄清起见，我问的原因是我已经定义了一个路径空间（就像在paths {A : UU} : A -> A -> UUUniMatha = b中一样），它就像一个等价关系，除了它a = b不是一个命题而是一个类型。出于这个原因，我无法将此关系添加为使用 的等价关系Add Parametric Relation。我正在尝试为这种路径空间关系制作 Ltac 的版本，symmetry但transitivity我不知道如何更改证明状态；了解如何symmetry以及transitivity实际工作可能会有所帮助。