The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> If you are using 8.5 you can do rewriting in Type.  Instead of importing
> SETOID SETOIDCLASS, import SETOID CEQUIVALENCE CMORPHISMS.  Then you can
> use crelation in place of relation.  (Actually. If you don't mind having
> your signature notations living in Prop. You can use crelations with the
> usual imports.  i just hate the mess that it makes out of my Proper
> declarations)

Oh, that is interesting -- thanks! I'll certainly try it, should this
come up again. (For now, it seems like we found another way.)

Will this work with the ssreflect rewrite?

Kind regards,
Ralf

> 
> 
> 
> Sent from Yahoo Mail on Android
> <https://overview.mail.yahoo.com/mobile/?.src=Android>
> 
>     On Thu, 10 Mar, 2016 at 16:33, Ralf Jung
>     
> <jung AT mpi-sws.org>
>  wrote:
> 
>     Hi all,
> 
>     I'm working in an axiom-free Coq development, and the elim restriction
>     is getting in our way. I considered moving parts of our development from
>     Prop to Type, but Coq's support for that is pretty poor -- in terms of
>     notation, but (most importantly) in terms of rewriting. The Setoid
>     mechanism forces the relation to be "A -> A -> Prop".
> 
>     However (if I recall correctly), the elim restriction is actually only
>     needed because Coq wants to remain compatible with classical axioms.
>     Since we try hard to avoid these, it is rather unfortunate that we still
>     have to pay this prize. Of course we could just assume an axiom
>     "inhabited T -> T", but that would not reduce properly, and of course it
>     would mean we are no longer axiom-free. (I'm not sure if the part about
>     computation would practically matter, but foundationally, it'd be nice
>     to keep everything computational.)
> 
>     So I wonder, would it be possible to add a flag to Coq to disable the
>     elim restriction? Would that make sense? It's a little like
>     type-in-type, except that it's not actually unsound if not combined with
>     classical axioms.
> 
>     Kind regards,
>     Ralf
>