SProp question: What can I actually do with a (Squash P) value?

Using Coq
1

Hi all, new to Discourse in general and this group in particular. I’ve known about Coq for years and played with it on and off, never done much serious development in it.

I recently learned about SProp and was particularly interested in its sigma types since I assume they would behave more like “real subsets”. But at the moment it looks like, short of reinventing the entire logic library in SProp, the only real way to put an interesting proposition into there is to ‘squash’ one from Prop. And having done so, I can’t find any way to actually make use of that proposition’s content.

For example: currently what I’d like to prove is that if a map f: A -> B has a left-inverse, then its restriction to Ssig (fun y:B => Squash (exists x:A, f x = y)) has a full inverse. This seems to me like it ought to be the case given proof-irrelevance. Here’s how that’s going:

Variables A B: Type.
Variables (f: A -> B) (fInv: B -> A).
Hypothesis lcancel: forall x, fInv (f x) = x.

Definition Img: Type :=
  Ssig (fun y:B => Squash (exists x, f x = y)).

Definition f' (x: A): Img :=
  Sexists _ (f x) (squash (ex_intro _ _ eq_refl)).

 Definition fInv' (y: Img): A := fInv (Spr1 y).

Property rcancel: forall y:Img, f' (fInv' y) = y.
Proof.
  intros [y sH]. (* sH: Squash (exists x, f x = y) *)
  apply Spr1_inj. now_show (f (fInv y) = y).
  enough (exists x, f x = y).
  { destruct H; rewrite <- H, -> lcancel; reflexivity. }

…and here I’m stuck. I can’t destruct sH to get the proposition I need, because "Case analysis on sort Prop is not allowed for inductive definition Squash." And without that proposition there is no way to complete the proof.

Based on this, I don’t understand how I am supposed to do anything at all with a value of type Squash P except admire it and then throw it away. I suppose if I just wanted a computation to require that some value satisfy a predicate while never actually needing to use that fact, I could accept a Squash (P x) for that purpose, but that’s about it. Is this analysis correct, or am I missing something?

2

Indeed you can prove forall y, Squash (f' (fInv' y) = y) but not the unsquashed equality.

Based on this, I don’t understand how I am supposed to do anything at all with a value of type Squash P except admire it and then throw it away.

You can also prove forall P, (~ ~ P -> P) -> Squash P -> P, decidable properties satisfy the condition so if you add an hypothesis that B has decidable equality then you can prove the unsquashed goal.
Notably False is decidable so Squash False -> False. So for instance you can define a Vector head function of type forall A n, Squash (exists k, n = S k) -> Vector.t A n -> A using the hypothesis only in the nil branch where it is absurd.

Alternatively you can use SProp (proof irrelevant propositions) — Coq 8.19+alpha documentation to declare an equality type in SProp and prove it equivalent to the usual equality, this also lets you prove the unsquashed goal. However note SProp (proof irrelevant propositions) — Coq 8.19+alpha documentation

3

Oh, that makes more sense. So once I move information into SProp it has to stay there (barring decidability), but I can continue to use it in defining other SProps. Meaning I can prove as an SProp that A and Img f are equipotent, but the witness of that proposition can never be used for anything except as a lemma for proving further results inside SProp. Which is fine, as long as my end goal is just to satisfy myself and/or others that those results are true.

That actually gives me a much better idea of what SProp is good for! Thanks!