have syntax without ":= by"

Stream: lean4

[Jakob von Raumer]

Just updated some of my projects from 4.3.0 to 4.6.0 and it seems like the syntax for have is now more restrictive? I used to be able to write

  have h : x + y = z
  · skip

But that doesn't seems to be parsed anymore, why is that?

[Jakob von Raumer]

Or better: Where should I be looking for a documentation of breaking changes like that before upgrading?

[Mauricio Collares]

In this particular case you can import Mathlib.Tactic.Have to recover it (see #10534). I don't think there is documentation for Mathlib breaking changes.

[Jakob von Raumer]

Ah, didn't know mathlib changed the syntax, thought it came directly from lean4

[Mauricio Collares]

In general https://github.com/leanprover/lean4/blob/master/RELEASES.md should list breaking upstream changes.

[Jakob von Raumer]

So the := by ... is the form that's recommended now? It seems a bit silly to go out and into tactic mode unnecessarily

[Michael Stoll]

You can still write have h : ... := <proof term>.

[Jakob von Raumer]

Yes, but I rarely write proofs terms directly when using haves

[Ruben Van de Velde]

The := form is the only one that exists in core lean 4 at this point; I don't know if there's appetite to add another spelling there

[Michael Stoll]

Jakob von Raumer said:

Yes, but I rarely write proofs terms directly when using haves

But then you want to be in tactic mode anyway.

[Ruben Van de Velde]

I think Jakob's point is that you use := to go from tactic to term mode and then immediately use by to return to tactic mode, which seems wasteful(?) in a way

[Eric Wieser]

You can always stay in tactic mode with

have foo : Bar := ?_

[Eric Wieser]

Which is consistent with things like

cases s with
| inl => ?_
| inr => ?_

[Chris Wong]

I didn't know ?_ worked there too!

[Chris Wong]

Does that mean refine is redundant now, if exact foo ?_ does the same thing :thinking:

[Johan Commelin]

But I don't think exact foo ?_ works...

[Kevin Buzzard]

Right -- exact is the redundant one as it can be replaced with refine, as can use, constructor,... .