能否在Coq中重写引用内部作用域变量的项？

问题场景 #

先看示例代码：

Theorem foo (f : nat -> nat) (rw : forall x, f x = 5) x : match x with
| 0 => 5
| S a => f a
end = 5.
  rewrite rw.
(* Error: Found no subterm matching "f ?M160" in the current goal. *)

  destruct x; try rewrite rw; apply eq_refl.
Qed.

直接调用rewrite rw失败，核心原因是match分支里的a属于局部作用域，顶层的rewrite无法匹配到这个绑定变量对应的f a。

无法直接跨作用域重写的原因 #

技术实现限制 #

Coq的rewrite策略默认只匹配当前证明上下文顶层可见的自由变量。而match、fun、fix这类构造中的绑定变量属于局部作用域，它们在顶层上下文里并不存在——a是match x with S a => ...分支内临时绑定的变量，顶层没有这个自由变量，所以rewrite rw（需要匹配f ?x，其中?x是自由变量）找不到对应的子项。

逻辑合理性与作用域封装 #

允许直接重写局部作用域的绑定变量会破坏作用域的封装性，引发变量泄漏问题：局部变量仅在对应分支或构造内有效，强行在顶层操作相当于把局部变量暴露到全局上下文，违背了逻辑构造的设计意图。此外，局部变量依赖于分支条件（比如x = S a）才存在，未拆分分支前变量取值不确定，直接重写会导致逻辑歧义。

fix构造的情况 #

对于fix定义的递归函数，规则完全一致：递归子句里的绑定变量（比如递归调用的参数）属于fix的局部作用域，顶层rewrite无法直接匹配。必须先通过unfold展开递归、destruct拆分递归结构等操作，把局部变量提升到当前证明上下文，才能进行重写。

总结 #

这类跨作用域直接重写并非逻辑上不可行，而是Coq策略设计的刻意限制——既维护作用域封装性，也避免逻辑歧义。实际证明中，必须先通过拆分结构（如destruct、case）将局部作用域的变量引入顶层上下文，再执行重写操作。

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