3

在我的 coq 开发过程中，我正在学习如何创建针对我的问题领域的新策略，就像 Adam Chlipala 教授一样。在该页面上，他描述了如何通过结合来创建强大的自定义repeat策略match。

现在，我已经有一个强大的单发战术在使用，auto. 它将从提示数据库中找到的步骤链串在一起。我已经投入了一些精力来管理这些提示数据库，所以我也想继续使用它。

然而，这提出了一个问题。 目前尚不清楚将auto's 的功能合并到定制策略中的“正确”方式是什么。

例如，由于（按其页面）auto总是要么解决目标要么什么都不做，将它放在循环中并不比在循环后调用它一次更强大。

要了解为什么这不理想，请考虑一种直接调用 的单个“步骤”的假设方法，auto如果可以进行更改（而不是仅在解决目标时），则该步骤成功，否则失败。这样的单步可以与匹配重复循环中的自定义行为交错，允许我们在搜索树中的例如try contradiction或try congruence中间点。

是否有很好的设计模式可以将auto's 的功能整合到自定义策略中？

的行为是否可以auto分解为我们可以使用的“单步”策略？

4

1 回答 1

2

我会做的是将其他策略纳入auto. 您可以使用Hint Extern num pat => mytactic : mybase命令 wherenum是优先级编号（0 是最高优先级），pat在何时应该使用提示时过滤的模式，当然也是您要应用的策略和要添加的mytactic基础mybase提示（不要使用默认值core；建立您的自定义基础并使用 调用它auto with mybase；如果您不想core在搜索中包含来自基础的引理，请添加假基础nocore：）auto with mybase nocore。

如果您开始auto非常依赖，我会改用几乎等效但表现更好的typeclasses eauto with mybase. 与其名称所暗示的相反，它是一种通用策略，与类型类无关（只要您明确提供它应该工作的提示基础）。要知道的主要行为差异之一是默认情况下搜索深度是无界的。因此，请注意可能的无限循环或使用变体修复有限限制typeclasses eauto num with mybase。

于 2016-12-17T16:25:27.743 回答