Расширяемая тактика в 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.

coq ltac
person Joachim Breitner    schedule 19.02.2018    source источник

Ответы (2)


arrow_upward
0
arrow_downward

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

person Lily Chung    schedule 28.07.2018
comment
Мне нравится модульный подход! - person Joachim Breitner; 30.07.2018

arrow_upward
1
arrow_downward

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

person Tej Chajed    schedule 20.02.2018
comment
Да, что-то в этом роде тоже лучшее, что я могу придумать. Но это раздражает, когда числа синхронизируются; если вы добавите лемму в середину файла, вам придется все перенумеровать. - person Joachim Breitner; 21.02.2018