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?
It seems like
Function
can't solve this problem. However, its cousinProgram Fixpoint
can.Let's define some lemmas treating well-foundedness first:
Now we can define the Ackermann-Péter function:
Some simple tests demonstrating that we can compute with
ack
:Using the Equations plugin by M. Sozeau and C. Mangin it is possible to define the function this way:
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.