提高coq策略的失败水平

Question

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

故障在较高级别上升“逃脱”周围的try或repeat区块，并可用于发出意外故障。

我缺少的是什么，甚至为0级运行策略tac和对待它的失败，是在一个较高的水平，同时保留了失败的消息的方式。这可以让我确保repeat不会由于我身边的Ltac编程错误而终止。

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

Answer 1

你可以写一个策略来实现在Ocaml。我把它放在GitHub here上。

例如，以下应该产生一个错误，而不是默默的成功：

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

Answer 2

我不知道是否有可能得到你想要什么，但我有时会用下面的习惯：

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

如果第一个战术失败，0水平，||将尝试运行第二个，它会以很高的水平失败并向你报告。

如果你能提供一个具体的用例来看看其他技术是否更适合，这将有所帮助。