coqの戦術の失敗レベルを上げる

Question

Ltacで複雑な戦術を実装すると、失敗すると予想されるLtacコマンドや戦術呼び出しがあります（例えば、repeatを終了する、またはバックトラックを引き起こすなど）。これらの障害は通常、障害レベル0で発生します。

高レベルで発生した障害は、周囲のtryまたはrepeatブロックを「エスケープ」し、予期しない障害を通知するのに役立ちます。

私が紛失しているのは、戦術を実行し、レベル0であっても、失敗のメッセージを保持しながら、レベル0でもその障害をより高いレベルで処理する方法です。これは私がrepeatが私の側でLtacプログラミングエラーのために終了しないようにするでしょう。

Ltacでこのような障害発生レベルの高次タクティックを実装できますか。

Answer 1

Ocamlで達成するための戦術を書くことができます。私はそれをGitHub hereに置いた。例えば

次の代わりに黙って、後続のエラーを発生させる必要があります。

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

Answer 2

あなたが望むものを正確に得ることが可能である場合、私は知らないが、私は時々、次のイディオムを使用します。最初の戦術は、レベル0で失敗した場合、||を実行しようとします

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

をそれは非常に高いレベルで失敗し、あなたに報告します。

具体的なユースケースを提供して、他の手法が適しているかどうかを確認するのに役立ちます。