如何消除表达式中的析取？以Coq中In_map_iff引理证明为例

你卡在这个子目标很正常，其实不用执着于“消除”析取项，反而可以利用存在量词的构造性和归纳假设直接完成证明。让我们一步步拆解：

当前你的目标是：

exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 l)

而上下文里有归纳假设 IHl : forall (f : A -> B) (y : B), In y (map f l) -> exists x : A, f x = y /\ In x l，还有前提 H : In y (map f l)。

核心思路 #

我们不需要处理析取里的 x = x0 分支——因为归纳假设已经给了我们一个完美的 x0：它满足 f x0 = y 且 In x0 l，而 In x0 l 直接蕴含 x = x0 \/ In x0 l（选析取的右边就行）。

具体证明步骤 #

在当前子目标下输入以下命令：

1. 先用归纳假设处理前提 H，得到存在的 x0 和对应的两个条件：

   destruct (IHl f y H) as [x0 [Hfx0 Hinl]].
   

   这一步会生成 x0 : A，Hfx0 : f x0 = y，Hinl : In x0 l。
2. 用这个 x0 实例化目标里的存在量词：

   exists x0.
   

3. 拆分合取目标：

   split.
   

4. 第一个子目标是 f x0 = y，直接用 Hfx0：

   - assumption.
   

5. 第二个子目标是 x = x0 \/ In x0 l，我们选右边的分支，用 Hinl：

   - right. assumption.
   

这样就完成了这个子目标的证明。

为什么你的之前尝试没用？ #

• left in ... 是用来在目标中选择析取的左边，但这里我们根本不需要走左边的分支——因为当前的 H 是 In y (map f l)，说明 y 不在 f x 里（前面的分支已经处理了 y = f x 的情况），所以左边的 x = x0 对我们没有帮助。
• 辅助函数改写存在量词下的项之所以无效，是因为存在量词的绑定会阻止直接重写——你需要先把存在的实例提取出来（也就是 destruct 那一步），才能操作里面的合取和析取。

内容的提问来源于stack exchange，提问作者Marko Grdinić