您可以遍历所有假设，直到找到匹配的假设：
Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
match goal with H : _ |- _ => pose (id := H : ty) end.
诀窍在于，您将要找到的类型不是作为模式，而是作为类型:)。具体来说，如果您发出类似 summon (P _) as id 的问题，那么 Coq 会将 _ 作为未解决的存在变量。反过来，每个假设都将针对P _ 进行类型检查，并尝试在此过程中实例化那个洞。当一个成功时，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，但需要there's no 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 Notations 来替换destruct、rewrite 等中的ident 参数与这些孔类型uconstrs到。确实，summon _ as _ 几乎就是你修改后的rename _ into _。
另一个警告：assert 是不透明的； summon 生成的定义看起来像是新假设，但并未表明它们与旧假设之一相等。应该使用 refine (let it := _ in _) 或 pose 之类的东西来纠正这个问题，但我的 Ltac-fu 不够强大，无法做到这一点。另见：这个问题提倡文字transparent assert。
（新答案解决了这个警告。）