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