Associativity of <;>

Stream: lean4

[Daniel Patterson]

Coming from Coq, I'm a little confused about how <;> is working.

I'd expect to be able to chain an entire sequence of tactics together with it, and have everything produced along the way get caught by the later tactics.

i.e. something like:

tac1 <;> tac2 <;> tac3 <;> tac4

I haven't minimized my example yet (sorry!), but I noticed, first, that whereas when I wrote something like the above, it wasn't closing the proof, but doing this was:

tac1 <;> tac2 all_goals tac3 all_goals tac4

(where there was only a single goal before tac1)

Based on my understanding how how <;> should work, there shouldn't be any difference (assuming there was only _one_ goal before tac1, which there was).

But then I realized that if I added parenthesis, I would get the right behavior, i.e.,

((tac1 <;> tac2) <;> tac3) <;> tac4

This seems... very confusing? Is this expected? I would have expected that this was the default associativity! Or is there something more subtle going on with regards to error behavior that the parentheses are working around?

[Reid Barton]

I would normally expect sequencing operations to be right associative (e.g. do { x ; y ; z } = x >> (y >> z).
However, I also can't think of a situation with <;> where it would make a difference...

[Reid Barton]

(Let's ignore tac4, since three tactics is enough to discuss associativity.)
Is the idea that tac2 fails on some of the goals from tac1, and then you want tac3 to run on them?

[Mario Carneiro]

<;> is associative, but if any of the tactic invocations fails then the whole sequence fails. If you want tactics to be able to fail and continue with the rest, you should use tac1 <;> (try tac2) <;> tac3 and the like

[Mario Carneiro]

@Daniel Patterson re: lack of MWE, it will be helpful to show the actual tactics involved rather than just tac1, tac2, because the goal-handling behavior of the involved tactics is potentially relevant

[Daniel Patterson]

Oh! I understand my issue, and it's (unsurprisingly) unrelated to what I thought it was.

The issue is that <;> binds tighter than try, so try has to be wrapped in parethesis, which I see in your use @Mario Carneiro . Two of my tactics (rws) I knew might fail, so I had wrapped them in try, but as <;> try (rw [...]) <;> ..., _not_ as <;> (try ...) <;>. As a result, the rw (which would sometimes fail) would take the entire rest of the chain with it.

Fixing that fixed the issue. So, apologies for the false report. I guess my actual issue was the binding precedence of <;>.

[David Renshaw]

it's not the first time this has come up: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/precedence.20of.20.60.3B.60.2F.60.3C.3B.3E.60.20vs.20.60try.60.2F.60repeat.60/near/314691801

[Daniel Patterson]

@David Renshaw Unfortunately, you can't search for <;> on here! Obviously, I'm new to Lean, but like you, I find the behavior very surprising, and I'm not sure what the purported benefit actually is. I'd much rather have to add braces / parens / something to be able to pass a block to try than to _need_ to have parens around it every time I use it with <;> (which, at least for me, I imagine will be much more common). I'm also anticipating this causing a lot of problems with my students (tbh, I'm wondering if its worth introducing them to try because of it... but it's kind of impossible to show any kind of automation without it...)

[David Renshaw]

I'm not sure what the purported benefit actually is

Using significant whitespace to avoid the need for explicit delimiters like {} seems to be one of the design goals of Lean 4.

[Mario Carneiro]

I think the challenge is more that we would need to make some complex parser changes to make it work, rather than that this is actually the desired behavior. I don't think anyone finds the current precedence to be sensible