Church numerals

Question

There are 4 exercises in Poly module related to Church numerals:

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

As far as I understand cnat is a function that takes a function f(x), it's argument x and returns it's value for this argument: f(x).

Then there are 4 examples for 0, 1, 2 and 3 represented in Church notation.

But how to solve this? I understand that we must apply the function one more time. The value returned by cnat will be the argument. But how to code it? Use a recursion?

Definition succ (n : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Update

I tried this:

Definition succ (n : cnat) : cnat :=
match n with
| zero => one
| X f x => X f f(x) <- ?

Answer 1

Remember that a Church numeral is a function of two arguments (or three if you also count the type). The arguments are a function f and a start value x0. The Church numeral applies f to x0 some number of times. Four f x0 would correspond to f (f (f (f x0))) and Zero f x0 would ignore f and just be x0.

For the successor of n, remember that n will apply any function f for you n times, so if your task is to create a function applies some f on some x0 n+1 times, just leave the bulk of the work to the church numeral n, by giving it your f and x0, and then finish off with one more application of f to the result returned by n.

You won't be needing any match because functions are not inductive data types that can be case analysed upon...