The Coq mailing list

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

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.

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

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?

Kind regards,
Ralf