Library Beroal.Ackermann

we can define Ackermann's function in Coq

Definition ackermann := fix recm (m : nat) := match m with
| O ⇒ S
| S pm ⇒ fix recn (n : nat) := match n with
        | O ⇒ recm pm 1
        | S pn ⇒ recm pm (recn pn)
        end
end.

our definition is equivalent to equational definition

Section check.
Variable pm n pn : nat.
Check (refl_equal _) : ackermann 0 n = S n.
Check (refl_equal _) : ackermann (S pm) 0 = ackermann pm 1.
Check (refl_equal _) : ackermann (S pm) (S pn)
= ackermann pm (ackermann (S pm) pn).
End check.