Расширяемая тактика в Coq

Допустим, у меня есть причудливая тактика, которая решает леммы определенного вида:

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.
Источник

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 из модулей не имеют значения, и они могут быть переименованы или переупорядочены, как вы хотите. Это не самая элегантная вещь в мире, но я думаю, что это улучшение.

Источник

Это не то, что я бы назвал элегантным, а вот чистое решение 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, но будет намного сложнее контролировать, когда и в каком порядке эти подсказки будут использованы, и они должны полностью решить поставленную задачу к концу.

Источник
Другие вопросы по тегам