CODEWITHSUNDEEP
coqproofformal-verification
Siddharth Bhat
Siddharth Bhat

Reputation: 843

Prove two inhabitants in Prop are not equal?

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.

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:

Upvotes: 1

Views: 230

Answers (1)

SCappella
SCappella

Reputation: 10474

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.

Upvotes: 1

Related Questions