Library CN

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

  Lemma add_correct m n :
    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))).
      now rewrite IHm, add_correct.
  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).

  Lemma add_correct m n :
    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.
    - now rewrite add_correct, IHm.
  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.