mutual recursion vs pairs

Stream: new members

[Horatiu Cheval]

Is mutual recursion more expressive than defining single pair-valued functions? For instance, I can redefine this:

mutual def f, g
with f : ℕ → ℕ
| 0 := 1
| (n + 1) := n + g n
with g : ℕ → ℕ
| 0 := 0
| (n + 1) := n * f n

as this:

def h : ℕ → ℕ × ℕ
| 0 := (1, 0)
| (n + 1) := (n + (h n).snd, n * (h n).fst)

Are there situations when such a translation would not be possible? Or maybe mutual is actually syntactic sugar for the second form?

[Alistair Tucker]

I believe your mutual def is syntactic sugar for something like

def fg : bool → ℕ → ℕ
| tt 0       := 1
| tt (n + 1) := n + fg ff n
| ff 0       := 0
| ff (n + 1) := n * fg tt n