Coq中destruct策略对任意类型假设的通用作用规则疑问

destruct 策略的通用运行规则 #

destruct 本质是对假设的类型所对应的归纳定义做构造子拆分，核心逻辑完全统一：

• 定位到假设H的类型对应的归纳定义，枚举该类型的所有构造子
• 每个构造子对应一个证明分支，构造子的参数会自动作为新的约束/假设引入上下文
• 拆分完成后原假设H会被移除

大家熟悉的合取/\、析取\/的拆分逻辑完全符合以上规则，接下来针对你遇到的两类特殊场景逐一解释： #

场景1：假设H为等式类型a = b #

Coq中等于关系eq是标准归纳类型，仅包含一个构造子eq_refl : forall A (x:A), x = x，即等式成立的唯一前提是等号两边的项完全相等。
当你执行destruct H且H的类型为a = b时，Coq会强制将上下文中所有的b替换为a（或反过来，取决于参数定义顺序），同时把目标中所有的b也替换为a，原假设H直接移除。
对应你的示例1：
H的类型是x = 4，destruct H后，目标中的4被统一替换为x，原本的目标x = 4就变成了x = x，和你观测到的结果完全一致。 #

场景2：假设H为蕴含类型A -> B #

蕴含类型本质是函数类型，你可以把H: A -> B理解为「只要给出一个A的证明，就能得到一个B的证明」。当你直接对蕴含类型的假设执行destruct时，Coq会自动执行两步操作：

1. 要求你先证明A（对应第一个分支，本质是要你先构造出H的输入参数）
2. 用你给出的A的证明应用H，得到B类型的项，再对这个B类型的项执行destruct拆分，得到后续分支

我们直接对应你的测试示例验证：

示例2匹配说明

H的类型是(x=4) -> (x=4)，即A为x=4，B为x=4：

• 第一步要求你证明A也就是x=4，对应第一个分支的目标
• 拿到A的证明后，应用H得到B类型的项x=4，再对这个项做destruct，此时你的目标是True，替换后无变化，对应第二个分支的目标True。

示例3匹配说明

和示例2的H完全一致，仅目标变为x=4：

• 第一个分支还是要求你证明A也就是x=4
• 应用H得到x=4的项后执行destruct，目标中的4被替换为x，所以第二个分支的目标变成x=x，和你观测到的结果完全匹配。

实用提示 #

日常写证明时，除非你明确知道拆分后的行为，否则不要直接对蕴含类型的假设执行destruct，通常我们会先调用apply策略，或者把蕴含应用到具体的前提上之后再做处理。

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