Coq Intro Pattern

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

首先是最基本的四种 pattern：

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

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

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

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