Defining the opposite order of an existing order

Stream: Is there code for X?

[Antoine Chambert-Loir]

docs#WellOrderingRel defines a well order on a given type σ. Because I wish to use the lexicographic order on σ →₀ ℕ, and I need that lexicographic order to be a well order, I need to take the opposite of the one given by docs#WellOrderingRel (which will satisfy docs#WellOrderGT).
The simplest thing I could do, for that, was to write these lines:

import Mathlib.Data.Finsupp.WellFounded

variable (σ : Type*)
local instance : LinearOrder σ where
  le x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).le y x
  lt x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).lt y x
  le_refl x := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).le_refl x
  le_trans x y z p q := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).le_trans z y x q p
  lt_iff_le_not_le x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).lt_iff_le_not_le y x
  le_antisymm x y p q := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).le_antisymm x y q p
  min x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).max y x
  max x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).min y x
  compare x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).compare y x
  le_total x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).le_total y x
  decidableLE x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).decidableLE y x
  decidableEq x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).decidableEq x y
  decidableLT x y := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).decidableLT y x
  min_def x y := by
    simp only [min, LE.le, (WellOrderingRel.isWellOrder.linearOrder (α := σ)).max_def]
  max_def x y := by
    simp only [max, LE.le, (WellOrderingRel.isWellOrder.linearOrder (α := σ)).min_def]
  compare_eq_compareOfLessAndEq x y := by
    have := (WellOrderingRel.isWellOrder.linearOrder (α := σ)).compare_eq_compareOfLessAndEq y x
    unfold compare compareOfLessAndEq at this ⊢
    simp only at this ⊢
    rw [this]
    congr 1
    by_cases h : y = x
    · rw [if_pos h, if_pos h.symm]
    · rw [if_neg h, if_neg (Ne.symm h)]

but probably there is a better thing to do.
(Unfortunately, the docs#OrderDual defines an ordering on σ but called σᵒᵈ, and involves given instances relative to σ, hence I didn't really try to pull it back to σ.)

[Edward van de Meent]

it seems to me that this can be done a bit simpler:

variable (σ : Type*)

noncomputable local instance : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder

[Edward van de Meent]

or am i missing the point?

[Edward van de Meent]

ah, i see that i am missing the point

[Edward van de Meent]

i think this might be what is missing:

import Mathlib.Data.Finsupp.WellFounded

variable (σ : Type*) (r:σ → σ → Prop) [IsWellOrder σ r]

/- define a linear order using `r` such that `r x y` -> `y < x` -/
noncomputable def IsWellOrder.linearOrderSwap : LinearOrder σ :=
  letI : IsStrictTotalOrder σ (Function.swap r) := IsStrictTotalOrder.swap r
  letI := fun x y => Classical.dec ¬r y x
  linearOrderOfSTO (Function.swap r)

[Eric Wieser]

I would think you can just use OrderDual here

[Antoine Chambert-Loir]

Thanks Edward, this short definition of linearOrderSwap was exactly the missing point.
(The second letI line is not necessary for me, since I start from a LinearOrder which already contains the required decidability instances.)

[Antoine Chambert-Loir]

I end up with

variable (σ : Type*)
def LinearOrder.swap (h : LinearOrder σ) : LinearOrder σ :=
  letI : IsStrictTotalOrder σ (Function.swap h.lt) := IsStrictTotalOrder.swap h.lt
  linearOrderOfSTO (Function.swap h.lt)

and, in my proof, the invocation of

    letI : LinearOrder σ := LinearOrder.swap WellOrderingRel.isWellOrder.linearOrder
    letI : WellFoundedGT σ := by
      unfold WellFoundedGT
      suffices IsWellFounded σ fun x y ↦ WellOrderingRel x y by
        exact this
      exact IsWellOrder.toIsWellFounded

[Eric Wieser]

I think this works, and has better defeqs?

def LinearOrder.swap (_h : LinearOrder X) : LinearOrder X :=
  inferInstanceAs <| LinearOrder (OrderDual X)

[Antoine Chambert-Loir]

It works, thanks! (up to the obvious typo, and lint insists on anonymising the argument h).

[Antoine Chambert-Loir]

Thinking about this solution, I would like to understand what happens actually? Imagine we have two docs#LinearOrder on X and we want to combine them in some way

def LinearOrder.swap (h1 h2 : LinearOrder X) : LinearOrder X :=
  sorry

and some action within the sorry uses instances. How will Lean choose h1 over h2?
Or, what if in the context of LinearOrder.swapas above, there were already another LinearOrder X floating around?

[Kevin Buzzard]

docs#LinearOrder

[Kevin Buzzard]

The moment typeclass inference can find more than one linear order on X, or more generally two instances of a class, then my mental model is that it will just use a random one and you have no control over which one it finds (it might be that there is some internal hashing system and it finds the one with the smallest hash, for example). In situations like this you just have to feed everything explicitly with @ and filling in the instance you want. You can see this occasionally in master, for example (at least in lean 3) this had to be worked around when defining the partial order structure on topological space instances on a type.