问题标签 [ltac]

考虑这个简单的发展。我有两种微不足道的数据类型：

现在我介绍一个关系的概念并定义数据类型的排序A并B表示为归纳数据类型：

最后，我引入一个自反性的概念，并证明我的两个关系都是自反的：

两个证明都是用auto策略完成的，第一个证明主要依靠，Hint Constructors第二个证明另外Hint Resolve AOrd_reflexive添加到提示数据库中。

A上面代码的一个丑陋之处在于对关系和B数据类型的排序有一个单独的符号。我希望能够在<=任何地方统一使用。这个答案提供了一个解决问题的方法：使用类型类。所以我引入了一个用于排序的类型类，并重新定义了我的排序关系以使用这个新符号：

但是现在证明自动化中断了！例如：

给我一个目标：

尽管构造函数在提示数据库中，但它auto不再解决。AOrd我可以通过以下方式解决目标constructor：

更多的问题出现在第二个证明中。做完之后：

我的目标是：

再次，auto不再解决这个目标。甚至apply AOrd_reflexive不起作用。

我的问题是：是否有可能通过依赖类型类来获得统一的符号并保持证明自动化的好处？或者是否有不同的解决方案来为各种数据类型提供统一的符号。

我需要在活页夹下概括表达。例如，我的目标中有两个表达式：

和

我想概括一下g _ _ c：

一种方法是先将它们重写为：

第二个进入：

然后，概括(fun x y, g x y c)为somefuntype A -> A -> A。这会将我的表达式变成：

和

这里的困难是我试图概括的表达是在活页夹下。我找不到操纵它的策略或 LTAC 表达式。我怎么能做这样的事情？

我目前正在尝试编写一种策略，该策略使用可以轻松生成的术语（在此特定示例中， from tauto）实例化存在量词。我的第一次尝试：

这种策略将适用于一个简单的问题，例如

但是它不适用于像这样的目标

在这里，我想使用这种策略，相信fwhich tautofinds 将是 just fun x => x，从而替换特定证明（应该是身份函数），而不仅仅是t我当前脚本中的泛型。我该如何编写这样的策略？

有时我有一个最好通过投影到不同空间来完成的证明。目前，我执行以下操作：

我试图用 Ltac 自动化这个：

但我收到以下错误：

这里有什么问题？

我正在尝试理解“上下文”表达式（与context 模式相反）。在手册中是这样描述的：

上下文标识 [ expr ]

ident 必须表示由匹配表达式的上下文模式绑定的上下文变量。此表达式求值用 expr 的值替换 ident 值的空洞。

有人可以分享一个例子来说明这个结构的用法吗？我想它必须涉及match使用context模式，然后使用上述形式来使用匹配的上下文。

假设我想有一个策略来一次清除多个假设，做类似的事情clear_multiple H1, H2, H3.。我尝试使用对来做到这一点，如下所示：

但是，问题是我必须放置括号才能得到Prod：

我的问题是，如何在不使用Prods 的情况下做到这一点？

我检查了这个问题，但这并不是我想要的，因为我想要的参数数量是未知的。

使用这个组的定义：

并证明了这个定理：

我如何编写一个 Ltac 来自动将给定的等式（目标本身或假设）乘以给定项的过程？

理想情况下，在证明中使用这个 Ltac 应该是这样的：

我有一个目标，其中包含对foo匹配分支中某些引理的调用。R该调用使用分支本地变量作为其参数之一：

我想执行 beta 扩展，foo以便调用变为：

这将使我能够进一步概括(fun d => foo a b c d)，这将不再依赖于分支本地的变量。因为我正在处理非常大的证明，所以我想用 Ltac 来写这个。这是一个尝试：

然而，“没有匹配的匹配子句”失败。如果我match用它替换分支的主体idtac仍然失败，那么问题显然是由于未能匹配给定的表达式造成的。但是，如果我少匹配一个参数，则匹配成功。例如：

在连续的行中打印“a”、“b”和“c”。我也可以说：

这成功了，但有趣的是，目标仍然没有改变，即。电话仍然是形式(foo a b c R)而不是((fun d => foo a b c d) R)。我在这里做错了什么？

我注意到符号可以被区别对待。例如<，它只是一个常规定义的符号，unfold "<"它的工作原理如下例所示：

但是，<=与类型相关联的符号le由于某种原因unfold "<="不起作用，如下例所示：

失败了Unable to interpret "<=" as a reference。

我可以用一些 ltac 命令转换4 <= 5成吗？le 4 5

我正在“coqtop -nois”下重新开发“Coq.Init.Prelude”和“HoTT.Basics.Overture”以进行练习。我发现很难直接写表达式。这就是我想使用战术的原因。我想知道为什么我不能使用“Ltac”。