如何匹配"匹配"表达式？

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关于几个变量或深度匹配的东西:一切都是用简单的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.