church numerals and coq and universes

(** **** Exercise: 4 stars, advanced (church_numerals)  *)

Module Church.

(** In this exercise, we will explore an alternative way of defining
    natural numbers, using the so-called _Church numerals_, named
    after mathematician Alonzo Church. We can represent a natural
    number [n] as a function that takes a function [f] as a parameter
    and returns [f] iterated [n] times. More formally, *)

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

(** Let's see how to write some numbers with this notation. Any
    function [f] iterated once shouldn't change. Thus, *)

Definition one : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

(** [two] should apply [f] twice to its argument: *)

Definition two : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).
Definition three : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f (f x)).

(** [zero] is somewhat trickier: how can we apply a function zero
    times? The answer is simple: just leave the argument untouched. *)

Definition zero : nat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

(** More generally, a number [n] will be written as [fun X f x => f (f
    ... (f x) ...)], with [n] occurrences of [f]. Notice in particular
    how the [doit3times] function we've defined previously is actually
    just the representation of [3]. *)


(** Complete the definitions of the following functions. Make sure
    that the corresponding unit tests pass by proving them with
    [reflexivity]. *)

(** Successor of a natural number *)

Definition succ (n : nat) : nat :=
  (* FILL IN HERE *) fun (X : Type) (f : X -> X) (x : X) => f (n X f x).


Example succ_1 : succ zero = one.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example succ_2 : succ one = two.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example succ_3 : succ two = three.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

(** Addition of two natural numbers *)

Eval compute in (three bool negb false).

Check nat.
Check succ.
(* Check three _ succ. <- this fails *)

(* this also fails *)
Definition plus (n m : nat) : nat := n _ succ m.

(*
Example plus_1 : plus zero one = one.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example plus_2 : plus two three = plus three two.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example plus_3 :
  plus (plus two two) three = plus one (plus three three).
Proof. (* FILL IN HERE *)  Proof. reflexivity. Qed.
*)

(** Multiplication *)

Definition mult (n m : nat) : nat := n _ (plus m) zero.
  (* FILL IN HERE *)

Example mult_1 : mult one one = one.
Proof. (* FILL IN HERE *)  Proof. reflexivity. Qed.

Example mult_2 : mult zero (plus three three) = zero.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example mult_3 : mult two three = plus three three.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

(** Exponentiation *)

(** Hint: Polymorphism plays a crucial role here. However, choosing
    the right type to iterate over can be tricky. If you hit a
    "Universe inconsistency" error, try iterating over a different
    type: [nat] itself is usually problematic. *)

Definition exp (n m : nat) : nat := m _ (mult n) one.
  (* FILL IN HERE *)

Example exp_1 : exp two two = plus two two.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example exp_2 : exp three two = plus (mult two (mult two two)) one.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.

Example exp_3 : exp three zero = one.
Proof. (* FILL IN HERE *) Proof. reflexivity. Qed.
End Church.

(** [] *)