Coq 中匹配假设的更短符号？
Shorter notation for matching hypotheses in 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]，不是一种选择——我厌倦了找到正确数量的 ?！）
例如，是否可以写一个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 Notations 来替换 destruct、rewrite 等中的 ident 参数。 -type uconstrs，如果你真的想要的话。的确，summon _ as _几乎就是你修改的rename _ into _.
另一个警告：assert 是不透明的； summon 生成的定义看起来像是新的假设，但并未表明它们与旧假设相同。应该使用 refine (let it := _ in _) 或 pose 之类的东西来纠正这个问题，但我的 Ltac-fu 不够强大，无法做到这一点。另见：这个问题提倡文字 transparent assert.
（新答案解决了这个问题。）
我发现自己经常想通过类型而不是名称来引用假设；特别是在语义规则倒置的证明中，即具有多个案例的规则，每个案例可能有多个前提。
我知道如何使用 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 Notations 来替换 destruct、rewrite 等中的 ident 参数。 -type uconstrs，如果你真的想要的话。的确，summon _ as _几乎就是你修改的rename _ into _.
另一个警告：assert 是不透明的； summon 生成的定义看起来像是新的假设，但并未表明它们与旧假设相同。应该使用 refine (let it := _ in _) 或 pose 之类的东西来纠正这个问题，但我的 Ltac-fu 不够强大，无法做到这一点。另见：这个问题提倡文字 transparent assert.
（新答案解决了这个问题。）