termination_by

Stream: lean4

[Marcus Rossel]

Is there documentation on termination_by anywhere?
I've only seen a couple examples here on Zulip and couldn't understand how it works just from that.

[Henrik Böving]

There is a bit of documentation for the underlying concept called "well founded recursion" in Lean 3 and also in other theorem provers since its a very general concept but I'm not aware of any Lean 4 specific documentation.

[Henrik Böving]

The basic idea is that you have to show that for every recursive function call you perform you call it with a smaller (according to some order relation) value than your input value and if you can prove that it is of course guaranteed that the values continue to decrease until you terminate at some point.

[Chris B]

I don't think so, it's not in the manual yet. termination_by takes a well-founded relation r, and decreasing_by requires you to show that for whatever argument you're claiming decreases, r recursive_case current_case.

In this example, the relation is measure (fun ...) which just uses Nat.lt, and the proof goal for decreasing_by is n/10 < n.

def natPrintAux (n : Nat) (sink : List Char) : List Char :=
  if h0 : n < 10
  then (n.digitChar :: sink)
  else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink)
termination_by measure (fun ⟨n, _⟩ => n)
decreasing_by exact div_decreasing ⟨show 2 <= 10 by decide, Nat.le_of_not_lt h0⟩

#eval natPrintAux 123 []

[Chris B]

In termination_by, the thing being destructured is a PSigma of all the function arguments, and I'm picking the decreasing one.

[Chris B]

If you want to unfold the definition later, you have to write an auxiliary lemma similar to div_eq. For this one it's:

theorem natPrintAux_eq (n : Nat) (sink : List Char) :
  natPrintAux n sink = if n < 10 then (n.digitChar :: sink) else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink) := by
  simp only [natPrintAux, natPrintAux._unary]
  rw [WellFounded.fix_eq]
  simp
  rfl

The ._unary thing is auto-generated.

[Alex J. Best]

You can find a few things in the tests folder at https://github.com/leanprover/lean4/search?q=termination_by which I've found helpful as additional examples

[Gabriel Ebner]

You can also look in mathlib4 for inspiration: https://github.com/leanprover-community/mathlib4/blob/560f08f7faa727bf49a4a722e8ef31b080c32a06/Mathlib/Data/BinaryHeap.lean#L57-L71

[Marcus Rossel]

Chris B said:

I don't think so, it's not in the manual yet. termination_by takes a well-founded relation r, and decreasing_by requires you to show that for whatever argument you're claiming decreases, r recursive_case current_case.

In this example, the relation is measure (fun ...) which just uses Nat.lt, and the proof goal for decreasing_by is n/10 < n.

def natPrintAux (n : Nat) (sink : List Char) : List Char :=
  if h0 : n < 10
  then (n.digitChar :: sink)
  else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink)
termination_by measure (fun ⟨n, _⟩ => n)
decreasing_by exact div_decreasing ⟨show 2 <= 10 by decide, Nat.le_of_not_lt h0⟩

#eval natPrintAux 123 []

What is div_decreasing? I can't find it anywhere.

[Chris B]

I forgot I defined that in the file. The statement is theorem div_decreasing {n b : Nat} : 2 <= b ∧ b ≤ n → (n / b) < n.

[Chris B]

If you need the proof I'll pm it to you, but it's really sloppy. I would just sorry it.

[Siddhartha Gadgil]

I am a bit confused about what is really checked with termination_by. For example, the following code compiles fine, though there is no unsafe or partial

def bad(n: Nat): Nat :=
  bad <| n + 1
  termination_by measure (fun n => n)

Is this expected? Should one regard using termination_by without decreasing_by as equivalent to unsafe (but no warning is given). Any clarification is appreciated.

Thanks.

[Henrik Böving]

Doesn't compile fine for me at all, it complains about an unsolved goal x + 1 < x.

[Siddhartha Gadgil]

Thanks. I updated my toolchain (which was from October) and now it fails to compile. Apparently a bug in the past now fixed.

[Anders Christiansen Sørby]

I'm trying to implement a function which generates a range from a bounded Nat (BNat)

def BNat.range {min max} {h' : min ≤ max} : List $ BNat min max h' :=
  let rec @[specialize] it : BNat min max h' → (List $ BNat min max h') := (λ n =>
    if h : n.val < max then
      List.cons n $ it
        { val := Nat.succ n.val
        , isLe := (by apply h)
        , isGe := (by
          apply ge_is_le
          apply Nat.le_of_lt
          apply Nat.lt_succ_of_le
          apply n.isGe
        )
        }
    else
      [BNat.mk n.val (by apply n.isLe) n.isGe]
  )
  it (BNat.mk min h' (by apply ge_refl))
termination_by measure λ b => b.snd.snd.snd.val
decreasing_by exact (by simp)

How do I prove that the function will eventually reach n.val = max and terminate?

[Sebastian Ullrich]

It looks like you'll want to use max - n.val as the measure, as yours is not decreasing.

[Sebastian Ullrich]

Note that the built-in Range simply uses structural recursion at the cost of an additional parameter, though all this has been written before termination_by existed. https://github.com/leanprover/lean4/blob/64971a1e3cbf00e89e394beb24c6ce9331d85a19/src/Init/Data/Range.lean#L20

[Anders Christiansen Sørby]

How does Range.forIn show termination? Or does this not apply to monads?

[Anders Christiansen Sørby]

And btw how do I solve this goal:

case a
h w : Nat
ax : h ≥ 1 ∧ w ≥ 1
b : Board h w ax
⊢ h * h * (w * w) ≥ 1

Why can't I just apply ax somehow and call it a day?

[Kevin Buzzard]

Because you will also need the lemma that if a>=1 and b>=1 then a*b>=1 and Lean has to be told that somehow, either explicitly by you or via some tactic which knows this trick.

[Kevin Buzzard]

By the way, ≥ is considered evil in mathlib, we only use <= (otherwise we would have to state every lemma about inequalities at least twice)

[Arthur Paulino]

I don't think we have a tactic that powerful in Lean 4 yet. You will need to tell Lean the baby steps to get there.

theorem mul_ge_one_of_ge_one {a b : Nat} (ha : a ≥ 1 ) (hb : b ≥ 1) : a * b ≥ 1 := sorry

This should help you

[Gabriel Ebner]

Kevin Buzzard said:

By the way, ≥ is considered evil in mathlib, we only use <= (otherwise we would have to state every lemma about inequalities at least twice)

This is fortunately no longer the case in Lean 4, all the technical issues with ≥ have been resolved afaict.

[Arthur Paulino]

Arthur Paulino said:

I don't think we have a tactic that powerful in Lean 4 yet. You will need to tell Lean the baby steps to get there.

theorem mul_ge_one_of_ge_one {a b : Nat} (ha : a ≥ 1 ) (hb : b ≥ 1) : a * b ≥ 1 := sorry

This should help you

Then in tactic mode you would do:

have hh := mul_ge_one_of_ge_one ax.1 ax.1
have ww := mul_ge_one_of_ge_one ax.2 ax.2
exact mul_ge_one_of_ge_one hh ww

Now the challenge is proving mul_ge_one_of_ge_one

[Anders Christiansen Sørby]

Also how do I use DecidableEq and the decide tactic properly? I keep getting errors that it contains meta variables.

[Anders Christiansen Sørby]

Is there any proof of mul_ge_one_of_ge_on in mathlib?

[Arthur Paulino]

Anders Christiansen Sørby said:

Is there any proof of mul_ge_one_of_ge_on in mathlib?

library_search said docs#one_le_mul