如何在Coq中证明A ∨ False → A？代码报错求助

你在Coq中尝试证明「A ∨ False → A」时遇到报错，使用的代码如下：

Goal forall A False : Prop, A / False -> A.

Proof.

intros A False H.

destruct H as [HP | HQ].

apply HP.

exfalso.

apply HQ.

得到报错信息：Unable to unify "False" with "Logic.False".

问题原因 #

你在forall语句里将False声明为自定义的Prop变量，这会覆盖Coq标准库中内置的Logic.False类型。此时假设HQ的类型是你自定义的False，但exfalso需要的是标准库原生的False，两者属于不同的类型，因此无法完成统一匹配。

修正后的代码 #

Goal forall A : Prop, A ∨ False → A.

Proof.
intros A H.
destruct H as [HP | HQ].
- apply HP.
- exfalso.
  apply HQ.
Qed.

关键说明 #

• 移除forall中的False : Prop声明，直接使用Coq内置的False常量
• 解构析取式H后，第一个分支直接应用HP即可完成证明
• 第二个分支里，HQ的类型就是标准库的False，可以直接传递给exfalso来触发矛盾证明

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