First contribution: MeasureTheory/Decomposition/JordanSub

Stream: mathlib4

[Loïc Simon]

JordanSub.lean
Hi,
I'm an associate professor in CS/Stats, and in my recent journey to learn Lean, I've develop a small contribution that links the sub of two positive measures to the Jordan decomposition of the sub of the associated signed measure. The file is attached. Before going on with the pull request process, I'd like to see if the contribution is worth the trouble. If so, I'd be interested in feedback on the contribution as well.

Best,
Loïc

[Kim Morrison]

It's much easier to even give a first opinion if you just push a branch somewhere, rather than attach a file.

[Kevin Buzzard]

The (edit) non-terminal simps won't be allowed in mathlib but in general this looks promising to me (although I'm not an expert in the area, maybe experts will have reasons why this work should be done in another way)

[Ruben Van de Velde]

Non-terminal, you mean, I imagine

[Loïc Simon]

I started lean proving last week, so I m not sure what you mean by non terminal simp edit. Is it the same as simp squeezing?

[Kevin Buzzard]

Yes, simp followed by more tactics is strongly discouraged in mathlib because as simp changes over time (i.e. gets better) these proofs can break and can be hard to fix. If simp isn't the last line in a proof, then please squeeze it!

[Jireh Loreaux]

Ah nice, I was meaning to get around to this recently. I'll have a look when I get in front of a computer.

[Loïc Simon]

I pushed a branch called DrLSimon_JordanSub if that's more convenient.

[Loïc Simon]

So just to be sure, the good practice is to:

• squeeze non terminal simps
• not squeeze terminal ones
  Also a simp is considered terminal if it's the last line or is followed by exact, right?

[Edward van de Meent]

it's not terminal when it's followed by exact

[Edward van de Meent]

as #style says, it's terminal when it closes the goal or is only followed by "flexible" tactics, but exact is not a flexible tactic

[Loïc Simon]

Ok, thanks, I may have read the guidelines backward. I'll check that more carefully tomorrow.

[Loïc Simon]

Back to the squeeze issue. I think I get the point now, but just to be sure I'd like to check on a couple of examples.

@[simp]
theorem sub_zero {μ : Measure α} : μ - 0 = μ := by
  rw [sub_def]
  apply le_antisymm
  · simp [add_zero]; exact sInf_le (by simp)
  · simp [add_zero]

Should be changed to (by squeezing the first simp, but not the second one)

@[simp]
theorem sub_zero {μ : Measure α} : μ - 0 = μ := by
  rw [sub_def]
  apply le_antisymm
  · simp only [add_zero] --squeeze
    exact sInf_le (by simp)
  · simp [add_zero] -- should remain unsqueezed

[simp]
theorem toSignedMeasure_le_iff : μ ≤ ν ↔ μ.toSignedMeasure ≤ ν.toSignedMeasure := by
  constructor
  · intro h A hA
    simp [toSignedMeasure_apply, hA, measure_ne_top, ENNReal.toReal_le_toReal]
    exact h A

Should be changed to

@[simp]
theorem toSignedMeasure_le_iff : μ ≤ ν ↔ μ.toSignedMeasure ≤ ν.toSignedMeasure := by
  constructor
  · intro h A hA
    simp only [toSignedMeasure_apply, hA, ↓reduceIte, ne_eq, measure_ne_top, not_false_eq_true, ENNReal.toReal_le_toReal] -- squeezed
    exact h A

The next one is less clear to me:

    ∃ s : Set α, SignedMeasure.SetWhereGe μ ν s := by
  obtain ⟨s, hs, h₂, h₃⟩ := (μ.toSignedMeasure - ν.toSignedMeasure).exists_compl_positive_negative
  simp at h₂ h₃ -- should this one be squeezed ?
  exact ⟨s, hs, h₂, h₃⟩

BTW, I read the guidelines again but it's mainly focusing on "not squeezing" terminal simps. I can't find any recommendation to squeeze non terminal ones. I guess, it's going to become part of the guidelines soon, but just in case, I preferred to report it.

[Michael Rothgang]

Often simp followed by exact mylemma can be turned into simpa using mylemma: that's another option here.

[Michael Rothgang]

I agree with your assessment if the first two examples.

[Michael Rothgang]

The third question: a simp at foo can be non-terminal also. I'm not 100% sure about this particular case. What does mathlib's flexible linter say? Write set_option linter.flexible true before the theorem to enable it.

[Michael Rothgang]

(That linter is not enabled in mathlib as there were about 200 instances in mathlib which didn't have a nice obvious fix. So mathlib may be slightly inconsistent about such non-terminal simps.)

[Michael Rothgang]

Non-terminal simps not mentioned: in my opinion, that's a bug. Can you share which particular document you were looking at? Then we can fix that :-)

[Loïc Simon]

Thanks,

Concerning the guidelines, I was referring to https://leanprover-community.github.io/contribute/style.html#squeezing-simp-calls. As far as I understood when reading the relevant part, it clearly implied that terminal simps should not be squeeze. But I can't see any guidelines to make sure that non-terminal simps are squeezed.

W.r.t the simp at foo matter the flexible linter reports:

'simp at h₂ h₃' is a flexible tactic modifying 'h₃'…
note: this linter can be disabled with `set_option linter.flexible false`

If I squeeze it the warning disappears, so I guess, it should be squeezed.

[Vlad Tsyrklevich]

Yes, it's discussed here on the Simplifier page

[Loïc Simon]

May be that needs to be touched on, in the style guidelines as well.

[Kexing Ying]

The statement for the simp lemma toSignedMeasure_le_iff should be swapped to μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν since simp will change the LHS to the RHS.

[Loïc Simon]

Ok, I'll fix that. Thank you.