How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

Question

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.

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.

So my question is:

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.

Guarneri

"Why" is not a programming question. – Boyett

Answer 1

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.

   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.

2. 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.
   

   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. *)
   

   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").

Erivan

Thanks for your wonderful answer. My initial goal was to prove: forall (P Q : Prop) (F : Prop -> Prop), (P <-> Q) -> (F P <-> F Q). But I can't, so I tried to prove the mentioned proposition. Unfortunately, I failed again. – Guarneri

Your initial goal and the mentioned proposition are actually equivalent in Coq without any additional axioms. (forall F, F P -> F Q) is even known as Leibniz equality. – Gymnosperm

@Gymnosperm I believe you misread it: the premise in the original goal is logical equivalence, not equality. If it were equality, it would indeed work. – Erivan

Let me try to be clearer: There is a Coq proof (sans additional axioms) of (forall (P Q : Prop) (F : Prop -> Prop), (P <-> Q) -> (F P <-> F Q)) <-> (forall (P Q : Prop), (P <-> Q) -> P = Q). – Gymnosperm

Oh, you are right, sorry, I was the one who misread what you had just written. – Erivan

@Arthur Azevedo De Amorim. Could you tell me why in the definition of true_not_false eq_refl => I:True gives a True type, while it's supposed to give a False type? – Guarneri

@Guarneri it's just the way dependent pattern-matching works. In our return clause, we are saying that we will return something of type if b then True else False, where the exact value of b may vary on each pattern-matching branch. There's just one branch, namely the eq_refl one, and on that branch b = true. Thus, we must return something of type if true then True else False = True. Outside, however, we're matching on true = false, thus the return type is actually if false then True else False = False. – Erivan