SSReflect中have语句与方括号模式的理解及学习建议

为理解SSReflect证明中的方括号模式，我尝试了以下几种have语句的写法：

Lemma test : True.
Proof.
have : exists v : nat, v > 0; last first.
Undo 1.
have []: exists v : nat, v > 0; last first.
Undo 1.
have [[]]: exists v : nat, v > 0; last first.
Undo 1.
have [[] []]: exists v : nat, v > 0; last first.
Undo 1.
have [a b]: exists v : nat, v > 0; last first.
Abort.

我理解have后的语句是存在命题exists v : nat, v > 0，其中have : ...、have []: ...、have [a b]: ...这三种模式的结果容易理解，但对以下两种情况存在困惑：

• 执行have [[]]: exists v : nat, v > 0; last first.后生成两个目标，猜测是对nat的归纳构造子展开，但不理解目标的对应关系，尤其是出现0 < 0这种不可能的情况。
• 执行have [[] []]: exists v : nat, v > 0; last first.后生成三个目标，完全不清楚其来源。

我查阅过SSReflect的论文，但相关章节多为规范说明，缺乏示例难以理解；常借助cheat sheet和教程学习，但担心方法有误，希望得到SSReflect的学习建议。

方括号模式的本质 #

SSReflect的have语句中方括号是模式匹配语法，用于直接解构归纳类型、存在类型等复合结构，不同的嵌套层级对应不同的解构深度，本质上等价于组合使用destruct/case等策略。

困惑情况解析 #

1. have [[]]: exists v : nat, v > 0; last first.

这里的[[]]是两层嵌套模式：

• 外层[]：解构存在类型exists v, P v，提取出见证者v和对应的命题P v（即v > 0）；
• 内层[]：对提取出的v : nat做归纳解构，遍历nat的两个构造子：
  • 第一个分支：v = O，此时命题变为O > 0（即0 < 0），对应第一个目标；
  • 第二个分支：v = S n，此时命题变为S n > 0，对应第二个目标。
    第一个目标是逻辑上的矛盾，后续可通过contradiction等策略直接排除。

2. have [[] []]: exists v : nat, v > 0; last first.

这里的[[] []]是对存在类型解构后的两个部分分别做模式匹配：

• 最外层[]先解构存在类型，得到v和v > 0两个元素；
• 第一个内层[]：对v : nat做归纳解构，生成O和S n两个分支；
• 第二个内层[]：对命题v > 0做解构——v > 0本质是基于归纳类型le（小于等于）定义的gt（大于），解构gt会遍历其底层归纳构造子。

将两个解构的分支组合后，会产生三个目标：

1. v = O且需要证明O > 0（矛盾目标）；
2. v = S n且通过le的第一个构造子证明S n > 0；
3. v = S n且通过le的第二个构造子证明S n > 0。

这种嵌套模式在实际证明中几乎不会用到，属于过度解构的写法。

SSReflect学习建议 #

• 先掌握基础解构逻辑：SSReflect的模式语法和Coq原生的destruct、case策略一一对应，先把原生策略对归纳类型、存在类型的解构逻辑搞清楚，再映射到方括号模式上，避免直接啃复杂嵌套。
• 用小例子调试验证：每次尝试新模式后，用Show命令查看上下文和目标的变化，对比模式前后的差异，明确每一层方括号的作用。比如在你的例子中，执行命令后用Show就能直观看到目标对应的构造子分支。
• 优先选择带示例的学习资源：跳过纯规范的论文，先看带大量证明例子的教程内容，cheat sheet仅作为速查工具，不能替代系统学习。
• 模仿成熟代码：参考Coq标准库中用SSReflect编写的证明，或者社区开源项目中的SSReflect代码，观察实际场景中模式的使用方式，避免无意义的嵌套写法。

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