Unexpected parsing in `do`

Stream: lean4

[Thomas Murrills]

Here is some parsing behavior that might be a bit unexpected:

-- succeeds
example (f : False → Nat) : Bool := Id.run do
  let c := f by exact true

Likewise, replacing by exact true with return true also succeeds, but in that case at least the unused variables linter fires on c. (Perhaps the silence of the unused variables linter here is its own issue.)

The context I noticed this in was trying to use by exact? to fill in a proof argument, which was shaped like this:

example (f : False → Nat) : Bool := Id.run do
  have := () -- autogenerated `Unit` hypothesis in practice
  let c := f by exact? -- Try this: [apply] exact this
  return true

[Jovan Gerbscheid]

You always need to use <| in front of by. Then you get the expected behaviour.

-- fails
example (f : False → Nat) : Bool := Id.run do
  let c := f <| by exact true

[Thomas Murrills]

My point is that I don't think that should be the case. :)

[Jovan Gerbscheid]

A quick search shows about 4000 occurrences of <| by in mathlib. So I guess with your proposed change, these can all be replaced with by?

[Jovan Gerbscheid]

It would make sense, because the <| in <| do is redundant, and I feel like do and by should do the same precedence-wise.

[Thomas Murrills]

Jovan Gerbscheid said:

A quick search shows about 4000 occurrences of <| by in mathlib. So I guess with your proposed change, these can all be replaced with by?

I would expect so! :)

Though admittedly I don't have an actual change to propose (yet). It's quite possible that this has already been tried and is infeasible or not worth the squeeze for certain parsing reasons; I haven't checked.

[Thomas Murrills]

Though given your observation about do, it seems that maybe one route is just making by the same as do precedence-wise? Is that the implication?

[Robin Arnez]

I guess an important point here would also be the difference between

example (f : False → Nat) : Bool :=
  let c := f /-  error -/ by exact true
  true

and

example (f : False → Nat) : Bool := Id.run do
  let c := f by exact true -- works

example (f : False → Nat) : Bool := Id.run do
  let c := f by exact (sorry : False) -- fails
  return true

[Jovan Gerbscheid]

Thomas Murrills said:

It seems that maybe one route is just making by the same as do precedence-wise?

Yes, I think this should be a reasonably straight forward change

[Thomas Murrills]

Robin Arnez said:

I guess an important point here would also be the difference between

example (f : False → Nat) : Bool :=
  let c := f /-  error -/ by exact true
  true

and

example (f : False → Nat) : Bool := Id.run do
  let c := f by exact true -- works

example (f : False → Nat) : Bool := Id.run do
  let c := f by exact (sorry : False) -- fails
  return true

Oh, I see. So is this issue restricted to by as a doElem? :thinking:

[Thomas Murrills]

It seems there's some issue within by blocks as well:

example (f : False → Nat) : Bool := by
  let c := f by exact true -- unexpected token 'by'; expected command
  exact true

[Thomas Murrills]

Thomas Murrills said:

Oh, I see. So is this issue restricted to by as a doElem? :thinking:

Nevermind--after looking at the syntax tree, it seems there is no special by doElem parser. It is indeed just interpreting by exact true as a term, the same as if you'd written true (up to this precedence difference).

[Jovan Gerbscheid]

The following is written in the lean source code.

/--
Maximum precedence used in term parsers, in particular for terms in
function position (`ident`, `paren`, ...)
-/
macro "max"  : prec => `(prec| 1024)
/-- Precedence used for application arguments (`do`, `by`, ...). -/
macro "arg"  : prec => `(prec| 1023)
/-- Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...). -/
macro "lead" : prec => `(prec| 1022)

It claims that by has the arg precedence, but this is not true, because by currently has the lead precedence, not the arg precedence.

This commit changed the precedence of by from max to lead: https://github.com/leanprover/lean4/commit/05e6a779ba7b44f61543ba3f8369d50584e0d74b

The reason stated in that commit was that there were issues with the have A by B notation. This problem should also apply to the show A by B term, and the suffices A by B tactic.

However, we all know that it is possible to write for A in B do without any problem. The reason it that the for notation uses a trick: instead of parsing B with termParser, the notation uses withForbidden "do" termParser.

The same workaround could be used for by to make suffices A by Betc. keep working.

[Thomas Murrills]

Very nice! :)

[Yaël Dillies]

Yes, please, I've been wanting to get rid of all those <| by in mathlib for a long long time

[Jovan Gerbscheid]

I made a draft PR (lean#11455), and the corresponding mathlib build failed in only one place, for which the fix is at #32342.