count how many recursion

Stream: Is there code for X?

[Asei Inoue]

This is a my trial to count recursion call of gcd function.
I use fuel trick here to count recursion, but this way has many problems.

def mygcd' (m n fuel : Nat) : Option Nat :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
    if h : m = 0 then
      n
    else
      have : n % m < m := by
        apply mod_lt
        omega
      mygcd' (n % m) m fuel

theorem gcd_bound (m n fuel : Nat) (h : m < fuel) : (mygcd' m n fuel).isSome := by
  induction fuel generalizing m n with
  | zero =>
    simp_all
  | succ fuel ih =>
    dsimp [mygcd']
    split
    case isTrue hm => simp
    case isFalse hm =>
      have : n % m < m := by
        apply mod_lt
        omega
      replace : n % m < fuel := by omega
      replace ih := ih (n % m) m this
      assumption

[Asei Inoue]

The following methods are being considered

1. define a function T that counts the number of times to recur by T(0, n) = 0, T(m, n) = T(n % m, m)+1 to show an upper bound for T. We give up on giving a rigorous proof.

2. define the mygcd function by reference to the gcd function, so that the logic of gcd does not have to be re-implemented in mygcd.

[Bjørn Kjos-Hanssen]

How about just proving that gcd_bound is sharp?

theorem gcd_bound_lower : ∃ m n fuel, m ≥ fuel ∧ (mygcd' m n fuel) = none := by
  sorry