Error in defining Ackermann in Coq

Question

I am trying to define the Ackermann-Peters function in Coq, and I'm getting an error message that I don't understand. As you can see, I'm packaging the arguments a, b of Ackermann in a pair ab; I provide an ordering defining an ordering function for the arguments. Then I use the Function form to define Ackermann itself, providing it with the ordering function for the ab argument.

Require Import Recdef.    
Definition ack_ordering (ab1 ab2 : nat * nat) :=
    match (ab1, ab2) with
    |((a1, b1), (a2, b2)) => 
       (a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))   
    end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, ack (a, b-1))
end.

What I get is the following error message:

Error: No such section variable or assumption: ack.

I'm not sure what bothers Coq, but searching the internet, I found a suggestion there may be a problem with using a recursive function defined with an ordering or a measure, where the recursive call occurs within a match. However, using the projections fst and snd and an if-then-else generated a different error message. Can someone please suggest how to define Ackermann in Coq?

Answer 1

It seems like Function can't solve this problem. However, its cousin Program Fixpoint can.

Let's define some lemmas treating well-foundedness first:

Require Import Coq.Program.Wf.
Require Import Coq.Arith.Arith.

Definition lexicographic_ordering (ab1 ab2 : nat * nat) : Prop :=
  match ab1, ab2 with
  | (a1, b1), (a2, b2) => 
      (a1 < a2) \/ ((a1 = a2) /\ (b1 < b2))
  end.

(* this is defined in stdlib, but unfortunately it is opaque *)
Lemma lt_wf_ind :
  forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof. intro p; intros; elim (lt_wf p); auto with arith. Defined.

(* this is defined in stdlib, but unfortunately it is opaque too *)
Lemma lt_wf_double_ind :
  forall P:nat -> nat -> Prop,
    (forall n m,
      (forall p (q:nat), p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
  intros P Hrec p. pattern p. apply lt_wf_ind.
  intros n H q. pattern q. apply lt_wf_ind. auto.
Defined.

Lemma lexicographic_ordering_wf : well_founded lexicographic_ordering.
Proof.
  intros (a, b); pattern a, b; apply lt_wf_double_ind.
  intros m n H1 H2.
  constructor; intros (m', n') [G | [-> G]].
  - now apply H1.
  - now apply H2.
Defined.

Now we can define the Ackermann-Péter function:

Program Fixpoint ack (ab : nat * nat) {wf lexicographic_ordering ab} : nat :=
  match ab with
  | (0, b) => b + 1
  | (S a, 0) => ack (a, 1)
  | (S a, S b) => ack (a, ack (S a, b))
  end.
Next Obligation.
  inversion Heq_ab; subst. left; auto. Defined.
Next Obligation.
  apply lexicographic_ordering_wf. Defined.

Some simple tests demonstrating that we can compute with ack:

Example test1 : ack (1, 2) = 4 := eq_refl.
Example test2 : ack (3, 4) = 125 := eq_refl.  (* this may take several seconds *)

---

Using the Equations plugin by M. Sozeau and C. Mangin it is possible to define the function this way:

From Equations Require Import Equations Subterm.

Equations ack (p : nat * nat) : nat :=
ack p by rec p (lexprod _ _ lt lt) :=
ack (pair 0 n) := n + 1;
ack (pair (S m) 0) := ack (m, 1);
ack (pair (S m) (S n)) := ack (m, ack (S m, n)).

Unfortunately, it's not possible to use the ( , ) notation for pairs due to issue #81. The code is taken from Equation's test suite: ack.v.