The Coq mailing list

[Paul Brauner <paul.brauner AT loria.fr>]

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