coq - Coq の拡張可能なタクティック

Answer 1

それは私がエレガントと呼ぶものではありませんが、純粋な Ltac ソリューションです。後で再定義するフックを戦術に残すことができます。次のヒントのために常にフックを残すことで、このパターンに従い続けることができます。

Axiom P : nat -> Prop.
Axiom P0 : P 0.
Axiom P_ind : forall n, P n -> P (S n).

Ltac P_hook := fail.

Ltac solve_P :=
  try apply P_ind;
  exact P0 || P_hook.

Theorem ex_1 : P 1.
Proof.
  solve_P.
Qed.

Ltac P_hook2 := fail.
Ltac P_hook ::= exact ex_1 || P_hook2.

Theorem ex_2 : P 2.
Proof.
  solve_P.
Qed.

Ltac P_hook3 := fail.
Ltac P_hook ::= exact ex_2 || P_hook3.

Theorem ex_3 : P 3.
Proof.
  solve_P.
Qed.

でこれを行う方法があるはずですが、Hint Externこれらのヒントが試行されるタイミングと順序を制御するのははるかに難しく、最後までに目標を完全に解決する必要があります。

Answer 2

solveFancy別の戦術を渡すために使用できる引数を追加します。

Ltac solveFancy hook :=
  some_preparation;
  repeat (first [important_step1 | important_step2 | hook];
          some_cleanup);
  solve_basecase.

(* use solveFancy without any extra available steps *)
[...] solveFancy fail [...]

Ltac important_step3 := [...]

(* use solveFancy with important_step3 *)
[...] solveFancy important_step3 [...]

これは、フックを再定義するよりもいくらか洗練されていますが、それ自体では拡張性の問題は解決しません。x以下は、モジュールが以前の定義を上書きせずに Ltac 名を再定義できるという事実を使用して、それ自体の以前のバージョンに関して戦術を繰り返し再定義するための戦略です。

Ltac x := idtac "a".

Goal False.
  x. (* a *)
Abort.

Module K0.
  Ltac x' := x.
  Ltac x := x'; idtac "b".
End K0.
Import K0.

Goal False.
  x. (* a b *)
Abort.

Module K1.
  Ltac x' := x.
  Ltac x := x'; idtac "c".
End K1.
Import K1.

Goal False.
  x. (* a b c *)
Abort.

K0モジュールの名前は重要ではなく、必要に応じて名前K1を変更したり並べ替えたりできることに注意してください。これは世界で最もエレガントなものではありませんが、改善だと思います。