Extensible tactic in Coq

Question

Let’s say I have a fancy tactic that solves lemmas of a certain kind:

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

Now I use this tactic to prove further lemmas of that kind, which I subsequently want to use in this tactic.

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

Now I could simply re-define Ltac solveFancy ::= … and add important_step3 to the list, but that quickly gets old.

Is there a more elegant way of now extending the list of important_step-tactics in solveFancy? I am imagining something like:

Add Hint SolveFancy important_step3.

Answer 1

I would add an argument to solveFancy which you can use to pass in another tactic:

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 [...]

This is somewhat more elegant than redefining a hook, though it doesn't solve the extensibility problem by itself. The following is a strategy for repeatedly redefining a tactic x in terms of previous versions of itself, using the fact that modules allow redefining an Ltac name without overwriting the previous definition.

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.

Note that the names K0, K1 of the modules don't matter and they can be renamed or reordered however you want. This isn't the most elegant thing in the world but I think it's an improvement.