trying to understand termination

Stream: lean4

[Alice Laroche]

So, i really want to understand how termination work, so i writed this function

def blah : Nat -> Nat -> Nat
| 0    , m  => 0
| n + 1, m => blah (blah n (n + 1)) (blah n (m + 1))

My natural language proof of this terminating is something like

let's prove that for all n m, blah n m terminate and is equal 0, by induction on n
if n equal 0 , then blah 0 m equal 0, so blah 0 m terminate and is equal 0
Let's assume blah n m terminate and is equal 0 for all m
So blah n (n + 1) terminate and is equal 0 and so does blah n (m + 1)
So blah (n + 1) m is equal to blah 0 0 which terminate and is equal 0
By induction, for all n m blah n m terminate and is equal 0

But i dn't know how to put this in lean, or if it it's how it's done to begin with

[Simon Hudon]

Your definition is especially tricky because in proving that a function with that definition exists (i.e. that it terminates). In the process of proving termination however, we do know that all the expressions involved are well-typed and this is something we can work with.

Instead of returning a natural number we're going to return a subtype: a natural number with the proof that it is always equal to zero:

def JustZero := { i : Nat // i = 0 }

theorem JustZero.property (x : JustZero) :
  x.val = 0 := Subtype.property x

then your function definition becomes:

def blah : Nat -> Nat -> JustZero
| 0    , m  => ⟨0, rfl⟩
| n + 1, m => blah (blah n (n + 1)).1 (blah n (m + 1)).1

termination_by
  blah n m => n

but Lean still needs a bit of help with proving that this actually decreases so we add:

decreasing_by
  simp [JustZero.property] <;>
  first
  | apply Nat.zero_lt_succ
  | apply Nat.lt_succ_self

[Simon Hudon]

My decreasing_by is not as polished as I'd like but I'm still getting familiar with the construct. Any comments on improving it would be welcome

[Gabriel Ebner]

A common pattern is to use decreasing_by assumption (or leave it out entirely). You then write the termination proof directly next to the recursive call:

have : (blah n (n + 1)).1 < n + 1 := by ...
blah (blah n (n + 1)).1 (blah n (m + 1)).1

[Simon Hudon]

Nice thanks! For some reason I didn't think of trying the Lean 3 approach.

The definition now becomes:

def blah : Nat -> Nat -> JustZero
| 0    , m  => ⟨0, rfl⟩
| n + 1, m =>
  have : (blah n (n + 1)).1 < n + 1 :=
    by simp [JustZero.property, Nat.zero_lt_succ]
  blah (blah n (n + 1)).1 (blah n (m + 1)).1

termination_by
  blah n m => n

[Patrick Johnson]

Doesn't this defeat the purpose of the recursive function?

def JustZero := { i : Nat // i = 0 }

You could just write:

def blah : Nat -> Nat -> Nat
| _, _  => 0

What if you can't simplify the function? I think the proper way would be to use termination_by to prove that it terminates for any m when n = 0 and then prove that if it terminates for some n, then it terminates for n + 1.

I don't know how it is supposed to be done in Lean 4, but in Isabelle/HOL you can prove termination partially and then use induction to prove termination for the rest of the cases. Maybe Lean 4 can implement a similar mechanism.

[Alice Laroche]

Well this function has no purpose anyway, it's just a tool for learning.
This construction is actually useful for me, but you're right I would like to do it the way you present

[Simon Hudon]

You can make that work with mathlib's roption type actually.

As for defeating the purpose, I think you need to take a step back and see that this is a minimized example. You can make it work with JustZero or with any other subtype you like.

[Reid Barton]

BTW, roption is called part now.

[Alice Laroche]

(deleted)

[Simon Hudon]

Thanks! That's a better name, I'm glad the change was made

[Alex J. Best]

Patrick Johnson said:

I don't know how it is supposed to be done in Lean 4, but in Isabelle/HOL you can prove termination partially and then use induction to prove termination for the rest of the cases. Maybe Lean 4 can implement a similar mechanism.

Can you point me to some Isabelle code to see how this looks?

[Patrick Johnson]

Can you point me to some Isabelle code to see how this looks?

See section 8.1 of https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/functions.pdf. After defining equations, but before proving termination, Isabelle automatically defines a partial function constrained to the domain where the actual function terminates. We can then inductively build the domain of the function, eventually proving that the domain covers all valid inputs.

It is much harder to do in Lean. Consider this function (in Lean 3):

def f : ℕ → ℕ → ℕ
| m 0 := m
| m (n + 1) := f n m + 1

How would you prove that it terminates, without modifying the type of the function or defining new functions? In Isabelle, you can simply prove that (m, 0) is in the domain for all m and prove that if (m, n) is in the domain, then (n, m) is also in the domain, and then you can prove that n < n + 1 to finish the termination proof.

[Alice Laroche]

Actually this one is easy, because (n + m) reduce every step
So you can do (in Lean 4)

theorem helper1 : ∀m n, m + n < Nat.succ n + m :=
by intros m n
   rw [succ_add, Nat.add_comm]
   apply Nat.succ_le_succ
   apply Nat.le_refl

def f : Nat → Nat → Nat
| m , 0       => m
| m , (n + 1) => have h := helper1 m n
                 f n m + 1
termination_by f m n => n + m

[Patrick Johnson]

Fair enough. But my point was that Lean 4 should have a mechanism to inductively build the domain of a function and also allow users to use partial function until they prove it's total.

[Alice Laroche]

Oh you're completely right, I just wanted to train actually

[František Silváši]

Somewhat unrelated, I was trying to think of where I've seen that before and then it hit me. There's a 'standard' example of a function that alternates elements of two sequences,

def alternate (l₁ : List α) : List α → List α
  | h₂ :: t₂ => h₂ :: alternate t₂ l₁
  | [] => l₁
termination_by alternate l₁ l₂ => l₁.length + l₂.length
decreasing_by ...

where this 'argument swap' has semantics beyond 'f', which I reckon makes it much clearer what the termination criterion is. (This of course is besides the point in more than one way.)

[Siddhartha Gadgil]

I had a related question: I had a function that makes three recursive calls to itself. Is there a good way to use termination_by for such a situation. I used an auxiliary bound. For concreteness, I mean something similar to the below definitions.

partial def gcd0(a b: Nat): Nat :=
  if b = 0 then a else
  if b < a then gcd b (a % b) else gcd (b % a) a

def gcd1(n: Nat)(a b: Nat)(wa: a ≤ n)(wb: b ≤ n): Nat := sorry -- the total definition with some work

[Mario Carneiro]

@Siddhartha Gadgil In that case, you could use a + b as a termination measure

[Mario Carneiro]

@Patrick Johnson I proposed something along those lines early in lean 4, and the response I got was that partial is a MVP to make writing general recursive functions possible, and making something more suitable for proofs was a low priority. We have since gained termination_by which helps with a lot of these types of proofs, but I still think that an automatic domain predicate is possible (I have a general idea of how to do the desugaring, although dependent types complicate matters), and there are some kinds of functions that can't be proven to terminate using only termination_by (like Alice's original blah function before Simon changed the codomain to JustZero) but can be proven with an external domain predicate.

[Siddhartha Gadgil]

Thanks @Mario Carneiro .
My actual case is more complicated - the recursive calls are to the tail of a list and the two pieces of a list strictly before and strictly after some element in the list. All can be proved shorter than the original list, so the auxiliary bound method works. I was wondering if there is some termination_by approach for this.

[Mario Carneiro]

You should not need to add another argument

[Mario Carneiro]

in fact I would advise against it since this affects code generation

[Mario Carneiro]

could you give an example?

[Siddhartha Gadgil]

The code with partial def is at https://github.com/siddhartha-gadgil/Polylean/blob/main/Polylean/LengthBound.lean.

[Mario Carneiro]

It sounds like you want to use l.length as the termination measure

[Siddhartha Gadgil]

It is short enough that I can paste it here (eliminating some extraneous measure).

[Siddhartha Gadgil]

inductive Letter where
  | α : Letter
  | β : Letter
  | α! : Letter
  | β! : Letter
  deriving DecidableEq, Repr, Hashable

def Letter.inv : Letter → Letter
  | α => α!
  | β  => β!
  | α! => α
  | β! => β

postfix:max "⁻¹" => Letter.inv

abbrev Word := List Letter

-- split a word into parts before and after each occurrence of a letter `l`
def splits(l : Letter) : Word → List (Word × Word)
  | [] => []
  | x :: ys =>
    let tailSplits := (splits l ys).map (fun (fst, snd) => (x :: fst, snd))
    if x = l then ([], ys) :: tailSplits else tailSplits

partial def length : Word → Nat
  | [] => 0
  | x :: ys =>
    let base := 1 + (length ys)
    let derived := (splits x⁻¹ ys).map (fun (fst, snd) => length fst + length snd)
    derived.foldl min base -- minimum of base and elements of derived

[Siddhartha Gadgil]

I think I understand. when I paste termination_by length l => l.length I get an error that assumption failed to prove List.length fst < Nat.succ (List.length ys). But following the idea mentioned by @Gabriel Ebner I should give proofs have ... with bounds for these just before termination_by.

I have to prove the bounds anyway, so I use them this way instead of with an auxiliary parameter. I will work on this.

[Mario Carneiro]

-- split a word into parts before and after each occurrence of a letter `l`
def splits (l : Letter) : (w : Word) → List {p : Word × Word // p.1.length + p.2.length < w.length}
  | [] => []
  | x :: ys =>
    let tailSplits := (splits l ys).map fun ⟨(fst, snd), h⟩ =>
      ⟨(x :: fst, snd), by simp [Nat.succ_add, Nat.succ_lt_succ h]⟩
    if x = l then ⟨([], ys), by simp [Nat.lt_succ_self]⟩ :: tailSplits else tailSplits

def length : Word → Nat
  | [] => 0
  | x :: ys =>
    let base := 1 + (length ys)
    let derived := (splits x⁻¹ ys).map fun ⟨(fst, snd), h⟩ =>
      have h := Nat.lt_trans h (Nat.lt_succ_self _)
      have := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) h
      have := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) h
      length fst + length snd
    derived.foldl min base -- minimum of base and elements of derived
