The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

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