The Coq mailing list

[Cody Roux <Cody.Roux AT loria.fr>]

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
>