Coq中case战术语法解析、等价destruct改写及官方文档查询咨询

嗨，我来帮你拆解这个Coq战术，同时给出等价的destruct写法，以及官方文档的查询方向~

一、case x : fun H => [|[]] // _. 的作用解析 #

我们把这个战术拆成几个核心部分逐一理解：

• case x :：指定对项x进行case分析，并且将x的原始值绑定到名字x上（这是case和destruct的关键差异之一——case会保留原项的绑定，后续证明中仍能引用原始的x，而destruct默认会直接拆解原项，不保留这个绑定）。
• fun H => [|[]]：这是分支匹配的自定义写法：
  • fun H表示第一个case分支会引入一个名为H的假设（通常和x对应类型的构造子前提相关）；
  • [|[]]是用竖线分隔的两个分支模板：第一个分支（|左侧）为空，表示匹配无参数的构造子（比如list类型的nil），直接保留对应子目标；第二个分支（|右侧）的[]表示该分支的子目标可直接被消解（或生成空目标）。
• // _：//是Coq的自动化战术简写，等价于对每个子目标应用auto（或默认的自动化证明策略）；_表示匹配所有剩余子目标，也就是对case分析后生成的所有子目标都尝试自动证明。

整体作用总结：对x做保留原绑定的case分析，分两个分支处理，第一个分支引入假设H并保留子目标，第二个分支生成可自动解决的子目标，最后尝试自动完成所有剩余证明。

二、等价的destruct改写 #

根据是否需要保留原项x的绑定，有两种等价写法：

1. 不需要保留原绑定的简化版本：

destruct x as [ | [] ] //

2. 需要保留原绑定（和原case x :效果完全对齐）的版本：

destruct x eqn:x as [ | [] ] //

这里的as [ | [] ]对应原战术的分支模式，//同样负责自动解决子目标，和原战术的// _效果一致。

三、官方文档的查询位置 #

你可以在Coq自带的**参考手册（Reference Manual）**里找到这类语法的详细说明：

• 先看「Tactics」章节下的case战术小节，里面会讲解case的扩展语法，包括带绑定、自定义分支模式的写法；
• 再看「Extended Pattern Matching」相关章节，里面会解释[|...]这种分支模式的语法规则；
• 另外，//这类自动化简写属于「Tactic Notations」的内容，在手册对应章节也有明确说明。

这些内容都在Coq官方的内置文档里，你可以通过CoqIDE、VsCoq等工具的帮助功能直接查看，不需要跳转外部网站。

备注：内容来源于stack exchange，提问作者user6584