doc-next-gen

Mathlib.Data.List.Cycle

Module docstring

{"# Cycles of a list

Lists have an equivalence relation of whether they are rotational permutations of one another. This relation is defined as IsRotated.

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 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.

"}

List.nextOr definition
: ∀ (_ : List α) (_ _ : α), α
Full source 
/-- Return the `z` such that `x :: z :: _` appears in `xs`, or `default` if there is no such `z`. -/
def nextOr : ∀ (_ : List α) (_ _ : α), α
  | [], _, default => default
  | [_], _, default => default
  -- Handles the not-found and the wraparound case
  | y :: z :: xs, x, default => if x = y then z else nextOr (z :: xs) x default
Next element in a list or default
Informal description
Given a list `xs` of elements of type `α`, an element `x` of type `α`, and a default value `default` of type `α`, the function returns the element `z` that immediately follows `x` in the list `xs`. If `x` does not appear in `xs` or is the last element, the function returns `default`. More precisely: - For an empty list `[]`, the result is `default`. - For a singleton list `[y]`, the result is `default`. - For a list `y :: z :: xs`, if `x = y`, then the result is `z`; otherwise, the function recursively checks the remainder of the list `z :: xs`.
List.nextOr_nil theorem
(x d : α) : nextOr [] x d = d
Full source 
@[simp]
theorem nextOr_nil (x d : α) : nextOr [] x d = d :=
  rfl
NextOr on Empty List Returns Default
Informal description
For any elements $x$ and $d$ of type $\alpha$, the function `nextOr` applied to an empty list `[]` with arguments $x$ and $d$ returns $d$. That is, $\text{nextOr}([], x, d) = d$.
List.nextOr_singleton theorem
(x y d : α) : nextOr [y] x d = d
Full source 
@[simp]
theorem nextOr_singleton (x y d : α) : nextOr [y] x d = d :=
  rfl
`nextOr` on a singleton list returns the default value
Informal description
For any elements $x, y, d$ of type $\alpha$, the function `nextOr` applied to the singleton list $[y]$, with arguments $x$ and $d$, returns $d$. That is, $\text{nextOr}([y], x, d) = d$.
List.nextOr_self_cons_cons theorem
(xs : List α) (x y d : α) : nextOr (x :: y :: xs) x d = y
Full source 
@[simp]
theorem nextOr_self_cons_cons (xs : List α) (x y d : α) : nextOr (x :: y :: xs) x d = y :=
  if_pos rfl
Next element after head in a list is the second element
Informal description
For any list `xs` of elements of type `α`, and elements `x`, `y`, `d` of type `α`, the function `nextOr` satisfies the equality: \[ \text{nextOr}(x :: y :: xs, x, d) = y \] This means that when the list starts with `x` followed by `y` and more elements, and we look for the element following `x`, the result is `y` regardless of the default value `d`.
List.nextOr_cons_of_ne theorem
(xs : List α) (y x d : α) (h : x ≠ y) : nextOr (y :: xs) x d = nextOr xs x d
Full source 
theorem nextOr_cons_of_ne (xs : List α) (y x d : α) (h : x ≠ y) :
    nextOr (y :: xs) x d = nextOr xs x d := by
  rcases xs with - | ⟨z, zs⟩
  · rfl
  · exact if_neg h
Next element in a list with head mismatch
Informal description
For any list `xs` of elements of type `alpha`, elements `y, x, d` of type `alpha`, and a proof `h` that `x ≠ y`, the function `nextOr` satisfies the equality: \[ \text{nextOr}(y :: xs, x, d) = \text{nextOr}(xs, x, d). \]
List.nextOr_eq_nextOr_of_mem_of_ne theorem
(xs : List α) (x d d' : α) (x_mem : x ∈ xs) (x_ne : x ≠ xs.getLast (ne_nil_of_mem x_mem)) : nextOr xs x d = nextOr xs x d'
Full source 
/-- `nextOr` does not depend on the default value, if the next value appears. -/
theorem nextOr_eq_nextOr_of_mem_of_ne (xs : List α) (x d d' : α) (x_mem : x ∈ xs)
    (x_ne : x ≠ xs.getLast (ne_nil_of_mem x_mem)) : nextOr xs x d = nextOr xs x d' := by
  induction' xs with y ys IH
  · cases x_mem
  rcases ys with - | ⟨z, zs⟩
  · simp at x_mem x_ne
    contradiction
  by_cases h : x = y
  · rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
  · rw [nextOr, nextOr, IH]
    · simpa [h] using x_mem
    · simpa using x_ne
Independence of `nextOr` from Default Value for Non-Last Elements
Informal description
For any list $xs$ of elements of type $\alpha$, elements $x, d, d'$ of type $\alpha$, if $x$ is an element of $xs$ and $x$ is not the last element of $xs$, then the result of $\text{nextOr}(xs, x, d)$ is equal to $\text{nextOr}(xs, x, d')$. In other words, when $x$ appears in $xs$ and is not the last element, the value of $\text{nextOr}$ does not depend on the choice of default value.
List.mem_of_nextOr_ne theorem
{xs : List α} {x d : α} (h : nextOr xs x d ≠ d) : x ∈ xs
Full source 
theorem mem_of_nextOr_ne {xs : List α} {x d : α} (h : nextOrnextOr xs x d ≠ d) : x ∈ xs := by
  induction' xs with y ys IH
  · simp at h
  rcases ys with - | ⟨z, zs⟩
  · simp at h
  · by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h
Membership Criterion via `nextOr`
Informal description
For any list `xs` of elements of type `α` and elements `x, d` of type `α`, if the result of `nextOr xs x d` is not equal to `d`, then `x` is an element of `xs`.
List.nextOr_concat theorem
{xs : List α} {x : α} (d : α) (h : x ∉ xs) : nextOr (xs ++ [x]) x d = d
Full source 
theorem nextOr_concat {xs : List α} {x : α} (d : α) (h : x ∉ xs) : nextOr (xs ++ [x]) x d = d := by
  induction' xs with z zs IH
  · simp
  · obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]
Default Behavior of `nextOr` on Appended Lists When Element is Absent
Informal description
For any list `xs` of elements of type `α`, an element `x` of type `α`, and a default value `d` of type `α`, if `x` does not belong to `xs`, then the result of `nextOr (xs ++ [x]) x d` is equal to `d`. Here, `nextOr` returns the element immediately following `x` in the concatenated list `xs ++ [x]`, or `d` if `x` is not found or is the last element.
List.nextOr_mem theorem
{xs : List α} {x d : α} (hd : d ∈ xs) : nextOr xs x d ∈ xs
Full source 
theorem nextOr_mem {xs : List α} {x d : α} (hd : d ∈ xs) : nextOrnextOr xs x d ∈ xs := by
  revert hd
  suffices ∀ xs' : List α, (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → nextOrnextOr xs x d ∈ xs' by
    exact this xs fun _ => id
  intro xs' hxs' hd
  induction' xs with y ys ih
  · exact hd
  rcases ys with - | ⟨z, zs⟩
  · exact hd
  rw [nextOr]
  split_ifs with h
  · exact hxs' _ (mem_cons_of_mem _ mem_cons_self)
  · exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)
Membership Preservation of `nextOr` in Lists
Informal description
For any list `xs` of elements of type `alpha`, and any elements `x` and `d` in `alpha`, if `d` is an element of `xs`, then the result of `nextOr xs x d` is also an element of `xs`. Here, `nextOr xs x d` returns the element immediately following `x` in `xs`, or `d` if `x` is not in `xs` or is the last element.
List.next definition
(l : List α) (x : α) (h : x ∈ l) : α
Full source 
/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the next
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

For example:
 * `next [1, 2, 3] 2 _ = 3`
 * `next [1, 2, 3] 3 _ = 1`
 * `next [1, 2, 3, 2, 4] 2 _ = 3`
 * `next [1, 2, 3, 2] 2 _ = 3`
 * `next [1, 1, 2, 3, 2] 1 _ = 1`
-/
def next (l : List α) (x : α) (h : x ∈ l) : α :=
  nextOr l x (l.get ⟨0, length_pos_of_mem h⟩)
Next element in a cyclic list
Informal description
Given a list `l` of elements of type `α` and an element `x ∈ l`, the function returns the element that immediately follows `x` in `l`. If `x` is the last element of `l`, the function returns the first element of `l`, making the list behave cyclically. More precisely: - For a singleton list `[y]`, the result is `y`. - For a list `y :: z :: xs`, if `x = y`, then the result is `z`; otherwise, the function recursively checks the remainder of the list `z :: xs`.
List.prev definition
: ∀ l : List α, ∀ x ∈ l, α
Full source 
/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the previous
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

 * `prev [1, 2, 3] 2 _ = 1`
 * `prev [1, 2, 3] 1 _ = 3`
 * `prev [1, 2, 3, 2, 4] 2 _ = 1`
 * `prev [1, 2, 3, 4, 2] 2 _ = 1`
 * `prev [1, 1, 2] 1 _ = 2`
-/
def prev : ∀ l : List α, ∀ x ∈ l, α
  | [], _, h => by simp at h
  | [y], _, _ => y
  | y :: z :: xs, x, h =>
    if hx : x = y then getLast (z :: xs) (cons_ne_nil _ _)
    else if x = z then y else prev (z :: xs) x (by simpa [hx] using h)
Previous element in a cyclic list
Informal description
Given a list `l : List α` and an element `x ∈ l`, the function `List.prev` returns the previous element of `x` in `l`, where the list is considered as a cycle. Specifically: - If `l` is empty, the function is undefined (as `x` cannot be in `l`). - If `l` is a singleton list `[y]`, then `prev [y] x _ = y`. - For a list `y :: z :: xs`, if `x = y`, then the result is the last element of `z :: xs`. - If `x = z`, then the result is `y`. - Otherwise, the function recursively checks the tail `z :: xs`.
List.next_singleton theorem
(x y : α) (h : x ∈ [y]) : next [y] x h = y
Full source 
@[simp]
theorem next_singleton (x y : α) (h : x ∈ [y]) : next [y] x h = y :=
  rfl
Next Element in Singleton Cycle is Itself
Informal description
For any elements $x$ and $y$ of type $\alpha$, if $x$ is in the singleton list $[y]$, then the next element of $x$ in this list (considered cyclically) is $y$.
List.prev_singleton theorem
(x y : α) (h : x ∈ [y]) : prev [y] x h = y
Full source 
@[simp]
theorem prev_singleton (x y : α) (h : x ∈ [y]) : prev [y] x h = y :=
  rfl
Previous element in a singleton cycle is itself
Informal description
For any elements $x$ and $y$ of type $\alpha$, if $x$ is in the singleton list $[y]$, then the previous element of $x$ in this list (considered cyclically) is $y$.
List.next_cons_cons_eq' theorem
(y z : α) (h : x ∈ y :: z :: l) (hx : x = y) : next (y :: z :: l) x h = z
Full source 
theorem next_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :
    next (y :: z :: l) x h = z := by rw [next, nextOr, if_pos hx]
Next element in a cons-cons list when $x$ is the head
Informal description
For any elements $x, y, z$ of type $\alpha$ and any list $l$ of type $\alpha$, if $x$ is in the list $y :: z :: l$ and $x = y$, then the next element after $x$ in this list is $z$.
List.next_cons_cons_eq theorem
(z : α) (h : x ∈ x :: z :: l) : next (x :: z :: l) x h = z
Full source 
@[simp]
theorem next_cons_cons_eq (z : α) (h : x ∈ x :: z :: l) : next (x :: z :: l) x h = z :=
  next_cons_cons_eq' l x x z h rfl
