英文:
How to prove A \/ False -> A in Coq?
问题
I am learning Coq and trying to prove "A / False -> A" but I am not sure what am I doing wrong.
I tried the following code:
Goal forall A False : Prop, A \/ False -> A.
Proof.
intros A False H.
destruct H as [HP | HQ].
apply HP.
exfalso.
apply HQ.
And expected to establish the premise for exfalso by applying the assumption HQ but it did not work and I got the following message: "Unable to unify "False" with "Logic.False"."
英文:
I am learning Coq and trying to prove "A \/ False -> A" but I am not sure what am I doing wrong.
I tried the following code:
Goal forall A False : Prop, A \/ False -> A.
Proof.
intros A False H.
destruct H as [HP | HQ].
apply HP.
exfalso.
apply HQ.
And expected to establish the premise for exfalso by applying the assumption HQ but it did not work and I got the following message: "Unable to unify "False" with "Logic.False"."
What am I missing?
答案1
得分: 2
你的陈述中，你量化了一个你称为 False 的命题。这与在 Logic 中定义的 False 产生冲突。因此，在你的环境中有两个 False，一个是你的命题，另一个是在 Logic 中定义的，它们不同。
你想要证明的陈述等同于 forall A B : Prop, A \/ B -> A。
英文:
In your statement you quantify over a proposition that you name False. There is a clash with the False that is defined in Logic. So in your environment you have two False your proposition and the one in Logic and they differ.
The statement you want to prove is equivalent to forall A B : Prop, A \/ B -> A
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论