coq - Coq 中匹配假设的更短表示法？

Question

我发现自己经常想通过假设的类型而不是名称来引用假设；特别是在语义规则反转的证明中，即具有多个案例的规则，每个案例可能有多个前因。

我知道如何使用将目标与...匹配来做到这一点，如以下简单示例所示。

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 = _⟩.

但我认为这是一个相当侵入性的改变。

Answer 1

您可以迭代所有假设，直到找到匹配的假设:

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。迭代的出现是因为匹配目标将不断重试不同的匹配，直到出现问题或一切都失败。

您可以定义一个不带 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.

旧答案

(您可能想阅读本文，因为上面的解决方案实际上是这个解决方案的变体，这里有更多解释。)

您可以使用 easert (name : ty) by easmination 将与类型模式匹配的假设召唤到名称中。。

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.

为什么这是一个改进？因为 _\/_ 和 _ = _ 现在是完整类型，而不仅仅是模式。它们只是包含 Unresolved 存在变量。在 eassert 和 easmination 之间，这些变量在匹配假设定位的同时得到解决。战术符号绝对可以与类型(即术语)一起使用。遗憾的是，解析规则似乎存在一些问题。具体来说，策略符号需要一个无类型术语(因此我们不会过早地尝试解析变量但失败)，因此我们需要 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.

我相信您可以创建一堆专门的战术符号来替换destruct中的ident参数，如果你真的想的话，可以用这些洞型uconstrs重写等。事实上，summon _ as _几乎就是你修改后的rename _ into _。

另一个警告:assert 是不透明的； summon 生成的定义看起来像是新的假设，但并不表明它们与旧的假设之一相同。像 refine (let it := _ in _) 或 pose 之类的东西应该用来纠正这个问题，但我的 L_tac-fu 不是足够强大来做到这一点。另请参阅:本期提倡字面意义 transparent assert .

(新答案解决了这个问题。)