The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

> From: Paul Brauner 
>Â <paul.brauner AT loria.fr>
> To: 
>Â coq-club AT pauillac.inria.fr
> Date: Thu, 04 Sep 2008 16:02:50 +0200
> Subject: [Coq-Club] system F naturals
>
> Hi,
>
> is it possible to define church integers in coq and to prove that we can
> translate them back and forth to peano integers ?
>
> i.e. if we define church integers like this :
>
>> Definition cnat := forall X:Type, X -> (X -> X) ->X.
>> Definition CZ : cnat := fun X z s => z.
>> Definition CS : cnat -> cnat := fun cn => fun X z s => cn X (s z) s.
>
> Then we can write translation functions to and from peano integers this
> way :
>
>> Definition cnat_to_nat (cn:cnat) := cn nat 0 S.
>> Definition nat_to_cnat (n:nat) : cnat :=
>>   fun (X:Type) z s => nat_rect (fun _ => X) z (fun _ => s) n.
>
> We can then easily prove the following lemma :
>
>> Lemma nat_to_cnat_to_nat :
>>   forall n:nat, (cnat_to_nat (nat_to_cnat n)) = n.
>> intros.
>> induction n; compute; auto.
>> Qed.
>
> My question is : is the dual lemma provable ?
>
>> Lemma cnat_to_nat_to_cnat :
>>   forall cn:cnat, (nat_to_cnat (cnat_to_nat cn)) = cn).
>
> It seems like it is not, but do you know why ?
>
> Paul
>
>
>
> --__--__--
>
> Message: 2
> Date: Thu, 04 Sep 2008 16:24:50 +0200
> From: Bruno Barras 
>Â <bruno.barras AT inria.fr>
> To: Paul Brauner 
>Â <paul.brauner AT loria.fr>
> CC: 
>Â coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] system F naturals
>
> Paul Brauner wrote:
>> Hi,
>>
>> is it possible to define church integers in coq and to prove that we can
>> translate them back and forth to peano integers ?
>>
>> i.e. if we define church integers like this :
>>
>>
>>> Definition cnat := forall X:Type, X -> (X -> X) ->X.
>>> Definition CZ : cnat := fun X z s => z.
>>> Definition CS : cnat -> cnat := fun cn => fun X z s => cn X (s z) s.
>>>
>>
>> Then we can write translation functions to and from peano integers this
>> way :
>>
>>
>>> Definition cnat_to_nat (cn:cnat) := cn nat 0 S.
>>> Definition nat_to_cnat (n:nat) : cnat :=
>>>   fun (X:Type) z s => nat_rect (fun _ => X) z (fun _ => s) n.
>>>
>>
>> We can then easily prove the following lemma :
>>
>>
>>> Lemma nat_to_cnat_to_nat :
>>>   forall n:nat, (cnat_to_nat (nat_to_cnat n)) = n.
>>> intros.
>>> induction n; compute; auto.
>>> Qed.
>>>
>>
>> My question is : is the dual lemma provable ?
>>
>>
>>> Lemma cnat_to_nat_to_cnat :
>>>   forall cn:cnat, (nat_to_cnat (cnat_to_nat cn)) = cn).
>>>
>>
>> It seems like it is not, but do you know why ?
>>
>>
>
> Hi,
> cnat is a product type, and in Coq equality on product types is not
> extentional.
> Assume you have (distinct) cn and cn' that apply twice the successor on
> zero (they will both be mapped to nat 2), but obviously nat_to_cnat
> cannot map 2 to both cn and cn'. Your lemma cannot hold in this model.
> Assuming cnat_to_nat_to_cnat introduces a (possibly weaker) form of
> functional extentionality.
>
> It is true however that the set of *closed lambda-terms* of type cnat is
> isomorphic to nat but:
> (1) this is a metatheoretical argument you cannot encode in the logic
> itself,
> (2) this does not hold for impredicative encodings of higher order
> inductive types (i.e. if an argument of a constructor is a product type,
> see Christine Paulin's "habilitation" thesis for more details).
>
> Bruno.
>
>

I may be wrong, but there is also cardinal impossibility for that
isomorphism:

cnat is a lot bigger than nat and even bigger than reals (true reals, not
floating ones), since for each real x, there exists a cnat c such that "c
real 0 _ = x", and as there is no bijection between nat and reals, there
is no bijection between nat and cnat.

nat_to_cnat is an injection
and cnat_to_nat as said by B.Barras is only a surjection

Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay