关于Coq中intros [|n]语法及空分支的技术咨询

好问题！这两个点都是Coq里模式匹配语法的实用细节，我来给你讲明白：

1. intros [|n]确实是intros + destruct的快捷方式 #

Coq的intros命令支持模式匹配式的变量引入，对于归纳类型的全称量词变量，直接用[|n]这种模式就能一步完成“引入变量+对变量做case analysis”的操作，省去了分开写intros和destruct的麻烦。

拿你的例子来说，原命题里的forall n : nat，intros [|n]完全等价于下面这两行代码：

intros n.
destruct n as [|n].

这是因为自然数nat的归纳定义是Inductive nat := O | S (n : nat).，模式[|n]正好对应它的两个构造子：

• 第一个空分支对应O（也就是0）的情况，这个构造子不带参数，所以不需要绑定任何变量；
• 第二个分支对应S n的情况，把构造子携带的自然数参数绑定到n上。

这种写法在处理简单归纳类型时特别高效，能帮你少写冗余代码。

2. 理解第一个分支为空的[ | H2]式case analysis #

这种写法本质是在匹配无参数的构造子。Coq的模式匹配语法里，竖线|分隔的每个分支对应归纳类型的一个构造子：

• 如果某个构造子没有携带参数（比如nat的O、布尔类型的true），那对应的分支就写成空的（也就是模式里的第一个空位置）；
• 如果构造子携带参数（比如nat的S、求和类型的inr），那就在分支里写上参数的绑定名（比如H2）。

举个更直观的例子，假设我们定义一个表示开关状态的类型：

Inductive switch : Type := | off | on (times : nat).

当我们对switch类型的变量s做case analysis时，destruct s as [ | t]就对应两种情况：

• 第一个空分支：匹配off构造子（开关关闭），这个分支里没有需要绑定的变量；
• 第二个分支：匹配on t构造子（开关打开，且记录了打开次数t），把构造子的参数绑定到t上。

如果看到类似[ | H2]的写法，直接对应“第一个构造子无参数，第二个构造子带一个参数并绑定到H2”的归纳类型即可。

内容的提问来源于stack exchange，提问作者user1868607