Estoy tratando de definir la función Ackermann-Peters en Coq, y aparece un mensaje de error que no entiendo. Como puedes ver, estoy empaquetando los argumentos.a, b de Ackermann en un parab; Proporciono un orden que define una función de orden para los argumentos. Entonces uso elFunction forma para definir el propio Ackermann, proporcionándole la función de orden para elab argumento.

<code>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.
</code>

Lo que recibo es el siguiente mensaje de error:

Error: No existe tal variable de sección o suposición:ack.

No estoy seguro de lo que molesta a Coq, pero al buscar en Internet, encontré una sugerencia de que podría haber un problema con el uso de una función recursiva definida con una ordenación o una medida, donde la llamada recursiva ocurre dentro de una coincidencia. Sin embargo, utilizando las proyecciones.fst ysnd y unif-then-else Se genera un mensaje de error diferente. ¿Alguien puede sugerir cómo definir Ackermann en Coq?