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

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模式：因此，当编写一个提到match的Ltac模式时，您应该始终尝试匹配它，就好像它是一个级别的match。

的第二个问题是，你不能在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.