TransCmp String

Stream: new members

[Ka Wing Li]

I am trying to prove the transitivity of string comparison for using the TreeMap.

instance : TransCmp (@compare String instOrdString) where
  eq_swap := by
    intros a b
    repeat rw [<- cmp_eq_compare]
    rw [cmp_swap]
  isLE_trans := by
    intros a b c ab bc
    sorry

It seems I have to prove the following lemma to use

lemma string_le : ∀ {a b : String}, (compare a b).isLE = true → a ≤ b := by
  intro a b h
  sorry

But seems I cannot progress here.

[Ka Wing Li]

Okay I figure it out:

instance : TransCmp (@compare String instOrdString) where
  eq_swap := OrientedOrd.eq_swap
  isLE_trans := TransOrd.isLE_trans

However, it is quite challenging to locate the mathlib documents. Is there a better way to look it up, or am I missing something important?

[Ka Wing Li]

Just curious why TransCmp (@compare String instOrdString) is not defined.

[Markus Himmel]

Seems to work for me?

import Std

open Std

instance : TransCmp (@compare String instOrdString) :=
  inferInstance

-- Prints `String.instTransOrd`
#synth TransCmp (@compare String instOrdString)