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，可以根据需要对它们进行重命名或重新排序。这不是世界上最优雅的事情，但我认为这是一种改进。