unfold succeeds when refl doesn't

Stream: general

[Niels Voss]

Another question I had about recursive functions was under what conditions an expression is definitionally equal to what it expands into, including its recursive call.
For example, given this function:

def myfun : ℕ → ℕ
| 0 := 0
| 1 := 3
| (n + 2) := have h : (n + 2) / 2 < n + 2 := sorry,
  myfun ((n + 2) / 2)

lemma myfun_check : myfun 2 = myfun ((0 + 2) / 2) := by refl -- fails
lemma myfun_check : myfun 2 = myfun ((0 + 2) / 2) := by unfold myfun -- succeeds

I cannot prove myfun_check using refl, despite the left side expanding into the right side through computation. However, unfolding seems to work for some reason. I didn't realize it was possible for unfold to close a goal when refl doesn't. Is there a reason why refl doesn't work? I tried giving myfun the reducible attribute, but it didn't change anything.

[Junyan Xu]

If you #print myfun._main._pack you'll see the equation compiler compiles this recursive definition using well-founded recursion, and for some reason the computation rule for well-founded recursion can't be made rfl. (Most recent discussion in this thread.)

[Niels Voss]

I'm still having a bit of difficulty understanding that thread you linked, since I mostly treat the equation compiler as a sort of black box program that rewrites recursion in terms of induction, and have never actually thought about how it worked in practice. I can perhaps take a closer look at thread later, but I guess its understandable that rfl doesn't work for axiomatic reasons.
I'm fine if this isn't a definitional equality, but is there a way to, for example, expand one level of a recursive function in general, without going into the details behind well-foundedness (which I know little about)? unfold seems to work in this case, but it can be a bit annoying to use, especially, when unfolding something like an operator that is actually a typeclass instance.

[Reid Barton]

In general the answer is unfold. If there is a type class or something involved then it can also be a good idea to create your own "equational lemmas" phrased in a convenient way, and rewrite with them

[Niels Voss]

I guess if unfold works best I'll use that. I guess I was originally confused because I had previously thought that rfl worked by computing both sides of the equation until they equaled the same thing but I guess it's more complicated than that.

[Reid Barton]

"computing" is a complicated word

[Niels Voss]

Yes, it is. My current understanding of computing, when it comes to Lean, is that lambda expressions are evaluated by replacing all instances of the bound variable with the argument, so that (fun x, x + 2) 3 is definitionally equal to 3 + 2. In addition, whenever Lean encounters a "recursor" it evaluates it according to special rules so that (nat.cases_on 3 "hello" (λ n, "world") : string) reduces to "world" despite the fact that nat.cases_on is not defined as a lambda expression.
However, I could see how in really complicated expressions generated by the equation compiler, it could potentially get stuck on a recursor with some variable inside. I don't know if this is why rfl doesn't work on all well-founded recursive functions though.

[Kevin Buzzard]

If you do #print prefix myfun then you'll see the equation lemmas generated by the definition. Those are what unfold knows. In an ideal world they'd all be proved by rfl but for technical reasons this is not always the case.