在Coq中匹配假设的简短表示法？

Question

我发现自己经常想通过类型而不是名称来引用假设。尤其是在语义规则倒置的证明中，即具有几种情况的规则，每种情况可能都有多个先例。

我知道如何使用来完成此操作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]不是一个选择，我已经厌倦了找到正确数量的?s！）

例如，是否可以编写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].

根据我对“ 战术符号”的理解，不可能使用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。之所以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- asname设为找到的假设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到更换ident的参数destruct，rewrite这些多孔型等uconstrs，如果你真的想。确实，summon _ as _几乎是你修改过的rename _ into _.

另一个警告：assert不透明；生成的定义summon看起来像是新假设，并没有表明它们等于旧假设之一。类似refine (let it := _ in _)或pose应该用来纠正这个问题，但我的 L _tac -fu 不够强大，无法做到这一点。另请参阅：这个问题提倡文字transparent assert.

（新答案解决了这个警告。）