The Coq mailing list

[Roger Witte <rogerwite AT yahoo.co.uk>]

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)

Sent from Yahoo Mail on 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