The Coq mailing list

[Venanzio Capretta <venanzio AT site.uottawa.ca>]

Hi Bill,
  you asked about Church numerals in Coq:

> How can you use Coq to show that...
> 
> (forall C: U0). C => (C => C) => C
> 
> can be seen as a representation of the type of natural numbers?

Here it is, with conversion functions to and from nat:

--------------------------------------------------
Definition Nat := forall X:Type, X -> (X->X) -> X.

Fixpoint nN (n:nat): Nat :=
match n with
  O => fun X x f => x
| (S n') => fun X x f => f (nN n' X x f)
end.

Definition Nn: Nat -> nat :=
fun N => N nat 0 S.
--------------------------------------------------

You cannot actually prove that this is an isomorphism.
In one direction it is easy by induction on nat:

------------------------------
Lemma id_nat_Nat:
  forall n:nat, Nn (nN n) = n.
Proof.
induction n.
trivial.
unfold Nn; simpl.
unfold Nn in IHn.
rewrite IHn.
trivial.
Qed.
-------------------------------

But the viceversa:

Lemma id_Nat_nat:
  forall N:Nat, nN (Nn N) = N.

is not provable.
You must at least formulate it extensionally:

Lemma id_Nat_nat:
  forall (N:Nat)(X:Type)(x:X)(f:X->X), nN (Nn N) X x f = N X x f.

But even like this I cannot prove it.
I suspect you need impredicativity to prove it. Does anyone know?

Cheers,
  Venanzio


-- 
Venanzio Capretta
Department of Mathematics and Statistics/
School of Information Technology and Engeneering
University of Ottawa, Canada
http://www.science.uottawa.ca/~vcapr396/