Next Element After Head in Cyclic List is Second Element
Informal description
For any element $x$ of type $\alpha$, any element $z$ of type $\alpha$, and any list $l$ of type $\alpha$, if $x$ is in the list $x :: z :: l$, then the next element after $x$ in this list is $z$.
List.next_ne_head_ne_getLast theorem
(h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y) (hx : x ≠ getLast (y :: l) (cons_ne_nil _ _)) : next (y :: l) x h = next l x (by simpa [hy] using h)
Full source 
theorem next_ne_head_ne_getLast (h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y)
    (hx : x ≠ getLast (y :: l) (cons_ne_nil _ _)) :
    next (y :: l) x h = next l x (by simpa [hy] using h) := by
  rw [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_of_ne]
  · rwa [getLast_cons] at hx
    exact ne_nil_of_mem (by assumption)
  · rwa [getLast_cons] at hx
Next Element in Extended Cyclic List When Not Head Nor Last
Informal description
Let $l$ be a list of elements of type $\alpha$, $x$ an element of $l$, and $y$ an element of type $\alpha$. Suppose $x$ is in the list $y :: l$ (the list formed by prepending $y$ to $l$), $x \neq y$, and $x$ is not the last element of $y :: l$. Then the next element after $x$ in the cyclic list $y :: l$ is equal to the next element after $x$ in the list $l$.
List.next_getLast_cons theorem
(h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y) (hx : x = getLast (y :: l) (cons_ne_nil _ _)) (hl : Nodup l) : next (y :: l) x h = y
Full source 
theorem next_getLast_cons (h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y)
    (hx : x = getLast (y :: l) (cons_ne_nil _ _)) (hl : Nodup l) : next (y :: l) x h = y := by
  rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]
  subst hx
  intro H
  obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H
  · rw [← Option.some_inj] at hk'
    rw [← getElem?_eq_getElem, dropLast_eq_take, getElem?_take_of_lt, getElem?_cons_zero,
      Option.some_inj] at hk'
    · exact hy (Eq.symm hk')
    rw [length_cons]
    exact length_pos_of_mem (by assumption)
  suffices k + 1 = l.length by simp [this] at hk
  rcases l with - | ⟨hd, tl⟩
  · simp at hk
  · rw [nodup_iff_injective_get] at hl
    rw [length, Nat.succ_inj]
    refine Fin.val_eq_of_eq <| @hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩
      ⟨tl.length, by simp⟩ ?_
    rw [← Option.some_inj] at hk'
    rw [← getElem?_eq_getElem, dropLast_eq_take, getElem?_take_of_lt, getElem?_cons_succ,
      getElem?_eq_getElem, Option.some_inj] at hk'
    · rw [get_eq_getElem, hk']
      simp only [getLast_eq_getElem, length_cons, Nat.succ_eq_add_one, Nat.succ_sub_succ_eq_sub,
        Nat.sub_zero, get_eq_getElem, getElem_cons_succ]
    simpa using hk
Next Element After Last in Non-Duplicate Cyclic List is Head
Informal description
Let $l$ be a list of elements of type $\alpha$, $x$ an element of $l$, and $y$ an element of type $\alpha$. Suppose $x$ is in the list $y :: l$ (the list formed by prepending $y$ to $l$), $x \neq y$, and $x$ is the last element of $y :: l$. If $l$ has no duplicate elements, then the next element after $x$ in the cyclic list $y :: l$ is $y$.
List.prev_getLast_cons' theorem
(y : α) (hxy : x ∈ y :: l) (hx : x = y) : prev (y :: l) x hxy = getLast (y :: l) (cons_ne_nil _ _)
Full source 
theorem prev_getLast_cons' (y : α) (hxy : x ∈ y :: l) (hx : x = y) :
    prev (y :: l) x hxy = getLast (y :: l) (cons_ne_nil _ _) := by cases l <;> simp [prev, hx]
Previous Element in Cyclic List when $x$ is Head and Equals $y$
Informal description
For any element $y$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $y :: l$ (i.e., $x$ is in the list formed by prepending $y$ to $l$) and $x = y$, then the previous element of $x$ in the cyclic list $y :: l$ is the last element of $y :: l$.
List.prev_getLast_cons theorem
(h : x ∈ x :: l) : prev (x :: l) x h = getLast (x :: l) (cons_ne_nil _ _)
Full source 
@[simp]
theorem prev_getLast_cons (h : x ∈ x :: l) :
    prev (x :: l) x h = getLast (x :: l) (cons_ne_nil _ _) :=
  prev_getLast_cons' l x x h rfl
Previous Element in Cyclic List when $x$ is Head
Informal description
For any element $x$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $x :: l$ (i.e., $x$ is in the list formed by prepending $x$ to $l$), then the previous element of $x$ in the cyclic list $x :: l$ is the last element of $x :: l$.
List.prev_cons_cons_eq' theorem
(y z : α) (h : x ∈ y :: z :: l) (hx : x = y) : prev (y :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _)
Full source 
theorem prev_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :
    prev (y :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _) := by rw [prev, dif_pos hx]
Previous Element in Cyclic List when $x$ is Head and Equals $y$
Informal description
For any elements $y, z$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $y :: z :: l$ (i.e., $x$ is in the list formed by prepending $y$ and $z$ to $l$) and $x = y$, then the previous element of $x$ in the cyclic list $y :: z :: l$ is the last element of $z :: l$.
List.prev_cons_cons_eq theorem
(z : α) (h : x ∈ x :: z :: l) : prev (x :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _)
Full source 
theorem prev_cons_cons_eq (z : α) (h : x ∈ x :: z :: l) :
    prev (x :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _) :=
  prev_cons_cons_eq' l x x z h rfl
Predecessor of Head Element in Cyclic List with Two Initial Elements
Informal description
For any element $z$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $x :: z :: l$ (i.e., $x$ is in the list formed by prepending $x$ and $z$ to $l$), then the previous element of $x$ in the cyclic list $x :: z :: l$ is the last element of $z :: l$.
List.prev_cons_cons_of_ne' theorem
(y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) : prev (y :: z :: l) x h = y
Full source 
theorem prev_cons_cons_of_ne' (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) :
    prev (y :: z :: l) x h = y := by
  cases l
  · simp [prev, hy, hz]
  · rw [prev, dif_neg hy, if_pos hz]
Predecessor of Second Element in Cyclic List
Informal description
For any elements $y, z$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $y :: z :: l$ (i.e., $x$ is in the concatenation of $[y, z]$ with $l$), and $x \neq y$ but $x = z$, then the previous element of $x$ in the cyclic list $y :: z :: l$ is $y$. In other words, when $x$ is the second element in the list $y :: z :: l$, its predecessor in the cyclic order is the first element $y$.
List.prev_cons_cons_of_ne theorem
(y : α) (h : x ∈ y :: x :: l) (hy : x ≠ y) : prev (y :: x :: l) x h = y
Full source 
theorem prev_cons_cons_of_ne (y : α) (h : x ∈ y :: x :: l) (hy : x ≠ y) :
    prev (y :: x :: l) x h = y :=
  prev_cons_cons_of_ne' _ _ _ _ _ hy rfl
Predecessor of Repeated Element in Cyclic List
Informal description
For any element $y$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $y :: x :: l$ (i.e., $x$ is in the concatenation of $[y, x]$ with $l$) and $x \neq y$, then the previous element of $x$ in the cyclic list $y :: x :: l$ is $y$.
List.prev_ne_cons_cons theorem
(y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x ≠ z) : prev (y :: z :: l) x h = prev (z :: l) x (by simpa [hy] using h)
Full source 
theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x ≠ z) :
    prev (y :: z :: l) x h = prev (z :: l) x (by simpa [hy] using h) := by
  cases l
  · simp [hy, hz] at h
  · rw [prev, dif_neg hy, if_neg hz]
Previous Element in List with Two Distinct Head Elements
Informal description
For any elements $y, z$ of type $\alpha$ and a list $l$ of type $\alpha$, if $x$ is an element of the list $y :: z :: l$ such that $x \neq y$ and $x \neq z$, then the previous element of $x$ in $y :: z :: l$ is equal to the previous element of $x$ in $z :: l$.
List.next_mem theorem
(h : x ∈ l) : l.next x h ∈ l
Full source 
theorem next_mem (h : x ∈ l) : l.next x h ∈ l :=
  nextOr_mem (get_mem _ _)
Membership Preservation of `next` in Cyclic Lists
Informal description
For any list $l$ of elements of type $\alpha$ and any element $x \in l$, the element obtained by applying the `next` function to $x$ in $l$ is also an element of $l$. More precisely, if $x$ is an element of $l$, then $\text{next}(l, x, h) \in l$, where $\text{next}(l, x, h)$ returns the element immediately following $x$ in $l$ (cyclically if $x$ is the last element).
List.prev_mem theorem
(h : x ∈ l) : l.prev x h ∈ l
Full source 
theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
  rcases l with - | ⟨hd, tl⟩
  · simp at h
  induction' tl with hd' tl hl generalizing hd
  · simp
  · by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)
