Prove two inhabitants in Prop are not equal?

1
votes

Is it possible to have some A, B : Prop such that we can provide a proof of:

Section QUESTION.
A: Prop := <whatever you want> .
B : Prop := <whatever you want> .
Theorem ANeqB: A <> B.
Proof.
<a proof of this fact>
Qed.

Intuitively, I think not, since this would let us "distinguish" between proofs, but one should not be able to do this without computing on A or B. However, Coq explicitly forbids us from inspecting a proof, since they must be erased at runtime. So, only Prop ought to be able to inspect Prop (due to erasure), but inspection is always computational, hence Prop cannot inspect Prop. Therefore, nothing can inspect Prop, and the above theorem ANeqB cannot be proved.

  • If my above explanation is incorrect, could you please explain to me why it is so?
  • If the theorem ANeqB cannot be proved, can you point me a proof of this fact?
  • If the theorem ANeqB can be proved, can you tell me where my intuition fails?

EDIT:

It just struck me that since we can take proof irrelevance as an extra axiom (Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.), the theorem ANeqB cannot be proven within Coq --- if it could, it would make it unsound to allow proof_irrelevance as an extra axiom.

This shifts my question, then:

  • Is it possible to prove ANeqB for some inhabitants A and B? (proof_irrelevance is stronger: it states that we cannot prove A <> B [actually, the more stronger statement that we can prove A = B] for all A, B)
  • If not, can someone furnish a proof that ANeqB cannot be proved in Coq's based axiomatic system?
1
coqproofformal-verification

1 Answers

1
votes

I think you might be thinking of something else. Prop itself isn't proof irrelevant. It definitely has distinguishable elements. For example, True <> False.

Section QUESTION.
Definition A: Prop := True.
Definition B : Prop := False.

Theorem ANeqB: A <> B.
Proof.
  unfold A, B.
  intro p.
  destruct p.
  exact I.
Qed.

End QUESTION.

Instead, it's elements of Prop that might be proof irrelevant. In the axiom

Axiom proof_irrelevance: forall (P: Prop) (p q: P), p = q.

p and q aren't themselves elements of Prop, but rather elements of some element of Prop.