Chaining <;>

Stream: mathlib4

[Etienne Marion]

Hi! In the style guide, here is what written about <;>:

Often t0 <;> t1 is used to execute t0 and then t1 on all new goals. Either write the tactics in one line, or indent the following tactic.

  cases x <;>
    simp [a, b, c, d]

I'm facing a case where I'd like to write t0 <;> t1 <;> t2 <;> t3. Here t0 creates two goals and t1, t2 and t3 both apply to these two goals without creating new ones. It does not fit on one line so I'd rather put each tactic on a different line. Should it be done like this,

t0 <;>
  t1 <;>
    t2 <;>
      t3

which I guess is what it should be if following the style guide, but feels a bit too much indent; or like this:

t0 <;>
  t1 <;>
  t2 <;>
  t3

which looks better to me.

[Eric Wieser]

Does t0 <;> (t1; t2; t3) work for you?

[Eric Wieser]

If so, that's a little easier for the reader to reason about

[Damiano Testa]

I agree with Eric: while <;> can be convenient when cleaning up a proof, any future breakage is usually pretty painful to fix and requires undoing all the <;>. So, I find that minimising the use of <;> is typically adisable except in the simplest of cases.

[Kenny Lau]

For my curiosity, what are the tactics in question?

[Etienne Marion]

Eric Wieser said:

Does t0 <;> (t1; t2; t3) work for you?

That does work! I did not know you could stack the tactics after <;> using parentheses, thanks!

[Eric Wieser]

To be very clear, this approach is better because the "apply to these two goals without creating new ones" is now part of the source code.

[Damiano Testa]

To be really very clear: the two in Eric's formulation is not present it is "at least two"! :nerd:

[Etienne Marion]

Kenny Lau said:

For my curiosity, what are the tactics in question?

Out of context:

  refine ⟨s, hs, ?_, ?_⟩ <;>
    (rw [Measure.le_iff]; intro t ht; rw [μ.restrict_apply ht, ν.restrict_apply ht])

It's line 181 in Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean in #23500.

[Damiano Testa]

By the way, the parentheses convert a sequence of tactics (which is a thing from the point of view of syntax) into a single tactic (which is another thing from the point of view of syntax). This is why Eric's suggestion works.

[Eric Wieser]

Did ; also bring it under the long line limit then?

[Etienne Marion]

Damiano Testa said:

By the way, the parentheses convert a sequence of tactics (which is a thing from the point of view of syntax) into a single tactic (which is another thing from the point of view of syntax). This is why Eric's suggestion works.

I see. I had already met this situation where I want to apply many tactics after <;> and I tried putting everything on the same line with separating ; but it didn't work. I understand now that I was missing parentheses.

[Etienne Marion]

Eric Wieser said:

Did ; also bring it under the long line limit then?

No but I indented the parentheses block and it fits.

[Eric Wieser]

Another good option here is

t1
all_goals =>
  t2
  t3
  t4

[Damiano Testa]

Does all_goals take a =>?

[Eric Wieser]

In your case simp_rw [Measure.le_iff] before the refine might also be a good option

[Kyle Miller]

Yeah, I was going to suggest all_goals. It also saves needing to give a bunch of fiddly arguments:

lemma hahn_decomposition' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    ∃ s : Set α, IsHahnDecomposition μ ν s := by
  obtain ⟨s, hs, h₁, h₂⟩ := hahn_decomposition ν μ
  refine ⟨s, hs, ?_, ?_⟩
  all_goals
    rw [Measure.le_iff]
    intros
    simp [*]

[Kyle Miller]

There's also the little-seen case _ | _ => for saying "the next two goals must be completed by this tactic sequence":

lemma hahn_decomposition' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    ∃ s : Set α, IsHahnDecomposition μ ν s := by
  obtain ⟨s, hs, h₁, h₂⟩ := hahn_decomposition ν μ
  refine ⟨s, hs, ?_, ?_⟩
  case _ | _ =>
    rw [Measure.le_iff]
    intros
    simp [*]

[Damiano Testa]

Nice! This does encode the two from above!

[Kyle Miller]

This can be made more explicit with

...
  refine ⟨s, hs, ?c1, ?c2⟩
  case c1 | c2 =>
    rw [Measure.le_iff]
    intros
    simp [*]
...

[Kyle Miller]

There's also simp +contextual [*] instead of intros; simp [*].

[Etienne Marion]

Wow! Well I learnt much more than I was expecting, thanks to you all!

[Kyle Miller]

It can also be done in one line :-)

  refine ⟨s, hs, ?_, ?_⟩ <;> simp +contextual [Measure.le_iff, *]

This might be considered golfing at this point, but on the other hand maybe everything here is "obvious".

[Kyle Miller]

One more one-liner option, use the use tactic:

lemma hahn_decomposition' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    ∃ s : Set α, IsHahnDecomposition μ ν s := by
  obtain ⟨s, hs, h₁, h₂⟩ := hahn_decomposition ν μ
  use s, hs <;> simp +contextual [Measure.le_iff, *]