The Coq mailing list

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

Le 10/03/2016 19:35, Ralf Jung a écrit :
> Hi,
>
>> Le 10/03/2016 17:33, Ralf Jung a écrit :
>>> 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.
>> If I remember correctly, this restriction is important to soundness :
>> because Prop is impredicative, we can build a proof of false from
>> inhabited T -> T.
> Oh, I see. So, having a function "inhabited T -> T" that actually
> computes would be unsound? Seems I misremembered, sorry.

Yes, this is unsound:

Check Hurkens.NoRetractFromTypeToProp.paradox.

Intuitivelly, the impredicativity of Prop gives you the right of putting
big things (in Types) in small boxes in type, using e.g., inhabited, but
you should never reopen the box.

> But having "inhabited T -> T", without any proof about *which* T you
> get, is fine?

This is an instance of the epsilon axiom (take P = fun _ => True) :

https://coq.inria.fr/library/Coq.Logic.Epsilon.html

>
> Recently, this has been suggested on the list:
> <https://sympa.inria.fr/sympa/arc/coq-club/2016-02/msg00224.html>
>
>> Inductive Erasable(A : Set) : Prop :=
>>   erasable: A -> Erasable A.
>>
>> Arguments erasable [A] _.
>> ...
>> Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a= erasable b -> 
>> a=b. 
> This also first had me confused, because it partially circumvents the
> elim restriction. (Erasable is the same as inhabited, as far as I can
> see). Certainly, this is incompatible with proof irrelevance. But other
> than that?

This is a bit different, and maybe unsound (I really don't know).
Anyway, this seems very dangerous, I would never use this without having
a proof that this is indeed correct.

-- 
JH Jourdan

>
> Kind regards,
> Ralf

Attachment: signature.asc
Description: OpenPGP digital signature