8

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

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。但如果是这样,为什么必须 coq 消除证明的内容?

没有上述命题,我就无法证明以下命题或它们的否定。

Lemma True_neq_True2 : True = True2 -> False.

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

所以我的问题是:

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

1 回答 1

13
  1. 您提到的原则forall P Q : Prop, (P <-> Q) -> P = Q通常称为命题外延性。这个原则在 Coq 的逻辑中是不可证明的,并且最初的逻辑是被设计成可以作为公理添加而不会造成伤害的。因此,在标准库Coq.Logic.ClassicalFacts(令人惊讶的是,最近发现 Coq 的逻辑与这个原则不兼容,但是出于一个非常微妙的原因。这被认为是一个错误,因为已经设计了逻辑,以便可以将其作为公理添加而不会造成伤害。他们想在新版本的 Coq 中解决这个问题,但我不知道它的当前状态是什么。从 8.4 版本开始,Coq 中的命题外延性是不一致的。

    无论如何,如果这个错误在未来的 Coq 版本中得到修复,那么在 Coq 中应该无法证明或反驳这个原则。换句话说,Coq 团队希望这个原则独立于 Coq 的逻辑。

  2. inversion H在那里不做任何事情,因为推理证明(类型为 a 的事物)的规则与推理Prop非证明(类型为 a 的事物Type)的规则不同。你可能知道 Coq 中的证明只是术语。在引擎盖下,inversion本质上是在构建以下术语:

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

    如果您尝试对boolin的版本执行相同操作Prop,则会收到更多信息错误:

    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 被设计为与另一个称为证明无关性的原则兼容(我认为这就是您所说的“证明独立性”)。

于 2014-10-26T15:22:56.100 回答