The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Robin Green a e'crit :
> I am curious about the general question of: given a type in the
> Calculus of Inductive Constructions, does there exist a unique term of
> that type? And moreover, if there does, how to prove this in Coq?
> 
> Here is a simple example (in Coq 8.1 syntax), based on id_t, the type of
> the polymorphic identity function id (Definition id (a:Type) (x:a) :
> a := x.)
> 
> Definition id_t := forall (a : Type), a -> a.
> 
> (* This is not allowed:
> Definition weird : id_t := fun (a : Set) (x : a) => match a with nat =>
> 0 | _ => x end. *)
> 
> Lemma uniqueness_of_id : exists! f:id_t, True.
> 
> I posit that all functions having type id_t must either:
> 
> a) be equal to id as defined above (note that I am assuming functional
> extensional equality), or
> 
> b) be of the same form as "weird" above, and hence disallowed.
> 
> and hence uniqueness_of_id is true in CiC.
> 
> However, how would I prove this in Coq?
> 
> Would I need any axioms other than those in the Coq standard library?
> 

Note that the fact that id_t has only one inhabitant is a
metatheoretical property: by enumerating all the terms, we can see that
only the identity has type id_t (up to beta-conversion), in the empty
context.
Note that in the context of:
Axiom type_nat_dec : forall a:Type, {a=nat}+{a<>nat}
(that is, we can decide if a type is nat or not), we can define your
"weird" function. So, the property does not hold in this context.

Now, for which type can we prove the property within Coq?
Well, without axiom, it is provable for some inductive types (like unit,
le), and that's it. With intentional equality, types like unit->unit may
have several inhabitants.
If functional extensional equality is assumed, then functions with
codomains reduced to a singleton type can be proven to be singleton. You
can also prove it if the domain is an empty type.

But still no way to prove it for id_t: it is likely that there exists a
set theoretical model of Coq (where A->B is interpreted as the set of
all set-theoretical functions from A to B, and Prop is interpreted as
bool). This model validates the functional extensional equality
property, but "weird" belongs to the interpretation of id_t.

If you really want to be able to prove it for id_t, then you need some
kind of "reflection principle", assuming that inhabitants of A->B have
to be built from the CIC constructions. This will give you a way to
"enumerate" the inhabitants of id_t and prove there exists only one. I
don't know if/how such a principle can be formalised, but you have to be
very careful not to go against Godel's 2nd incompleteness theorem...

Hope this helps,
Bruno Barras.