First experiments with recursive functions

Stream: new members

[Madir Mabbott]

My first recursive functions were so familiar and direct (addition, Fibonacci), no explicit termination_byhints were necessary. Now I'm having problems when the function structure gets more complicated. Even as little as wrapping the function parameter in a structure foils me.

 /-Obvious termination :: Iterate down a list, discarding terms, until we hit the empty string -/
  def recurse_to_empty1 (lst : List String) : List String  :=
    match lst with
    | [] => []
    | _  :: tl  => recurse_to_empty1 tl
    termination_by  sizeOf lst  -- termination is automatically determined, but can be made explicit

  #eval recurse_to_empty1 [ "a", "b", "c"] : List String
   -- [] -- as proven, the evaluation terminates

 -- Now wrap the solitary parameter in a structure
  structure wrapper where lst : List String
  def  wrappedLst : wrapper  := { lst := [ "a", "b", "c"] }

   /-- Unclear termination :: The same recursion as before, but now the input parameter is wrapped in a structure -/
   def recurse_to_empty2 (w : wrapper) : List String  :=
   match  w.lst with
      | []  =>  []
      | _  :: tl  =>  recurse_to_empty2  { lst := tl : wrapper}
       termination_by sorry  -- variants attempted, w, w.lst, sizeOf w, sizeOf w.lst, List.length w.lst

   #eval recurse_to_empty2 wrappedLst
   -- []  -- nevertheless, it does terminate

Can anyone help?

[Mitchell Lee]

Here's what the termination goal for your recurse_to_empty2 looks like if you use termination_by w.lst.length.

w : wrapper
tl : List String
⊢ List.length tl < List.length w.lst

Of course, this is not provable. Essentially, there is a missing hypothesis like w.lst = head✝ :: tl. Unfortunately, it seems that Lean does not "remember" this fact.

Here's one way to fix this.

def recurse_to_empty3 (w : wrapper) : List String :=
match w with
  | { lst := [] } => []
  | { lst := _ :: tl } => recurse_to_empty3 { lst := tl }

Or, a bit cleaner:

def recurse_to_empty4 (w : wrapper) : List String :=
match w with
  | ⟨[]⟩ => []
  | ⟨_ :: tl⟩ => recurse_to_empty4 ⟨tl⟩

Sorry if this isn't the most satisfactory answer.

[Madir Mabbott]

Many thanks. I will study this closely.

[Marcus Rossel]

Note that you can make Lean remember what w has matched against (by adding the h :):

def recurse_to_empty2 (w : wrapper) : List String  :=
  match h : w.lst with
  | []  =>  []
  | _  :: tl  =>  recurse_to_empty2  { lst := tl : wrapper}
termination_by w.lst.length
decreasing_by
  simp_wf
  simp [h]