Using "by" with "have"

Stream: new members

[Auguste Poiroux]

Hello everyone!

I have a quick question about the use of "have" in a tactic mode. When you use it, you get a new goal (and an hypothesis) added to the panel. But when I use "by" right after to prove it, the panel is completely empty. On the other hand if I use "begin"-"end" or "{"-"}", the goals are in the panel.
I made a little trivial example on the online version of Lean: https://leanprover.github.io/live/3.3.0/#code=example%20:%20(1%20=%201)%20:=%0Abegin%0A%20%20have%20:%201=1,%0A%20%20refl,%0A%20%20exact%20this,%0Aend%0A%0Aexample%20:%20(1%20=%201)%20:=%0Abegin%0A%20%20have%20:%201=1,%0A%20%20begin%20refl%20end,%0A%20%20exact%20this,%0Aend%0A%0Aexample%20:%20(1%20=%201)%20:=%0Abegin%0A%20%20have%20:%201=1,%0A%20%20by%20refl,%0A%20%20exact%20this,%0Aend
If I place my cursor at the end of line 3 or line 10, I get two goals that appear in the panel. But if I place my cursor at the end of line 17, nothing is displayed.
Yet according to https://leanprover.github.io/reference/tactics.html, "by" is equivalent to a "begin"-"end" with a single tactic.
Is there something I missed?

Thank you in advance!

[Patrick Massot]

This is a quirk of the Lean server info request. You can use by { } to get back info.

[Patrick Massot]

And you shouldn't be using this web editor which uses a very badly outdated Lean, but rather https://leanprover-community.github.io/lean-web-editor/

[Auguste Poiroux]

Ok thanks!
So I tried "by { }" on the new editor (https://leanprover-community.github.io/lean-web-editor/#code=--%20Live%20WebAssembly%20version%20of%20Lean%0A%23eval%20let%20v%20%3A%3D%20lean.version%20in%20let%20s%20%3A%3D%20lean.special_version_desc%20in%20string.join%0A%5B%22Lean%20%28version%20%22%2C%20v.1.repr%2C%20%22.%22%2C%20v.2.1.repr%2C%20%22.%22%2C%20v.2.2.repr%2C%20%22%2C%20%22%2C%0Aif%20s%20%E2%89%A0%20%22%22%20then%20s%20%2B%2B%20%22%2C%20%22%20else%20s%2C%20%22commit%20%22%2C%20%28lean.githash.to_list.take%2012%29.as_string%2C%20%22%29%22%5D%0A%0Aexample%20%3A%20%281%20%3D%201%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%201%3D1%2C%0A%20%20refl%2C%0A%20%20exact%20this%2C%0Aend%0A%0Aexample%20%3A%20%281%20%3D%201%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%201%3D1%2C%0A%20%20begin%20refl%20end%2C%0A%20%20exact%20this%2C%0Aend%0A%0Aexample%20%3A%20%281%20%3D%201%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%201%3D1%2C%0A%20%20by%20refl%2C%0A%20%20exact%20this%2C%0Aend%0A%0A%0Aexample%20%3A%20%281%20%3D%201%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%201%3D1%2C%0A%20%20by%20%7Brefl%7D%2C%0A%20%20exact%20this%2C%0Aend%0A%0Aexample%20%3A%20%281%20%3D%201%29%20%3A%3D%0Abegin%0A%20%20have%20%3A%201%3D1%2C%0A%20%20%7Brefl%7D%2C%0A%20%20exact%20this%2C%0Aend%0A)
and I have the same issue. But using only "{ }" works...

[Patrick Massot]

It works for me

[Patrick Massot]

Putting the cursor after { in by { refl }

[Bryan Gin-ge Chen]

Note that if you are already in tactic mode, by doesn't really do anything. See e.g. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/library_search.20bug.3F/near/204334342

[Patrick Massot]

It does something if you put a single tactic, without curly braces: it clearly signals that a goal is meant to be closed here (which is good for maintainence).

[Bryan Gin-ge Chen]

Yes, that's true. My habit is to always write have ... :=(instead of using a comma) in which case adding by also changes from term mode to tactic mode.

[Auguste Poiroux]

Oh ok! I meant about getting "2 goals
⊢ 1 = 1

this: 1 = 1
⊢ 1 = 1" at the end of the "have" line (22 or 30 here).

[Bryan Gin-ge Chen]

I would chalk this up to what Patrick said. There are some quirks in how the tactic state is saved and returned.

[If you really want to dig into it, you could (after learning about tactic writing) look at the definition of the tactic have and see whether some save_infos should be inserted.]

[Auguste Poiroux]

Ok, thank you!