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: Oct 04 2023 at 18:01 UTC