Сопоставить шаблон контекста в тактической / тактической нотации - PullRequest
Новая
       8

Сопоставить шаблон контекста в тактической / тактической нотации

0 голосов
/ 07 января 2019

Я нахожу схему в своей цели с помощью тактики.

Почему это не получается: 

        Tactic Notation "my_context_match" uconstr(g) :=
          match goal with
          | |- context[g] => idtac
          end.

          my_context_match _.

Пока это удается? 

        match goal with
          | |- context[_] => idtac
        end.

Есть ли способ написать my_context_match, чтобы я мог пропустить неполные паттерны (с _ на них) и посмотреть, соответствует ли что-нибудь внутри моей цели шаблону

1 Ответ

0 голосов
/ 08 января 2019

Поддержка uconstr очень неоднородна. Я только что сообщил # 9321 . Обратите внимание, что даже это не помогает: 

Goal True.
  let v := uconstr:(True) in
  lazymatch constr:(v) with
  | v => idtac
  end. (* Error: No matching clauses for match. *)

Как подсказывает @eponier в комментарии, вы можете использовать open_constr вместо uconstr. Тем не менее, это оставит нерешенными проблемы. Вот тактика, которая сработает, и не оставит неразрешенными проблемы: 

Tactic Notation "my_context_match" uconstr(g) :=
  (* [match] does not support [uconstr], cf COQBUG(https://github.com/coq/coq/issues/9321),
     so we use [open_constr] *)
  let g := open_constr:(g) in
  (* turning [g] into an [open_constr] creates new evars, so we must
     eventually unify them with the goal *)
  let G := match goal with |- ?G => G end in
  (* We now search for [g] in the goal, and then replace the matching
     subterm with the [open_constr] [g], so that we can unify the
     result with the goal [G] to resolve the new evars we created *)
  match G with
  | context cG[g]
    => let G' := context cG[g] in
       unify G G'
  end.

Goal True /\ True.
  my_context_match _.
  my_context_match (_ /\ _).
  Fail my_context_match (_ \/ _).
  my_context_match True.
  exact (conj I I).
Qed.
...