我发现自己经常想通过类型而不是名称来指代假设。尤其是在语义规则反演的证明中，即具有几种情况的规则，每种情况可能都有多个先例。
我知道如何使用match goal with ...进行此操作，如以下简单示例所示。
Lemma l0:
forall P1 P2,
P1 \/ (P1 = P2) ->
P2 ->
P1.
Proof.
intros.
match goal with H:_ \/ _ |- _ => destruct H as [H1|H2] end.
assumption.
match goal with H: _ = _ |- _ => rewrite H end.
assumption.
Qed.
有没有更简洁的方法？还是更好的方法？
（像
intros [???? HA HB|??? HA|????? HA HB HC HD]这样的引入模式不是一种选择，我已经厌倦了找到正确数量的?！）例如，是否可以编写
grab策略来组合模式和策略，如 grab [H:P1 \/ _] => rename H into HH.
grab [H:P1 \/ _] => destruct H into [H1|H2].
grab [P1 \/ _] => rename it into HH.
grab [P1 \/ _] => destruct it into [H1|H2].
根据我对Tactic Notations的理解，不可能使用cpattern作为参数，但是也许还有另一种方法吗？
理想情况下，我希望能够在Isabelle的任何策略中使用假设模式而不是标识符：
rename ⟨P1 \/ _⟩ into HH.
destruct ⟨P1 \/ _⟩ as [H1|H2].
rewrite ⟨P1 = _⟩.
但是我认为这是一个相当大的改变。
最佳答案
您可以遍历所有假设，直到找到匹配的假设：
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 Notation来用这些有漏洞的ident替换destruct，rewrite等中的uconstrs参数。实际上，summon _ as _几乎是您修改后的rename _ into _。另一个警告：
assert是不透明的； summon生成的定义看起来像新的假设，但并没有揭示它们等于旧的假设之一。应该使用诸如refine (let it := _ in _)或pose之类的东西来纠正此问题，但是我的Ltac-fu不够强大，无法做到这一点。另请参阅：此问题主张使用文字transparent assert。（新答案解决了这一警告。）
关于coq - Coq中匹配假设的缩写表示法？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/55992567/