coq - 如何匹配 "match"表达式？

Question

我正在尝试编写假设规则，在 match 的帮助下制定 build :

Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat.
intros.

x : nat
H : match x with
    | 0%nat => 10%nat
    | 1%nat => 5%nat
    | S (S _) => 10%nat
    end = 5%nat
============================
 x = 1%nat

我怎样才能匹配这样的假设？以下直接方法失败:

match goal with
  |[H:match ?e with | ?a => ?x | ?b => ?y | ?c => ?z end = ?b] => idtac
end.

> Syntax error: 'end' expected after [branches] (in [match_constr]).

Answer 1

match 上的模式匹配陈述有些奇怪。

您应该知道的第一件事是，在 Coq 内部，没有 match 这样的东西。在几个变量上或深度匹配:一切都以更简单的match来翻译陈述。因此，您编写的术语实际上是以下术语的语法糖:

match x with
| 0 => 10
| S x' =>
  match x' with
  | 0 => 5
  | S x'' => 10
  end
end

这就是 Coq 在打印你的证明状态时所暗示的。问题是这种语法糖对 Ltac 模式不起作用:因此，当编写提到 match 的 Ltac 模式时，您应该始终尝试将其匹配为一级 match .

第二个问题是不能绑定(bind) match 的模式部分。 : 就像是

match goal with
| H : match ?x => _ | ?y => _ end = 5 |- _ => (* ... *)
end

在 Ltac 中真的没有意义。

您有两种选择来解决您的问题，然后:

写下match您期望在模式部分上有您类型的构造函数的确切列表，例如

match goal with
| H : match x with 0 => _ | S _  => _ end = 5 |- _ => (* ... *)
end

使用特殊的 match (* ... *) with _ => _ end语法，匹配任何 match任何:

match goal with
| H : match x with _ => _ end = 5 |- _ => (* ... *)
end

通常，就像你的情况一样，人们仍然想考虑 match 的所有分支。 ，包括深的。在这种情况下，这个成语通常会派上用场:

repeat match goal with
| H : match ?x with _ => _ end = _ |- _ =>
  destruct x; try solve [inversion H]
end.