how to show termination of McCarthy `M`

Stream: new members

[Asei Inoue]

/-- McCarthy's 91 function -/
def M (n : Nat) : Nat :=
  if n > 100 then
    n - 10
  else
    M (M (n + 11))

[Asei Inoue]

I don't even know what to specify for termination_by.

[Timo Carlin-Burns]

Here's my attempt

/-- McCarthy's 91 function -/
def M (n : Nat) : { m : Nat // m ≥ n - 10 } :=
  if h : n > 100 then
    ⟨n - 10, Nat.le_refl (n - 10)⟩
  else
    have := (M (n + 11)).property
    have :=
      calc n - 10
        _ ≤ (n + 11) - 10 - 10 := by omega
        _ ≤ (M (n + 11)).val - 10 := Nat.sub_le_sub_right this 10
        _ ≤ (M (M (n + 11)).val).val := (M (M (n + 11)).val).property
    ⟨(M (M (n + 11)).val).val, this⟩
termination_by 101 - n

[Timo Carlin-Burns]

To show that the outer recursive call terminates you need some properties of M, and you're not allowed to unfold M while defining it, so my workaround was to have M return a subtype with the necessary properties.

[Asei Inoue]

@Timo Carlin-Burns Thank you. It's a nice solution!!