Coq中的可扩展策略

Question

假设我有一种奇特的策略可以解决某种类型的引理:

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

现在我使用这种策略来证明这种类型的进一步的引理,我后来想在这种策略中使用它.

Lemma fancy3 := …. Proof. … Qed.
Ltac important_step3 := apply fancy3;[some|specific|stuff].

现在我可以简单地重新定义Ltac solveFancy ::= …并添加important_step3到列表中,但很快就会变老.

现在是否有更优雅的方式扩展important_step-tactics 列表solveFancy？我想象的是:

Add Hint SolveFancy important_step3.

Answer 1

我会添加一个参数，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这不是世界上最优雅的事情，但我认为这是一种进步。