The Coq mailing list

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

On Tue, 2009-10-20 at 13:04 -0400, Vladimir Voevodsky wrote:
> (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.
> 
  Indeed. If you could define such a function, than you could take any
\Pi^0_1 sentence P (a proposition of one parameter n that is decidable
for each instance of that parameter), and define a function f:nat->nat
in Coq such that:

f n reduces to (S 0) if the proposition P(n) is true
f n reduces to    0  if the proposition P(n) is false

taking your min:(nat->nat)->nat function, we could decide of the truth
of such a sentence: it suffices to test whether (min f) reduces to 0 or
to 1 which it necessarily does by the previous argument. This would
allow us to solve the halting problem.

Hope this helps,

Cody



> 
> 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
> >>
>