Although the SProp sort is still marked as experimental in the Coq documentation, given that it has been present for some three years I think one can guess it is here to stay in one form or another. Given that, I’ve started looking into using it as an alternative to importing Coq.Logic.ProofIrrelevance when I need or want a proof-irrelevant sort.
In my handful of experiments, working with SProp has felt like an uphill battle. I understand exactly why you can’t eliminate an SProp term to get a Prop term or anything else, but given that the entire standard library and just about every Coq user puts all their propositions in Prop it can result in some pretty rough ergonomics (not to mention aesthetics). One is constantly boxing and unboxing and squashing, and frequently discovers only at the end of a proof, when Qed fails, that one has inadvertently performed some invalid operation that was not caught at the time. And if everything does go right, one has a result that can only be used by people who are willing to put all their own work in SProp, which is kind of a big ask and not something I really expect most people to do.
By contrast, admitting proof irrelevance as an axiom couldn’t possibly be simpler. It works exactly as one would expect, produces no inscrutable elimination errors, and as far as I can see is already included in most libraries where it is at all useful. I assume it breaks some nice metatheoretic property or another, but then I don’t really understand how SProp can avoid doing the same thing (assuming the problem is with proof irrelevance as a concept and not with axioms per se).
I like to work without importing extra axioms when I don’t actually need them, but in this case I feel like trying to avoid it is just making things difficult for its own sake. So I ask: is there any reason one should prefer to work in SProp? Is there anything important list by importing proof irrelevance for Prop that isn’t already lost by being in SProp anyway? Have I completely misunderstood and this is not the problem SProp is supposed to solve in the first place?
I realize the way this is written makes it sound like I’ve already made my choice, but I really am interested in learning if there is some application where SProp shines.
(Related but tangential question: is Prop = SProp consistent with the theory of Coq?)
I assume it breaks some nice metatheoretic property or another, but then I don’t really understand how SProp can avoid doing the same thing (assuming the problem is with proof irrelevance as a concept and not with axioms per se).
The problem is with axioms. If you are fine with axioms (and the typical consequence of sometimes having a reduction block on the axiom) then feel free to use them.
Thanks for the link. I actually wasn’t sure if there were any significant developments using SProp so it’s good to have one to look at. Might be interesting to go through and find an example of a computation that would block if using axioms but is not blocked with SProp.
This may be a way out, right? We could start using Pprop = SProp as an axiom to bridge the gap between Prop+proof_irrelevance and people using SProp:
For people currently using proof_irrelevance, this does not change their logic, and it makes it possible to interact easily with “nice” newer developments using SProp.
For people currently using SProp but limited interoperability-wise, they have the option to use this axiom to simplify their life during the transition period where everyone else is still using Prop. This changes the logic (compared to standard Coq with both Prop and SProp), but maybe they would have moved to Prop + proof_irrelevance anyway if SProp did not exist.
In this setting a PropIsSProp axiom could work as a clutch to ease the transition from Prop to SProp. Hopefully after some time, it becomes easy enough to work with SProp entirely, and the clutch can be removed – in the meantime it can be gradually pushed away towards the boundaries of the SProp-centric codebase.
The command has indeed failed with message:
Universe inconsistency. Cannot enforce SProp = Prop.
Rewriting did not fare much better.
Fail rewrite H.
The command has indeed failed with message:
Abstracting over the term “Prop” leads to a term λ T : Type, ∀ (P : T) (p1 p2 : P), p1 = p2
which is ill-typed.
Reason is: In environment H : Prop = SProp T : Type P : T
The term “P” has type “T” which should be Set, Prop or Type.
One more try:
intros.
Fail rewrite H in P.
The command has indeed failed with message:
Cannot change P, it is used in conclusion.
Abort.
I do understand the second error (rewriting requires a generalization of Prop to a “generic type” T, whereas the goal is only well-formed when T is a sort), and the third is not really surprising since I run into such problems all the time, but the first seems to indicate a more fundamental problem. Is there a way around it? Like @gasche I like the idea of using this axiom as a replacement for directly axiomatized proof irrelevance, but it doesn’t seem actually usable if I can’t use it to prove proof irrelevance in Prop.
I think the first error may be a bug, but if I try a fix I just get the second error.
I think Prop = SProp is insufficient to do what you want, it somehow says that Prop and SProp are isomorphic but not that the isomorphism maps inhabited propositions to inhabited strict propositions (and vice versa).
Oh yeah, that does it. Even just postulating a right inverse does it, and gives us an unsquash : Squash P -> P proof in the bargain. In fact it’s pretty obvious why this must be the case, because boxed SProps are already proof-irrelevant and this implies every Prop is a boxed SProp.
Require Import StrictProp.
Axiom Unbox : Prop -> SProp.
Axiom Box_Unbox : forall (P : Prop), Box (Unbox P) = P.
Definition proof_irrelevance (P : Prop) : forall (p p' : P), p = p' :=
match Box_Unbox P with eq_refl =>
fun p p' => match p, p' with box s, box s' => eq_refl end
end.
Definition unsquash [P : Prop] : Squash P -> P :=
match Box_Unbox P with eq_refl =>
fun s => box (match s with squash (box u) => u end)
end.
It would probably be simpler and work just as well to directly postulate that Box (Squash P) = P; this is technically a “stronger” statement but not in a way that anyone cares about if they are postulating proof-irrelevance in the first place.
This is actually really interesting from a model-theoretic perspective; you’re saying in effect that there could be some model of Coq+(Prop=SProp) where inhabitation is interpreted differently for propositions vs. strict propositions, so that even though Prop and SProp are the same sort, an element thereof might be “inhabited as a Prop” but not “inhabited as an SProp” or vice-versa?
It won’t help you directly with your problem in practice, but we had a similar discussion at Types this year with Rafaël Bocquet who conjectured/claimed that you could axiomatically specify that Squash is a weak equivalence (in the HoTT sense) between hProp (homotopy propositions, e.g. “types with at most one element”) and SProp inducing weak equivalences between the corresponding decodings of propositions (If P : hProp then there is a weak equivalence between P and Squash P) while retaining all metatheoretical properties but relaxing canonicity to hold up to an identity/path (aka weak canonicity).
Since the reply by @kyod reminded me of this topic, I’d like to also mention that it suffices if, in addition to having an equality SProp = Prop, the type-rewrite by this equality is extensionally equal to Box; that is:
Require Import StrictProp.
Import EqNotations.
Axiom SProp_is_Prop : SProp = Prop.
Axiom Box_eq : forall (S : SProp), Box S = rew [@id Type] SProp_is_Prop in S.
and then it is immediately clear that Box has an inverse, so proof irrelevance in Prop follows. If the idea is to postulate that SProp and Prop are “the same thing” then this seems like the way to go about it.