The Coq mailing list

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

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.