如何证明排除的中间在Coq中是无可辩驳的? [英] How to prove excluded middle is irrefutable in Coq?

问题描述

我试图从在线当然，排除中间部分是无可辩驳的，但是在步骤1中却被卡住了很多:

I was trying to prove the following simple theorem from an online course that excluded middle is irrefutable, but got stuck pretty much at step 1:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

现在我得到了:

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

如果我是apply H，则目标将是P \/ ~P，该目标被排除在中间，不能被建设性地证明.但是除了apply之外，我不知道关于假设P \/ (P -> False) -> False可以做什么:蕴涵->是原始的，我不知道如何destruct或分解它.这是唯一的假设.

If I apply H, then the goal would be P \/ ~P, which is excluded middle and can't be proven constructively. But other than apply, I don't know what can be done about the hypothesis P \/ (P -> False) -> False: implication -> is primitive, and I don't know how to destruct or decompose it. And this is the only hypothesis.

我的问题是，如何仅使用原始策略(

My question is, how can this be proven using only primitive tactics (as characterized here, i.e. no mysterious autos)?

谢谢.

推荐答案

我不是该主题的专家，但是最近在双重否定翻译.

I'm not an expert on this subject, but it was recently discussed on the Coq mailing-list. I'll summarize the conclusion from this thread. If you want to understand these kinds of problems more thoroughly, you should look at double-negation translation.

该问题属于直觉命题演算，因此可以由 tauto确定.

The problem falls within intuitionistic propositional calculus and can thus be decided by tauto.

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  tauto.
Qed.

该线程还提供了更详尽的证明.我将尝试解释我将如何提出这个证明.请注意，对我来说，处理引理的编程语言解释通常更容易，所以这就是我要做的:

The thread also provides a more elaborate proof. I'll attempt to explain how I would have come up with this proof. Note that it's usually easier for me to deal with the programming language interpretation of lemmas, so that's what I'll do:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  unfold not.
  intros P f.

要求我们编写一个函数，该函数采用函数f并产生类型为False的值.此时到达False的唯一方法是调用函数f.

We are asked to write a function that takes the function f and produces a value of type False. The only way to get to False at this point is to invoke the function f.

 apply f.

因此，要求我们为函数f提供参数.我们有两个选择，可以通过P或P -> False.我看不到构造P的方法，所以我选择第二个选项.

Consequently, we are asked to provide the arguments to the function f. We have two choices, either pass P or P -> False. I don't see a way to construct a P so I'm choosing the second option.

  right.
  intro p.

我们回到第一个方格，除了我们现在有一个p可以使用！ 因此，我们应用f是因为这是我们唯一可以做的事情.

We are back at square one, except that we now have a p to work with! So we apply f because that's the only thing we can do.

  apply f.

同样，我们被要求提供f的参数.现在，这很容易，因为我们有一个p可以使用.

And again, we are asked to provide the argument to f. This is easy now though, because we have a p to work with.

  left.
  apply p.
Qed. 

该线程还提到了基于一些更简单引理的证明.第一个引理是~(P /\ ~P).

The thread also mentions a proof that is based on some easier lemmas. The first lemma is ~(P /\ ~P).

Lemma lma (P:Prop) : ~(P /\ ~P).
  unfold not.
  intros H.
  destruct H as [p].
  apply H.
  apply p.
Qed.

第二个引理是~(P \/ Q) -> ~P /\ ~Q:

Lemma lma' (P Q:Prop) : ~(P \/ Q) -> ~P /\ ~Q.
  unfold not.
  intros H.
  constructor.
  - intro p.
    apply H.
    left.
    apply p.
  - intro q.
    apply H.
    right.
    apply q.
Qed.   

这些引理足以满足节目需求:

These lemmas suffice to the show:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  intros P H.
  apply lma' in H.
  apply lma in H.
  apply H.
Qed.

这篇关于如何证明排除的中间在Coq中是无可辩驳的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！