Why is it not possible to eliminate a `Prop`

in the following way?

```
Definition is_left {P Q} (H : P \/ Q) : Prop := match H with | or_introl x => True | or_intror x => False
```

I understand that it is not possible to eliminate in a Set such as `nat`

, since Props have to be erasable and computation cannot depend on it. However, when eliminating to the Type `Prop`

, I don't see how a computation could depend on it. Is there a different reason?

That definition + propositional proof irrelevance would give you a proof of False, I think?

Basically, proof irrelevance gives you `or_intror x = or_introl y`

, which you can turn into `False = True`

:

```
Require Import Coq.Logic.ProofIrrelevance.
Require Import Utf8.
Require Import ssreflect.
Section PQ.
Context {P Q : Prop}.
Definition is_left (H : P \/ Q) : Prop. Admitted.
Axiom is_left_introl : ∀ x, is_left (or_introl x) = True.
Axiom is_left_intror : ∀ y, is_left (or_intror y) = False.
End PQ.
Goal False.
rewrite -(@is_left_intror True True I).
rewrite (_ : or_intror I = or_introl I). { exact: proof_irrelevance. }
by rewrite is_left_introl.
Qed.
```

while propositional proof irrelevance does _not_ let you prove False, and the extra axioms I added just encode your definition

so, it's true that types are typically not needed at runtime, but that does not make them irrelevant. And that's why `p = q : P`

is fine if `P : Prop`

, not if `P = Prop`

or `P = Type`

Maybe the answer you wanted to hear was that `Prop`

itself is not a `Prop`

, so the restrictions on eliminating propositions kick in.

Last updated: Oct 04 2023 at 18:01 UTC