提高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水平，||將嘗試運行第二個，它會以很高的水平失敗並向你報告。

如果你能提供一個具體的用例來看看其他技術是否更適合，這將有所幫助。