mathlib

mathlib copied to clipboard

Prior to #18163, the behavior was to sort based on the repr, meaning, that {0, 5, 10} is sorted as {0, 10, 5}.

After #18163, the order is non-deterministic and depends on how the set is constructed.

I think a better approach would be to hide the meta behind a typeclass instance: something like:

import logic.embedding.basic
import data.prod.lex
import data.pi.lex
import logic.equiv.basic
import data.string.basic
import data.multiset.sort

/-- When printing collections of `α`, sort via a representation in `αo` -/
class has_repr_order_key (α : Type*) (αo : out_param Type*) [linear_order αo] :=
(to_key : α ↪ αo)

instance linear_order.to_has_repr_order_key {α} [linear_order α] : has_repr_order_key α α :=
⟨function.embedding.refl _⟩

instance prod.to_has_repr_order_key {α β αo βo}
  [linear_order αo] [linear_order βo] [has_repr_order_key α αo] [has_repr_order_key β βo] :
  has_repr_order_key (α × β) (αo ×ₗ βo) :=
⟨(has_repr_order_key.to_key.prod_map has_repr_order_key.to_key).trans to_lex.to_embedding⟩

-- TODO: `pi` order

instance (α αo : Type*) [linear_order αo] [has_repr_order_key α αo]:
  is_linear_order α ((≤) on has_repr_order_key.to_key) :=
@has_le.le.is_linear_order _ $
  linear_order.lift' (has_repr_order_key.to_key : α → αo) has_repr_order_key.to_key.injective

/-- fallback instance using string sorting -/
@[priority 100, instance]
meta instance has_repr.to_has_repr_order_key {α} [has_repr α] :
  has_repr_order_key α string :=
⟨⟨repr, sorry⟩⟩  -- We can cheat to make this not a sorry since this is meta, right?

#eval ({1, (1, 5), (5, 1), 11} : multiset (ℕ × ℕ)).sort ((≤) on has_repr_order_key.to_key)

Originally posted by @eric-wieser in https://github.com/leanprover-community/mathlib/issues/18075#issuecomment-1374682665