unfold tactic fails

Stream: new members

[Patrick Johnson]

Hello! This is my first post in Zulip chat. I'm just wondering why does unfold f not work in this example?

def f : ℕ → ℕ → Prop
| 0 0 := true
| (n + 1) (m + 1) := f n m
| _ _ := false

lemma lem1 : ¬f 0 1 := begin
  -- unfold f,
  exact id,
end

[Scott Morrison]

You can see what the equation compiler came up with using #print prefix f.

[Scott Morrison]

If you add the case | 0 (n+1) := false it does a better job, and unfold f will work.

[Scott Morrison]

The equation compiler is very useful, but can't be "perfect".

[Kyle Miller]

Curiously rw f does something, splitting it into two goals.