data.list.cycle

# Cycles of a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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[2, 1, 4, 3]. Two equal cycles may be printed differently if their internal representation is different.

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
Instances for cycle
@[protected, 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 α) :
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.

Equations
@[simp]
theorem cycle.coe_nil {α : Type u_1} :
@[simp]
theorem cycle.coe_eq_nil {α : Type u_1} (l : list α) :
@[protected, instance]
def cycle.has_emptyc {α : Type u_1} :

For consistency with list.has_emptyc.

Equations
@[simp]
theorem cycle.empty_eq {α : Type u_1} :
@[protected, instance]
def cycle.inhabited {α : Type u_1} :
Equations
theorem cycle.induction_on {α : Type u_1} {C : Prop} (s : cycle α) (H0 : C cycle.nil) (HI : (a : α) (l : list α), C l C (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 : cycle α) :
Prop

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

Equations
@[protected, 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
@[simp]
theorem cycle.not_mem_nil {α : Type u_1} (a : α) :
@[protected, instance]
def cycle.decidable_eq {α : Type u_1} [decidable_eq α] :
Equations
@[protected, 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 α) :
@[simp]
theorem cycle.reverse_nil {α : Type u_1} :
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_nil {α : Type u_1} :
@[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.subsingleton_nil {α : Type u_1} :
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
Instances for cycle.nontrivial
@[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
Instances for cycle.nodup
@[simp]
theorem cycle.nodup_nil {α : Type u_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
@[simp]
theorem cycle.coe_to_multiset {α : Type u_1} (l : list α) :
@[simp]
theorem cycle.nil_to_multiset {α : Type u_1} :
@[simp]
theorem cycle.card_to_multiset {α : Type u_1} (s : cycle α) :
@[simp]
theorem cycle.to_multiset_eq_nil {α : Type u_1} {s : cycle α} :
def cycle.map {α : Type u_1} {β : Type u_2} (f : α β) :

The lift of list.map.

Equations
• = _
@[simp]
theorem cycle.map_nil {α : Type u_1} {β : Type u_2} (f : α β) :
@[simp]
theorem cycle.map_coe {α : Type u_1} {β : Type u_2} (f : α β) (l : list α) :
l = (list.map f l)
@[simp]
theorem cycle.map_eq_nil {α : Type u_1} {β : Type u_2} (f : α β) (s : cycle α) :
@[simp]
theorem cycle.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {b : β} {s : cycle α} :
b s (a : α), a s f a = b
def cycle.lists {α : Type u_1} (s : cycle α) :

The multiset of lists that can make the cycle.

Equations
@[simp]
theorem cycle.lists_coe {α : Type u_1} (l : list α) :
@[simp]
theorem cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : cycle α} {l : list α} :
l s.lists l = s
@[simp]
theorem cycle.lists_nil {α : Type u_1} :
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
@[protected, instance]
def cycle.nontrivial.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :
Equations
@[protected, instance]
def cycle.nodup.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :
Equations
@[protected, instance]
def cycle.fintype_nodup_cycle {α : Type u_1} [decidable_eq α] [fintype α] :
fintype {s // s.nodup}
Equations
@[protected, instance]
Equations
def cycle.to_finset {α : Type u_1} [decidable_eq α] (s : cycle α) :

The s : cycle α as a finset α.

Equations
@[simp]
theorem cycle.to_finset_to_multiset {α : Type u_1} [decidable_eq α] (s : cycle α) :
@[simp]
theorem cycle.coe_to_finset {α : Type u_1} [decidable_eq α] (l : list α) :
@[simp]
theorem cycle.nil_to_finset {α : Type u_1} [decidable_eq α] :
@[simp]
theorem cycle.to_finset_eq_nil {α : Type u_1} [decidable_eq α] {s : cycle α} :
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
@[protected, instance]
meta 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 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 : cycle α) :
Prop

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

Equations
• c = (λ (l : list α), cycle.chain._match_1 r l) _
• cycle.chain._match_1 r (a :: m) = a (m ++ [a])
• cycle.chain._match_1 r list.nil = true
@[simp]
theorem cycle.chain.nil {α : Type u_1} (r : α α Prop) :
@[simp]
theorem cycle.chain_coe_cons {α : Type u_1} (r : α α Prop) (a : α) (l : list α) :
(a :: l) a (l ++ [a])
@[simp]
theorem cycle.chain_singleton {α : Type u_1} (r : α α Prop) (a : α) :
[a] r a a
theorem cycle.chain_ne_nil {α : Type u_1} (r : α α Prop) {l : list α} (hl : l list.nil) :
l (l.last hl) l
theorem cycle.chain_map {α : Type u_1} {β : Type u_2} {r : α α Prop} (f : β α) {s : cycle β} :
s) cycle.chain (λ (a b : β), r (f a) (f b)) s
theorem cycle.chain_range_succ (r : Prop) (n : ) :
(list.range n.succ) r n 0 (m : ), m < n r m m.succ
theorem cycle.chain.imp {α : Type u_1} {s : cycle α} {r₁ r₂ : α α Prop} (H : (a b : α), r₁ a b r₂ a b) (p : s) :
s
theorem cycle.chain_mono {α : Type u_1} :

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

theorem cycle.chain_of_pairwise {α : Type u_1} {r : α α Prop} {s : cycle α} :
( (a : α), a s (b : α), b s r a b) s
theorem cycle.chain_iff_pairwise {α : Type u_1} {r : α α Prop} {s : cycle α} [ r] :
s (a : α), a s (b : α), b s r a b
theorem cycle.chain.eq_nil_of_irrefl {α : Type u_1} {r : α α Prop} {s : cycle α} [ r] [ r] (h : s) :
theorem cycle.chain.eq_nil_of_well_founded {α : Type u_1} {r : α α Prop} {s : cycle α} [ r] (h : s) :
theorem cycle.forall_eq_of_chain {α : Type u_1} {r : α α Prop} {s : cycle α} [ r] [ r] (hs : s) {a b : α} (ha : a s) (hb : b s) :
a = b