Membership Preservation of `prev` in Cyclic Lists
Informal description
For any list $l$ of elements of type $\alpha$ and any element $x \in l$, the element obtained by applying the `prev` function to $x$ in $l$ is also an element of $l$. More precisely, if $x$ is an element of $l$, then $\text{prev}(l, x, h) \in l$, where $\text{prev}(l, x, h)$ returns the element immediately preceding $x$ in $l$ (cyclically if $x$ is the first element).
List.next_getElem theorem
(l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) : next l l[i] (get_mem _ _) = (l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi)))
Full source 
theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
    next l l[i] (get_mem _ _) =
      (l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi))) :=
  match l, h, i, hi with
  | [], _, i, hi => by simp at hi
  | [_], _, _, _ => by simp
  | x::y::l, _h, 0, h0 => by
    have h₁ : (x :: y :: l)[0] = x := by simp
    rw [next_cons_cons_eq' _ _ _ _ _ h₁]
    simp
  | x::y::l, hn, i+1, hi => by
    have hx' : (x :: y :: l)[i+1](x :: y :: l)[i+1] ≠ x := by
      intro H
      suffices (i + 1 : ℕ) = 0 by simpa
      rw [nodup_iff_injective_get] at hn
      refine Fin.val_eq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ ?_)
      simpa using H
    have hi' : i ≤ l.length := Nat.le_of_lt_succ (Nat.succ_lt_succ_iff.1 hi)
    rcases hi'.eq_or_lt with (hi' | hi')
    · subst hi'
      rw [next_getLast_cons]
      · simp [hi', get]
      · rw [getElem_cons_succ]; exact get_mem _ _
      · exact hx'
      · simp [getLast_eq_getElem]
      · exact hn.of_cons
    · rw [next_ne_head_ne_getLast _ _ _ _ _ hx']
      · simp only [getElem_cons_succ]
        rw [next_getElem (y::l), ← getElem_cons_succ (a := x)]
        · congr
          dsimp
          rw [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'),
            Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 (Nat.succ_lt_succ_iff.2 hi'))]
        · simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), hi']
        · exact hn.of_cons
      · rw [getLast_eq_getElem]
        intro h
        have := nodup_iff_injective_get.1 hn h
        simp at this; simp [this] at hi'
      · rw [getElem_cons_succ]; exact get_mem _ _
Cyclic Next Element Formula for Distinct Lists: $\text{next}(l, l[i]) = l[(i + 1) \bmod |l|]$
Informal description
For any list $l$ of distinct elements of type $\alpha$ and any index $i$ such that $i < \text{length}(l)$, the next element of $l[i]$ in the cyclic list $l$ is given by $l[(i + 1) \bmod \text{length}(l)]$. Here: - $\text{length}(l)$ denotes the length of the list $l$ - $l[i]$ denotes the $i$-th element of $l$ (0-indexed) - The modulo operation ensures the index stays within bounds when wrapping around the cyclic list
List.prev_getElem theorem
(l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) : prev l l[i] (get_mem _ _) = (l[(i + (l.length - 1)) % l.length]'(Nat.mod_lt _ (by omega)))
Full source 
theorem prev_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
    prev l l[i] (get_mem _ _) =
      (l[(i + (l.length - 1)) % l.length]'(Nat.mod_lt _ (by omega))) :=
  match l with
  | [] => by simp at hi
  | x::l => by
    induction l generalizing i x with
    | nil => simp
    | cons y l hl =>
      rcases i with (_ | _ | i)
      · simp [getLast_eq_getElem]
      · simp only [mem_cons, nodup_cons] at h
        push_neg at h
        simp only [zero_add, getElem_cons_succ, getElem_cons_zero,
          List.prev_cons_cons_of_ne _ _ _ _ h.left.left.symm, length, add_comm,
          Nat.add_sub_cancel_left, Nat.mod_self]
      · rw [prev_ne_cons_cons]
        · convert hl i.succ y h.of_cons (Nat.le_of_succ_le_succ hi) using 1
          have : ∀ k hk, (y :: l)[k] = (x :: y :: l)[k + 1]'(Nat.succ_lt_succ hk) := by
            simp
          rw [this]
          congr
          simp only [Nat.add_succ_sub_one, add_zero, length]
          simp only [length, Nat.succ_lt_succ_iff] at hi
          set k := l.length
          rw [Nat.succ_add, ← Nat.add_succ, Nat.add_mod_right, Nat.succ_add, ← Nat.add_succ _ k,
            Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt]
          · exact Nat.lt_succ_of_lt hi
          · exact Nat.succ_lt_succ (Nat.lt_succ_of_lt hi)
        · intro H
          suffices i.succ.succ = 0 by simpa
          suffices Fin.mk _ hi = ⟨0, by omega⟩ by rwa [Fin.mk.inj_iff] at this
          rw [nodup_iff_injective_get] at h
          apply h; rw [← H]; simp
        · intro H
          suffices i.succ.succ = 1 by simpa
          suffices Fin.mk _ hi = ⟨1, by omega⟩ by rwa [Fin.mk.inj_iff] at this
          rw [nodup_iff_injective_get] at h
          apply h; rw [← H]; simp
Cyclic Previous Element Formula for Distinct Lists: $\text{prev}(l, l[i]) = l[(i + |l| - 1) \bmod |l|]$
Informal description
For any list $l$ of distinct elements of type $\alpha$, an index $i$ such that $i < \text{length}(l)$, the previous element of $l[i]$ in the cyclic list $l$ is given by $l[(i + \text{length}(l) - 1) \bmod \text{length}(l)]$. Here: - $\text{length}(l)$ denotes the length of the list $l$ - $l[i]$ denotes the $i$-th element of $l$ (0-indexed) - The modulo operation ensures the index stays within bounds when wrapping around the cyclic list
List.pmap_next_eq_rotate_one theorem
(h : Nodup l) : (l.pmap l.next fun _ h => h) = l.rotate 1
Full source 
theorem pmap_next_eq_rotate_one (h : Nodup l) : (l.pmap l.next fun _ h => h) = l.rotate 1 := by
  apply List.ext_getElem
  · simp
  · intros
    rw [getElem_pmap, getElem_rotate, next_getElem _ h]
Cyclic Next Mapping Equals Single Rotation: $\text{map}_{\text{next}}(l) = l.\text{rotate}\, 1$
Informal description
For any list $l$ of distinct elements of type $\alpha$, the list obtained by mapping each element $x \in l$ to its next element in the cyclic list is equal to rotating $l$ by one position. In symbols: $$\text{map}_{\text{next}}(l) = l.\text{rotate}\, 1$$ where $\text{map}_{\text{next}}(l)$ denotes applying the $\text{next}$ function to each element of $l$.
List.pmap_prev_eq_rotate_length_sub_one theorem
(h : Nodup l) : (l.pmap l.prev fun _ h => h) = l.rotate (l.length - 1)
Full source 
theorem pmap_prev_eq_rotate_length_sub_one (h : Nodup l) :
    (l.pmap l.prev fun _ h => h) = l.rotate (l.length - 1) := by
  apply List.ext_getElem
  · simp
  · intro n hn hn'
    rw [getElem_rotate, getElem_pmap, prev_getElem _ h]
Cyclic Previous Mapping Equals Rotation by Length Minus One
Informal description
For any list $l$ of distinct elements of type $\alpha$, the list obtained by mapping each element to its previous element (in the cyclic sense) is equal to rotating $l$ by $|l| - 1$ positions, where $|l|$ denotes the length of $l$. In symbols: $$\text{pmap}(\text{prev}, l) = l.\text{rotate}(|l| - 1)$$
List.prev_next theorem
(l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : prev l (next l x hx) (next_mem _ _ _) = x
Full source 
theorem prev_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    prev l (next l x hx) (next_mem _ _ _) = x := by
  obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
  simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
  rcases l with - | ⟨hd, tl⟩
  · simp at hn
  · have : (n + 1 + length tl) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, Nat.succ_eq_add_one, this]
Cyclic List Property: $\text{prev} \circ \text{next} = \text{id}$
Informal description
For any list $l$ of distinct elements of type $\alpha$ and any element $x \in l$, the previous element of the next element of $x$ in $l$ is $x$ itself. That is, $\text{prev}(l, \text{next}(l, x)) = x$. Here: - $\text{next}(l, x)$ denotes the element immediately following $x$ in the cyclic list $l$ - $\text{prev}(l, y)$ denotes the element immediately preceding $y$ in the cyclic list $l$ - The list $l$ is assumed to have no duplicate elements (Nodup $l$)
List.next_prev theorem
(l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : next l (prev l x hx) (prev_mem _ _ _) = x
Full source 
theorem next_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    next l (prev l x hx) (prev_mem _ _ _) = x := by
  obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
  simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
  rcases l with - | ⟨hd, tl⟩
  · simp at hn
  · have : (n + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp [this]
Cyclic List Property: $\text{next}(\text{prev}(x)) = x$ for Distinct Elements
Informal description
For any list $l$ of distinct elements of type $\alpha$ and any element $x \in l$, the next element of the previous element of $x$ in $l$ (considered cyclically) is equal to $x$ itself. More precisely, if $l$ has no duplicates and $x$ is an element of $l$, then $\text{next}(l, \text{prev}(l, x)) = x$, where: - $\text{prev}(l, x)$ gives the element immediately preceding $x$ in $l$ (wrapping around cyclically if $x$ is the first element) - $\text{next}(l, y)$ gives the element immediately following $y$ in $l$ (wrapping around cyclically if $y$ is the last element)
List.prev_reverse_eq_next theorem
(l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : prev l.reverse x (mem_reverse.mpr hx) = next l x hx
Full source 
theorem prev_reverse_eq_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    prev l.reverse x (mem_reverse.mpr hx) = next l x hx := by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  have lpos : 0 < l.length := k.zero_le.trans_lt hk
  have key : l.length - 1 - k < l.length := by omega
  rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]
  simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]
  rw [← getElem_pmap l.reverse.prev fun _ h => h]
  · simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
    rw [getElem_eq_getElem_reverse]
    · simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]
  · simpa
Previous in Reversed List Equals Next in Original List for Distinct Elements
Informal description
For any list $l$ of distinct elements of type $\alpha$ and any element $x \in l$, the previous element of $x$ in the reversed list $l^{\mathrm{rev}}$ is equal to the next element of $x$ in the original list $l$. In symbols: $$\text{prev}(l^{\mathrm{rev}}, x) = \text{next}(l, x)$$
List.next_reverse_eq_prev theorem
(l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : next l.reverse x (mem_reverse.mpr hx) = prev l x hx
Full source 
theorem next_reverse_eq_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    next l.reverse x (mem_reverse.mpr hx) = prev l x hx := by
  convert (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm
  exact (reverse_reverse l).symm
Next in Reversed List Equals Previous in Original List for Distinct Elements
Informal description
For any list $l$ of distinct elements of type $\alpha$ and any element $x \in l$, the next element of $x$ in the reversed list $l^{\mathrm{rev}}$ is equal to the previous element of $x$ in the original list $l$. In symbols: $$\text{next}(l^{\mathrm{rev}}, x) = \text{prev}(l, x)$$
List.isRotated_next_eq theorem
{l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) : l.next x hx = l'.next x (h.mem_iff.mp hx)
Full source 
theorem isRotated_next_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
    l.next x hx = l'.next x (h.mem_iff.mp hx) := by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  obtain ⟨n, rfl⟩ := id h
  rw [next_getElem _ hn]
  simp_rw [getElem_eq_getElem_rotate _ n k]
  rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]
  simp [add_assoc]
Next Element Invariance under List Rotation for Distinct Lists
Informal description
For any two lists $l$ and $l'$ of type $\alpha$ that are rotated versions of each other (i.e., $l \sim_r l'$), if $l$ has no duplicate elements, then for any element $x \in l$, the next element of $x$ in $l$ is equal to the next element of $x$ in $l'$. In symbols: $$l \sim_r l' \land \text{Nodup}(l) \land x \in l \Rightarrow \text{next}(l, x) = \text{next}(l', x)$$
List.isRotated_prev_eq theorem
{l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) : l.prev x hx = l'.prev x (h.mem_iff.mp hx)
Full source 
theorem isRotated_prev_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
    l.prev x hx = l'.prev x (h.mem_iff.mp hx) := by
  rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
  exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _
Previous Element Invariance under List Rotation for Distinct Lists
Informal description
For any two lists $l$ and $l'$ of type $\alpha$ that are rotated versions of each other (i.e., $l \sim_r l'$), if $l$ has no duplicate elements, then for any element $x \in l$, the previous element of $x$ in $l$ is equal to the previous element of $x$ in $l'$. In symbols: $$l \sim_r l' \land \text{Nodup}(l) \land x \in l \Rightarrow \text{prev}(l, x) = \text{prev}(l', x)$$
Cycle definition
(α : Type*) : Type _
Full source 
/-- `Cycle α` is the quotient of `List α` by cyclic permutation.
Duplicates are allowed.
-/
def Cycle (α : Type*) : Type _ :=
  Quotient (IsRotated.setoid α)
Cycle type as quotient of lists by rotation
Informal description
The type `Cycle α` is the quotient of the type `List α` by the equivalence relation of cyclic permutation. This means that two lists are considered equivalent if one can be rotated to obtain the other, and `Cycle α` consists of equivalence classes under this relation. Duplicate elements within lists are allowed in this construction.
Cycle.ofList definition
: List α → Cycle α
Full source 
/-- The coercion from `List α` to `Cycle α` -/
@[coe] def ofList : List α → Cycle α :=
  Quot.mk _
Canonical map from lists to cycles
Informal description
The function maps a list `l` of type `α` to its equivalence class in the quotient type `Cycle α`, where two lists are equivalent if one is a rotation of the other.
Cycle.instCoeList instance
: Coe (List α) (Cycle α)
Full source 
instance : Coe (List α) (Cycle α) :=
  ⟨ofList⟩
Canonical Inclusion of Lists into Cycles
Informal description
There is a canonical way to view any list of type $\alpha$ as an element of the cycle type $\text{Cycle } \alpha$, where cycles are equivalence classes of lists under rotation.
Cycle.coe_eq_coe theorem
{l₁ l₂ : List α} : (l₁ : Cycle α) = (l₂ : Cycle α) ↔ l₁ ~r l₂
Full source 
@[simp]
theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Cycle α) = (l₂ : Cycle α) ↔ l₁ ~r l₂ :=
  @Quotient.eq _ (IsRotated.setoid _) _ _
Equality of Cycle Representatives iff Lists are Rotationally Equivalent
Informal description
For any two lists $l_1$ and $l_2$ of type $\alpha$, their images under the canonical map to the cycle type $\text{Cycle}\,\alpha$ are equal if and only if $l_1$ and $l_2$ are rotationally equivalent, i.e., $l_1 \sim_r l_2$.
Cycle.mk_eq_coe theorem
(l : List α) : Quot.mk _ l = (l : Cycle α)
Full source 
@[simp]
theorem mk_eq_coe (l : List α) : Quot.mk _ l = (l : Cycle α) :=
  rfl
Equivalence of Quotient Map and Coercion for Cycles
Informal description
For any list `l` of elements of type `α`, the equivalence class of `l` under the rotation relation is equal to the canonical image of `l` in the cycle type `Cycle α`. In other words, the quotient map `Quot.mk` applied to `l` is equal to the coercion of `l` to `Cycle α`.
Cycle.mk''_eq_coe theorem
(l : List α) : Quotient.mk'' l = (l : Cycle α)
Full source 
@[simp]
theorem mk''_eq_coe (l : List α) : Quotient.mk'' l = (l : Cycle α) :=
  rfl
Equivalence of Quotient Construction and Canonical Map for Cycles
Informal description
For any list $l$ of elements of type $\alpha$, the equivalence class of $l$ under the rotation relation is equal to the canonical image of $l$ in the cycle type, i.e., $\text{Quotient.mk''}(l) = (l : \text{Cycle } \alpha)$.
Cycle.coe_cons_eq_coe_append theorem
(l : List α) (a : α) : (↑(a :: l) : Cycle α) = (↑(l ++ [a]) : Cycle α)
Full source 
theorem coe_cons_eq_coe_append (l : List α) (a : α) :
    (↑(a :: l) : Cycle α) = (↑(l ++ [a]) : Cycle α) :=
  Quot.sound ⟨1, by rw [rotate_cons_succ, rotate_zero]⟩
Cycle equivalence of cons and append-singleton: $\overline{a :: l} = \overline{l ++ [a]}$
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the equivalence class of the list $a :: l$ in the cycle type `Cycle α` is equal to the equivalence class of the list $l ++ [a]$, i.e., $\overline{a :: l} = \overline{l ++ [a]}$ in $\text{Cycle}\,\alpha$.
Cycle.nil definition
: Cycle α
Full source 
/-- The unique empty cycle. -/
def nil : Cycle α :=
  ([] : List α)
Empty cycle
Informal description
The empty cycle, which is the equivalence class of the empty list in the quotient type `Cycle α`.
Cycle.coe_nil theorem
: ↑([] : List α) = @nil α
Full source 
@[simp]
theorem coe_nil : ↑([] : List α) = @nil α :=
  rfl
Empty List Yields Empty Cycle: $\overline{[]} = \text{nil}$
Informal description
The equivalence class of the empty list in the cycle type `Cycle α` is equal to the empty cycle, i.e., $\overline{[]} = \text{nil}$.
Cycle.coe_eq_nil theorem
(l : List α) : (l : Cycle α) = nil ↔ l = []
Full source 
@[simp]
theorem coe_eq_nil (l : List α) : (l : Cycle α) = nil ↔ l = [] :=
  coe_eq_coe.trans isRotated_nil_iff
Cycle Representation of Empty List is Nil iff List is Empty
Informal description
For any list $l$ of type $\alpha$, the image of $l$ under the canonical map to the cycle type $\text{Cycle}\,\alpha$ is equal to the empty cycle if and only if $l$ is the empty list, i.e., $(l : \text{Cycle}\,\alpha) = \text{nil} \leftrightarrow l = []$.
Cycle.instEmptyCollection instance
: EmptyCollection (Cycle α)
Full source 
/-- For consistency with `EmptyCollection (List α)`. -/
instance : EmptyCollection (Cycle α) :=
  ⟨nil⟩
Empty Cycle as Empty Collection
Informal description
The type `Cycle α` of cycles over a type `α` has an empty collection, which is the equivalence class of the empty list in the quotient construction of cycles.
Cycle.empty_eq theorem
: ∅ = @nil α
Full source 
@[simp]
theorem empty_eq : ∅ = @nil α :=
  rfl
Empty Collection Equals Nil Cycle
Informal description
The empty collection of cycles is equal to the empty cycle, i.e., $\varnothing = \text{nil}$.
Cycle.instInhabited instance
: Inhabited (Cycle α)
Full source 
instance : Inhabited (Cycle α) :=
  ⟨nil⟩
Inhabitedness of Cycle Type
Informal description
The type `Cycle α` of cycles over a type `α` is inhabited, with the empty cycle `nil` as a canonical inhabitant.
Cycle.induction_on theorem
{C : Cycle α → Prop} (s : Cycle α) (H0 : C nil) (HI : ∀ (a) (l : List α), C ↑l → C ↑(a :: l)) : C s
Full source 
/-- An induction principle for `Cycle`. Use as `induction s`. -/
@[elab_as_elim, induction_eliminator]
theorem induction_on {C : Cycle α → Prop} (s : Cycle α) (H0 : C nil)
    (HI : ∀ (a) (l : List α), C ↑l → C ↑(a :: l)) : C s :=
  Quotient.inductionOn' s fun l => by
    refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]
    assumption'
Induction Principle for Cycles
Informal description
Let $C$ be a predicate on cycles of type $\text{Cycle}\,\alpha$. To prove that $C(s)$ holds for every cycle $s$, it suffices to: 1. Show that $C$ holds for the empty cycle $\text{nil}$. 2. For any element $a \in \alpha$ and list $l \in \text{List}\,\alpha$, show that if $C$ holds for the cycle $\uparrow l$ (the cycle corresponding to $l$), then $C$ also holds for the cycle $\uparrow (a :: l)$ (the cycle corresponding to the list with $a$ prepended to $l$).
Cycle.Mem definition
(s : Cycle α) (a : α) : Prop
Full source 
/-- For `x : α`, `s : Cycle α`, `x ∈ s` indicates that `x` occurs at least once in `s`. -/
def Mem (s : Cycle α) (a : α) : Prop :=
  Quot.liftOn s (fun l => a ∈ l) fun _ _ e => propext <| e.mem_iff
Membership in a cycle
Informal description
For an element $x$ of type $\alpha$ and a cycle $s$ of type $\text{Cycle}\,\alpha$, the predicate $x \in s$ holds if $x$ appears at least once in the cycle $s$. This is defined by lifting the list membership relation through the quotient construction of $\text{Cycle}\,\alpha$, ensuring it respects the equivalence relation of cyclic permutation.
Cycle.instMembership instance
: Membership α (Cycle α)
Full source 
instance : Membership α (Cycle α) :=
  ⟨Mem⟩
Membership Relation for Cycles
Informal description
For any type $\alpha$, the type $\text{Cycle}\,\alpha$ of cycles (quotients of lists by cyclic permutation) has a membership relation $\in$ where $x \in s$ holds if $x$ appears in any representative list of the cycle $s$.
Cycle.mem_coe_iff theorem
{a : α} {l : List α} : a ∈ (↑l : Cycle α) ↔ a ∈ l
Full source 
@[simp]
theorem mem_coe_iff {a : α} {l : List α} : a ∈ (↑l : Cycle α)a ∈ (↑l : Cycle α) ↔ a ∈ l :=
  Iff.rfl
Membership in Lifted List Cycle
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\text{List}\,\alpha$, the element $a$ belongs to the cycle obtained from $l$ (denoted by $\uparrow l$) if and only if $a$ is an element of the list $l$. In other words, $a \in \uparrow l \leftrightarrow a \in l$.
Cycle.not_mem_nil theorem
(a : α) : a ∉ nil
Full source 
@[simp]
theorem not_mem_nil (a : α) : a ∉ nil :=
  List.not_mem_nil
No Element in Empty Cycle
Informal description
For any element $a$ of type $\alpha$, $a$ is not a member of the empty cycle $\text{nil}$.
Cycle.instDecidableMemOfDecidableEq instance
[DecidableEq α] (x : α) (s : Cycle α) : Decidable (x ∈ s)
Full source 
instance [DecidableEq α] (x : α) (s : Cycle α) : Decidable (x ∈ s) :=
  Quotient.recOnSubsingleton' s fun l => show Decidable (x ∈ l) from inferInstance
Decidability of Membership in Cycles
Informal description
For any type $\alpha$ with decidable equality, given an element $x \in \alpha$ and a cycle $s$ in $\text{Cycle}\,\alpha$, it is decidable whether $x$ is a member of $s$.
Cycle.reverse definition
(s : Cycle α) : Cycle α
Full source 
/-- Reverse a `s : Cycle α` by reversing the underlying `List`. -/
nonrec def reverse (s : Cycle α) : Cycle α :=
  Quot.map reverse (fun _ _ => IsRotated.reverse) s
Reversal of a cycle
Informal description
The function reverses a cycle \( s : \text{Cycle } \alpha \) by reversing its underlying list representation. This operation is well-defined since the rotation equivalence relation is preserved under list reversal.
Cycle.reverse_coe theorem
(l : List α) : (l : Cycle α).reverse = l.reverse
Full source 
@[simp]
theorem reverse_coe (l : List α) : (l : Cycle α).reverse = l.reverse :=
  rfl
Reversing a List Commutes with Cycle Formation: $\text{reverse}(c[l]) = c[\text{reverse}(l)]$
Informal description
For any list $l$ of type $\alpha$, the reverse of the cycle obtained from $l$ is equal to the cycle obtained from the reverse of $l$. In other words, $\text{reverse}(\text{ofList}(l)) = \text{ofList}(\text{reverse}(l))$.
Cycle.mem_reverse_iff theorem
{a : α} {s : Cycle α} : a ∈ s.reverse ↔ a ∈ s
Full source 
@[simp]
theorem mem_reverse_iff {a : α} {s : Cycle α} : a ∈ s.reversea ∈ s.reverse ↔ a ∈ s :=
  Quot.inductionOn s fun _ => mem_reverse
Membership in Reversed Cycle iff Membership in Original Cycle
Informal description
For any element $a$ of type $\alpha$ and any cycle $s$ of type $\text{Cycle}\,\alpha$, the element $a$ belongs to the reverse of $s$ if and only if $a$ belongs to $s$.
Cycle.reverse_reverse theorem
(s : Cycle α) : s.reverse.reverse = s
Full source 
@[simp]
theorem reverse_reverse (s : Cycle α) : s.reverse.reverse = s :=
  Quot.inductionOn s fun _ => by simp
Double Reversal of a Cycle is Identity
Informal description
For any cycle $s$ of type $\text{Cycle } \alpha$, reversing the cycle twice returns the original cycle, i.e., $(s^{\text{rev}})^{\text{rev}} = s$.
Cycle.reverse_nil theorem
: nil.reverse = @nil α
Full source 
@[simp]
theorem reverse_nil : nil.reverse = @nil α :=
  rfl
Reversing the Empty Cycle Yields the Empty Cycle
Informal description
The reverse of the empty cycle is equal to the empty cycle itself, i.e., $\text{reverse}(\text{nil}) = \text{nil}$.
Cycle.length definition
(s : Cycle α) : ℕ
Full source 
/-- The length of the `s : Cycle α`, which is the number of elements, counting duplicates. -/
def length (s : Cycle α) : ℕ :=
  Quot.liftOn s List.length fun _ _ e => e.perm.length_eq
Length of a cycle
Informal description
The function maps a cycle \( s \) of type `Cycle α` to its length, which is the number of elements in the cycle (counting duplicates). The length is invariant under rotation, meaning that rotating the cycle does not change its length.
Cycle.length_coe theorem
(l : List α) : length (l : Cycle α) = l.length
Full source 
@[simp]
theorem length_coe (l : List α) : length (l : Cycle α) = l.length :=
  rfl
Length Preservation under List-to-Cycle Canonical Map
Informal description
For any list $l$ of elements of type $\alpha$, the length of the cycle obtained by viewing $l$ as a cycle (via the canonical map `Cycle.ofList`) is equal to the length of the list $l$.
Cycle.length_nil theorem
: length (@nil α) = 0
Full source 
@[simp]
theorem length_nil : length (@nil α) = 0 :=
  rfl
Length of Empty Cycle is Zero
Informal description
The length of the empty cycle is zero, i.e., $\text{length}(\text{nil}) = 0$.
Cycle.length_reverse theorem
(s : Cycle α) : s.reverse.length = s.length
Full source 
@[simp]
theorem length_reverse (s : Cycle α) : s.reverse.length = s.length :=
  Quot.inductionOn s fun _ => List.length_reverse
Length Preservation under Cycle Reversal
Informal description
For any cycle $s$ of type $\text{Cycle } \alpha$, the length of the reversed cycle $s.\text{reverse}$ is equal to the length of $s$.
Cycle.Subsingleton definition
(s : Cycle α) : Prop
Full source 
/-- A `s : Cycle α` that is at most one element. -/
def Subsingleton (s : Cycle α) : Prop :=
  s.length ≤ 1
Subsingleton cycle
Informal description
A cycle \( s \) of type `Cycle α` is called *subsingleton* if its length is at most 1. In other words, \( s \) contains zero or one element.
Cycle.subsingleton_nil theorem
: Subsingleton (@nil α)
Full source 
theorem subsingleton_nil : Subsingleton (@nil α) := Nat.zero_le _
Empty cycle is subsingleton
Informal description
The empty cycle is a subsingleton cycle.
Cycle.length_subsingleton_iff theorem
{s : Cycle α} : Subsingleton s ↔ length s ≤ 1
Full source 
theorem length_subsingleton_iff {s : Cycle α} : SubsingletonSubsingleton s ↔ length s ≤ 1 :=
  Iff.rfl
Subsingleton Cycle Characterization via Length
Informal description
For any cycle $s$ of type $\text{Cycle} \alpha$, $s$ is a subsingleton (i.e., has at most one element) if and only if the length of $s$ is less than or equal to 1.
Cycle.subsingleton_reverse_iff theorem
{s : Cycle α} : s.reverse.Subsingleton ↔ s.Subsingleton
Full source 
@[simp]
theorem subsingleton_reverse_iff {s : Cycle α} : s.reverse.Subsingleton ↔ s.Subsingleton := by
  simp [length_subsingleton_iff]
Reversed Cycle is Subsingleton iff Original is Subsingleton
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, the reversed cycle $s.\text{reverse}$ is a subsingleton (i.e., has length at most 1) if and only if $s$ is a subsingleton.
Cycle.Subsingleton.congr theorem
{s : Cycle α} (h : Subsingleton s) : ∀ ⦃x⦄ (_hx : x ∈ s) ⦃y⦄ (_hy : y ∈ s), x = y
Full source 
theorem Subsingleton.congr {s : Cycle α} (h : Subsingleton s) :
    ∀ ⦃x⦄ (_hx : x ∈ s) ⦃y⦄ (_hy : y ∈ s), x = y := by
  induction' s using Quot.inductionOn with l
  simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
    length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h
  rcases h with (rfl | ⟨z, rfl⟩) <;> simp
Equality of Elements in a Subsingleton Cycle
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, if $s$ is a subsingleton (i.e., has length at most 1), then any two elements $x$ and $y$ in $s$ are equal. In other words, $x = y$ for all $x, y \in s$.
Cycle.Nontrivial definition
(s : Cycle α) : Prop
Full source 
/-- A `s : Cycle α` that is made up of at least two unique elements. -/
def Nontrivial (s : Cycle α) : Prop :=
  ∃ x y : α, x ≠ y ∧ x ∈ s ∧ y ∈ s
Nontrivial cycle
Informal description
A cycle $s : \text{Cycle}\,\alpha$ is called *nontrivial* if there exist two distinct elements $x$ and $y$ in $\alpha$ such that both $x$ and $y$ belong to $s$.
Cycle.nontrivial_coe_nodup_iff theorem
{l : List α} (hl : l.Nodup) : Nontrivial (l : Cycle α) ↔ 2 ≤ l.length
Full source 
@[simp]
theorem nontrivial_coe_nodup_iff {l : List α} (hl : l.Nodup) :
    NontrivialNontrivial (l : Cycle α) ↔ 2 ≤ l.length := by
  rw [Nontrivial]
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp
  · simp
  · simp only [mem_cons, exists_prop, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]
    refine ⟨hd, hd', ?_, by simp⟩
    simp only [not_or, mem_cons, nodup_cons] at hl
    exact hl.left.left
Nontrivial Cycle Condition for Duplicate-Free Lists: $\text{Nontrivial}([l]) \leftrightarrow 2 \leq \text{length}(l)$
Informal description
For any list $l$ of type $\alpha$ with no duplicate elements, the cycle formed from $l$ is nontrivial if and only if the length of $l$ is at least 2.
Cycle.nontrivial_reverse_iff theorem
{s : Cycle α} : s.reverse.Nontrivial ↔ s.Nontrivial
Full source 
@[simp]
theorem nontrivial_reverse_iff {s : Cycle α} : s.reverse.Nontrivial ↔ s.Nontrivial := by
  simp [Nontrivial]
Reversed Cycle Nontriviality: $s^{\text{reverse}}$ is nontrivial $\leftrightarrow$ $s$ is nontrivial
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, the reversed cycle $s^{\text{reverse}}$ is nontrivial if and only if $s$ is nontrivial.
Cycle.length_nontrivial theorem
{s : Cycle α} (h : Nontrivial s) : 2 ≤ length s
Full source 
theorem length_nontrivial {s : Cycle α} (h : Nontrivial s) : 2 ≤ length s := by
  obtain ⟨x, y, hxy, hx, hy⟩ := h
  induction' s using Quot.inductionOn with l
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp at hx
  · simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
    simp [hx, hy] at hxy
  · simp [Nat.succ_le_succ_iff]
Minimum Length of Nontrivial Cycles: $\text{length}(s) \geq 2$
Informal description
For any nontrivial cycle $s$ of type $\text{Cycle}\,\alpha$, the length of $s$ is at least 2.
Cycle.Nodup definition
(s : Cycle α) : Prop
Full source 
/-- The `s : Cycle α` contains no duplicates. -/
nonrec def Nodup (s : Cycle α) : Prop :=
  Quot.liftOn s Nodup fun _l₁ _l₂ e => propext <| e.nodup_iff
No duplicates in a cycle
Informal description
A cycle \( s : \text{Cycle } \alpha \) is said to be nodup (no duplicates) if its underlying list representation contains no duplicate elements. This property is well-defined under the rotation equivalence relation on lists.
Cycle.nodup_nil theorem
: Nodup (@nil α)
Full source 
@[simp]
nonrec theorem nodup_nil : Nodup (@nil α) :=
  nodup_nil
Empty Cycle Has No Duplicates
Informal description
The empty cycle has no duplicate elements, i.e., $\text{Nodup}(\text{nil})$.
Cycle.nodup_coe_iff theorem
{l : List α} : Nodup (l : Cycle α) ↔ l.Nodup
Full source 
@[simp]
theorem nodup_coe_iff {l : List α} : NodupNodup (l : Cycle α) ↔ l.Nodup :=
  Iff.rfl
Cycle Nodup Equivalence: $l$ is nodup as a cycle iff $l$ is nodup as a list
Informal description
For any list $l$ of elements of type $\alpha$, the cycle obtained from $l$ (denoted as $l : \text{Cycle } \alpha$) has no duplicates if and only if the original list $l$ has no duplicates.
Cycle.nodup_reverse_iff theorem
{s : Cycle α} : s.reverse.Nodup ↔ s.Nodup
Full source 
@[simp]
theorem nodup_reverse_iff {s : Cycle α} : s.reverse.Nodup ↔ s.Nodup :=
  Quot.inductionOn s fun _ => nodup_reverse
Reversed Cycle Has No Duplicates iff Original Cycle Has No Duplicates
Informal description
For any cycle $s$ of type $\text{Cycle } \alpha$, the reversed cycle $s.\text{reverse}$ has no duplicates if and only if the original cycle $s$ has no duplicates.
Cycle.Subsingleton.nodup theorem
{s : Cycle α} (h : Subsingleton s) : Nodup s
Full source 
theorem Subsingleton.nodup {s : Cycle α} (h : Subsingleton s) : Nodup s := by
  induction' s using Quot.inductionOn with l
  obtain - | ⟨hd, tl⟩ := l
  · simp
  · have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
    simp [this]
Subsingleton Cycles Have No Duplicates
Informal description
For any cycle $s$ of type $\text{Cycle } \alpha$, if $s$ is a subsingleton (i.e., has length at most 1), then $s$ has no duplicate elements.
Cycle.Nodup.nontrivial_iff theorem
{s : Cycle α} (h : Nodup s) : Nontrivial s ↔ ¬Subsingleton s
Full source 
theorem Nodup.nontrivial_iff {s : Cycle α} (h : Nodup s) : NontrivialNontrivial s ↔ ¬Subsingleton s := by
  rw [length_subsingleton_iff]
  induction s using Quotient.inductionOn'
  simp only [mk''_eq_coe, nodup_coe_iff] at h
  simp [h, Nat.succ_le_iff]
Nontriviality of Duplicate-Free Cycles via Non-Subsingleton Condition
Informal description
For a cycle $s$ of type $\text{Cycle}\,\alpha$ with no duplicate elements, $s$ is nontrivial (contains at least two distinct elements) if and only if $s$ is not a subsingleton (i.e., its length is greater than 1).
Cycle.toMultiset definition
(s : Cycle α) : Multiset α
Full source 
/-- The `s : Cycle α` as a `Multiset α`.
-/
def toMultiset (s : Cycle α) : Multiset α :=
  Quotient.liftOn' s (↑) fun _ _ h => Multiset.coe_eq_coe.mpr h.perm
Multiset representation of a cycle
Informal description
The function maps a cycle `s : Cycle α` to its underlying multiset, obtained by lifting the canonical embedding of lists into multisets to the quotient of lists by rotation equivalence. Specifically, for any cycle `s`, the multiset `toMultiset s` is the multiset corresponding to any representative list of `s`, with the guarantee that the result is independent of the choice of representative due to the rotation equivalence relation.
Cycle.coe_toMultiset theorem
(l : List α) : (l : Cycle α).toMultiset = l
Full source 
@[simp]
theorem coe_toMultiset (l : List α) : (l : Cycle α).toMultiset = l :=
  rfl
Multiset Preservation in List-to-Cycle Canonical Map
Informal description
For any list $l$ of elements of type $\alpha$, the multiset representation of the cycle obtained from $l$ is equal to $l$ itself as a multiset. In other words, the canonical map from lists to cycles preserves the multiset structure.
Cycle.nil_toMultiset theorem
: nil.toMultiset = (0 : Multiset α)
Full source 
@[simp]
theorem nil_toMultiset : nil.toMultiset = (0 : Multiset α) :=
  rfl
Empty Cycle Maps to Empty Multiset
Informal description
The multiset representation of the empty cycle is equal to the empty multiset, i.e., $\text{toMultiset}(\text{nil}) = 0$.
Cycle.card_toMultiset theorem
(s : Cycle α) : Multiset.card s.toMultiset = s.length
Full source 
@[simp]
theorem card_toMultiset (s : Cycle α) : Multiset.card s.toMultiset = s.length :=
  Quotient.inductionOn' s (by simp)
Cardinality of Cycle's Multiset Equals Cycle Length
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, the cardinality of its underlying multiset $\text{toMultiset}\,s$ is equal to the length of the cycle $s$.
Cycle.toMultiset_eq_nil theorem
{s : Cycle α} : s.toMultiset = 0 ↔ s = Cycle.nil
Full source 
@[simp]
theorem toMultiset_eq_nil {s : Cycle α} : s.toMultiset = 0 ↔ s = Cycle.nil :=
  Quotient.inductionOn' s (by simp)
Empty Cycle Characterization via Multiset
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, the underlying multiset $\text{toMultiset}\,s$ is equal to the empty multiset $0$ if and only if $s$ is the empty cycle $\text{nil}$.
Cycle.map definition
{β : Type*} (f : α → β) : Cycle α → Cycle β
Full source 
/-- The lift of `list.map`. -/
def map {β : Type*} (f : α → β) : Cycle α → Cycle β :=
  Quotient.map' (List.map f) fun _ _ h => h.map _
Mapping of cycles under a function
Informal description
The function `Cycle.map` lifts a function $f : \alpha \to \beta$ to a function between cycles of type $\alpha$ and cycles of type $\beta$. Specifically, given a cycle represented as a quotient of lists under rotation equivalence, applying `Cycle.map f` to it yields the cycle obtained by applying $f$ to each element of the underlying lists, preserving the rotation equivalence relation.
Cycle.map_nil theorem
{β : Type*} (f : α → β) : map f nil = nil
Full source 
@[simp]
theorem map_nil {β : Type*} (f : α → β) : map f nil = nil :=
  rfl
Mapping Preserves the Empty Cycle
Informal description
For any function $f : \alpha \to \beta$, the image of the empty cycle under the mapping function `Cycle.map f` is the empty cycle, i.e., $\text{map}\, f\, \text{nil} = \text{nil}$.
Cycle.map_coe theorem
{β : Type*} (f : α → β) (l : List α) : map f ↑l = List.map f l
Full source 
@[simp]
theorem map_coe {β : Type*} (f : α → β) (l : List α) : map f ↑l = List.map f l :=
  rfl
Mapping Function Commutes with Cycle Formation
Informal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the image of the cycle $\overline{l}$ (the equivalence class of $l$ under rotation) under the map $f$ is equal to the cycle obtained from the mapped list $f(l)$, i.e., $f(\overline{l}) = \overline{f(l)}$.
Cycle.map_eq_nil theorem
{β : Type*} (f : α → β) (s : Cycle α) : map f s = nil ↔ s = nil
Full source 
@[simp]
theorem map_eq_nil {β : Type*} (f : α → β) (s : Cycle α) : mapmap f s = nil ↔ s = nil :=
  Quotient.inductionOn' s (by simp)
Empty Cycle Preservation under Mapping
Informal description
For any function $f : \alpha \to \beta$ and any cycle $s$ of type $\alpha$, the image of $s$ under $f$ is the empty cycle if and only if $s$ itself is the empty cycle. In other words, $f(s) = \text{nil} \leftrightarrow s = \text{nil}$.
Cycle.mem_map theorem
{β : Type*} {f : α → β} {b : β} {s : Cycle α} : b ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b
Full source 
@[simp]
theorem mem_map {β : Type*} {f : α → β} {b : β} {s : Cycle α} :
    b ∈ s.map fb ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b :=
  Quotient.inductionOn' s (by simp)
Membership in Mapped Cycle: $b \in f(s) \leftrightarrow \exists a \in s, f(a) = b$
Informal description
For any function $f : \alpha \to \beta$, element $b \in \beta$, and cycle $s$ of type $\text{Cycle}\,\alpha$, the element $b$ belongs to the image cycle $\text{map}\,f\,s$ if and only if there exists an element $a \in \alpha$ such that $a$ belongs to $s$ and $f(a) = b$. In symbols: $$ b \in \text{map}\,f\,s \leftrightarrow \exists a \in s, f(a) = b $$
Cycle.lists definition
(s : Cycle α) : Multiset (List α)
Full source 
/-- The `Multiset` of lists that can make the cycle. -/
def lists (s : Cycle α) : Multiset (List α) :=
  Quotient.liftOn' s (fun l => (l.cyclicPermutations : Multiset (List α))) fun l₁ l₂ h => by
    simpa using h.cyclicPermutations.perm
Multiset of cyclic permutations for a cycle
Informal description
For a cycle `s : Cycle α`, the function `Cycle.lists` returns the multiset of all lists that are cyclic permutations of any representative of `s`. More precisely, given a cycle `s` (which is an equivalence class of lists under rotation), `Cycle.lists s` is the multiset obtained by taking any representative list `l` of `s` and collecting all its cyclic permutations. The result is independent of the choice of representative due to the properties of the quotient construction.
Cycle.lists_coe theorem
(l : List α) : lists (l : Cycle α) = ↑l.cyclicPermutations
Full source 
@[simp]
theorem lists_coe (l : List α) : lists (l : Cycle α) = ↑l.cyclicPermutations :=
  rfl
Equality of Cyclic Permutation Multisets for a List and its Cycle
Informal description
For any list `l` of elements of type `α`, the multiset of cyclic permutations of the cycle obtained from `l` (via the canonical map `Cycle.ofList`) is equal to the multiset obtained by lifting the list of all cyclic permutations of `l` to a multiset. In other words, the multiset `lists (ofList l)` is equal to the multiset `↑(cyclicPermutations l)`.
Cycle.mem_lists_iff_coe_eq theorem
{s : Cycle α} {l : List α} : l ∈ s.lists ↔ (l : Cycle α) = s
Full source 
@[simp]
theorem mem_lists_iff_coe_eq {s : Cycle α} {l : List α} : l ∈ s.listsl ∈ s.lists ↔ (l : Cycle α) = s :=
  Quotient.inductionOn' s fun l => by
    rw [lists, Quotient.liftOn'_mk'']
    simp
Equivalence of List Membership in Cycle's Permutations and Cycle Equality
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ and any list $l$ of type $\text{List}\,\alpha$, the list $l$ is in the multiset of cyclic permutations of $s$ if and only if the equivalence class of $l$ under rotation is equal to $s$. In other words, $l \in \text{lists}(s) \leftrightarrow [l] = s$, where $[l]$ denotes the equivalence class of $l$ in $\text{Cycle}\,\alpha$.
Cycle.decidableNontrivialCoe definition
: ∀ l : List α, Decidable (Nontrivial (l : Cycle α))
Full source 
/-- Auxiliary decidability algorithm for lists that contain at least two unique elements.
-/
def decidableNontrivialCoe : ∀ l : List α, Decidable (Nontrivial (l : Cycle α))
  | [] => isFalse (by simp [Nontrivial])
  | [x] => isFalse (by simp [Nontrivial])
  | x :: y :: l =>
    if h : x = y then
      @decidable_of_iff' _ (Nontrivial (x :: l : Cycle α)) (by simp [h, Nontrivial])
        (decidableNontrivialCoe (x :: l))
    else isTrue ⟨x, y, h, by simp, by simp⟩
Decidability of nontrivial cycles from lists
Informal description
For any list $l$ of type $\alpha$, it is decidable whether the corresponding cycle $[l]$ is nontrivial, i.e., contains at least two distinct elements. The decision is made as follows: - The empty list and singleton lists are trivially not nontrivial. - For a list with at least two elements, if the first two elements are distinct, the cycle is nontrivial. Otherwise, the decision reduces to checking the rest of the list.
Cycle.instDecidableNontrivial instance
{s : Cycle α} : Decidable (Nontrivial s)
Full source 
instance {s : Cycle α} : Decidable (Nontrivial s) :=
  Quot.recOnSubsingleton s decidableNontrivialCoe
Decidability of Nontrivial Cycles
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, it is decidable whether $s$ is nontrivial, meaning it contains at least two distinct elements.
Cycle.instDecidableNodup instance
{s : Cycle α} : Decidable (Nodup s)
Full source 
instance {s : Cycle α} : Decidable (Nodup s) :=
  Quot.recOnSubsingleton s List.nodupDecidable
Decidability of No Duplicates in Cycles
Informal description
For any cycle $s$ of type $\text{Cycle } \alpha$, it is decidable whether $s$ has no duplicate elements.
Cycle.fintypeNodupCycle instance
[Fintype α] : Fintype { s : Cycle α // s.Nodup }
Full source 
instance fintypeNodupCycle [Fintype α] : Fintype { s : Cycle α // s.Nodup } :=
  Fintype.ofSurjective (fun l : { l : List α // l.Nodup } => ⟨l.val, by simpa using l.prop⟩)
    fun ⟨s, hs⟩ => by
    induction' s using Quotient.inductionOn' with s hs
    exact ⟨⟨s, hs⟩, by simp⟩
Finiteness of Nodup Cycles on Finite Types
Informal description
For any finite type $\alpha$, the set of nodup cycles (cycles without duplicate elements) in $\text{Cycle } \alpha$ is finite.
Cycle.fintypeNodupNontrivialCycle instance
[Fintype α] : Fintype { s : Cycle α // s.Nodup ∧ s.Nontrivial }
Full source 
instance fintypeNodupNontrivialCycle [Fintype α] :
    Fintype { s : Cycle α // s.Nodup ∧ s.Nontrivial } :=
  Fintype.subtype
    (((Finset.univ : Finset { s : Cycle α // s.Nodup }).map (Function.Embedding.subtype _)).filter
      Cycle.Nontrivial)
    (by simp)
Finiteness of Nodup and Nontrivial Cycles on Finite Types
Informal description
For any finite type $\alpha$, the set of nodup and nontrivial cycles in $\text{Cycle } \alpha$ is finite.
Cycle.toFinset definition
(s : Cycle α) : Finset α
Full source 
/-- The `s : Cycle α` as a `Finset α`. -/
def toFinset (s : Cycle α) : Finset α :=
  s.toMultiset.toFinset
Finite set representation of a cycle
Informal description
The function maps a cycle `s : Cycle α` to its underlying finite set, obtained by converting the multiset representation of the cycle to a finite set. This ensures that duplicate elements in the cycle are collapsed into a single element in the finite set.
Cycle.toFinset_toMultiset theorem
(s : Cycle α) : s.toMultiset.toFinset = s.toFinset
Full source 
@[simp]
theorem toFinset_toMultiset (s : Cycle α) : s.toMultiset.toFinset = s.toFinset :=
  rfl
Equality of Finite Set Representations from Multiset and Cycle
Informal description
For any cycle $s$ of type $\text{Cycle}~\alpha$, the finite set obtained from the multiset representation of $s$ is equal to the finite set representation of $s$ itself. That is, $\text{toFinset}(\text{toMultiset}(s)) = \text{toFinset}(s)$.
Cycle.coe_toFinset theorem
(l : List α) : (l : Cycle α).toFinset = l.toFinset
Full source 
@[simp]
theorem coe_toFinset (l : List α) : (l : Cycle α).toFinset = l.toFinset :=
  rfl
Preservation of Finite Sets under List-to-Cycle Conversion
Informal description
For any list $l$ of elements of type $\alpha$, the finite set associated with the cycle obtained from $l$ is equal to the finite set associated with $l$ itself. In other words, the canonical map from lists to cycles preserves the underlying finite set structure.
Cycle.nil_toFinset theorem
: (@nil α).toFinset = ∅
Full source 
@[simp]
theorem nil_toFinset : (@nil α).toFinset = ∅ :=
  rfl
Empty Cycle Yields Empty Finite Set
Informal description
The finite set representation of the empty cycle is the empty set, i.e., $\text{toFinset}(\text{nil}) = \emptyset$.
Cycle.toFinset_eq_nil theorem
{s : Cycle α} : s.toFinset = ∅ ↔ s = Cycle.nil
Full source 
@[simp]
theorem toFinset_eq_nil {s : Cycle α} : s.toFinset = ∅ ↔ s = Cycle.nil :=
  Quotient.inductionOn' s (by simp)
Empty Cycle Characterization via Finite Set Representation
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$, the finite set representation of $s$ is empty if and only if $s$ is the empty cycle.
Cycle.next definition
: ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α
Full source 
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the next element after `x ∈ s`. -/
nonrec def next : ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α := fun s =>
  Quot.hrecOn (motive := fun (s : Cycle α) => ∀ (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s), α) s
  (fun l _hn x hx => next l x hx) fun l₁ l₂ h =>
    Function.hfunext (propext h.nodup_iff) fun h₁ h₂ _he =>
      Function.hfunext rfl fun x y hxy =>
        Function.hfunext (propext (by rw [eq_of_heq hxy]; simpa [eq_of_heq hxy] using h.mem_iff))
  fun hm hm' he' => heq_of_eq
    (by rw [heq_iff_eq] at hxy; subst x; simpa using isRotated_next_eq h h₁ _)
Next element in a cycle with no duplicates
Informal description
Given a cycle \( s \) of type \( \text{Cycle } \alpha \) with no duplicate elements (i.e., \( \text{Nodup } s \)) and an element \( x \in s \), the function returns the next element after \( x \) in the cycle \( s \). More precisely, if \( s \) is represented by a list \( l \) (up to rotation), then the result is the element that immediately follows \( x \) in \( l \), wrapping around to the first element if \( x \) is the last element of \( l \).
Cycle.prev definition
: ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α
Full source 
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the previous element before `x ∈ s`. -/
nonrec def prev : ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α := fun s =>
  Quot.hrecOn (motive := fun (s : Cycle α) => ∀ (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s), α) s
  (fun l _hn x hx => prev l x hx) fun l₁ l₂ h =>
    Function.hfunext (propext h.nodup_iff) fun h₁ h₂ _he =>
      Function.hfunext rfl fun x y hxy =>
        Function.hfunext (propext (by rw [eq_of_heq hxy]; simpa [eq_of_heq hxy] using h.mem_iff))
  fun hm hm' he' => heq_of_eq
    (by rw [heq_iff_eq] at hxy; subst x; simpa using isRotated_prev_eq h h₁ _)
Previous element in a cycle with no duplicates
Informal description
Given a cycle \( s : \text{Cycle } \alpha \) with no duplicate elements and an element \( x \in s \), the function returns the previous element of \( x \) in the cycle \( s \). The cycle is considered as a cyclic list, so the previous element of the first element is the last element of the cycle.
Cycle.prev_reverse_eq_next theorem
(s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s), s.reverse.prev (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.next hs x hx
Full source 
nonrec theorem prev_reverse_eq_next (s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s),
    s.reverse.prev (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.next hs x hx :=
  Quotient.inductionOn' s prev_reverse_eq_next
Previous in Reversed Cycle Equals Next in Original Cycle for Distinct Elements
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ with no duplicate elements, and for any element $x \in s$, the previous element of $x$ in the reversed cycle $s^{\text{rev}}$ equals the next element of $x$ in the original cycle $s$. In symbols: $$\text{prev}(s^{\text{rev}}, x) = \text{next}(s, x)$$
Cycle.prev_reverse_eq_next' theorem
(s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) : s.reverse.prev hs x hx = s.next (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)
Full source 
@[simp]
nonrec theorem prev_reverse_eq_next' (s : Cycle α) (hs : Nodup s.reverse) (x : α)
    (hx : x ∈ s.reverse) :
    s.reverse.prev hs x hx = s.next (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx) :=
  prev_reverse_eq_next s (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)
Previous in Reversed Cycle Equals Next in Original Cycle (Variant)
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ such that its reverse $s^{\text{rev}}$ has no duplicate elements, and for any element $x \in s^{\text{rev}}$, the previous element of $x$ in $s^{\text{rev}}$ equals the next element of $x$ in the original cycle $s$. In symbols: $$\text{prev}(s^{\text{rev}}, x) = \text{next}(s, x)$$
Cycle.next_reverse_eq_prev theorem
(s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.reverse.next (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.prev hs x hx
Full source 
theorem next_reverse_eq_prev (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) :
    s.reverse.next (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.prev hs x hx := by
  simp [← prev_reverse_eq_next]
Next in Reversed Cycle Equals Previous in Original Cycle
Informal description
Let $s$ be a cycle of type $\text{Cycle}\,\alpha$ with no duplicate elements, and let $x$ be an element of $s$. Then the next element of $x$ in the reversed cycle $s^{\text{rev}}$ is equal to the previous element of $x$ in the original cycle $s$. More precisely, if $s$ is nodup (has no duplicates) and $x \in s$, then: $$ s^{\text{rev}}.\text{next}\,(\text{nodup\_reverse\_iff.mpr}\,hs)\,x\,(\text{mem\_reverse\_iff.mpr}\,hx) = s.\text{prev}\,hs\,x\,hx $$
Cycle.next_reverse_eq_prev' theorem
(s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) : s.reverse.next hs x hx = s.prev (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)
Full source 
@[simp]
theorem next_reverse_eq_prev' (s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) :
    s.reverse.next hs x hx = s.prev (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx) := by
  simp [← prev_reverse_eq_next]
Next in Reversed Cycle Equals Previous in Original Cycle
Informal description
Let $s$ be a cycle of elements of type $\alpha$ such that the reversed cycle $s^{\text{rev}}$ has no duplicate elements. For any element $x \in s^{\text{rev}}$, the next element of $x$ in $s^{\text{rev}}$ is equal to the previous element of $x$ in the original cycle $s$. More precisely, if $s^{\text{rev}}$ is nodup and $x$ is in $s^{\text{rev}}$, then: $$ s^{\text{rev}}.\text{next}\,hs\,x\,hx = s.\text{prev}\,(hs')\,x\,(hx') $$ where $hs'$ is the proof that $s$ is nodup (obtained from $hs$ via `nodup_reverse_iff.mp`) and $hx'$ is the proof that $x \in s$ (obtained from $hx$ via `mem_reverse_iff.mp`).
Cycle.next_mem theorem
(s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.next hs x hx ∈ s
Full source 
@[simp]
nonrec theorem next_mem (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.next hs x hx ∈ s := by
  induction s using Quot.inductionOn
  apply next_mem; assumption
Membership preservation of next element in a duplicate-free cycle
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ with no duplicate elements and any element $x \in s$, the next element after $x$ in $s$ (denoted $s.\text{next}\,hs\,x\,hx$) is also an element of $s$.
Cycle.prev_mem theorem
(s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.prev hs x hx ∈ s
Full source 
theorem prev_mem (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.prev hs x hx ∈ s := by
  rw [← next_reverse_eq_prev, ← mem_reverse_iff]
  apply next_mem
Membership preservation of previous element in a duplicate-free cycle
Informal description
For any cycle $s$ of elements of type $\alpha$ with no duplicate elements, and for any element $x \in s$, the previous element of $x$ in $s$ (denoted $s.\text{prev}\,hs\,x\,hx$) is also an element of $s$.
Cycle.prev_next theorem
(s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s), s.prev hs (s.next hs x hx) (next_mem s hs x hx) = x
Full source 
@[simp]
nonrec theorem prev_next (s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s),
    s.prev hs (s.next hs x hx) (next_mem s hs x hx) = x :=
  Quotient.inductionOn' s prev_next
Cycle Property: $\text{prev} \circ \text{next} = \text{id}$ on Duplicate-Free Cycles
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ with no duplicate elements, and for any element $x \in s$, the previous element of the next element of $x$ in $s$ is equal to $x$ itself. That is, $s.\text{prev}(s.\text{next}(x)) = x$. Here: - $s.\text{next}(x)$ denotes the element immediately following $x$ in the cycle $s$ - $s.\text{prev}(y)$ denotes the element immediately preceding $y$ in the cycle $s$ - The cycle $s$ is assumed to have no duplicate elements ($\text{Nodup}\, s$)
Cycle.next_prev theorem
(s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s), s.next hs (s.prev hs x hx) (prev_mem s hs x hx) = x
Full source 
@[simp]
nonrec theorem next_prev (s : Cycle α) : ∀ (hs : Nodup s) (x : α) (hx : x ∈ s),
    s.next hs (s.prev hs x hx) (prev_mem s hs x hx) = x :=
  Quotient.inductionOn' s next_prev
Cycle Property: $\text{next} \circ \text{prev} = \text{id}$ on Duplicate-Free Cycles
Informal description
For any cycle $s$ of elements of type $\alpha$ with no duplicate elements, and for any element $x \in s$, the next element of the previous element of $x$ in $s$ is equal to $x$ itself. That is, $s.\text{next}(s.\text{prev}(x)) = x$. Here: - $s.\text{prev}(x)$ denotes the element immediately preceding $x$ in the cycle $s$ - $s.\text{next}(y)$ denotes the element immediately following $y$ in the cycle $s$ - The cycle $s$ is assumed to have no duplicate elements ($\text{Nodup}\, s$)
Cycle.instRepr instance
[Repr α] : Repr (Cycle α)
Full source 
/-- We define a representation of concrete cycles, available when viewing them in a goal state or
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.
-/
unsafe instance [Repr α] : Repr (Cycle α) :=
  ⟨fun s _ => "c[" ++ Std.Format.joinSep (s.map repr).lists.unquot.head! ", " ++ "]"⟩
Representation of Cycles
Informal description
For any type $\alpha$ with a representation, the type $\text{Cycle}\,\alpha$ of cycles (quotient of lists by rotation) has a canonical representation. This representation displays cycles in a readable format, such as `c[2, 1, 4, 3]` for the cycle $(2\,1\,4\,3)$. Note that two equal cycles may be displayed differently if their internal representations differ.
Cycle.Chain definition
(r : α → α → Prop) (c : Cycle α) : Prop
Full source 
/-- `chain R s` means that `R` holds between adjacent elements of `s`.

`chain R ([a, b, c] : Cycle α) ↔ R a b ∧ R b c ∧ R c a` -/
nonrec def Chain (r : α → α → Prop) (c : Cycle α) : Prop :=
  Quotient.liftOn' c
    (fun l =>
      match l with
      | [] => True
      | a :: m => Chain r a (m ++ [a]))
    fun a b hab =>
    propext <| by
      rcases a with - | ⟨a, l⟩ <;> rcases b with - | ⟨b, m⟩
      · rfl
      · have := isRotated_nil_iff'.1 hab
        contradiction
      · have := isRotated_nil_iff.1 hab
        contradiction
      · dsimp only
        obtain ⟨n, hn⟩ := hab
        induction' n with d hd generalizing a b l m
        · simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        · rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]
Chain relation on cycles
Informal description
Given a binary relation $r$ on a type $\alpha$ and a cycle $c$ of type $\text{Cycle} \alpha$, the predicate $\text{Chain} \, r \, c$ holds if for every adjacent pair of elements $(a, b)$ in the cycle $c$, the relation $r(a, b)$ is satisfied. For the empty cycle, the predicate is trivially true. For a non-empty cycle represented by a list $a :: l$, the predicate holds if the relation $r$ holds between every consecutive pair in the list $l ++ [a]$, forming a closed chain. More formally: - For the empty cycle $[]$, $\text{Chain} \, r \, []$ is always true. - For a cycle represented by a non-empty list $a :: l$, $\text{Chain} \, r \, (a :: l)$ is equivalent to $\text{List.Chain} \, r \, a \, (l ++ [a])$, where $\text{List.Chain}$ checks that $r$ holds between every consecutive pair in the list $l ++ [a]$.
Cycle.Chain.nil theorem
(r : α → α → Prop) : Cycle.Chain r (@nil α)
Full source 
@[simp]
theorem Chain.nil (r : α → α → Prop) : Cycle.Chain r (@nil α) := by trivial
Empty Cycle Satisfies Any Chain Relation
Informal description
For any binary relation $r$ on a type $\alpha$, the empty cycle satisfies the chain relation $\text{Chain}\,r\,[]$.
Cycle.chain_coe_cons theorem
(r : α → α → Prop) (a : α) (l : List α) : Chain r (a :: l) ↔ List.Chain r a (l ++ [a])
Full source 
@[simp]
theorem chain_coe_cons (r : α → α → Prop) (a : α) (l : List α) :
    ChainChain r (a :: l) ↔ List.Chain r a (l ++ [a]) :=
  Iff.rfl
Chain Relation for Cycle Construction via List Concatenation
Informal description
For any binary relation $r$ on a type $\alpha$, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the cycle formed by $a$ followed by $l$ satisfies the chain relation $\text{Chain} \, r \, (a :: l)$ if and only if the list $l$ concatenated with $[a]$ satisfies the chain relation $\text{List.Chain} \, r \, a \, (l ++ [a])$.
Cycle.chain_singleton theorem
(r : α → α → Prop) (a : α) : Chain r [a] ↔ r a a
Full source 
theorem chain_singleton (r : α → α → Prop) (a : α) : ChainChain r [a] ↔ r a a := by
  rw [chain_coe_cons, nil_append, List.chain_singleton]
Chain Relation for Singleton Cycle: $\text{Chain} \, r \, [a] \leftrightarrow r(a, a)$
Informal description
For any binary relation $r$ on a type $\alpha$ and any element $a \in \alpha$, the cycle consisting of the single element $a$ satisfies the chain relation $\text{Chain} \, r \, [a]$ if and only if the relation $r(a, a)$ holds.
Cycle.chain_ne_nil theorem
(r : α → α → Prop) {l : List α} : ∀ hl : l ≠ [], Chain r l ↔ List.Chain r (getLast l hl) l
Full source 
theorem chain_ne_nil (r : α → α → Prop) {l : List α} :
    ∀ hl : l ≠ [], ChainChain r l ↔ List.Chain r (getLast l hl) l :=
  l.reverseRecOn (fun hm => hm.irrefl.elim) (by
    intro m a _H _
    rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton])
Chain Relation for Non-Empty Cycles via Last Element
Informal description
For any binary relation $r$ on a type $\alpha$ and any non-empty list $l$ of elements of $\alpha$, the cycle formed by $l$ satisfies the chain relation $\text{Chain}\, r\, l$ if and only if the list $l$ satisfies the chain relation $\text{List.Chain}\, r\, (\text{getLast}\, l\, hl)\, l$, where $\text{getLast}\, l\, hl$ is the last element of $l$ (with proof $hl$ that $l$ is non-empty).
Cycle.chain_map theorem
{β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} : Chain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s
Full source 
theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} :
    ChainChain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s :=
  Quotient.inductionOn s fun l => by
    rcases l with - | ⟨a, l⟩
    · rfl
    · simp [← concat_eq_append, ← List.map_concat, List.chain_map f]
Chain Relation Preservation under Cycle Mapping
Informal description
For any binary relation $r$ on a type $\alpha$, any function $f : \beta \to \alpha$, and any cycle $s$ of type $\text{Cycle} \beta$, the following equivalence holds: the cycle $\text{map} \, f \, s$ satisfies the chain relation $\text{Chain} \, r$ if and only if the original cycle $s$ satisfies the chain relation $\text{Chain} \, (r \circ f)$, where $(r \circ f)(a, b) = r(f(a), f(b))$. In other words, $\text{Chain} \, r \, (\text{map} \, f \, s) \leftrightarrow \text{Chain} \, (r \circ f) \, s$.
Cycle.chain_range_succ theorem
(r : ℕ → ℕ → Prop) (n : ℕ) : Chain r (List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Full source 
nonrec theorem chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
    ChainChain r (List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ := by
  rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, chain_range_succ]
Chain condition for the cycle $[0, \dots, n]$: $r(n,0) \land (\forall m < n, r(m, m+1))$
Informal description
For any binary relation $r$ on the natural numbers and any natural number $n$, the cycle formed by the list $[0, 1, \dots, n]$ satisfies the chain relation $\text{Chain}\, r$ if and only if: 1. $r(n, 0)$ holds, and 2. For every natural number $m < n$, the relation $r(m, m+1)$ holds.
Cycle.Chain.imp theorem
{r₁ r₂ : α → α → Prop} (H : ∀ a b, r₁ a b → r₂ a b) (p : Chain r₁ s) : Chain r₂ s
Full source 
theorem Chain.imp {r₁ r₂ : α → α → Prop} (H : ∀ a b, r₁ a b → r₂ a b) (p : Chain r₁ s) :
    Chain r₂ s := by
  induction s
  · trivial
  · rw [chain_coe_cons] at p ⊢
    exact p.imp H
Chain Relation Implication for Cycles
Informal description
For any binary relations $r_1$ and $r_2$ on a type $\alpha$, if $r_1$ implies $r_2$ (i.e., $r_1(a, b) \to r_2(a, b)$ for all $a, b \in \alpha$), then for any cycle $s$ in $\text{Cycle}\,\alpha$, if $s$ satisfies the chain relation $\text{Chain}\,r_1$, then it also satisfies $\text{Chain}\,r_2$.
Cycle.chain_mono theorem
: Monotone (Chain : (α → α → Prop) → Cycle α → Prop)
Full source 
/-- As a function from a relation to a predicate, `chain` is monotonic. -/
theorem chain_mono : Monotone (Chain : (α → α → Prop) → Cycle α → Prop) := fun _a _b hab _s =>
  Chain.imp hab
Monotonicity of the Chain Relation on Cycles
Informal description
The function $\text{Chain} : (\alpha \to \alpha \to \text{Prop}) \to \text{Cycle} \alpha \to \text{Prop}$ is monotonic with respect to the implication order on relations. That is, if $r_1 \leq r_2$ (meaning $r_1(a,b) \to r_2(a,b)$ for all $a, b \in \alpha$), then for any cycle $c \in \text{Cycle} \alpha$, $\text{Chain}\,r_1\,c$ implies $\text{Chain}\,r_2\,c$.
Cycle.chain_of_pairwise theorem
: (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s
Full source 
theorem chain_of_pairwise : (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s := by
  induction' s with a l _
  · exact fun _ => Cycle.Chain.nil r
  intro hs
  have Ha : a ∈ (a :: l : Cycle α) := by simp
  have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
  rw [Cycle.chain_coe_cons]
  apply Pairwise.chain
  rw [pairwise_cons]
  refine
    ⟨fun b hb => ?_,
      pairwise_append.2
        ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc),
          pairwise_singleton r a, fun b hb c hc => ?_⟩⟩
  · rw [mem_append] at hb
    rcases hb with hb | hb
    · exact hs a Ha b (Hl hb)
    · rw [mem_singleton] at hb
      rw [hb]
      exact hs a Ha a Ha
  · rw [mem_singleton] at hc
    rw [hc]
    exact hs b (Hl hb) a Ha
Pairwise Relation Implies Chain Relation on Cycles
Informal description
For any cycle $s$ of type $\text{Cycle}\,\alpha$ and any binary relation $r$ on $\alpha$, if for all elements $a$ and $b$ in $s$ the relation $r(a, b)$ holds, then the chain relation $\text{Chain}\,r\,s$ is satisfied.
Cycle.chain_iff_pairwise theorem
[IsTrans α r] : Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b
Full source 
theorem chain_iff_pairwise [IsTrans α r] : ChainChain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b :=
  ⟨by
    induction' s with a l _
    · exact fun _ b hb => (not_mem_nil _ hb).elim
    intro hs b hb c hc
    rw [Cycle.chain_coe_cons, List.chain_iff_pairwise] at hs
    simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
      IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
    simp only [mem_coe_iff, mem_cons] at hb hc
    rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)
    · exact hs.1 c (Or.inr rfl)
    · exact hs.1 c (Or.inl hc)
    · exact hs.2.2 b hb
    · exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc)), Cycle.chain_of_pairwise⟩
Chain Relation on Cycles is Equivalent to Pairwise Relation for Transitive Relations
Informal description
Let $\alpha$ be a type with a transitive binary relation $r$. For any cycle $s$ of type $\text{Cycle}\,\alpha$, the chain relation $\text{Chain}\,r\,s$ holds if and only if for all elements $a$ and $b$ in $s$, the relation $r(a, b)$ holds.
Cycle.forall_eq_of_chain theorem
[IsTrans α r] [IsAntisymm α r] (hs : Chain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : a = b
Full source 
theorem forall_eq_of_chain [IsTrans α r] [IsAntisymm α r] (hs : Chain r s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : a = b := by
  rw [chain_iff_pairwise] at hs
  exact antisymm (hs a ha b hb) (hs b hb a ha)
All Elements Equal in a Transitive Antisymmetric Cycle Chain
Informal description
Let $\alpha$ be a type equipped with a transitive and antisymmetric binary relation $r$. For any cycle $s$ of type $\text{Cycle}\,\alpha$, if the chain relation $\text{Chain}\,r\,s$ holds and elements $a$ and $b$ are both members of $s$, then $a = b$.