Why is this evaluation not provable with rfl?

Stream: new members

[Ruotong]

Hi! I am new to Lean and trying to understand how rfl works. I wrote a function f as follows:

def f : α × List α → List (α × List α)
  | (a, [])       => [(a, [])]
  | (a, b :: bs)  => (a, bs) :: f (b, bs)

I thought f (0, []) should be definitionally equal to [(0, [])] because that's literally the definition. #reduce seems to confirm this, but the rfl constructor fails:

#reduce f (0, []) -- [(0, [])]
example : f (0, []) = [(0, [])] := rfl -- type mismatch

I tried a few things and found that I can prove this if

• the other branch of f is made non-recursive, or
• rfl is replaced with by rw [f].

But still, why does my original attempt with rfl fail?

Thank you!

[Chris Bailey]

When you use Prod to wrap the diminishing argument(s), the resulting definition is not as simple as it would be if it were "curried" as A -> List A -> List A; the function yielded by the Prod version uses well-founded recursion instead of structural recursion. If you look at the output of #print f with the product as an arg, it's marked as irreducible and the motive is a product; but for rfl to succeed in one go it needs to be able to do some reduction. Where possible you'll generally get better results by dropping wrappers like Prod, as in:

def f : α → List α → List (α × List α)
  | a, []       => [(a, [])]
  | a, b :: bs  => (a, bs) :: f b bs

#reduce f 0 [] -- [(0, [])]
example : f 0 [] = [(0, [])] := rfl

[Chris Bailey]

Also fwiw I do not see what you're seeing as the output of reduce with the α × List α arg, I see

Acc.rec
  (fun x₁ h ih =>
    List.rec (fun x => [(x₁.1, [])]) (fun head tail tail_ih x => (x₁.1, tail) :: x (head, tail) ⋯) x₁.2 ih)
  ⋯

Which is expected.

[Ruotong]

Thanks! This is very helpful!

As for reduce, what I tried was

#reduce f (0, [])

and this prints [(0, [])]. With

#reduce f

alone, I see the same thing.

[Robin Arnez]

You're probably on an older version then; in newer versions, you can't reduce functions defined by well-founded recursion

[Ruotong]

Robin Arnez said:

You're probably on an older version then; in newer versions, you can't reduce functions defined by well-founded recursion

Indeed! I just checked, and it turns out that the Git repo that I cloned specifies the Lean version to be an old one.

#reduce being consistent with rfl is much clearer.