# Documentation

Mathlib.Data.List.Cycle

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

def List.nextOr {α : Type u_1} [] :
List αααα

Return the z such that x :: z :: _ appears in xs, or default if there is no such z.

Equations
Instances For
@[simp]
theorem List.nextOr_nil {α : Type u_1} [] (x : α) (d : α) :
List.nextOr [] x d = d
@[simp]
theorem List.nextOr_singleton {α : Type u_1} [] (x : α) (y : α) (d : α) :
List.nextOr [y] x d = d
@[simp]
theorem List.nextOr_self_cons_cons {α : Type u_1} [] (xs : List α) (x : α) (y : α) (d : α) :
List.nextOr (x :: y :: xs) x d = y
theorem List.nextOr_cons_of_ne {α : Type u_1} [] (xs : List α) (y : α) (x : α) (d : α) (h : x y) :
List.nextOr (y :: xs) x d = List.nextOr xs x d
theorem List.nextOr_eq_nextOr_of_mem_of_ne {α : Type u_1} [] (xs : List α) (x : α) (d : α) (d' : α) (x_mem : x xs) (x_ne : x List.getLast xs (_ : xs [])) :
List.nextOr xs x d = List.nextOr xs x d'

nextOr does not depend on the default value, if the next value appears.

theorem List.mem_of_nextOr_ne {α : Type u_1} [] {xs : List α} {x : α} {d : α} (h : List.nextOr xs x d d) :
x xs
theorem List.nextOr_concat {α : Type u_1} [] {xs : List α} {x : α} (d : α) (h : ¬x xs) :
List.nextOr (xs ++ [x]) x d = d
theorem List.nextOr_mem {α : Type u_1} [] {xs : List α} {x : α} {d : α} (hd : d xs) :
List.nextOr xs x d xs
def List.next {α : Type u_1} [] (l : List α) (x : α) (h : x l) :
α

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
Instances For
def List.prev {α : Type u_1} [] (l : List α) (x : α) (_h : x l) :
α

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
Equations
Instances For
@[simp]
theorem List.next_singleton {α : Type u_1} [] (x : α) (y : α) (h : x [y]) :
List.next [y] x h = y
@[simp]
theorem List.prev_singleton {α : Type u_1} [] (x : α) (y : α) (h : x [y]) :
List.prev [y] x h = y
theorem List.next_cons_cons_eq' {α : Type u_1} [] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hx : x = y) :
List.next (y :: z :: l) x h = z
@[simp]
theorem List.next_cons_cons_eq {α : Type u_1} [] (l : List α) (x : α) (z : α) (h : x x :: z :: l) :
List.next (x :: z :: l) x h = z
theorem List.next_ne_head_ne_getLast {α : Type u_1} [] (l : List α) (x : α) (h : x l) (y : α) (h : x y :: l) (hy : x y) (hx : x List.getLast (y :: l) (_ : y :: l [])) :
List.next (y :: l) x h = List.next l x (_ : x l)
theorem List.next_cons_concat {α : Type u_1} [] (l : List α) (x : α) (y : α) (hy : x y) (hx : ¬x l) (h : optParam (x y :: l ++ [x]) (_ : x y :: l ++ [x])) :
List.next (y :: l ++ [x]) x h = y
theorem List.next_getLast_cons {α : Type u_1} [] (l : List α) (x : α) (h : x l) (y : α) (h : x y :: l) (hy : x y) (hx : x = List.getLast (y :: l) (_ : y :: l [])) (hl : ) :
List.next (y :: l) x h = y
theorem List.prev_getLast_cons' {α : Type u_1} [] (l : List α) (x : α) (y : α) (hxy : x y :: l) (hx : x = y) :
List.prev (y :: l) x hxy = List.getLast (y :: l) (_ : y :: l [])
@[simp]
theorem List.prev_getLast_cons {α : Type u_1} [] (l : List α) (x : α) (h : x x :: l) :
List.prev (x :: l) x h = List.getLast (x :: l) (_ : x :: l [])
theorem List.prev_cons_cons_eq' {α : Type u_1} [] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hx : x = y) :
List.prev (y :: z :: l) x h = List.getLast (z :: l) (_ : z :: l [])
theorem List.prev_cons_cons_eq {α : Type u_1} [] (l : List α) (x : α) (z : α) (h : x x :: z :: l) :
List.prev (x :: z :: l) x h = List.getLast (z :: l) (_ : z :: l [])
theorem List.prev_cons_cons_of_ne' {α : Type u_1} [] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hy : x y) (hz : x = z) :
List.prev (y :: z :: l) x h = y
theorem List.prev_cons_cons_of_ne {α : Type u_1} [] (l : List α) (x : α) (y : α) (h : x y :: x :: l) (hy : x y) :
List.prev (y :: x :: l) x h = y
theorem List.prev_ne_cons_cons {α : Type u_1} [] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hy : x y) (hz : x z) :
List.prev (y :: z :: l) x h = List.prev (z :: l) x (_ : x z :: l)
theorem List.next_mem {α : Type u_1} [] (l : List α) (x : α) (h : x l) :
List.next l x h l
theorem List.prev_mem {α : Type u_1} [] (l : List α) (x : α) (h : x l) :
List.prev l x h l
theorem List.next_get {α : Type u_1} [] (l : List α) (_h : ) (i : Fin ()) :
List.next l (List.get l i) (_ : List.get l { val := i, isLt := (_ : i < ) } l) = List.get l { val := (i + 1) % , isLt := (_ : (i + 1) % < ) }
@[deprecated List.next_get]
theorem List.next_nthLe {α : Type u_1} [] (l : List α) (h : ) (n : ) (hn : n < ) :
List.next l (List.nthLe l n hn) (_ : List.nthLe l n hn l) = List.nthLe l ((n + 1) % ) (_ : (n + 1) % < )
theorem List.prev_nthLe {α : Type u_1} [] (l : List α) (h : ) (n : ) (hn : n < ) :
List.prev l (List.nthLe l n hn) (_ : List.nthLe l n hn l) = List.nthLe l ((n + ( - 1)) % ) (_ : (n + ( - 1)) % < )
theorem List.pmap_next_eq_rotate_one {α : Type u_1} [] (l : List α) (h : ) :
List.pmap () l (_ : ∀ (x : α), x lx l) =
theorem List.pmap_prev_eq_rotate_length_sub_one {α : Type u_1} [] (l : List α) (h : ) :
List.pmap () l (_ : ∀ (x : α), x lx l) = List.rotate l ( - 1)
theorem List.prev_next {α : Type u_1} [] (l : List α) (h : ) (x : α) (hx : x l) :
List.prev l (List.next l x hx) (_ : List.next l x hx l) = x
theorem List.next_prev {α : Type u_1} [] (l : List α) (h : ) (x : α) (hx : x l) :
List.next l (List.prev l x hx) (_ : List.prev l x hx l) = x
theorem List.prev_reverse_eq_next {α : Type u_1} [] (l : List α) (h : ) (x : α) (hx : x l) :
List.prev () x (_ : ) = List.next l x hx
theorem List.next_reverse_eq_prev {α : Type u_1} [] (l : List α) (h : ) (x : α) (hx : x l) :
List.next () x (_ : ) = List.prev l x hx
theorem List.isRotated_next_eq {α : Type u_1} [] {l : List α} {l' : List α} (h : l ~r l') (hn : ) {x : α} (hx : x l) :
List.next l x hx = List.next l' x (_ : x l')
theorem List.isRotated_prev_eq {α : Type u_1} [] {l : List α} {l' : List α} (h : l ~r l') (hn : ) {x : α} (hx : x l) :
List.prev l x hx = List.prev l' x (_ : x l')
def Cycle (α : Type u_1) :
Type u_1

