Simple reductions in Coq from Coq Art.

reduction.v

Definition ninc (n : nat) : nat := n + 1.
Definition ntwice (f : nat -> nat) (n : nat) : nat := f (f n).

Eval cbv in (ntwice ninc 0).
(* = 2 *)

Eval cbv delta [ninc ntwice] in (ntwice ninc 0).
(* = (fun (f : nat -> nat) (n : nat) => f (f n)) (fun n : nat => n + 1) 1 *)

Eval cbv delta [ninc] in (ntwice ninc 0).
(* = ntwice (fun n : nat => n + 1) 0 *)

Eval cbv beta delta [ninc ntwice] in (ntwice ninc 0).
(* = 0 + 1 + 1 *)

Eval cbv beta in (ntwice ninc 0).
(* = ntwice ninc 0 *)

Eval cbv zeta delta in (ntwice ninc 0).
(* = (fun (f : nat -> nat) (n : nat) => f (f n))
         (fun n : nat =>
          (fix add (n0 m : nat) {struct n0} : nat :=
             match n0 with
             | 0 => m
             | S p => S (add p m)
             end) n 1) 0
*)

Eval cbv beta zeta delta in (ntwice ninc 0).
(* = (fix add (n m : nat) {struct n} : nat :=
          match n with
          | 0 => m
          | S p => S (add p m)
          end)
         ((fix add (n m : nat) {struct n} : nat :=
             match n with
             | 0 => m
             | S p => S (add p m)
             end) 0 1) 1
*)

Eval cbv zeta in (ntwice ninc 0).
(* = ntwice ninc 0 *)

Eval cbv beta zeta delta [ntwice] in (ntwice ninc 0).
(* = ninc (ninc 0) *)

Eval cbv iota beta zeta delta in (ntwice ninc 0).
(* 2 *)

Compute (ntwice ninc 0).
(* 2 *)

Script based from http://www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/specprog/SRC/chap2.v

(since I am lazy and did not want to open the book)