(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L10 (Natural numbers, orders, Ackermann)

    The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Require Import Coq.Arith.Arith.

Section l10.

Fixpoint pow (m n : nat) {struct n} : nat :=
  match n with
  | O => 1
  | S n' => m * (pow m n')
  end. 

Eval compute in (pow 2 3).
Eval compute in (pow 3 2).

Fixpoint powpow (m n:nat){struct n} : nat :=
  match n with
  | O => m
  | S n' => pow (powpow m n') m
  end.

Eval compute in (powpow 2 2).
Eval compute in (powpow 2 3).

Fixpoint rep (m:nat)(f : nat -> nat)(n : nat) {struct n} : nat :=
  match n with
  | O => m
  | S n => f (rep m f n)
  end.

Definition plus' (m n : nat) : nat
                            := rep n S m.

Eval compute in (plus' 2 3).

Definition times'(m n: nat) : nat
                            := rep 0 (plus' n) m.

Eval compute in (times' 2 3).

Definition pow'(m n: nat) : nat 
                          := rep 1 (times' m) n.

Eval compute in (pow' 2 3).

Definition powpow'(m n: nat) : nat 
                             := rep n (pow' n) m.

Eval compute in (powpow' 2 2).

Fixpoint ack (m n : nat) {struct m} : nat :=
  match m with
  | O => S n
  | S m' => rep 1 (ack m') (S n)
  end.

(* ack(0,n) = n + 1 *)
Eval compute in (ack 0 4).
(* ack(1,n) = n + 2 *)
Eval compute in (ack 1 4).
(* ack(2,n) = 2 * n + 3 *)
Eval compute in (ack 2 4).
(* ack(3,n) = 2^(n+3) - 3 *)
Eval compute in (ack 3 4).

Definition fomega(n : nat) : nat 
  := ack n n.

Eval compute in (fomega 0).
Eval compute in (fomega 1).
Eval compute in (fomega 2).
Eval compute in (fomega 3).
(* Eval compute in (fomega 4). *)

End l10.