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

Based on this, we define the quotient of lists by the rotation relation, called cycle.

We also define a representation of concrete cycles, available when viewing them in a goal state or via #eval, when over representatble types. For example, the cycle (2 1 4 3) will be shown as c[1, 4, 3, 2]. The representation of the cycle sorts the elements by the string value of the underlying element. This representation also supports cycles that can contain duplicates.

def list.next_or {α : Type u_1} [decidable_eq α] (xs : list α) (x default : α) :
α

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

Equations
@[simp]
theorem list.next_or_nil {α : Type u_1} [decidable_eq α] (x d : α) :
d = d
@[simp]
theorem list.next_or_singleton {α : Type u_1} [decidable_eq α] (x y d : α) :
[y].next_or x d = d
@[simp]
theorem list.next_or_self_cons_cons {α : Type u_1} [decidable_eq α] (xs : list α) (x y d : α) :
(x :: y :: xs).next_or x d = y
theorem list.next_or_cons_of_ne {α : Type u_1} [decidable_eq α] (xs : list α) (y x d : α) (h : x y) :
(y :: xs).next_or x d = xs.next_or x d
theorem list.next_or_eq_next_or_of_mem_of_ne {α : Type u_1} [decidable_eq α] (xs : list α) (x d d' : α) (x_mem : x xs) (x_ne : x xs.last _) :
xs.next_or x d = xs.next_or x d'

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

theorem list.mem_of_next_or_ne {α : Type u_1} [decidable_eq α] {xs : list α} {x d : α} (h : xs.next_or x d d) :
x xs
theorem list.next_or_concat {α : Type u_1} [decidable_eq α] {xs : list α} {x : α} (d : α) (h : x xs) :
(xs ++ [x]).next_or x d = d
theorem list.next_or_mem {α : Type u_1} [decidable_eq α] {xs : list α} {x d : α} (hd : d xs) :
xs.next_or x d xs
def list.next {α : Type u_1} [decidable_eq α] (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
Equations
def list.prev {α : Type u_1} [decidable_eq α] (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
@[simp]
theorem list.next_singleton {α : Type u_1} [decidable_eq α] (x y : α) (h : x [y]) :
[y].next x h = y
@[simp]
theorem list.prev_singleton {α : Type u_1} [decidable_eq α] (x y : α) (h : x [y]) :
[y].prev x h = y
theorem list.next_cons_cons_eq' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x y :: z :: l) (hx : x = y) :
(y :: z :: l).next x h = z
@[simp]
theorem list.next_cons_cons_eq {α : Type u_1} [decidable_eq α] (l : list α) (x z : α) (h : x x :: z :: l) :
(x :: z :: l).next x h = z
theorem list.next_ne_head_ne_last {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x y :: l) (hy : x y) (hx : x (y :: l).last _) :
(y :: l).next x h = l.next x _
theorem list.next_cons_concat {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (hy : x y) (hx : x l) (h : x y :: l ++ [x] := _) :
(y :: l ++ [x]).next x h = y
theorem list.next_last_cons {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x y :: l) (hy : x y) (hx : x = (y :: l).last _) (hl : l.nodup) :
(y :: l).next x h = y
theorem list.prev_last_cons' {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x y :: l) (hx : x = y) :
(y :: l).prev x h = (y :: l).last _
@[simp]
theorem list.prev_last_cons {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x x :: l) :
(x :: l).prev x h = (x :: l).last _
theorem list.prev_cons_cons_eq' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x y :: z :: l) (hx : x = y) :
(y :: z :: l).prev x h = (z :: l).last _
@[simp]
theorem list.prev_cons_cons_eq {α : Type u_1} [decidable_eq α] (l : list α) (x z : α) (h : x x :: z :: l) :
(x :: z :: l).prev x h = (z :: l).last _
theorem list.prev_cons_cons_of_ne' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x y :: z :: l) (hy : x y) (hz : x = z) :
(y :: z :: l).prev x h = y
theorem list.prev_cons_cons_of_ne {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x y :: x :: l) (hy : x y) :
(y :: x :: l).prev x h = y
theorem list.prev_ne_cons_cons {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x y :: z :: l) (hy : x y) (hz : x z) :
(y :: z :: l).prev x h = (z :: l).prev x _
theorem list.next_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x l) :
l.next x h l
theorem list.prev_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x l) :
l.prev x h l
theorem list.next_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ) (hn : n < l.length) :
l.next (l.nth_le n hn) _ = l.nth_le ((n + 1) % l.length) _
theorem list.prev_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ) (hn : n < l.length) :
l.prev (l.nth_le n hn) _ = l.nth_le ((n + (l.length - 1)) % l.length) _
theorem list.pmap_next_eq_rotate_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :
l _ = l.rotate 1
theorem list.pmap_prev_eq_rotate_length_sub_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :
l _ = l.rotate (l.length - 1)
theorem list.prev_next {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x l) :
l.prev (l.next x hx) _ = x
theorem list.next_prev {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x l) :
l.next (l.prev x hx) _ = x
theorem list.prev_reverse_eq_next {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x l) :
l.reverse.prev x _ = l.next x hx
theorem list.next_reverse_eq_prev {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x l) :
l.reverse.next x _ = l.prev x hx
theorem list.is_rotated_next_eq {α : Type u_1} [decidable_eq α] {l l' : list α} (h : l ~r l') (hn : l.nodup) {x : α} (hx : x l) :
l.next x hx = l'.next x _
theorem list.is_rotated_prev_eq {α : Type u_1} [decidable_eq α] {l l' : list α} (h : l ~r l') (hn : l.nodup) {x : α} (hx : x l) :
l.prev x hx = l'.prev x _
def cycle (α : Type u_1) :
Type u_1

