3

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) <- ?
user4035
  • 22,508
  • 11
  • 59
  • 94

3 Answers3

3

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...

larsr
  • 5,447
  • 19
  • 38
3

You can write the Definition for succ in the following way:

Definition succ (n : cnat) : cnat :=
    fun (X : Type) (f : X -> X) (x : X) => f (n X f x).
Md Johirul Islam
  • 5,042
  • 4
  • 23
  • 56
1

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).

Note that cnat itself isn't a function. Instead, cnat is the type of all such functions. Also note that elements of cnat take X as an argument as well. It'll help to keep the definition of cnat in mind.

Definition succ (n: cnat): cnat.
Proof.
  unfold cnat in *. (* This changes `cnat` with its definition everywhere *)
  intros X f x.

After this, our goal is just X, and we have n : forall X : Type, (X -> X) -> X -> X, X, f and x as premises.

If we applied n to X, f and x (as n X f x), we would get an element of X, but this isn't quite what we want, since the end result would just be n again. Instead, we need to apply f an extra time somewhere. Can you see where? There are two possibilities.

SCappella
  • 9,534
  • 1
  • 26
  • 35
  • I tried to play with your code, but it's the first time when I see a definition being made with proof. I don't think it was in the book before. `Qed` at the end doesn't work. – user4035 Feb 16 '19 at 23:07
  • "Instead, we need to apply f an extra time somewhere" - we need to apply it to x. But how to write it in coq syntax? – user4035 Feb 16 '19 at 23:07
  • For a simple definition like this, proof mode is mainly useful for exploring the types of things and experimenting. Once you have the final definition, you can put it in `:=` form. Note that the proof isn't complete, so you can't end it with `Qed.` quite yet. I just want you to see what premises are available and what the output type should be. – SCappella Feb 16 '19 at 23:10
  • I tried to use it with Compute and it failed because of Proof. – user4035 Feb 16 '19 at 23:12
  • I don't understand, how to use the Proof mode here. Your explanations are too brief, and it's nowhere in the book. Please, look at the update. I think, ?I am on the right way here. But how to write the correct constructor for n? – user4035 Feb 16 '19 at 23:24
  • `n` is a function rather than an element of an inductive type, so to use it, you'll apply it to some arguments (like `n X f x` in my answer). There won't be any recursion in the solution. – SCappella Feb 17 '19 at 00:07