Coq中如何将P(?x)转为exists x,P(x)实现不同子目标的差异化实例化？

你遇到的核心问题是Coq的存在变量（evar，即?x这类符号）是全局绑定的：一旦在某个分支中实例化了?x，所有其他分支都会共享这个实例，导致后续分支无法匹配所需的取值。以下是几种可行的解决思路：

1. 将P(?x)转换为exists x, P(x)（最直接的方案） #

完全可以把原目标转换成带显式存在量词的形式，这样每个分支可以独立指定x的取值，不会互相干扰。具体操作有两种：

• 用eexists命令：直接将目标从P(?x)转为exists x, P(x)，此时Coq会生成一个新的存在变量（比如?x0），但这个变量是被存在量词包裹的，后续每个分支可以单独实例化：

  eexists.  (* 目标变为 exists x, P(x) *)
  

  之后在每个分支里，用refine (exist _ <具体值> _)来指定当前分支的x实例，比如分支1用refine (exist _ 1 _)，分支2用refine (exist _ 0 _)，各自的实例化互不影响。
• 用assert显式断言：如果需要更清晰的步骤，可以先断言存在性命题，再关联到原目标：

  assert (H : exists x, P(x)).
  { (* 在这里分分支证明H，每个分支指定不同的x *) }
  exact H.  (* 将断言的结果应用到原目标 *)
  

2. 用case_eq替代普通destruct保留更多信息 #

普通的destruct在解构项t时会丢失t与构造子的等式关联，可能导致Coq提前实例化?x。改用case_eq可以在每个分支中保留t = <构造子>的假设，让你可以在需要的时候再实例化?x：

case_eq t.  (* 解构t，每个分支多一个假设：t = 某个构造子 *)

之后你可以根据每个分支的假设，手动指定?x的实例，而不是让Coq自动绑定全局的evar。

3. 用set临时绑定存在变量 #

如果不想引入显式的存在量词，可以先用set把?x绑定到一个临时变量，避免全局实例化：

set (my_x := ?x).  (* 原目标变为P(my_x)，?x被隐藏在my_x后面 *)

之后在每个分支里，你可以用unfold my_x并指定具体值，或者用rewrite替换my_x的取值，完成当前分支的证明后，不会影响其他分支的my_x绑定。

4. 高级方案：multiequal策略 #

如果存在变量在目标的多个位置出现，且不同分支需要不同的实例，可以使用multiequal策略，它允许你在不同分支为同一个存在变量指定不同的实例。不过这个策略相对复杂，适合处理多位置evar的场景：

multiequal ?x.  (* 标记?x为可多分支实例化的变量 *)

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