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

Question

在 Ltac 中实现复​​杂的策略时，有一些 Ltac 命令或策略调用我预计会失败以及预期失败(例如终止 repeat 或导致回溯)。这些故障通常在故障级别 0 时引发。

更高级别引发的故障“逃避”周围 try或 repeat阻止，并且可用于发出意外故障的信号。

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

能不能在 Ltac 中实现这种提升失败级别的高阶战术？

Answer 1

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

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

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