如何或可能证明或伪造“所有人"(P Q:Prop)，(P-> Q)-> (Q-> P)-> P =Q. [英] How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

问题描述

我想证明或伪造Coq中的forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q..这是我的方法.

I want to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq. Here is my approach.

Inductive True2 : Prop :=
 | One : True2
 | Two : True2.

Lemma True_has_one : forall (t0 t1 : True), t0 = t1.
Proof.
  intros.
  destruct t0. destruct t1.
  reflexivity.
Qed.

Lemma not_True2_has_one : (forall (t0 t1 : True2), t0 = t1) -> False.
Proof.
  intros.
  specialize (H One Two).
  inversion H.

但是，inversion H什么也不做.我认为可能是因为coq的证明独立性(我不是英语母语人士，并且我不知道确切的单词，请原谅我的无知)，并且coq使得不可能证明One = Two-> False.但是，如果是这样，为什么必须要求消除证明的内容呢?

But, inversion H does nothing. I think maybe it's because the coq's proof independence (I'm not a native English speaker, and I don't know the exact words, please forgive my ignorance), and coq makes it impossible to prove One = Two -> False. But if so why has to coq eliminate the content of a proof?

没有上述主张，我无法证明以下内容或它们的否定.

Without the above proposition, I can't prove the followings or their negations.

Lemma True_neq_True2 : True = True2 -> False.

Theorem iff_eq : forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.

所以我的问题是:

1. 如何或有可能在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.?
2. 为什么inversion H什么也不做；是因为coq的证明独立性，如果是这样，为什么Coq这样做会浪费能量.

1. How to or is that possible to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq?
2. Why inversion H does nothing; does it's because the coq's proof independence, and if so, why does Coq waste energy in doing this.

推荐答案

1. 您提到的原理forall P Q : Prop, (P <-> Q) -> P = Q通常称为命题可扩展性.该原理在Coq的逻辑中无法得到证明，并且最初设计该逻辑是为了使其可以作为无公害的公理添加.因此，在标准库(Coq.Logic.ClassicalFacts)中，可以找到有关此原理的许多定理，并将其与经典推理的其他众所周知的逻辑原理相关联.令人惊讶的是，最近发现Coq的逻辑与此不兼容.原理，但是有一个非常微妙的原因.这被认为是一个错误，因为已经对逻辑进行了设计，因此可以将其作为公理添加而没有任何危害.他们想在新版本的Coq中解决此问题，但我不知道它的当前状态是什么.从8.4版开始，命题可扩展性在Coq中是不一致的.

1. The principle you're mentioning, forall P Q : Prop, (P <-> Q) -> P = Q, is usually known as propositional extensionality. This principle is not provable in Coq's logic, and originally the logic had been designed so that it could be added as an axiom with no harm. Thus, in the standard library (Coq.Logic.ClassicalFacts), one can find many theorems about this principle, relating it to other well-known logical principles of classical reasoning. Surprisingly, it was recently found out that Coq's logic is incompatible with this principle, but for a very subtle reason. This is considered a bug, since the logic had been designed so that this could be added as an axiom with no harm. They wanted to fix this problem in the new version of Coq, but I don't know what the current status of that is. As of version 8.4, propositional extensionality is inconsistent in Coq.

无论如何，如果此错误在Coq的将来版本中已修复，则不可能在Coq中证明或反驳此原理.换句话说，Coq团队希望此原理与Coq逻辑无关.

In any case, if this bug is fixed in future versions of Coq, it should not be possible to prove nor disprove this principle in Coq. In other words, the Coq team wants this principle to be independent of Coq's logic.

inversion H在那里不做任何事情，因为关于证明的推理规则(类型为Prop的事物)与关于非证明的推理规则(类型为的事物)不同c8>).您可能知道Coq中的证明只是条款.在引擎盖下，inversion本质上是在构造以下术语:

inversion H doesn't do anything there because the rules for reasoning about proofs (things whose type is a Prop) are different from the ones for reasoning about non-proofs (things whose type is a Type). You may know that proofs in Coq are just terms. Under the hood, inversion is essentially constructing the following term:

Definition true_not_false : true <> false :=
  fun H =>
    match H in _ = b
            return if b then True else False
    with
    | eq_refl => I
    end.

如果您尝试对Prop中的bool版本执行相同操作，则会得到更多信息错误:

If you try to do the same with a version of bool in Prop, you get a more informative error:

Inductive Pbool : Prop :=
| Ptrue : Pbool
| Pfalse : Pbool.

Fail Definition Ptrue_not_Pfalse : Ptrue <> Pfalse :=
  fun H =>
    match H in _ = b
            return if b then True else False
    with
    | eq_refl => I
    end.

(* The command has indeed failed with message: *)
(* => Error: *)
(*    Incorrect elimination of "b" in the inductive type "Pbool": *)
(*    the return type has sort "Type" while it should be "Prop". *)
(*    Elimination of an inductive object of sort Prop *)
(*    is not allowed on a predicate in sort Type *)
(*    because proofs can be eliminated only to build proofs. *)

实际上，这样做的原因之一是Coq被设计为与另一个称为证明无关的原则兼容(我认为这就是您所说的证明独立性").

Indeed, one of the reasons for this is that Coq was designed to be compatible with another principle called proof irrelevance (I think that's what you meant by "proof independence").

这篇关于如何或可能证明或伪造“所有人"(P Q:Prop)，(P-> Q)-> (Q-> P)-> P =Q.的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！