Coq中unfold策略delta规约后beta规约触发条件的疑问

核心原因：规约的前提是表达式可被化简 #

Coq的unfold策略确实会先执行delta展开（即展开定义），再尝试beta、iota、zeta等规约，但这些后续规约只有当表达式处于可规约状态时才会触发。你的例子中，destruct t前后unfold myFunction的表现差异，本质是t的形态不同导致后续规约的条件是否满足。

1. 未destruct t时的情况 #

当t是一个未实例化的变量时：

• unfold myFunction会展开myFunction的定义，但定义中else分支的match t with tree_cons subtrees => ...是对变量的模式匹配。此时Coq无法确定t的构造子，因此无法执行iota规约（模式匹配的化简规则）。
• 而定义中的let l' := l++[index] in ...会被zeta规约为函数抽象的应用形式，再执行beta规约（即把(fun l' => body) (l++[index])替换为body中l'被l++[index]替换后的内容），这部分其实是执行了的，但可能你没有关注到这一点，而是聚焦在match t未被化简的部分。

2. destruct t后的情况 #

当你执行destruct t as [subtrees]后，t被实例化为tree_cons subtrees（因为tree归纳类型只有这一个构造子）：

• 此时unfold myFunction展开定义后，else分支的match t with tree_cons subtrees => ...就变成了对具体构造子的模式匹配，满足iota规约的条件，会直接化简为分支内的flat_map_index (myFunction l') O subtrees。
• 同时，let绑定的zeta/beta规约依然会正常执行，所以你会看到整个表达式被进一步化简，看起来像是“触发了更多规约”。

澄清beta规约和iota规约的区别 #

你提到的“beta规约”可能混淆了两个概念：

• beta规约：针对函数应用，即把(fun x => e) v化简为e[v/x]，比如let绑定的本质就是匿名函数的应用，所以let x := v in e会被zeta+beta规约为e[v/x]。
• iota规约：针对模式匹配，即当匹配的表达式是已知构造子的实例时，直接替换为对应的分支内容，比如match tree_cons l with tree_cons subtrees => subtrees end会被iota规约为l。

你的例子中，destruct前后最明显的差异是iota规约是否被触发，而beta规约在两次unfold中其实都执行了（针对let绑定的部分）。

验证方法 #

你可以在未destruct t时执行unfold myFunction; simpl，会发现let绑定的部分被化简，但match t依然保留；而destruct t后执行unfold myFunction; simpl，match t会被直接替换为对应的分支内容。

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