bug in included variables

Stream: lean4

[Jireh Loreaux]

This issue came up in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unexpected.20variables. After applying cases to a hypothesis in the local context, another unused hypothesis which depends (in the dependent type sense) on that hypothesis is included in the type signature of the resulting declaration. This can be circumvented by clearing the unwanted hypothesis before doing cases, but that seems undesirable.

variable {n : Nat}
variable {a : Fin n}

theorem foo (c : Fin n) : c = c := by
  cases n
  · rfl
  · rfl

#check @foo
-- @foo : ∀ {n : Nat} {a : Fin n} (c : Fin n), c = c

theorem foo' (c : Fin n) : c = c := by
  clear a
  cases n
  · rfl
  · rfl

#check @foo'
-- @foo' : ∀ {n : Nat} (c : Fin n), c = c

theorem bar (c : Fin n) : c = c := rfl

#check @bar
-- @bar : ∀ {n : Nat} (c : Fin n), c = c

[Sebastian Ullrich]

That looks quite hard/unlikely to be fixed. cases can't know what variables you will use in the remaining proof, nor is adjusting the proof post-hoc a real option.

[Kevin Buzzard]

Interesting! But this wasn't happening in lean 3, right? I don't think I've ever seen a theorem in mathlib with a variable randomly being pulled in like that. Or am I wrong?

[Sebastian Ullrich]

Lean 3 was "include always unless omitted" afair. Lean 4 is "include if used in declaration", which turns out is tough to decide for cases.

[Kevin Buzzard]

The issues will manifest themselves very quickly (random "can't work out what this irrelevant term should be" errors) so it probably won't be too much of a hassle to work around

[Jireh Loreaux]

Sebastian, that's not the Lean 3 behavior. The above code would work in Lean 3 with a not appearing in the type signatures of any of the decorations.

[Jireh Loreaux]

Kevin, these errors are actually going to be hard/ annoying to spot. The way it came up for me is I had a rewrite with one of these bad lemmas that generated random goals. But the bad variables were implicit, so I only found it by looking at the full type signature of each declaration in the list.

[Mario Carneiro]

Yes, the lean 4 behavior is different and hopefully better. It eliminates the need for most uses of include

[Jireh Loreaux]

But now we need it again! Because we need omit

[Mario Carneiro]

I would fix the issue in this case by using {n} in the binder list

[Mario Carneiro]

and also just using variable less, generally

[Jireh Loreaux]

I tried removing the a as a variable, but it was needed many places.

[Jireh Loreaux]

(with autoImplicit on)

[Mario Carneiro]

even then I would just insert the binders if it's not ridiculous

[Mario Carneiro]

variables make the code harder to read

[Mario Carneiro]

clear a seems like a pretty close approximation to omit a as long as there are only a few lemmas that need to omit the variable and almost everything else uses it

[Jireh Loreaux]

I think the difference with omit vs clear is that the former occurs outside of the declaration, whereas the latter is inside it. And it seems very strange to have to reference a variable in the proof which is explicitly not used in the proof.

[Jireh Loreaux]

For readability that seems nightmarish.

[Mario Carneiro]

isn't that always the case with arguments to clear?

[Jireh Loreaux]

The {n} trick seems reasonable.

[Mario Carneiro]

if you wanted to use a hypothesis you wouldn't clear it, so things being cleared are basically always unused

[Mario Carneiro]

I typically need to use clear before cases and induction when they touch things they shouldn't

[Jireh Loreaux]

No? I mean clear can be used to remove a hypothesis that was used previously but is no longer necessary.

[Mario Carneiro]

so this example seems very normal

[Mario Carneiro]

you can find instances of clear _let_match and stuff in mathlib

[Mario Carneiro]

these are definitely not used variables

[Jireh Loreaux]

Okay, but the_let_match that occurred was generated by something used earlier in the proof, right?

[Mario Carneiro]

?? it's an automatically generated variable, I as the user did nothing to put it there and it is not for me

[Mario Carneiro]

you could say the same thing about variables in lean 4, if you hadn't set up your sections like that the variable wouldn't be there

[Jireh Loreaux]

I view something that was generated by something else meaningful I did in the proof (i.e., _let_match) very differently than something which is not related to anything in the declaration or proof script (I.e. a). However, I understand this may be just personal opinion. I wonder if @Kevin Buzzard feels the same or differently though.

[Kevin Buzzard]

I'm still coming to terms with the new way variables are used in lean 4. I absolutely agree that use of variables decreases readability but it hadn't occurred to me that with autoImplicit it might actually be the case that we'll be using variable a whole lot less.