antipattern

Stream: batteries

[Kim Morrison]

I am to blame here as I put this on the merge queue

theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
  simp [getLast?]
  split
  · exact absurd ‹_› scanr_ne_nil
  · simp [←‹_›, getLast_scanr]

but let's please never use ←‹_›, in Batteries or elsewhere.

[Ruben Van de Velde]

Rust has the turbofish, should we not have equally inscrutable syntax patterns?

[Weiyi Wang]

Harpoonfish?

[Wrenna Robson]

Kim Morrison said:

I am to blame here as I put this on the merge queue

theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
  simp [getLast?]
  split
  · exact absurd ‹_› scanr_ne_nil
  · simp [←‹_›, getLast_scanr]

but let's please never use ←‹_›, in Batteries or elsewhere.

Yeah I'll be honest I have never seen this before this moment.

[Wrenna Robson]

It looks evil though

[Alfredo Moreira-Rosa]

why not being a litle more explicit ?

theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
  unfold getLast?
  split <;> rename_i hscanr_eq
  · exact absurd hscanr_eq scanr_ne_nil
  · simp [←hscanr_eq, getLast_scanr]

or using cases and grind :

theorem getLast?_scanr {f : α → β → β} : (scanr f b l).getLast? = some b := by
  unfold getLast?
  cases _: scanr f b l
  · grind [scanr_ne_nil]
  · grind [getLast_scanr]

[Kim Morrison]

Exactly. (Actually, I replaced the whole thing with a grind.)

[Kyle Miller]

Huh, this is a creative use of ‹_›... I almost want to say that this syntax should throw an error if there are metavariables in the type (basically have ‹T› elaborated as show T by assumption) — or at least if there are metavariables it should check that there's exactly one hypothesis that matches!

Side note: I was idly thinking recently — unseriously — about what if the syntax for ‹T› were that T. Sort of like in "we know that T hence ...". If the term after that were optional, then, ignoring some precedence issues, that on its own could refer to a recent assumption :smiling_devil:

[cmlsharp]

I’d love some more evocative syntax for \f<. As someone kind of new to lean, I find myself misreading it as \< fairly often.

[Eric Wieser]

For what it's worth, AlphaProof was already pushing this ‹_› syntax in 2024 :)

[Jovan Gerbscheid]

I think the underlying problem here is that the split tactic has no syntax for giving a name to the introduced variable.

[Alfredo Moreira-Rosa]

there is a long standing proposal to improve split : https://github.com/leanprover/lean4/issues/2745