coq - 提高 coq 策略的失败级别

Question

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

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

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

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

score 3 · Accepted Answer

您可以编写一个策略来在 Ocaml 中实现这一目标。我把它放在 GitHub上。

例如，以下应该引发错误而不是默默地成功：

repeat (match goal with 
          | [ |- _ ] => 
            raise_error_level (assert (3 = 3) by idtac)
        end).

score 1 · Accepted Answer

我不知道是否有可能得到你想要的，但我有时会使用以下成语：

tactic_expression_that_may_fail_with_level_0
|| fail 1000 "There was some problem here"

如果第一个策略以 0 级失败，||则将尝试运行第二个策略，该策略将以非常高的级别失败并报告给您。

如果您可以提供一个具体的用例来看看其他一些技术是否更适合，那将会有所帮助。

2 回答 2