cycle α is the quotient of list α by cyclic permutation. Duplicates are allowed.

Equations
@[instance]
def cycle.has_coe {α : Type u_1} :
has_coe (list α) (cycle α)
Equations
@[simp]
theorem cycle.coe_eq_coe {α : Type u_1} {l₁ 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 α) :
@[instance]
def cycle.inhabited {α : Type u_1} :
Equations
def cycle.mem {α : Type u_1} (a : α) (s : cycle α) :
Prop

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

Equations
@[instance]
def cycle.has_mem {α : Type u_1} :
(cycle α)
Equations
@[simp]
theorem cycle.mem_coe_iff {α : Type u_1} {a : α} {l : list α} :
a l a l
@[instance]
def cycle.decidable_eq {α : Type u_1} [decidable_eq α] :
Equations
@[instance]
def cycle.has_mem.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (s : cycle α) :
Equations
def cycle.reverse {α : Type u_1} (s : cycle α) :

Reverse a s : cycle α by reversing the underlying list.

Equations
@[simp]
theorem cycle.reverse_coe {α : Type u_1} (l : list α) :
@[simp]
theorem cycle.mem_reverse_iff {α : Type u_1} {a : α} {s : cycle α} :
a s.reverse a s
@[simp]
theorem cycle.reverse_reverse {α : Type u_1} (s : cycle α) :
def cycle.length {α : Type u_1} (s : cycle α) :

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

Equations
@[simp]
theorem cycle.length_coe {α : Type u_1} (l : list α) :
@[simp]
theorem cycle.length_reverse {α : Type u_1} (s : cycle α) :
def cycle.subsingleton {α : Type u_1} (s : cycle α) :
Prop

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

Equations
theorem cycle.length_subsingleton_iff {α : Type u_1} {s : cycle α} :
@[simp]
theorem cycle.subsingleton_reverse_iff {α : Type u_1} {s : cycle α} :
theorem cycle.subsingleton.congr {α : Type u_1} {s : cycle α} (h : s.subsingleton) ⦃x : α⦄ (hx : x s) ⦃y : α⦄ (hy : y s) :
x = y
def cycle.nontrivial {α : Type u_1} (s : cycle α) :
Prop

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

Equations
@[simp]
theorem cycle.nontrivial_coe_nodup_iff {α : Type u_1} {l : list α} (hl : l.nodup) :
@[simp]
theorem cycle.nontrivial_reverse_iff {α : Type u_1} {s : cycle α} :
theorem cycle.length_nontrivial {α : Type u_1} {s : cycle α} (h : s.nontrivial) :
def cycle.nodup {α : Type u_1} (s : cycle α) :
Prop

The s : cycle α contains no duplicates.

Equations
• s.nodup = cycle.nodup._proof_1
@[simp]
theorem cycle.nodup_coe_iff {α : Type u_1} {l : list α} :
@[simp]
theorem cycle.nodup_reverse_iff {α : Type u_1} {s : cycle α} :
theorem cycle.subsingleton.nodup {α : Type u_1} {s : cycle α} (h : s.subsingleton) :
theorem cycle.nodup.nontrivial_iff {α : Type u_1} {s : cycle α} (h : s.nodup) :
def cycle.to_multiset {α : Type u_1} (s : cycle α) :

The s : cycle α as a multiset α.

Equations
def cycle.map {α : Type u_1} {β : Type u_2} (f : α → β) :

The lift of list.map.

Equations
• = _
def cycle.lists {α : Type u_1} (s : cycle α) :

The multiset of lists that can make the cycle.

Equations
@[simp]
theorem cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : cycle α} {l : list α} :
l s.lists l = s
def cycle.decidable_nontrivial_coe {α : Type u_1} [decidable_eq α] (l : list α) :

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

Equations
@[instance]
def cycle.nontrivial.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :
Equations
@[instance]
def cycle.nodup.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :
Equations
@[instance]
def cycle.fintype_nodup_cycle {α : Type u_1} [decidable_eq α] [fintype α] :
fintype {s // s.nodup}
Equations
@[instance]
Equations
def cycle.to_finset {α : Type u_1} [decidable_eq α] (s : cycle α) :

The s : cycle α as a finset α.

Equations
def cycle.next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
α

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

Equations
def cycle.prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
α

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

Equations
@[simp]
theorem cycle.prev_reverse_eq_next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.reverse.prev _ x _ = s.next hs x hx
@[simp]
theorem cycle.next_reverse_eq_prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.reverse.next _ x _ = s.prev hs x hx
@[simp]
theorem cycle.next_mem {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.next hs x hx s
theorem cycle.prev_mem {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.prev hs x hx s
@[simp]
theorem cycle.prev_next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.prev hs (s.next hs x hx) _ = x
@[simp]
theorem cycle.next_prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x s) :
s.next hs (s.prev hs x hx) _ = x
@[instance]
def cycle.has_repr {α : Type u_1} [has_repr α] :

We define a representation of concrete cycles, available when viewing them in a goal state or via #eval, when over representatble types. For example, the cycle (2 1 4 3) will be shown as c[1, 4, 3, 2]. The representation of the cycle sorts the elements by the string value of the underlying element. This representation also supports cycles that can contain duplicates.

Equations