Error in defining Ackermann in Coq

Link:: https://stackoverflow.com/q/10292421

Display all goals and responses

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 ab} : nat :=
  match ab with
  | (0, b) => b + 1
  | (a, 0) => ack (a - 1, 1)
  | (a, b) => ack (a - 1, ack (a, b - 1))
  end.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 (Anton Trunov)

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.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n intro p.p: nat
forall P : nat -> Prop,
(forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
P p intros.p: nat
P: nat -> Prop
H: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
P p elim (lt_wf p).p: nat
P: nat -> Prop
H: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall x : nat,
(forall y : nat, y < x -> Acc lt y) ->
(forall y : nat, y < x -> P y) -> P x 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.forall P : nat -> nat -> Prop,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
Proof.forall P : nat -> nat -> Prop,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
  intros P Hrec p.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p: nat
forall m : nat, P p m pattern p.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p: nat
(fun n : nat => forall m : nat, P n m) p apply lt_wf_ind.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p: nat
forall n : nat,
(forall m : nat, m < n -> forall m0 : nat, P m m0) ->
forall m : nat, P n m
  intros n H q.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p, n: nat
H: forall m : nat, m < n -> forall m0 : nat, P m m0
q: nat
P n q pattern q.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p, n: nat
H: forall m : nat, m < n -> forall m0 : nat, P m m0
q: nat
(fun n0 : nat => P n n0) q apply lt_wf_ind.P: nat -> nat -> Prop
Hrec: forall n m : nat,
(forall p q : nat, p < n -> P p q) ->
(forall p : nat, p < m -> P n p) -> P n m
p, n: nat
H: forall m : nat, m < n -> forall m0 : nat, P m m0
q: nat
forall n0 : nat,
(forall m : nat, m < n0 -> P n m) -> P n n0 auto.
Defined.

Lemma lexicographic_ordering_wf : well_founded lexicographic_ordering.well_founded lexicographic_ordering
Proof.well_founded lexicographic_ordering
  intros (a, b).a, b: nat
Acc lexicographic_ordering (a, b) pattern a, b.a, b: nat
(fun n n0 : nat => Acc lexicographic_ordering (n, n0))
  a b apply lt_wf_double_ind.a, b: nat
forall n m : nat,
(forall p q : nat,
 p < n -> Acc lexicographic_ordering (p, q)) ->
(forall p : nat,
 p < m -> Acc lexicographic_ordering (n, p)) ->
Acc lexicographic_ordering (n, m)
  intros m n H1 H2.a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
Acc lexicographic_ordering (m, n)
  constructor.a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
forall y : nat * nat,
lexicographic_ordering y (m, n) ->
Acc lexicographic_ordering y intros (m', n') [G | [-> G]].a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
m', n': nat
G: m' < m
Acc lexicographic_ordering (m', n')
a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
n': nat
G: n' < n
Acc lexicographic_ordering (m, n')
  -a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
m', n': nat
G: m' < m
Acc lexicographic_ordering (m', n') now apply H1.
  -a, b, m, n: nat
H1: forall p q : nat,
p < m -> Acc lexicographic_ordering (p, q)
H2: forall p : nat,
p < n -> Acc lexicographic_ordering (m, p)
n': nat
G: n' < n
Acc lexicographic_ordering (m, n') 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.n, n0: nat
ack: forall ab : nat * nat, lexicographic_ordering ab (n, n0) -> nat
a, b: nat
Heq_ab: (S a, S b) = (n, n0)
a < n \/
a = n /\
ack (S a, b) (ack_obligation_2 (n, n0) ack a b Heq_ab) <
n0
  inversion Heq_ab.n, n0: nat
ack: forall ab : nat * nat,
lexicographic_ordering ab (n, n0) -> nat
a, b: nat
Heq_ab: (S a, S b) = (n, n0)
H0: S a = n
H1: S b = n0
a < n \/
a = n /\
ack (S a, b) (ack_obligation_2 (n, n0) ack a b Heq_ab) <
n0 subst.a, b: nat
Heq_ab: (S a, S b) = (S a, S b)
ack: forall ab : nat * nat,
lexicographic_ordering ab (S a, S b) -> nat
a < S a \/
a = S a /\
ack (S a, b)
  (ack_obligation_2 (S a, S b) ack a b Heq_ab) < 
S b left.a, b: nat
Heq_ab: (S a, S b) = (S a, S b)
ack: forall ab : nat * nat,
lexicographic_ordering ab (S a, S b) -> nat
a < S a auto. Defined.
Next Obligation.well_founded
  (MR lexicographic_ordering
     (fun recarg : nat * nat => recarg))
  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.

Answer (wires)

You get this error because you are referencing the ack function while you are defining it. Self reference is only allowed in Fixpoints (ie. recursive functions) but the problem is, as you probably know, that the Ackermann function is not a primitive recursive function.

See Coq'Art section 4.3.2.2 for some more information on this.

So one alternative way to define it is by inlining a second recursive function that is structurally recursive for the second argument; so something like

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.

Q: I wasn't using Fixpoint, but Function. This is supposed to work with total functions that have a decreasing argument, and I should be able to do so using either a measure or a comparison, followed by a theorem that arguments in recursive calls either have a smaller measure or are less than the original arguments, as per the comparator. I know Ackermann is 2nd-order PR, but obviously the PR status of the function didn't prevent you from encoding it in some way. What I'm wondering about is what is wrong with the encoding I gave, which seems to follow the description in the manual.