# Church Numerals

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

Definition zero : Nat := fun X f x => x.

Definition succ : Nat -> Nat := fun n X f x => f (n X f x).

Definition N : nat -> Nat := fun n => nat_iter n succ zero.

Lemma NS n :
N (S n) = succ (N n).

Proof.

reflexivity.

Qed.

Compute (N 5).

Fixpoint pow (x y : nat) : nat :=
match y with
| 0 => 1
| S y' => x * pow x y'
end.

Dedekind version of addition, multiplication, and exponentiation. Does not require Coq's eta-conversion.

Module AME.

Definition add : Nat -> Nat -> Nat := fun m => m Nat succ.

Definition mul : Nat -> Nat -> Nat := fun m n => m Nat (add n) (N 0).

Definition exp : Nat -> Nat -> Nat := fun m n => n Nat (mul m) (N 1).

add (N m) (N n) = N (m + n).

Proof.

induction m; simpl.

- reflexivity.

- change (add (N (S m)) (N n)) with (succ (add (N m) (N n))).

now rewrite IHm.

Qed.

Lemma mul_correct m n :
mul (N m) (N n) = N (m * n).

Proof.

induction m; simpl.

- reflexivity.

- change (mul _ _) with (add (N n) (mul (N m) (N n))).

Qed.

Lemma exp_correct m n :
exp (N m) (N n) = N (pow m n).

Proof.

induction n; simpl.

- reflexivity.

- change (exp _ _) with (mul (N m) (exp (N m) (N n))).

now rewrite IHn, mul_correct.

Qed.

End AME.

Church's version of addition, multiplication, and exponentiation. Exploits Coq's eta-conversion.

Module AME_Church.

Definition add : Nat -> Nat -> Nat := fun m n X f x => m X f (n X f x).

Definition mul : Nat -> Nat -> Nat := fun m n X f => m X (n X f).

Definition exp : Nat -> Nat -> Nat := fun m n X => n (X -> X) (m X).

Compute exp (N 2) (N 3).

N (m + n) = add (N m) (N n).

Proof.

induction m; simpl.

- reflexivity.

- change (N (S (m+n))) with (succ (N (m+n))).

now rewrite IHm.

Qed.

Lemma mul_correct m n :
N (m * n) = mul (N m) (N n).

Proof.

induction m; simpl.

- reflexivity.

Qed.

Lemma exp_correct m n :
N (pow m n) = exp (N m) (N n).

Proof.

induction n; simpl.

- reflexivity.

- now rewrite mul_correct, IHn.

Qed.

End AME_Church.

Pairs

Set Implicit Arguments.

Definition Prod (X Y : Prop) : Prop :=
forall Z : Prop, (X -> Y -> Z) -> Z.

Definition pair (X Y : Prop) : X -> Y -> Prod X Y :=
fun x y Z f => f x y.

Definition fst (X Y : Prop) : Prod X Y -> X :=
fun p => p X (fun x y => x).

Definition snd (X Y : Prop) : Prod X Y -> Y :=
fun p => p Y (fun x y => y).

Lemma fst_correct (X Y : Prop) (x : X) (y : Y) :
fst (pair x y) = x.

Proof.

cbv.
reflexivity.
Qed.

The eta-law for pairs pair (fst p) (snd p) = p cannot be shown.
Primitive recursion

Section Prec.

Variable X : Prop.

Variable x : X.

Variable f : Nat -> X -> X.

Definition P := Prod Nat X.

Definition a : P := pair (N 0) x.

Definition step (p : P) : P :=
pair (succ (fst p)) (f (fst p) (snd p)).

Definition prec (n : Nat) : X :=
snd (n P step a).

Lemma precO :
prec (N 0) = x.

Proof.

reflexivity.

Qed.

Lemma precS' n :
(N (S n)) P step a = pair (N (S n)) (f (N n) (snd (N n P step a))).

Proof.

induction n.

- reflexivity.

- change (N (S (S n)) P step a) with (step (N (S n) P step a)).

rewrite IHn.
reflexivity.
Qed.

Lemma precS n :
prec (N (S n)) = f (N n) (prec (N n)).

Proof.

unfold prec.
now rewrite precS'.
Qed.

End Prec.

Predecessor

Definition pre : Nat -> Nat := prec (N 0) (fun n' _ => n').

Lemma pre_correct n :
pre (N n) = N (pred n).

Proof.

destruct n.

- reflexivity.

- unfold pre.
now rewrite precS.
Qed.