Cycle α is the quotient of List α by cyclic permutation. Duplicates are allowed.

Instances For
def Cycle.ofList {α : Type u_1} :
List α

The coercion from List α to Cycle α

Instances For
instance Cycle.instCoeListCycle {α : Type u_1} :
Coe (List α) ()
@[simp]
theorem Cycle.coe_eq_coe {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ = l₂ l₁ ~r l₂
@[simp]
theorem Cycle.mk_eq_coe {α : Type u_1} (l : List α) :
Quot.mk Setoid.r l = l
@[simp]
theorem Cycle.mk''_eq_coe {α : Type u_1} (l : List α) :
= l
theorem Cycle.coe_cons_eq_coe_append {α : Type u_1} (l : List α) (a : α) :
↑(a :: l) = ↑(l ++ [a])
def Cycle.nil {α : Type u_1} :

The unique empty cycle.

Instances For
@[simp]
theorem Cycle.coe_nil {α : Type u_1} :
[] = Cycle.nil
@[simp]
theorem Cycle.coe_eq_nil {α : Type u_1} (l : List α) :
l = Cycle.nil l = []
instance Cycle.instEmptyCollectionCycle {α : Type u_1} :

For consistency with EmptyCollection (List α).

@[simp]
theorem Cycle.empty_eq {α : Type u_1} :
= Cycle.nil
theorem Cycle.induction_on {α : Type u_1} {C : Prop} (s : ) (H0 : C Cycle.nil) (HI : (a : α) → (l : List α) → C lC ↑(a :: l)) :
C s

An induction principle for Cycle. Use as induction s using Cycle.induction_on.

def Cycle.Mem {α : Type u_1} (a : α) (s : ) :

For x : α, s : Cycle α, x ∈ s indicates that x occurs at least once in s.

Instances For
@[simp]
theorem Cycle.mem_coe_iff {α : Type u_1} {a : α} {l : List α} :
a l a l
@[simp]
theorem Cycle.not_mem_nil {α : Type u_1} (a : α) :
¬a Cycle.nil
instance Cycle.instDecidableMemCycleInstMembershipCycle {α : Type u_1} [] (x : α) (s : ) :
def Cycle.reverse {α : Type u_1} (s : ) :

Reverse a s : Cycle α by reversing the underlying List.

Instances For
@[simp]
theorem Cycle.reverse_coe {α : Type u_1} (l : List α) :
= ↑()
@[simp]
theorem Cycle.mem_reverse_iff {α : Type u_1} {a : α} {s : } :
a s
@[simp]
theorem Cycle.reverse_reverse {α : Type u_1} (s : ) :
@[simp]
theorem Cycle.reverse_nil {α : Type u_1} :
Cycle.reverse Cycle.nil = Cycle.nil
def Cycle.length {α : Type u_1} (s : ) :

The length of the s : Cycle α, which is the number of elements, counting duplicates.

Instances For
@[simp]
theorem Cycle.length_coe {α : Type u_1} (l : List α) :
@[simp]
theorem Cycle.length_nil {α : Type u_1} :
Cycle.length Cycle.nil = 0
@[simp]
theorem Cycle.length_reverse {α : Type u_1} (s : ) :
def Cycle.Subsingleton {α : Type u_1} (s : ) :

A s : Cycle α that is at most one element.

Instances For
theorem Cycle.length_subsingleton_iff {α : Type u_1} {s : } :
@[simp]
theorem Cycle.subsingleton_reverse_iff {α : Type u_1} {s : } :
theorem Cycle.Subsingleton.congr {α : Type u_1} {s : } (h : ) ⦃x : α (_hx : x s) ⦃y : α (_hy : y s) :
x = y
def Cycle.Nontrivial {α : Type u_1} (s : ) :

A s : Cycle α that is made up of at least two unique elements.

Instances For
@[simp]
theorem Cycle.nontrivial_coe_nodup_iff {α : Type u_1} {l : List α} (hl : ) :
2
@[simp]
theorem Cycle.nontrivial_reverse_iff {α : Type u_1} {s : } :
theorem Cycle.length_nontrivial {α : Type u_1} {s : } (h : ) :
def Cycle.Nodup {α : Type u_1} (s : ) :

The s : Cycle α contains no duplicates.

Instances For
@[simp]
theorem Cycle.nodup_nil {α : Type u_1} :
Cycle.Nodup Cycle.nil
@[simp]
theorem Cycle.nodup_coe_iff {α : Type u_1} {l : List α} :
@[simp]
theorem Cycle.nodup_reverse_iff {α : Type u_1} {s : } :
theorem Cycle.Subsingleton.nodup {α : Type u_1} {s : } (h : ) :
theorem Cycle.Nodup.nontrivial_iff {α : Type u_1} {s : } (h : ) :
def Cycle.toMultiset {α : Type u_1} (s : ) :

The s : Cycle α as a Multiset α.

Instances For
@[simp]
theorem Cycle.coe_toMultiset {α : Type u_1} (l : List α) :
= l
@[simp]
theorem Cycle.nil_toMultiset {α : Type u_1} :
Cycle.toMultiset Cycle.nil = 0
@[simp]
theorem Cycle.card_toMultiset {α : Type u_1} (s : ) :
Multiset.card () =
@[simp]
theorem Cycle.toMultiset_eq_nil {α : Type u_1} {s : } :
s = Cycle.nil
def Cycle.map {α : Type u_1} {β : Type u_2} (f : αβ) :

The lift of list.map.

Instances For
@[simp]
theorem Cycle.map_nil {α : Type u_1} {β : Type u_2} (f : αβ) :
Cycle.map f Cycle.nil = Cycle.nil
@[simp]
theorem Cycle.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
Cycle.map f l = ↑(List.map f l)
@[simp]
theorem Cycle.map_eq_nil {α : Type u_1} {β : Type u_2} (f : αβ) (s : ) :
= Cycle.nil s = Cycle.nil
@[simp]
theorem Cycle.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : } :
b a, a s f a = b
def Cycle.lists {α : Type u_1} (s : ) :

