Вы можете перебирать все предположения, пока не найдете подходящее:
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.
(Новый ответ решает эту оговорку.)