Coq Intro Pattern

今天介绍一下 Coq 里面的 intro pattern， 当前使用的版本是 Coq 8.9.0。 这个特性虽然叫 intro pattern， 但是除了在 intro 的时候可以用， 它还可以用在 assert、pose proof、specialize、desturct、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 都是可以组合的， 用起来非常灵活， 极大减小证明长度， 至于可读性那就见仁见智了。