The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi,

If you want to avoid using axiom, I think you should really avoid using
Type for proofs. In my experience, once you do this choice, either you
decide to put everything in Type (thus giving up on impredicativity), or
you have to use some sort of axiom of choice.

What is the actual reason justifying this choice ?

-- 
JH


Le 10/03/2016 19:26, Ralf Jung a écrit :
> 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
>>

Attachment: signature.asc
Description: OpenPGP digital signature