coq - 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 的列表？ - solveFancy 中的战术?我在想像:

Add Hint SolveFancy important_step3.

Answer 1

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

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 应该有办法做到这一点，但是要控制尝试这些提示的时间和顺序要困难得多，并且它们必须在最后完全解决目标。