proof termination

Stream: lean4

[Notification Bot]

Alexandre Rademaker has marked this topic as unresolved.

[Alexandre Rademaker]

One more proof of termination that I can't finish

def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
 let rec seek (a b : Nat) : List Nat :=
  dbg_trace "seek {a} {b}"
  let m := (a + b) / 2
  if      h₁ : a > b   then []
  else if h₂ : t = f m then [m]
  else if h₃ : t < f m then
    seek a (m - 1)
  else
    seek (m + 1) b
 termination_by (b - a)
 seek 0 t

I have tried many possible variations in the termination_by clause.

EDITED: I was able to obtain a termination with the following code. But I wonder if I can avoid the duplicated test of t = f m

def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
 let rec seek (a b : Nat) : List Nat :=
  let m := (a + b) / 2
  if      h₁ : a ≥ b   then
   if t = f m then [m] else []
  else if h₂ : t = f m then [m]
  else if h₃ : t < f m then
    seek a (m - 1)
  else
    seek (m + 1) b
 termination_by (b - a)
 seek 0 t

[Joachim Breitner]

The first code works with a better termination tactic:

def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
 let rec seek (a b : Nat) : List Nat :=
  dbg_trace "seek {a} {b}"
  let m := (a + b) / 2
  if      h₁ : a > b   then []
  else if h₂ : t = f m then [m]
  else if h₃ : t < f m then
    seek a (m - 1)
  else
    seek (m + 1) b
  termination_by (b - a)
  decreasing_by grind
 seek 0 t

So once grind is done and ready for production, it’ll just work.

[Johannes Tantow]

Joachim Breitner schrieb:

The first code works with a better termination tactic:

def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
 let rec seek (a b : Nat) : List Nat :=
  dbg_trace "seek {a} {b}"
  let m := (a + b) / 2
  if      h₁ : a > b   then []
  else if h₂ : t = f m then [m]
  else if h₃ : t < f m then
    seek a (m - 1)
  else
    seek (m + 1) b
  termination_by (b - a)
  decreasing_by grind
 seek 0 t

So once grind is done and ready for production, it’ll just work.

Really? What if f is a constant function larger than t. Than we will always decrease b while a stays zero.
native_decide will overflow in the first case as well, but not in the second case.

[Joachim Breitner]

Sorry, my bad. The “The grind tactic is experimental and still under development. Avoid using it in production projects.” message obscured the fact that the tactic failed.

So whatever Johannes says :-)

[Alexandre Rademaker]

Thank you both for the feedback. The final code I presented above works with some redundant tests. I can finish with an empty list in two cases and return with a singleton list in two cases. Anyway, if I have the proof that h₁: ¬a = b so termination is proved for all recursive calls.

But what is unexpected is that grind didn't work in this code!

def search₂ (f : Nat → Nat) (t : Nat) : List Nat :=
 let rec seek (a b : Nat) : List Nat :=
  let m := (a + b) / 2
  if      h₁ : a = b   then
   if t = f m then [m] else []
  else if h₉ : a > b   then []
  else if h₂ : t = f m then [m]
  else if h₃ : t < f m then
    seek a (m - 1)
  else
    seek (m + 1) b
 termination_by (b - a)
 seek 0 t

I could also have kept the previous version with h₁ : a ≥ b, a single test for the two cases above, but I am not sure if I want to eventually return a value outside of the initial range (a,b) when a > b.