Вы можете перебирать все предположения, пока не найдете подходящее:
Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
match goal with H : _ |- _ => pose (id := H : ty) end.
Хитрость в том, что вы берете тип, который будет найден не как шаблон, а как тип :). В частности, если вы выдадите что-то вроде summon (P _) as id
, то Coq примет _
в качестве нерешенной экзистенциальной переменной. В свою очередь, каждое предположение будет проверено на тип * против 1006 *, пытаясь создать экземпляр этой дыры на своем пути. Когда это удается, pose
называет его id
. Итерация возникает из-за того, что match goal
будет повторять попытки с разными совпадениями, пока что-то не застрянет или все не получится.
Вы можете определить форму без as
, которая просто называет найденную вещь it
(отбрасывая все остальное):
Tactic Notation "summon" uconstr(ty) :=
let new_it := fresh "it"
in try (rename it into new_it); summon ty as it.
Та-да!
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
summon (_ \/ _).
destruct it.
assumption.
summon (_ = _).
rewrite it.
assumption.
Qed.
Вы также можете получить синтаксис =>
. Я не думаю, что это ужасно полезно, но ...
(* assumption of type ty is summoned into id for the duration of tac
anything that used to be called id is saved and restored afterwards,
if possible. *)
Tactic Notation "summon" uconstr(ty) "as" ident(id) "=>" tactic(tac) :=
let saved_id := fresh id
in try (rename id into saved_id);
summon ty as id; tac;
try (rename saved_id into id).
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
summon (_ \/ _) as H => destruct H.
assumption.
summon (_ = _) as H => rewrite H.
assumption.
Qed.
Старый ответ
(Вы можете прочитать это, потому что вышеприведенное решение действительно является вариантом этого, и здесь есть более подробное объяснение.)
Вы можете вызвать предположение, совпадающее с шаблоном типа, в имя с помощью eassert (name : ty) by eassumption.
.
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
eassert (HH : _ \/ _) by eassumption.
destruct HH.
assumption.
eassert (HH : _ = _) by eassumption.
rewrite HH.
assumption.
Qed.
Почему это улучшение? Потому что _ \/ _
и _ = _
теперь являются полными типами, а не просто шаблонами. Они просто содержат нерешенные экзистенциальные переменные. Между eassert
и eassumption
эти переменные решаются одновременно с предположением о соответствии. Тактические нотации могут определенно работать с типами (то есть терминами). К сожалению, в правилах синтаксического анализа, похоже, произошла ошибка. В частности, тактической нотации нужен нетипизированный термин (поэтому мы не пытаемся и не можем разрешить переменные слишком рано), поэтому нам нужно uconstr
, но нет luconstr
, то есть мы вынужден добавлять лишние скобки. Чтобы избежать брекет-мании, я переработал синтаксис вашего grab
. Я также не совсем уверен, имеет ли смысл ваш синтаксис =>
, потому что почему бы просто не ввести имя в область видимости навсегда, а не только на =>
, как вы, похоже, подразумеваете?
Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
eassert (id : ty) by eassumption.
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
summon (_ \/ _) as HH.
destruct HH.
assumption.
summon (_ = _) as HH.
rewrite HH.
assumption.
Qed.
Вы можете заставить summon
-sans- as
назвать найденное допущение it
, загружая при этом все остальное под этим именем.
Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
eassert (id : ty) by eassumption.
Tactic Notation "summon" uconstr(ty) :=
let new_it := fresh "it"
in (try (rename it into new_it); summon ty as it).
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
(* This example is actually a bad demonstration of the name-forcing behavior
because destruct-ion, well, destroys.
Save the summoned proof under the name it, but destroy it from another,
then observe the way the second summon shoves the original it into it0. *)
summon (_ \/ _) as prf.
pose (it := prf).
destruct prf.
assumption.
summon (_ = _).
rewrite it.
assumption.
Qed.
Идиоматически, это действительно было бы
Lemma l0 : forall P1 P2, P1 \/ (P1 = P2) -> P2 -> P1.
Proof.
intros.
summon (_ \/ _).
destruct it.
assumption.
summon (_ = _).
rewrite it.
assumption.
Qed.
Я полагаю, что вы могли бы пойти и создать группу специализированных Tactic Notation
для замены ident
аргументов в destruct
, rewrite
и т. Д. На эти дырочные uconstrs
, если вы действительно хотели к. Действительно, summon _ as _
- это почти ваш модифицированный rename _ into _
.
Еще одна оговорка: assert
непрозрачен; определения, сгенерированные summon
, выглядят как новые предположения, которые не показывают, что они равны одному из старых. Что-то вроде refine (let it := _ in _)
или pose
должно быть использовано, чтобы исправить это, но мой L tac -fu недостаточно силен, чтобы сделать это. Смотрите также: этот вопрос защищает буквальное значение transparent assert
.
(Новый ответ решает эту оговорку.)