The Multiset of lists that can make the cycle.

Instances For
@[simp]
theorem Cycle.lists_coe {α : Type u_1} (l : List α) :
@[simp]
theorem Cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : } {l : List α} :
l l = s
@[simp]
theorem Cycle.lists_nil {α : Type u_1} :
Cycle.lists Cycle.nil = [[]]
def Cycle.decidableNontrivialCoe {α : Type u_1} [] (l : List α) :

Auxiliary decidability algorithm for lists that contain at least two unique elements.

Equations
• One or more equations did not get rendered due to their size.
• = isFalse (_ : ¬x x_1 _h, x Cycle.nil x_1 Cycle.nil)
• = isFalse (_ : ¬x x_1 _h, x [x_1] x_1 [x_1])
Instances For
instance Cycle.instDecidableNontrivial {α : Type u_1} [] {s : } :
instance Cycle.instDecidableNodup {α : Type u_1} [] {s : } :
instance Cycle.fintypeNodupCycle {α : Type u_1} [] [] :
Fintype { s // }
instance Cycle.fintypeNodupNontrivialCycle {α : Type u_1} [] [] :
Fintype { s // }
def Cycle.toFinset {α : Type u_1} [] (s : ) :

The s : Cycle α as a Finset α.

Instances For
@[simp]
theorem Cycle.toFinset_toMultiset {α : Type u_1} [] (s : ) :
@[simp]
theorem Cycle.coe_toFinset {α : Type u_1} [] (l : List α) :
@[simp]
theorem Cycle.nil_toFinset {α : Type u_1} [] :
Cycle.toFinset Cycle.nil =
@[simp]
theorem Cycle.toFinset_eq_nil {α : Type u_1} [] {s : } :
s = Cycle.nil
def Cycle.next {α : Type u_1} [] (s : ) (_hs : ) (x : α) (_hx : x s) :
α

Given a s : Cycle α such that Nodup s, retrieve the next element after x ∈ s.

Instances For
def Cycle.prev {α : Type u_1} [] (s : ) (_hs : ) (x : α) (_hx : x s) :
α

Given a s : Cycle α such that Nodup s, retrieve the previous element before x ∈ s.

Instances For
theorem Cycle.prev_reverse_eq_next {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.prev () (_ : ) x (_ : ) = Cycle.next s hs x hx
@[simp]
theorem Cycle.prev_reverse_eq_next' {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : ) :
Cycle.prev () hs x hx = Cycle.next s (_ : ) x (_ : x s)
theorem Cycle.next_reverse_eq_prev {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.next () (_ : ) x (_ : ) = Cycle.prev s hs x hx
@[simp]
theorem Cycle.next_reverse_eq_prev' {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : ) :
Cycle.next () hs x hx = Cycle.prev s (_ : ) x (_ : x s)
@[simp]
theorem Cycle.next_mem {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.next s hs x hx s
theorem Cycle.prev_mem {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.prev s hs x hx s
@[simp]
theorem Cycle.prev_next {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.prev s hs (Cycle.next s hs x hx) (_ : Cycle.next s hs x hx s) = x
@[simp]
theorem Cycle.next_prev {α : Type u_1} [] (s : ) (hs : ) (x : α) (hx : x s) :
Cycle.next s hs (Cycle.prev s hs x hx) (_ : Cycle.prev s hs x hx s) = x
unsafe instance Cycle.instReprCycle {α : Type u_1} [Repr α] :
Repr ()

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.

def Cycle.Chain {α : Type u_1} (r : ααProp) (c : ) :

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

Instances For
@[simp]
theorem Cycle.Chain.nil {α : Type u_1} (r : ααProp) :
Cycle.Chain r Cycle.nil
@[simp]
theorem Cycle.chain_coe_cons {α : Type u_1} (r : ααProp) (a : α) (l : List α) :
Cycle.Chain r ↑(a :: l) List.Chain r a (l ++ [a])
theorem Cycle.chain_singleton {α : Type u_1} (r : ααProp) (a : α) :
Cycle.Chain r [a] r a a
theorem Cycle.chain_ne_nil {α : Type u_1} (r : ααProp) {l : List α} (hl : l []) :
theorem Cycle.chain_map {α : Type u_1} {β : Type u_2} {r : ααProp} (f : βα) {s : } :
Cycle.Chain r () Cycle.Chain (fun a b => r (f a) (f b)) s
theorem Cycle.chain_range_succ (r : Prop) (n : ) :
Cycle.Chain r ↑() r n 0 ((m : ) → m < nr m ())
theorem Cycle.Chain.imp {α : Type u_1} {s : } {r₁ : ααProp} {r₂ : ααProp} (H : (a b : α) → r₁ a br₂ a b) (p : Cycle.Chain r₁ s) :
theorem Cycle.chain_mono {α : Type u_1} :
Monotone Cycle.Chain

As a function from a relation to a predicate, chain is monotonic.

theorem Cycle.chain_of_pairwise {α : Type u_1} {r : ααProp} {s : } :
((a : α) → a s(b : α) → b sr a b) →
theorem Cycle.chain_iff_pairwise {α : Type u_1} {r : ααProp} {s : } [IsTrans α r] :
(a : α) → a s(b : α) → b sr a b
theorem Cycle.Chain.eq_nil_of_irrefl {α : Type u_1} {r : ααProp} {s : } [IsTrans α r] [IsIrrefl α r] (h : ) :
s = Cycle.nil
theorem Cycle.Chain.eq_nil_of_well_founded {α : Type u_1} {r : ααProp} {s : } [] (h : ) :
s = Cycle.nil
theorem Cycle.forall_eq_of_chain {α : Type u_1} {r : ααProp} {s : } [IsTrans α r] [] (hs : ) {a : α} {b : α} (ha : a s) (hb : b s) :
a = b