问题标签 [ltac]

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

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

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

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

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

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

我正在寻找一种方法来通过它的名称来获得低血压以匹配它。像这样 ：

这将像这样使用：

谢谢。

我想在 coq 中制定一个 Ltac 策略，它需要 1 个或 3 个参数。我已经阅读ltac_No_arg了LibTactics模块中的内容，但如果我理解正确，我将不得不调用我的策略：

这不是很方便。

有没有办法得到这样的结果？：

我正在研究一种可以创造两个新假设的策略

从那种形式的假设

这是我的 Ltac 代码：

wereh是要分解的假设，x新变量t的名称和新假设的名称。该策略按预期工作，但在证明结束时我得到了这个：

该evar策略似乎创建了一种名为 D 的新类型，而不是使用现有的类型。请注意，如果我使用

在 coqtop 中，它可以完美运行。

在 Ltac 中实施复​​杂的策略时，有一些 Ltac 命令或策略调用我预计会失败以及预期会失败（例如终止 arepeat或导致回溯）。这些故障通常在故障级别 0 时提出。

在更高级别引发的故障“逃离”周围try或repeat阻塞，并且对于发出意外故障的信号很有用。

我缺少的是一种运行策略tac并处理其失败的方法，即使在 0 级，也可以处于更高的级别，同时保留失败的信息。这将让我确保repeat不会因为我这边的 Ltac 编程错误而终止。

我可以在 Ltac 中实施这种失败提升级别的高阶策略吗？

假设我在 Coq 中有以下定义：

现在考虑这个引理：

此时证明状态如下所示：

我想写 Ltacmatch goal来检测：

a）有一个假设x : nat被用作compare量化假设内部某处的论据H

b) 还有一些其他类型的假设nat——即y——可以用来专门化量化假设。

c）一旦我们有这两件事H专门y

我试着这样做：

但是这段代码至少有两点有问题：

1. context在 a 下使用似乎forall是不允许的。

2. 我想不出一个正确的方法来X作为参数传递给compare 它，因为它被认为是作为假设存在的东西。这样做是这样的：

如何rewrite在 ltac 中调用以仅重写一次出现？我认为 coq 的文档中提到了一些内容，rewrite at但我无法在实践中实际使用它，也没有示例。

这是我正在尝试做的一个例子：

假设我有以下设置：

我尝试使用自定义策略来证明一个简单的定理：

这失败了，因为目标不是形式adt (CE ?N)而是形式adt (nat_to_exp ?N)（这在使用时明确显示Set Printing Coercions）。

试图证明一个稍微不同的定理是可行的：

我知道的可能的解决方法：

• 不使用强制。
• 在策略中展开强制（带有unfold nat_to_exp）。这稍微缓解了问题，但是一旦引入了该策略不知道的新强制，就会失败。

理想情况下，如果在展开所有定义后模式匹配，我希望模式匹配成功（当然，定义不应保持展开）。

这可能吗？如果不是，有什么理由不可以吗？

我有几个遵循相同结构的证明。第一个可以用 完成trivial，所有其他的可以用 完成，第一个证明完成后，提示数据库auto with foo_db在哪里foo_db填充提示。我想编写一个 Ltac 程序auto with foo_db来解决所有这些证明。但是，当运行 Ltac 来解决我的第一个证明时foo_db，还不存在，所以 Coq 抱怨：Error: No such Hint database: foo_db.. 有没有办法初始化一个空的提示数据库？