termination_by from exists lemma

Stream: new members

[Markus Schmaus]

How can I show termination in this mwe?

import Mathlib

def foo (g : Nat → Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
  let rec loop (i : Nat) (x : Nat) : Nat :=
    if x = 0 then i
    else loop (i+1) (g x)
  loop 0 x

[Joachim Breitner]

Tricky. Note that loop on its own isn’t terminating on all inputs (set g i = i and i > 0). So you at least have to thread through the finiteness assumption through loop.

Then I you’d need a well-founded relation to decrease. If your finiteness predicate was in Type and not Prop (finite : { n : Nat // g^[n] x = 0}), you could extract that n and then use n - i as a decreasing measure. Is that an option for you?

[Timo Carlin-Burns]

I think this strategy could work:

import Mathlib

def foo (g : Nat → Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
  let rec loop (i : Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
    if hx : x = 0 then i
    else
      have finite' : ∃ (n : Nat), g^[n] (g x) = 0 := sorry
      have : ∀ (m : ℕ), (∀ n < m, ¬g^[n] (g x) = 0) → ¬g^[m] x = 0 := sorry
      loop (i+1) (g x) finite'
  termination_by Nat.find finite
  loop 0 x finite

[Joachim Breitner]

Quite likely, given that foo is essentially Nat.find :) The implementation of Nat.find shows one way of defining this.

[Timo Carlin-Burns]

def foo (g : Nat → Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
  let rec loop (i : Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
    if hx : x = 0 then i
    else
      have finite' : ∃ (n : Nat), g^[n] (g x) = 0 := by
        rcases finite with ⟨n, h⟩
        match n with
        | 0 => contradiction
        | (n + 1) => use n, h
      have : ∀ (m : ℕ), (∀ n < m, ¬g^[n] (g x) = 0) → ¬g^[m] x = 0
        | 0, _ => hx
        | (m + 1), h => h m (Nat.lt_succ_self m)
      loop (i+1) (g x) finite'
  termination_by Nat.find finite
  loop 0 x finite

[Markus Schmaus]

Thank you both for your help. It turns out this question was trickier than I thought it would.

[Timo Carlin-Burns]

To be explicit, this minimized example would be better written using Nat.find directly like so:

def foo (g : Nat → Nat) (x : Nat) (finite : ∃ (n : Nat), g^[n] x = 0) : Nat :=
  Nat.find finite

I don't know if that applies to your original problem too.