Как или это возможно доказать или фальсифицировать `forall (P Q: Prop), (P -> Q) -> (Q -> P) -> P = Q` в Coq?

Question

Я хочу доказать или фальсифицировать 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. Но если это так, то почему необходимо исключить содержание доказательства?

Без вышеизложенного я не могу доказать следующее или их отрицания.

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 тратит энергию на это.

Answer 1

1. Принцип, который вы упоминаете, forall P Q : Prop, (P <-> Q) -> P = Q, обычно известный как экстенсиональность высказываний. Этот принцип не доказуем в логике Кока, и изначально логика была разработана таким образом, чтобы его можно было добавить в качестве аксиомы без вреда. Таким образом, в стандартной библиотеке (Coq.Logic.ClassicalFacts), можно найти много теорем об этом принципе, связывая его с другими хорошо известными логическими принципами классического мышления. Удивительно, но недавно выяснилось, что логика Кока несовместима с этим принципом, но по очень тонкой причине. Это считается ошибкой, поскольку логика была разработана таким образом, чтобы ее можно было добавить в качестве аксиомы без вреда. Они хотели исправить эту проблему в новой версии Coq, но я не знаю, каково это текущее состояние. Начиная с версии 8.4, пропозициональная экстенсиональность несовместима с Coq.

   В любом случае, если эта ошибка будет исправлена ​​в будущих версиях Coq, не будет возможности доказать или опровергнуть этот принцип в Coq. Другими словами, команда Coq хочет, чтобы этот принцип не зависел от логики Coq.

2. inversion H ничего не делает там, потому что правила рассуждений о доказательствах (вещи, тип которых Prop) отличаются от рассуждений о не доказательствах (вещи, тип которых 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.
   

   Если вы попытаетесь сделать то же самое с версией bool в 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 был разработан, чтобы быть совместимым с другим принципом, называемым доказательством неуместности (я думаю, это то, что вы подразумевали под "независимостью доказательства").