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 添加到列表中，但这很快就变老了。

现在是否有更优雅的方法来扩展 solveFancy 中的 important_step 策略列表？我在想象这样的事情：

Add Hint SolveFancy important_step3.

Answer 1

这不是我所说的优雅，但这是一个纯粹的 Ltac 解决方案。您可以在稍后 re-define 的策略中留下一个钩子，并且您可以通过始终为下一个提示留下一个钩子来继续遵循此模式：

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

Coq 中的可扩展策略

Extensible tactic in Coq

coq

ltac