Proving Termination using Pattern Matching information

Stream: lean4

[Bernardo Borges]

Hello everybody.
I am working on a definition of the log2 function, to practice, this is my implementation:

def log2 (x : ℕ) : ℕ := go x 0 where
  go
  | 0,_ => 0
  | 1,y => y
  | x,y =>
    have : x > 1 := sorry
    have : x / 2 < x := Nat.log2_terminates x this
    go (x/2) (y+1)

As you can see, my termination proof uses sorry, because I was not able to prove x > 1. How can I use the fact that the pattern match got this far into the proof?

[Damiano Testa]

Can you use | x + 2, y => in your last pattern match, and adjust the rest accordingly? Proving x + 2 > 1 should be easy! (Untested)

[Joachim Breitner]

Damiano’s suggestion is probably the best . Or don’t use match but if h0 : x = 0 … else if h1 : x = 1 … .
I think some people have considered making this “overlap hypothesis” available in the cases somehow, but it needs a good syntax and needs someone doing it.

[Bernardo Borges]

I tryied the x+2 solution but I didnt make an improvement with this.
Then, with @Joachim Breitner suggestion, I replaced the matchi with if's that get the proof, but the code changed dramatically:

def log2 (x : ℕ) : ℕ :=
  if h0 : x > 1 then
    go x 1 h0
  else 0
  where
  go (x y : ℕ) (h : x > 1) : ℕ :=
    have : x / 2 < x := Nat.log2_terminates x h
    if h0 : x / 2 > 1 then
      go (x/2) (y+1) h0
    else y