如何指示`auto`在证明搜索过程中简化目标？

Question

我的问题的最小示例如下：

Goal let x := True in x.

这可以立即通过

simpl. auto.

解决，但是

auto.

不起作用。

在我的实际情况中，搜索树比这要大一些。它涉及许多中间步骤，其中

auto

能够继续进行，但它会被一些 zeta 可约化的

let

表达式吓退。即使我愿意，我什至无法让它停在那里并让我手动插入那个

simpl

（因为

auto

要么解决目标，要么保持目标不变）。

处理这个问题的正确方法是什么？如果可能的话，我想避免添加

Extern Hint simpl

来粗暴地将

simpl

应用于程序中各处的每个

let

。我不需要坚持

auto

；任何其他能够以非多余的方式完成这项工作的策略对我来说都很好。

Answer 1

您可以使用 Hint extern 让 auto 尝试任意策略。

例如

Hint Extern 5 => progress simpl : core.

会起作用的。但这很危险，可能会导致汽车速度变慢。数字 (5) 是成本 - 自动将首先尝试成本较低的所有提示。进度确保提示在不更改任何内容的情况下不适用，因此 simpl 不会循环。