时间戳

首页 > 解决方案 > 在 Coq 中匹配假设的更短的符号？

coq - 在 Coq 中匹配假设的更短的符号？

问题描述

我发现自己经常想按类型而不是名称来引用假设；尤其是在语义规则倒置的证明中，即具有多个案例的规则，每个案例可能有多个前件。

我知道如何使用 来执行此操作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].

根据我对Tactic Notations的理解，不可能有cpattern作为参数，但也许还有另一种方法？

理想情况下，我希望能够在 Isabelle 中的任何策略中使用假设模式而不是标识符：

rename ⟨P1 \/ _⟩ into HH.
destruct ⟨P1 \/ _⟩ as [H1|H2].
rewrite ⟨P1 = _⟩.

但我认为这是一个相当具有侵略性的变化。

标签： coqtheorem-provingcoq-tactic

解决方案

您可以遍历所有假设，直到找到匹配的假设：

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.

为什么这是一个改进？因为_ \/ _and_ = _现在是完整类型，而不仅仅是模式。它们只包含未解决的存在变量。在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 Notation的 s 来用这些有孔的类型替换 , 等中的ident参数。确实，几乎是你的修改。destructrewriteuconstrssummon _ as _rename _ into _

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

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

推荐阅读