Termination_by tutorial pointers?

Stream: new members

[Britt Anderson]

Doing some practice to familiarize myself with syntax by writing something to reverse a string.

def rstr (s : String) : String :=
    if (String.length s < 2)
    then s
    else
        let sprime := (String.drop s 1)
        (rstr sprime) ++ (String.singleton (String.front s))

which will do what I want with #eval!, but of course lean doesn't recognize that it will terminate. What I am looking for is some concise tutorial or demo code that deals with elementary examples like this to explain how one goes about this termination determination. At this point searching the internet just doesn't help the novice find the right beginners material. Thanks.

[Chris Bailey]

https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction

and you can skip to the part that starts with "In the following example, we prove termination by showing that as.size - i is decreasing in the recursive application" if you just want to see termination_by/decreasing_by

[Britt Anderson]

I have worked on this a bit without success. I have looked at the example and also the discussion in Functional Programming in Lean. I think I would benefit from a concrete example to help me get to grips with termination_by and friends. I suspect I could change my string to a list and then change it back and Lean could do a lot more of the work for me, but I am hoping to have an example with String so that I can see both the concrete implementation and the approach used with a data structure that doesn't have an easy to determine size. Proving the theorem that for a string 's' (s.drop 1).length < s.length for all s.length > 0 seems like it should be easier than I have been making it. Any help would be appreciated.

[Vlad Tsyrklevich]

I don't see many theorems proving much about String.drop or String sizeOf so you are having to prove it yourself instead of relying on the standard library. Question for others: Is there no way to prove that sizeOf s = s.length for a given String s? That would make proving this much easier. I don't see equivalents for List, so perhaps I misunderstand how sizeOf is supposed to be reasoned about.

The reverse string given by ChatGPT side steps this by using String.foldl:

def reverseString (s : String) : String :=
  s.foldl (fun acc c => c.toString ++ acc) ""

#eval reverseString "Lean4"  -- Output: "4naeL"

One thing that often happens is that different approaches can make proving something much easier or harder, and choosing an easier way to implement something is part of the art. It was much easier to just re-implement your function as the following, which lean can understand terminates by having an explicitly decreasing parameter:

def rstr_helper (s : String) (len : Nat) : String :=
    if len <= 1 then s
    else
        let sprime := (String.drop s 1)
        (rstr_helper sprime (len-1)) ++ (String.singleton s.front)

def rstr (s : String) : String :=
    rstr_helper s s.length

Here's what I got to force it, probably it's sub-optimal as I'm not familiar with this API:

import Mathlib

theorem helper {s :String} (h : 0 < s.length): sizeOf (s.drop 1) < sizeOf s := by
  rw [String.drop_eq]
  induction s
  rename_i list
  simp only [List.drop_one, String.mk.sizeOf_spec, add_lt_add_iff_left]
  induction list <;> simp_all

def rstr (s : String) : String :=
    if (String.length s < 2)
    then s
    else
        let sprime := (String.drop s 1)
        (rstr sprime) ++ (String.singleton (String.front s))
decreasing_by
  exact helper (by omega)

[Britt Anderson]

Thank you for the clear and thoughtful comments. I did not get that function from the free chat gpt, but I did from Gemini 2.0. I'll take a look at Sonnet 3.5. Your proof of theorem helper is much appreciated, but it is clearly something that I will not be able to do anytime soon; still I will soldier on, but I should take most to heart your suggestion that I think longer about setting up the function in the first place. The foldl is quite nice, but just adding the length value is something that I might have been able to figure out. The quick help is very encouraging, and I appreciate all of you spending time to help us beginneers.