The Coq mailing list

[Dirk Pattinson <dirk.pattinson AT anu.edu.au>]

I was wondering about the same.

For the example below, I gather that you are aware that Qed succeeds if you 
"Set Allow StrictProp” before the lemma.

I’d be looking for example uses of SProp to escape “setoid hell”, 
specifically on defining Sigma-types of the form

  { x: A & P x }

that inherit their equality from the equality of A such (i.e. P would be 
SProp valued).

All the best,

Dirk.


> On 18 Jan 2020, at 7:03 pm, 
> jonikelee AT gmail.com
>  wrote:
> 
> Is anyone using SProp?
> 
> I'm wondering how to use it when all the theories and builtin
> tactics are written in terms of Prop, Set and Type.  And because SProp
> is not involved in cumulativity, nothing designed for Types works for
> it.  Or, actually worse...
> 
> Consider:
> 
> Lemma triv (P : SProp)(a : P): a = a.
> Proof.
>  tauto. (* succeeds! *)
> Fail Qed.
> 
> My reading of the SProp doc is that Qed fails because tauto is ignorant
> of the existence of anything not under Type, and so it used Type-based
> eq theories. It doesn't fail immediately in tauto because the
> non-cumulativity of SProp into Type is known only to the kernel, which
> waits until Qed to troll you.
> 
> OK - but how does one make practical use of SProp then?  There are no
> theories that work for it, yet every tactic thinks that all theories
> work for it.  Until they don't - at Qed.
> 
> I want to figure this out because I have some ideas on how to use Prop
> and SProp together where some Props are made relevant and SProp is of
> course irrelevant.  I just can't figure out how to start.
> 
> -- Jonathan