with_fuel.lean

def foo : Nat → Nat | 0 => 0 | n+1 => foo (n/2) + 1
termination_by n => n

def lots_of_fuel : Nat := 9223372036854775807

def with_fuel {α : Sort u} (x : α) (f : α → α) : α :=
  Nat.rec x (fun _ ih => f ih) lots_of_fuel

theorem with_fuel_spec {α : Sort u} {x : α} {f : α → α} (h : x = f x) :
    x = with_fuel x f := by
  unfold with_fuel
  exact Nat.rec rfl (fun _ ih => h.trans (congrArg f ih)) lots_of_fuel

abbrev with_fuel_helper {α : Sort u} (x : α) {f : α → α} (h : x = f x) : α :=
  with_fuel x f

def foo' : Nat → Nat := by
  have h := @foo.eq_unfold
  generalize foo = x at h
  exact with_fuel_helper x (by apply h)

theorem foo_eq_foo' : @foo = @foo' := by
  unfold foo' with_fuel_helper
  apply with_fuel_spec foo.eq_unfold

/--
error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
#reduce foo 1000

/-- info: 9 -/
#guard_msgs in
#reduce foo' 1000