今天介绍一下 Coq 里面的 intro pattern,当前使用的版本是 Coq 8.9.0。这个特性虽然叫 intro pattern,但是除了在 intro 的时候可以用,它还可以用在 assert、pose proof、specialize、desturct、injection、apply 等等 tactics 中,因此学习性价比非常高。我趁着刚看完文档,记忆还热乎的时候先总结一下。详细的解释可以看文档

首先是最基本的四种 pattern:

  1. _ 下划线,表示忽略这一项
  2. ? 表示让 Coq 自己取个不重复的名字
  3. ?ident 让 Coq 根据 ident 来取一个不重复的名字,在写 Ltac 的时候可以配合 fresh 来用
  4. ident 指定 ident,可能会冲突

接下来就是一些附带其他行为(副作用)的 pattern。

  1. [intro_pattern_list | ... | intro_pattern_list]相当于 destruct,内部的 pattern 可以递归
  2. (p1 , p2 , ... , pn) 等价于 [p1 p2 ... pn],也就是对只有一个 constructor 的项做 pattern matching
  3. (p1 & p2 & ... & pn) 等价于 [p1 [p2 [... [... p]]]],可以把一串右结合的项 destruct 掉,比如 /\exists
  4. [= p1 p2 ...] 会对该项应用 injection 然后对得到的 n 个前提分别使用后续的 pattern
  5. -><- 会对该项使用相应方向的 rewrite
  6. p%t1 t2 ... 会依次 apply t1, t2, ... 到 p 上

以上这些 pattern 都是可以组合的,用起来非常灵活,极大减小证明长度,至于可读性那就见仁见智了。