The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

(cont.) Does it imply that in the empty context it is impossible to  
define a function (nat -> nat) -> nat which maps f to its minimal value?

V.


On Oct 20, 2009, at 6:56 AM, Cody Roux wrote:

> On Tue, 2009-10-20 at 12:43 -0400, Vladimir Voevodsky wrote:
> > (cont.) Is it also true  that any closed term of type nat reduces  
> > to a
> > term of the form S ... S O ?
> >
> > V.
> Also true, if as Adam has said, you work in a system without (non
> computational) axioms. This can be generalized to all inductive types,
> though one must notice that in the presence of dependent types, some
> instances of the inductive types may be empty e.g.
>
> Inductive ZeroEmpty: nat->Type:=
> |Notzero: forall n, ZeroEmpty (S n)
> .
>
> In this case (ZeroEmpty 0) is uninhabited. Nevertheless, every term of
> type (ZeroEmpty 0) in the empty context (in this case there are no  
> such
> terms) does reduce to (Notzero t).
>
> Cody
>
>
> > On Oct 20, 2009, at 6:38 AM, Cody Roux wrote:
> >
> > > On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
> > > > Given an inductive type such as
> > > >
> > > > Inductive two_el := el_1 | el_2 .
> > > >
> > > > are there closed terms of type two_el which do not reduce to either
> > > > el_1 or el_2 ?
> > >
> > > No. This can be deduced from the strong normalisation property of  
> > > the
> > > underlying calculus of Coq (CIC+Predicative Set+Universes), combined
> > > with the Inversion Property: It is easy to show by case analysis  
> > > that
> > > any term in normal form and in the empty context of type two_el must
> > > be
> > > one of the constructors of this type. This can be compared with the
> > > disjunction property which states:
> > >
> > > If t is a term of type A\/B in the empty context then t reduces to
> > > inl t1   or to    inr t2
> > >
> > > Which happens to be quite a desirable property in constructive
> > > mathematics.
> > >
> > > Cheers
> > >
> > > Cody