Definition of the Ackermann-Peter function in Coq, as an inductive relation and also a fixpoint

ackermann.v

(* Let's look at the Ackermann-Peter function, the canonical example of a
total computable function that is not primitive recursive. As such it should
be possible to write it as a computation in Gallina but the normal Fixpoint
termination check won't work.

The function can be defined case-wise:
A(0, n)     = n+1
A(m+1, 0)   = A(m, 1)
A(m+1, n+1) = A(m,A(m+1,n))

Below is the "obvious" fixpoint definition but Coq won't accept it: "Cannot
guess decreasing argument of fix." *)

(*
Fixpoint ack_fix1 (m n : nat) : nat :=
  match m with
  | O => S n
  | S m' =>
    match n with
    | O => ack_fix1 m' 1
    | S n' => ack_fix1 m' (ack_fix1 m n')
    end
  end.
*)

(* Some generic definitions about relations *)
Section Rel.
  Variables A B : Type.
  Definition Rel := A -> B -> Prop.

  Definition partial_func (R : Rel) :=
    forall x y1 y2, R x y1 -> R x y2 -> y1 = y2.

  Definition left_total (R : Rel) :=
    forall x, exists y, R x y.

  Definition func (R : Rel) :=
    forall x, exists! y, R x y.

  Theorem partial_func_total__func :
    forall R, partial_func R -> left_total R -> func R.
  Proof.
    unfold partial_func, left_total, func.
    intros R Hpf Hlt x.
    specialize (Hlt x).
    inversion Hlt as (y1, Hy1); subst; clear Hlt.
    exists y1.
    split; try assumption.
    intros y2 Hy2.
    apply Hpf with x; assumption.
  Qed.
End Rel.

(* Ackermann-Peter defined as an inductive relation. NB this follows pretty
directly from the definition. *)

Inductive ack_rel : nat -> nat -> nat -> Prop :=
| ack_1 : forall n,
  ack_rel 0 n (S n)
| ack_2 : forall m o,
  ack_rel m 1 o ->
  ack_rel (S m) 0 o
| ack_3 : forall m n n' o,
  ack_rel (S m) n n' ->
  ack_rel m n' o ->
  ack_rel (S m) (S n) o.

(* We should prove that we really did define a function *)
Lemma ack_rel_partial_func :
  forall m n o1 o2, ack_rel m n o1 -> ack_rel m n o2 -> o1 = o2.
Proof.
  intros m n o1 o2 Ho1.
  generalize dependent o2.
  induction Ho1; intros o2 Ho2;
    inversion Ho2; subst; clear Ho2; try auto.
  specialize (IHHo1_1 n'0 H1); subst; auto.
Qed.

Lemma ack_rel_left_total :
  forall m n, exists o, ack_rel m n o.
Proof.
  intros m.
  induction m.
  - intros n; exists (S n); constructor.
  - induction n.
    + specialize (IHm 1).
      inversion IHm.
      exists x.
      apply ack_2; assumption.
    + inversion IHn as (n',Hn').
      specialize (IHm n').
      inversion IHm as (o, Ho).
      exists o.
      apply ack_3 with n'; assumption.
Qed.

Theorem ack_rel_func :
  forall m n, exists! o, ack_rel m n o.
Proof.
  intros m n.
  assert (exists o, ack_rel m n o) by apply ack_rel_left_total.
  inversion H as (o1, Ho1).
  exists o1.
  split; try assumption.
  intros o2 Ho2.
  apply (ack_rel_partial_func m n); assumption.
Qed.

(* Here is a clever way to write the function as a fixpoint that avoids the
problem from the first fixpoint definition above. *)

Fixpoint ack (n m : nat) : nat :=
  match n with
  | O => S m
  | S p => let fix ackn (m : nat) :=
               match m with
               | O => ack p 1
               | S q => ack p (ackn q)
               end
           in ackn m
  end.

(* We can prove that our relation defines the same function. *)
Theorem ack__ack_rel :
  forall x y z, ack_rel x y z <-> ack x y = z.
Proof.
  intros x y z.
  split; intros H.
  - induction H.
    + reflexivity.
    + simpl; assumption.
    + simpl; subst; reflexivity.
  - subst.
    generalize dependent y.
    induction x; intros y.
    + constructor.
    + induction y.
      * simpl; constructor; apply IHx.
      * apply ack_3 with (ack (S x) y); auto.
        eapply IHx.
Qed.


(* Using constructive definite description, we can turn our relation into a
"function" that we can use like normal and prove behaves as per the relational
spec. But note that we cannot actually compute values with this definition! *)

From Coq.Logic Require Import Description.

Definition ack_cdd_sig (x y : nat) : {z : nat | ack_rel x y z }.
  apply constructive_definite_description.
  apply ack_rel_func.
Qed.

Definition ack_cdd (x y : nat) : nat := proj1_sig (ack_cdd_sig x y).

Check (ack_cdd 3 4).
(* ack_cdd 3 4 : nat *)

(* This version cannot actually compute *)
Compute (ack_cdd 3 4).
(*
ack_cdd 3 4
	 : nat
	 = let (x, _) := ack_cdd_sig 3 4 in x
     : nat
*)

(* Contrast with the computable version: *)
Compute (ack 3 4).
(* = 125 : nat*)

Theorem ack_cdd__ack_rel :
  forall x y z, ack_rel x y z <-> ack_cdd x y = z.
Proof.
  unfold ack_cdd.
  intros x y z1.
  destruct (ack_cdd_sig x y) as (z2, Hz2); simpl.
  split; intros Hz1.
  apply (ack_rel_partial_func x y); assumption.
  subst; assumption.
Qed.