precedence of `;`/`<;>` vs `try`/`repeat`

Stream: lean4

[David Renshaw]

I find this behavior surprising:

variable {α : Type} (a b c : α)

-- works
example (h₁ : a = b) (h₂ : c = b) : b = a :=
by try rw[h₂]
   rw[h₁]

-- does not work
example (h₁ : a = b) (h₂ : c = b) : b = a :=
by try rw[h₂]; rw[h₁]
   -- goal not closed yet
   sorry

-- works with parentheses
example (h₁ : a = b) (h₂ : c = b) : b = a :=
by (try rw[h₂]); rw[h₁]

This came up in https://github.com/leanprover-community/mathlib4/pull/914, and earlier in https://github.com/leanprover-community/mathlib4/pull/370#discussion_r949498757.

Have other people hit trouble with this? Should I open an issue on the lean4 repo?

[Mario Carneiro]

While I agree with the sentiment, I'm not sure what the better alternative is, because try takes a tactic block, which can be indented and have internal semicolons, and it's not clear where to make it stop

[David Renshaw]

It's especially confusing, because the current relative precedences are different from how they are in Lean 3, so we're bound to keep running into it during the port

[David Renshaw]

(though I suppose we can ask mathport to insert parens)

[Mario Carneiro]

note that in lean 3 there was explicit bracketing

[David Renshaw]

what do you mean by that?

[Mario Carneiro]

which we could also do, try { tac } is legal syntax and does what you want

[Mario Carneiro]

example (h₁ : a = b) (h₂ : c = b) : b = a :=
by try {rw[h₂]}; rw[h₁] -- works

[Mario Carneiro]

mathport should currently be adding parentheses iff they are necessary. Are you saying that it is producing incorrect code?

[David Renshaw]

https://github.com/leanprover-community/mathlib4/pull/700 added a comment with syntax that did not include the parens:

    -- This used to be almost automatic with `split_ifs` and `cc`
    -- The split_ifs regression is noted in https://github.com/leanprover-community/mathlib4/issues/760
    -- split_ifs  at h <;> try subst b <;> try simp only [f.injective.eq_iff] at * <;> cc⟩

I was assuming that this came from the mathport output.

[David Renshaw]

It's possible that it was just manually copied / imperfectly ported.

[Sebastian Ullrich]

This has come up before and I think the best compromise we could come up with is that try etc on a single line should accept only a single tactic (with high precedence), while try followed by a linebreak should continue to work as right now

[Mario Carneiro]

The current parenthesizer is indeed broken:

import Lean
open Lean PrettyPrinter

#eval show MetaM _ from do
  let tac ← `(tactic| try skip)
  let stx ← `(tactic| ($tac; skip))
  formatTactic (← parenthesizeTactic stx)
-- (try skip; skip)

[Mario Carneiro]

(the correct answer there is ((try skip); skip))

[Sebastian Ullrich]

The fix is the same: ; should have a lower precedence than try. Currently it doesn't have any precedence at all in any sense, so the parenthesizer is powerless to do anything.

[Mario Carneiro]

the parenthesizer shouldn't be powerless here, even though it doesn't have a precedence in the usual sense

[Mario Carneiro]

Any issues of try parsing too much (under the current semantics) can be fixed with appropriately located parentheses, so it does seem like a job for the parenthesizer

[Sebastian Ullrich]

Precedence in the usual sense is all the current parenthesizer knows about

[Mario Carneiro]

okay, but this does seem to be part of the job description of the parenthesizer even if it isn't represented nicely for it

[Mario Carneiro]

I recall there being some text in the module doc about how the general problem is impossible to solve

[David Renshaw]

This has come up before and I think the best compromise we could come up with is that try etc on a single line should accept only a single tactic (with high precedence), while try followed by a linebreak should continue to work as right now

I'm worried that it would be confusing for these to have different meaning:

 try A
     B

 try
   A
   B

[Mario Carneiro]

those would both mean try (A; B)

[Sebastian Ullrich]

Yes, I think my description was more restrictive than a sensible implementation would be

[Mario Carneiro]

the counterintuitive behavior in sebastian's proposal is that

try A; B

means (try A); B but

try A; B
    C

means try (A; B; C)

[Mario Carneiro]

Here's a much simpler option: try takes a tactic, try => takes a tactic block

[Sebastian Ullrich]

A precedence ordering implementation should lead to

((try A); B)
     C

I believe, which would be a parse error, but I think I like your proposal more!

[Mario Carneiro]

what's the input? ((try A); B)\n C?

[Mario Carneiro]

I'm not sure why the C is hanging there

[Sebastian Ullrich]

The first line should be the partial syntax tree to your input, then the indented C is a parse error because of the checkColEq in sepBy1Indent

[Sebastian Ullrich]

with the precedence ordering ; < try < \n

[Sebastian Ullrich]

Ah, but we also want \n<;... yeah, that doesn't work

[Sebastian Ullrich]

Where's that paper about non-transitive precedence relations... :)

[David Renshaw]

Sebastian Ullrich said:

This has come up before and I think the best compromise we could come up with is that try etc on a single line should accept only a single tactic (with high precedence), while try followed by a linebreak should continue to work as right now

I wonder if instead we could introduce some lightweight (non-whitespace) syntax to mark the "now block" case. Like, maybe try: with a colon means "open a new block".

[Sebastian Ullrich]

Yes, that sounds similar to
Mario Carneiro said:

Here's a much simpler option: try takes a tactic, try => takes a tactic block

We probably don't want both => and :

[Sebastian Ullrich]

Combinators like case that already have => would presumably not have an inline version, which should be o.k.