feat(data/list/cycle): cycle.map and has_repr (#8170)

src/data/list/cycle.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import data.list.rotate
-import data.finset.basic
+import data.finset.sort
 import data.fintype.list
 
 /-!
@@ -15,6 +15,11 @@ This relation is defined as `is_rotated`.
 
 Based on this, we define the quotient of lists by the rotation relation, called `cycle`.
 
+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.
+
 -/
 
 namespace list
@@ -577,6 +582,12 @@ The `s : cycle α` as a `multiset α`.
 def to_multiset (s : cycle α) : multiset α :=
 quotient.lift_on' s (λ l, (l : multiset α)) (λ l₁ l₂ (h : l₁ ~r l₂), multiset.coe_eq_coe.mpr h.perm)
 
+/--
+The lift of `list.map`.
+-/
+def map {β : Type*} (f : α → β) : cycle α → cycle β :=
+quotient.map' (list.map f) $ λ l₁ l₂ h, h.map _
+
 section decidable
 
 variable [decidable_eq α]
@@ -612,6 +623,22 @@ fintype.subtype (((finset.univ : finset {s : cycle α // s.nodup}).map
   (function.embedding.subtype _)).filter cycle.nontrivial)
   (by simp)
 
+/--
+The `multiset` of lists that can make the cycle.
+-/
+def lists (s : cycle α) : multiset (list α) :=
+quotient.lift_on' s
+  (λ l, (l.permutations.filter (λ (l' : list α), (l' : cycle α) = s) : multiset (list α))) $
+  λ l₁ l₂ (h : l₁ ~r l₂), by simpa using perm.filter _ h.perm.permutations
+
+@[simp] lemma mem_lists_iff_coe_eq {s : cycle α} {l : list α} :
+  l ∈ s.lists ↔ (l : cycle α) = s :=
+begin
+  induction s using quotient.induction_on',
+  rw [lists, quotient.lift_on'_mk'],
+  simpa using is_rotated.perm
+end
+
 /--
 The `s : cycle α` as a `finset α`.
 -/
@@ -663,4 +690,13 @@ by { rw [←next_reverse_eq_prev, ←mem_reverse_iff], exact next_mem _ _ _ _ }
 
 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.
+-/
+instance [has_repr α] : has_repr (cycle α) :=
+⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
+
 end cycle

src/data/list/rotate.lean

@@ -275,6 +275,16 @@ begin
       { exact nat.sub_lt_self (by simp) nat.succ_pos' } } }
 end
 
+lemma map_rotate {β : Type*} (f : α → β) (l : list α) (n : ℕ) :
+  map f (l.rotate n) = (map f l).rotate n :=
+begin
+  induction n with n hn IH generalizing l,
+  { simp },
+  { cases l with hd tl,
+    { simp },
+    { simp [hn] } }
+end
+
 section is_rotated
 
 variables (l l' : list α)
@@ -376,6 +386,14 @@ begin
   exact ⟨λ ⟨n, hn, h⟩, ⟨n, nat.lt_succ_of_le hn, h⟩, λ ⟨n, hn, h⟩, ⟨n, nat.le_of_lt_succ hn, h⟩⟩
 end
 
+@[congr] theorem is_rotated.map {β : Type*} {l₁ l₂ : list α} (h : l₁ ~r l₂) (f : α → β) :
+  map f l₁ ~r map f l₂ :=
+begin
+  obtain ⟨n, rfl⟩ := h,
+  rw map_rotate,
+  use n
+end
+
 section decidable
 
 variables [decidable_eq α]

test/cycle.lean

@@ -0,0 +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 ℤ))