coq - 如何匹配“匹配”表达式？

Question

我正在尝试为假设编写一条规则，在match构造的帮助下制定：

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关于多个变量或深度匹配的 a 之类的东西：一切都被翻译成更简单的match语句。因此，您编写的术语实际上是以下术语的语法糖：

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

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

第二个问题是您不能绑定 a 的模式部分match：类似于

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

在 Ltac 中真的没有意义。

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

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

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

2. 使用匹配任何内容的特殊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.