termination_by _ l => l.length

[Siddhartha Gadgil]

That's very nice. Thanks a lot. it shows me how to use sub-types effectively too (instead of custom types I have been using).

[Alice Laroche]

So, i was trying to apply my new knowledge about subtypes on more intricated functions, and the i got into this :

def Inf : Nat -> Type := fun n => {n' : Nat // n' <= n}

def blah : Nat -> (n : Nat) -> Inf n
| 0      , m       => ⟨0, Nat.zero_le _⟩
| (n + 1), 0       => ⟨0, Nat.le.refl⟩
| (n + 1), (m + 1) => ⟨(blah (blah n (n + 1)).1 m).1,
                        by have h := (blah (blah n (n + 1)).val m).2
                           apply Nat.le_trans h
                           apply Nat.le_succ
                      ⟩
termination_by blah x y => (x, y)

Here the subtypes say that blah n (n + 1) is inferior or equal to (n + 1)
But lean can't infer that ((blah n (n + 1).val , m) < (n + 1, m + 1)

[Patrick Johnson]

It works if you parametrize Inf with the first argument instead of the second:

def Inf (n : Nat) : Type := {n' : Nat // n' <= n}

def blah : (n : Nat) → Nat → Inf n
| 0      , m       => ⟨0, Nat.zero_le _⟩
| (n + 1), 0       => ⟨0, Nat.zero_le _⟩
| (n + 1), (m + 1) => have : (blah n (n + 1)).1 < n + 1 := by
                        cases blah n (n + 1)
                        apply Nat.lt_succ_of_le
                        assumption
                      ⟨(blah (blah n (n + 1)).1 m).1,
                        by have h := (blah (blah n (n + 1)).val m).2
                           apply Nat.le_trans h
                           apply Nat.le_of_lt
                           assumption ⟩
termination_by blah x y => (x, y)