## Stream: Coq users

### Topic: Eliminate Prop in a Prop

#### spaceloop (Dec 16 2022 at 23:05):

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?

#### Paolo Giarrusso (Dec 16 2022 at 23:09):

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

#### Paolo Giarrusso (Dec 16 2022 at 23:20):

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

#### Paolo Giarrusso (Dec 16 2022 at 23:23):

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

#### Paolo Giarrusso (Dec 16 2022 at 23:24):

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`

#### James Wood (Dec 22 2022 at 12:50):

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: Jun 15 2024 at 05:01 UTC