bug in mathlib's have extension

Stream: mathlib4

[Floris van Doorn]

Mathlib extends the have tactic syntax that allows you to write have h : P which produces a new goal. However, it doesn't check whether P is actually a type.

import Mathlib.Tactic.Have

example : True := by
  have h : Eq -- should fail, but doesn't
  · sorry -- fails

[Ruben Van de Velde]

Do we want to keep it?

[Eric Wieser]

This doesn't error in the tactics:

example : True := by
  have h : Eq -- should fail, but doesn't
  sorry
  sorry

[Eric Wieser]

Somehow a single goal is made up of two goals!

image.png

[Floris van Doorn]

I still like this syntax for have, and judging from #6964 I'm not the only one. That said, I don't feel strongly about it.

[Floris van Doorn]

have := by feels a little awkward to me, since you go from tactic mode to term mode and back to tactic mode.

[Eric Rodriguez]

It's seen as a lean3-ism by some core maintainers, I think :/

[Yaël Dillies]

I am against have := by, and strongly against it being the only spelling.

[Eric Rodriguez]

I agree, and also think it's more elegant the other way. But it minimises auxiliary goal creation, which I think is a desirable feature

[Ruben Van de Velde]

I don't care all that much about the syntax, but I strongly prefer having only one

[Mario Carneiro]

Floris van Doorn said:

have := by feels a little awkward to me, since you go from tactic mode to term mode and back to tactic mode.

Well, this whole "mode" terminology is a bit outmoded... they are not and have never really been modes, but lean 4 even less so because it doesn't isolate elaboration results between by blocks like it used to. They are really just different syntax for the same thing.

The counterpoint here is that the := by syntax must always exist as long as := and by exist separately, so any other spelling will always be "a second way to write it"

[Mario Carneiro]

And having fewer more orthogonal features which combine together sounds like a better design IMO

[Mario Carneiro]

Also IIRC there are still some parsing issues with this syntax, I think the test file has a have in parentheses because of it

[Mario Carneiro]

This is all of course completely irrelevant to the actual bug report, of course we should fix that

[Mario Carneiro]

#8445