Zulip Chat Archive

Stream: new members

Topic: Strange recursion question


Matej Penciak (Feb 24 2022 at 00:52):

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 (Feb 24 2022 at 00:55):

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

Yaël Dillies (Feb 24 2022 at 00:57):

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 (Feb 24 2022 at 01:08):

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

Matej Penciak (Feb 24 2022 at 04:18):

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 (Feb 24 2022 at 04:18):

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 (Feb 24 2022 at 04:40):

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


Last updated: Dec 20 2023 at 11:08 UTC