Strange recursion question

Stream: new members

[Matej Penciak]

I'm fairly certain this kind of thing will never come up in any serious applications of Lean, so I first want to preface this question with an apology for how strange this might seem.

I've been writing up some notes for some students I've been talking to about formal verification, and I wanted to get across the idea that Lean is nothing more than a functional programming language, and that the tactics block is nothing more than a (very) fancy way of assembling a function.

I wanted to have a silly example of this by implementing the function that finds the maximum of a list. I tried with the first definition max_of_list.

def max_of_list : list ℕ → ℕ :=
begin
intro L,
cases L with head tail,
exact 0,
exact max head (max_of_list tail) -- This doesn't work
end

But this doesn't work because Lean complains that it doesn't know max_of_list when it calls itself. I then remembered a similar issue I ran into when I tried to write another silly example of a function which takes in a list of stuff and eventually outputs it to another function which prints it.

import system.io
meta def get_stuff (stuff : list string) : io (list string) := do
  io.put_str "Give an input (no to stop)\n",
  input ← io.get_line,
  if input = "no" then return stuff
  else get_stuff (input :: stuff) -- This also doesn't work

meta def get_stuff' : list string → io (list string)
| stuff := do
  io.put_str "Give an input (no to stop)\n",
  input ← io.get_line,
  if input = "no" then return stuff
  else get_stuff (input :: stuff) -- This does work though!

So after I made the same adjustment to max_of_list...

def max_of_list' : list ℕ → ℕ
| L :=
begin
cases L with head tail,
exact 0,
exact max head (max_of_list tail) -- Now it works!
end

It works! I was curious about what exactly is going on here which makes the first examples max_of_list and get_stuff not like the recursive call. But as soon as I define the function matching on the input, it has no issues with it.

[Yaël Dillies]

Your second try does pattern matching, which allows well-founded recursion. You simply can't do that in your first try.

[Yaël Dillies]

You might want to optimize this by actually pattern-matching on the list.

def max_of_list : list ℕ → ℕ
| [] := 0
| (head :: tail) := max head (max_of_list tail)

[Mauricio Collares]

https://exlean.org/well-founded-recursion/ is a related guide, I think (see the "Well-founded recursion by hand" section)

[Matej Penciak]

Yaël Dillies said:

Your second try does pattern matching, which allows well-founded recursion. You simply can't do that in your first try.

Is there a reason why well-founded recursion can work with pattern matching, but not defined in the different way? Is this more than a choice of how things are implemented in Lean?

[Matej Penciak]

Mauricio Collares said:

https://exlean.org/well-founded-recursion/ is a related guide, I think (see the "Well-founded recursion by hand" section)

I haven't seen this (or exlean in general) before! There are so many good resources out there, thank you!

[Yakov Pechersky]

Instead of cases, use "induction l using list.rec_on"