LE instance for Prod String Nat and Sort

Stream: lean4

[Alexandre Rademaker]

What am I doing wrong? Is there an easier way to implement the sort of a list of pairs of (String, Nat)?

instance Prod.LE [LE α] [LE β] : LE (Prod α β) :=
 ⟨fun p q => (p.fst ≤ q.fst) ∧ (p.snd ≤ q.snd)⟩

def x : String × Nat := ("test",2)
def y : String × Nat := ("test",4)

#eval x ≤ y

def test :=
 let words := insertionSort (· ≤ ·) $ (proc doc1 1) ++ (proc doc2 2)
 words

The insertSort was implemented as

section InsertSort

variable {α : Type u} (r : α → α → Prop) [DecidableRel r]
local infixl:50 " ≼ " => r

def orderedInsert [LE α] (a : α)  : List α → List α
  | [] => [a]
  | b :: l => if a ≼ b then a :: b :: l else b :: orderedInsert a l

def insertionSort [LE α] : List α → List α
  | [] => []
  | b :: l => orderedInsert r b (insertionSort l)

end InsertSort

[Eric Wieser]

That instance you ask for already exists!

[Eric Wieser]

(deleted)

[Eric Wieser]

docs#Prod.instLE_mathlib

[Eric Wieser]

As, I think, does docs#List.insertionSort

[Alexandre Rademaker]

Thank you, you are right. I wonder why in the Mathlib and not in Batteries?

[Sebastian Ullrich]

For programming we usually use docs#lexOrd from core (which is not an instance because it can lead to diamonds, so apply locally)

[Eric Wieser]

Alexandre Rademaker said:

I wonder why in the Mathlib and not in Batteries?

Sometimes the answer is "no one has asked to move it yet"; but indeed there's some friction in choosing between LE and Ord here