Eu estou tentando definir a função Ackermann-Peters no Coq, e estou recebendo uma mensagem de erro que não entendo. Como você pode ver, estou empacotando os argumentosa, b de Ackermann em um parab; Eu forneço uma ordenação definindo uma função de ordenação para os argumentos. Então eu uso oFunction forma de definir o próprio Ackermann, fornecendo-lhe a função de ordenação para oab 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>

O que recebo é a seguinte mensagem de erro:

Erro: Nenhuma variável ou suposição de seção:ack.

Eu não tenho certeza do que incomoda a Coq, mas pesquisando na internet, eu encontrei uma sugestão de que pode haver um problema com o uso de uma função recursiva definida com uma ordenação ou uma medida, onde a chamada recursiva ocorre dentro de uma correspondência. No entanto, usando as projeçõesfst esnd e umif-then-else gerou uma mensagem de erro diferente. Alguém pode sugerir como definir Ackermann em Coq?