proving termination using bitwise shiftr

Stream: lean4

[David Stainton 🦡]

I'm fairly new to Lean and I'm hoping to get some advice for proving termination of this recursive function

def untilSet (fst snd : Nat) : Nat × Nat :=
  match fst, snd with
  | 0, _ => (0, snd)
  | f, s => if f % 2 != 0 then (f, s) else untilSet (f >>> 1) (s >>> 1)
  termination_by fst
  decreasing_by
  sorry

I'm told that it might be possible to replace the above shiftr operations to some equivalent in mathlib where the benefit would be a plethora of theorems where one of them might be useful in writing my proof of termination. So far I found this:

https://leanprover-community.github.io/mathlib_docs/init/data/nat/bitwise.html#nat.shiftr

[Henrik Böving]

def untilSet (fst snd : Nat) : Nat × Nat :=
  match fst, snd with
  | 0, _ => (0, snd)
  | f, s =>
    if h2 : f % 2 != 0 then
      (f, s)
    else
      have : f >>> 1 < f := by
        rw [Nat.shiftRight_eq_div_pow]
        sorry
      untilSet (f >>> 1) (s >>> 1)
termination_by fst

From here on it's some basic arithmetic theorem

[David Stainton 🦡]

interesting... i haven't seen this "have" key word yet

[Henrik Böving]

The error message tells you to use it.

[Henrik Böving]

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
fstfs: Nat
h2: ¬(f % 2 != 0) = true
⊢ f >>> 1 < f

[David Stainton 🦡]

aha that's right. it does tell me to use a it

[David Stainton 🦡]

thanks! that helps