Proving that nil = [] ?

Stream: new members

[Deidre House]

I'm self-studying lean and this has me really stumped. From Theorem Proving in Lean 4 / Inductive Types / Other Recursive Data Types , there's an exercise (notation modified slightly from the book to avoid collisions):

def append' {α : Type} (as bs : List α) : List α :=
  match as with
  | List.nil       => bs
  | List.cons ha ta => List.cons ha (append' ta bs)

theorem append_nil (as : List α) : append' as nil = as :=
  by cases as with
  | nil => rw [append']; rfl
  | cons b bs => {rw [append']; apply congrArg (List.cons b); exact append_nil bs}

It doesn't recognize the induction base case for append_nil as valid:

tactic 'rfl' failed, the left-hand side
  nil
is not definitionally equal to the right-hand side
  []

Now I thought that [] was just an alias for nil? I'm not sure what to tell Lean here. It seems Lean has no difficulty determining that [] = nil normally, for example via #eval. If there is a built in theorem establishing the equality, I wasn't able to find it. What is the correct way to show this?

[Aaron Liu]

Do set_option autoImplicit false and try again.

[Aaron Liu]

nil is being parsed as a new free variable instead of List.nil.

[Deidre House]

Oh wow, it was that easy? Changing the top line fixed it:

theorem append_nil (as : List α) : append' as List.nil = as :=
  by cases as with
  | nil => rw [append']
  | cons b bs => {rw [append']; apply congrArg (List.cons b); exact append_nil bs}

[Kevin Buzzard]

set_option autoImplicit false is a great option to set when you're just beginning with Lean. When you're beyond a certain level apparently it's safe to switch it to true, but I've never got to that level :-/ so I have it on false by default and it's saved me a lot of pain. Every typo I make, makes a new type, with autoImplicit set to true!

[Aaron Liu]

For that I look at the infoview, and it shows a list of all local declarations at the top of the goal state or expected type window. This has also saved me a lot of pain.

[Eric Wieser]

When you're beyond a certain level apparently it's safe to switch it off

I guess that level is "you are contributing to mathlib", because once you're there autoImplicit false is the default so no switching is needed...

[Kevin Buzzard]

By "I always have it switched to false " I really mean "I only ever contribute to projects where it's set to false by default" :-)

[Eric Wieser]

But also "and get tripped up by it frequently in the web editor, where it is not disabled", I assume - since this is certainly my experience

[Kevin Buzzard]

Yeah, I only ever click on the web editor to verify that the problem with someone's code is that they didn't set it to false!

[Matt Diamond]

I guess that level is "you are contributing to mathlib", because once you're there autoImplicit false is the default so no switching is needed...

Wait, I thought Kevin meant that it's safe to switch it on once you've reached a certain level. You're telling me beginners end up dealing with autoImplicit true and mathlib maintainers end up with autoImplicit false?? That seems kind of backwards...

[Matt Diamond]

(I mean I wouldn't want it enabled for Mathlib either... really it should only be enabled for proficient users who just want to quickly sketch out an idea)

[Kevin Buzzard]

Beginners don't know any better and start with their own repos or on the web editor

[Matt Diamond]

well yes, and that's a bad thing, right? and then some of them show up here and we have to tell them to turn off autoImplicit so they can see what the actual error is, and maybe some people don't even bother with Zulip and just give up and move on to something else

[Eric Wieser]

We could switch the default on the "mathlib" preset in the web editor?

[Eric Wieser]

(and leave it alone for the "Lean nightly" preset)

[Matt Diamond]

Sure, I think that could be a useful change... just my opinion, of course

[Eric Wieser]

Technically such a change is very easy, but to avoid needing FRO buy-in I think the web editor would need to distinguish "stable Lean without mathlib with autoImplicit", and "stable Lean with Mathlib without autoImplicit"

[Eric Wieser]

And then the playground link in Zulip has to decide which version to link to

[Matt Diamond]

eh... that seems like it would make the UI too confusing... maybe it's not worth the trouble

[Kyle Miller]

There's a neat new feature that will show up in the next release where autoimplicits get printed inline:

image.png

https://github.com/leanprover/lean4/pull/6768

[Matt Diamond]

ah neat! that should help a lot

[Sebastian Ullrich]

Improvements to error messages are also planned