chore(data/multiset/sort): make multiset repr a meta instance (#18163)

ChrisHughes24 · eric-wieser · ChrisHughes24 · commit 00638177efd1 · 2023-01-14T03:06:08.000Z
Co-authored-by: Chris Hughes &lt;33847686+ChrisHughes24@users.noreply.github.com&gt;
Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean
@@ -211,6 +211,6 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of
 
 end sort_linear_order
 
-instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
+meta instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
 end finset
diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean
@@ -17,8 +17,8 @@ Based on this, we define the quotient of lists by the rotation relation, called
 
 We also define a representation of concrete cycles, available when viewing them in a goal state or
 via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
-as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
-underlying element. This representation also supports cycles that can contain duplicates.
+as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
+is different.
 
 -/
 
@@ -728,12 +728,12 @@ end decidable
 
 /--
 We define a representation of concrete cycles, available when viewing them in a goal state or
-via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
-as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
-underlying element. This representation also supports cycles that can contain duplicates.
+via `#eval`, when over representable types. For example, the cycle `(2 1 4 3)` will be shown
+as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
+is different.
 -/
-instance [has_repr α] : has_repr (cycle α) :=
-⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
+meta instance [has_repr α] : has_repr (cycle α) :=
+⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.unquot).head ++ "]"⟩
 
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
 
diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import data.list.sort
 import data.multiset.basic
-import data.string.basic
 
 /-!
 # Construct a sorted list from a multiset.
@@ -50,7 +49,8 @@ list.merge_sort_singleton r a
 
 end sort
 
-instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩
+-- TODO: use a sort order if available, gh-18166
+meta instance [has_repr α] : has_repr (multiset α) :=
+⟨λ s, "{" ++ string.intercalate ", " (s.unquot.map repr) ++ "}"⟩
 
 end multiset
diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
@@ -24,12 +24,15 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
+@[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
+-- `@[derive]` doesn't work for `meta` instances
+meta instance : has_repr prime_multiset := by delta prime_multiset; apply_instance
+
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)
 
diff --git a/src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/cycle/concrete.lean
@@ -537,7 +537,7 @@ def iso_cycle' : {f : perm α // is_cycle f} ≃ {s : cycle α // s.nodup ∧ s.
 notation `c[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
   cycle.form_perm ↑l (cycle.nodup_coe_iff.mpr dec_trivial)
 
-instance repr_perm [has_repr α] : has_repr (perm α) :=
+meta instance repr_perm [has_repr α] : has_repr (perm α) :=
 ⟨λ f, repr (multiset.pmap (λ (g : perm α) (hg : g.is_cycle),
   iso_cycle ⟨g, hg⟩) -- to_cycle is faster?
   (perm.cycle_factors_finset f).val
diff --git a/test/cycle.lean b/test/cycle.lean
@@ -1,5 +1,5 @@
 import data.list.cycle
 
 run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
-run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[2, 1, 4, 3] : cycle ℕ))
-run_cmd guard ("c[-1, 2, 1, 4]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))
+run_cmd guard ("c[2, 1, 4, 3]" = repr (↑[2, 1, 4, 3] : cycle ℕ))
+run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))
