a = b ∨ a < b vs a ≤ b

Stream: new members

[Moritz R]

Im a bit surprised we dont simp a = b ∨ a < b into a ≤ b in PartialOrder.
Is there a good reason for this?

[Snir Broshi]

A link to docs#le_iff_eq_or_lt would help

[Moritz R]

Yes sorry, im wondering why the reverse direction of that theorem isn't @[simp]

[Violeta Hernández]

In practice it's quite rare that you ever simplify something into a < b or a = b. There's only 41 uses of le_iff_eq_or_lt in Mathlib, only like three occur in simp calls, and they all simplify the other way around!

[Eric Wieser]

Violeta, the proposal was to use @[<- simp] I think

[Violeta Hernández]

My point is that it's rare for a simp call to leave you with the expression a < b ∨ a = b. So ← le_iff_eq_or_lt not a bad simp lemma in principle, but in practice it rarely ever does much for you.

[Moritz R]

This came up for me in the following. My order turns out to be equivalent to a threeway lexicographic order.
The middle condition can typically be completely evaluated, which in some cases essentially leaves me (from the last check, which is stated first here) with
(big = big' ∧ True ∧ small < small')
which simps to
(big = big' ∧ small < small')

Full lemma description:

/-- Comparing Literals is equivalent to first comparing the larger term of both atoms.
    If these are equal, tiebreak with polarity (neg > pos).
    If these are equal, tiebreak with the smaller term of both atoms.
    If these are also equal, then the literals are equal. -/
lemma LiteralOrder_iff_lexicographic
    [LinearOrder (Term F α)] (L1 L2 : Literal F α)
    (small big small' big' : Term F α)
    (hL1 : L1.toPos = .pos s(small, big))
    (hL2 : L2.toPos = .pos s(small', big'))
    (h1 : small ≤ big) (h2 : small' ≤ big') :
    L1 < L2 ↔
      (big = big' ∧ ((L1.isPos ∧ L2.isPos) ∨ (L1.isNeg ∧ L2.isNeg)) ∧ small < small')
      ∨ (big = big' ∧ L1.isPos ∧ L2.isNeg)
      ∨ big < big'
       := by

[Violeta Hernández]

Probably best to just manually add the lemma to your simp call.

[Alex Meiburg]

Or: you can add it to a custom simp set, that you then use throughout the relevant code!