Двойные подцели в Coq

Question

Существует ли какая-либо тактика Coq для предотвращения генерации нескольких идентичных подцелей?Если нет, то можно ли написать какую-то тактику для устранения дублирующих подцелей сразу после ее генерации?В Изабель вы можете сделать это:

apply (tactic {* distinct_subgoals_tac *})

Answer 1

Невозможно устранить дубликаты по факту без написания кода OCaml, но вы можете создать evar, который является соединением всех подцелей, дедуплицированных. Примерно так:

Ltac distinct_subgoals_tactical tac :=
  let H := fresh in
  unshelve epose proof _ as H;
  [ |
  | tac;
    [ (* first split apart the hypothesis containing the conjunction of all previous subgoals *)
      repeat match type of H with prod _ _ => destruct H as [? H] end;
      (* see if any of them solve the goal *)
      try assumption;
      (* otherwise, add another conjunct to the hypothesis and use the first part of it to solve the current goal *)
      refine (fst H) .. ] ];
    [ exact True (* fill the final conjunct with True *)
    | repeat apply pair; try exact I .. ].

Тогда вы можете вызвать его как distinct_subgoals_tactical ltac:(<apply tactic here>)