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

ink

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

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

Equations

• List.nextOr [] x x = x
• List.nextOr [head] x x = x
• List.nextOr (y :: z :: xs) x x = if x = y then z else List.nextOr (z :: xs) x x

ink

@[simp]

theorem List.nextOr_nil {α : Type u_1} [inst : DecidableEq α] (x : α) (d : α) : List.nextOr [] x d = d

ink

@[simp]

theorem List.nextOr_singleton {α : Type u_1} [inst : DecidableEq α] (x : α) (y : α) (d : α) : List.nextOr [y] x d = d

ink

@[simp]

theorem List.nextOr_self_cons_cons {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x : α) (y : α) (d : α) : List.nextOr (x :: y :: xs) x d = y

ink

theorem List.nextOr_cons_of_ne {α : Type u_1} [inst : DecidableEq α] (xs : List α) (y : α) (x : α) (d : α) (h : x ≠ y) : List.nextOr (y :: xs) x d = List.nextOr xs x d

ink

theorem List.nextOr_eq_nextOr_of_mem_of_ne {α : Type u_1} [inst : DecidableEq α] (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.

ink

theorem List.mem_of_nextOr_ne {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} {d : α} (h : List.nextOr xs x d ≠ d) : x ∈ xs

ink

theorem List.nextOr_concat {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} (d : α) (h : ¬x ∈ xs) : List.nextOr (xs ++ [x]) x d = d

ink

theorem List.nextOr_mem {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} {d : α} (hd : d ∈ xs) : List.nextOr xs x d ∈ xs

ink

def List.next {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l) : α

Given an element x : α of l : list α such that x ∈ l∈ 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

• List.next l x h = List.nextOr l x (List.get l { val := 0, isLt := (_ : 0 < List.length l) })

ink

def List.prev {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (_h : x ∈ l) : α

Given an element x : α of l : list α such that x ∈ l∈ 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

• List.prev [] x x_1 = False.elim (_ : False)
• List.prev [y] x x_1 = y
• List.prev (y :: z :: xs) x x_1 = if hx : x = y then List.getLast (z :: xs) (_ : z :: xs ≠ []) else if x = z then y else List.prev (z :: xs) x (_ : x ∈ z :: xs)

ink

@[simp]

theorem List.next_singleton {α : Type u_1} [inst : DecidableEq α] (x : α) (y : α) (h : x ∈ [y]) : List.next [y] x h = y

ink

@[simp]

theorem List.prev_singleton {α : Type u_1} [inst : DecidableEq α] (x : α) (y : α) (h : x ∈ [y]) : List.prev [y] x h = y

ink

theorem List.next_cons_cons_eq' {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x ∈ y :: z :: l) (hx : x = y) : List.next (y :: z :: l) x h = z

ink

@[simp]

theorem List.next_cons_cons_eq {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (z : α) (h : x ∈ x :: z :: l) : List.next (x :: z :: l) x h = z

ink

theorem List.next_ne_head_ne_getLast {α : Type u_1} [inst : DecidableEq α] (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)

ink

theorem List.next_cons_concat {α : Type u_1} [inst : DecidableEq α] (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

ink

theorem List.next_getLast_cons {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y) (hx : x = List.getLast (y :: l) (_ : y :: l ≠ [])) (hl : List.Nodup l) : List.next (y :: l) x h = y

ink

theorem List.prev_getLast_cons' {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (y : α) (hxy : x ∈ y :: l) (hx : x = y) : List.prev (y :: l) x hxy = List.getLast (y :: l) (_ : y :: l ≠ [])

ink

@[simp]

theorem List.prev_getLast_cons {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ x :: l) : List.prev (x :: l) x h = List.getLast (x :: l) (_ : x :: l ≠ [])

ink

theorem List.prev_cons_cons_eq' {α : Type u_1} [inst : DecidableEq α] (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 ≠ [])

ink

theorem List.prev_cons_cons_eq {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (z : α) (h : x ∈ x :: z :: l) : List.prev (x :: z :: l) x h = List.getLast (z :: l) (_ : z :: l ≠ [])

ink

theorem List.prev_cons_cons_of_ne' {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) : List.prev (y :: z :: l) x h = y

ink

theorem List.prev_cons_cons_of_ne {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (y : α) (h : x ∈ y :: x :: l) (hy : x ≠ y) : List.prev (y :: x :: l) x h = y

ink

theorem List.prev_ne_cons_cons {α : Type u_1} [inst : DecidableEq α] (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)

ink

theorem List.next_mem {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l) : List.next l x h ∈ l

ink

theorem List.prev_mem {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l) : List.prev l x h ∈ l

ink

theorem List.next_get {α : Type u_1} [inst : DecidableEq α] (l : List α) (_h : List.Nodup l) (i : Fin (List.length l)) : List.next l (List.get l i) (_ : List.get l { val := ↑i, isLt := (_ : ↑i < List.length l) } ∈ l) = List.get l { val := (↑i + 1) % List.length l, isLt := (_ : (↑i + 1) % List.length l < List.length l) }

ink

theorem List.next_nthLe {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (n : ℕ) (hn : n < List.length l) : List.next l (List.nthLe l n hn) (_ : List.nthLe l n hn ∈ l) = List.nthLe l ((n + 1) % List.length l) (_ : (n + 1) % List.length l < List.length l)

ink

theorem List.prev_nthLe {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (n : ℕ) (hn : n < List.length l) : List.prev l (List.nthLe l n hn) (_ : List.nthLe l n hn ∈ l) = List.nthLe l ((n + (List.length l - 1)) % List.length l) (_ : (n + (List.length l - 1)) % List.length l < List.length l)

ink

theorem List.pmap_next_eq_rotate_one {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) : List.pmap (List.next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l) = List.rotate l 1

ink

theorem List.pmap_prev_eq_rotate_length_sub_one {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) : List.pmap (List.prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l) = List.rotate l (List.length l - 1)

ink

theorem List.prev_next {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (x : α) (hx : x ∈ l) : List.prev l (List.next l x hx) (_ : List.next l x hx ∈ l) = x

ink

theorem List.next_prev {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (x : α) (hx : x ∈ l) : List.next l (List.prev l x hx) (_ : List.prev l x hx ∈ l) = x

ink

theorem List.prev_reverse_eq_next {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (x : α) (hx : x ∈ l) : List.prev (List.reverse l) x (_ : x ∈ List.reverse l) = List.next l x hx

ink

theorem List.next_reverse_eq_prev {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : List.Nodup l) (x : α) (hx : x ∈ l) : List.next (List.reverse l) x (_ : x ∈ List.reverse l) = List.prev l x hx

ink

theorem List.isRotated_next_eq {α : Type u_1} [inst : DecidableEq α] {l : List α} {l' : List α} (h : l ~r l') (hn : List.Nodup l) {x : α} (hx : x ∈ l) : List.next l x hx = List.next l' x (_ : x ∈ l')

ink

theorem List.isRotated_prev_eq {α : Type u_1} [inst : DecidableEq α] {l : List α} {l' : List α} (h : l ~r l') (hn : List.Nodup l) {x : α} (hx : x ∈ l) : List.prev l x hx = List.prev l' x (_ : x ∈ l')

ink

def Cycle (α : Type u_1) : Type u_1

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

Equations

• Cycle α = Quotient (List.IsRotated.setoid α)

ink

def Cycle.ofList {α : Type u_1} : List α → Cycle α

The coercion from List α to Cycle α

Equations

• Cycle.ofList = Quot.mk Setoid.r

ink

instance Cycle.instCoeListCycle {α : Type u_1} : Coe (List α) (Cycle α)

Equations

• Cycle.instCoeListCycle = { coe := Cycle.ofList }

ink

@[simp]

theorem Cycle.coe_eq_coe {α : Type u_1} {l₁ : List α} {l₂ : List α} : ↑l₁ = ↑l₂ ↔ l₁ ~r l₂

ink

@[simp]

theorem Cycle.mk_eq_coe {α : Type u_1} (l : List α) : Quot.mk Setoid.r l = ↑l

ink

@[simp]

theorem Cycle.mk''_eq_coe {α : Type u_1} (l : List α) : Quotient.mk'' l = ↑l

ink

theorem Cycle.coe_cons_eq_coe_append {α : Type u_1} (l : List α) (a : α) : ↑(a :: l) = ↑(l ++ [a])

ink

def Cycle.nil {α : Type u_1} : Cycle α

The unique empty cycle.

Equations

• Cycle.nil = ↑[]

ink

@[simp]

theorem Cycle.coe_nil {α : Type u_1} : ↑[] = Cycle.nil

ink

@[simp]

theorem Cycle.coe_eq_nil {α : Type u_1} (l : List α) : ↑l = Cycle.nil ↔ l = []

ink

instance Cycle.instEmptyCollectionCycle {α : Type u_1} : EmptyCollection (Cycle α)

For consistency with EmptyCollection (List α).

Equations

• Cycle.instEmptyCollectionCycle = { emptyCollection := Cycle.nil }

ink

@[simp]

theorem Cycle.empty_eq {α : Type u_1} : ∅ = Cycle.nil

ink

instance Cycle.instInhabitedCycle {α : Type u_1} : Inhabited (Cycle α)

Equations

• Cycle.instInhabitedCycle = { default := Cycle.nil }

ink

theorem Cycle.induction_on {α : Type u_1} {C : Cycle α → 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.

ink

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

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

Equations

• Cycle.Mem a s = Quot.liftOn s (fun l => a ∈ l) (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → (fun l => a ∈ l) x = (fun l => a ∈ l) x_1)

ink

instance Cycle.instMembershipCycle {α : Type u_1} : Membership α (Cycle α)

Equations

• Cycle.instMembershipCycle = { mem := Cycle.Mem }

ink

@[simp]

theorem Cycle.mem_coe_iff {α : Type u_1} {a : α} {l : List α} : a ∈ ↑l ↔ a ∈ l

ink

@[simp]

theorem Cycle.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ Cycle.nil

ink

instance Cycle.instDecidableEqCycle {α : Type u_1} [inst : DecidableEq α] : DecidableEq (Cycle α)

Equations

• Cycle.instDecidableEqCycle s₁ s₂ = Quotient.recOnSubsingleton₂' s₁ s₂ fun x x_1 => decidable_of_iff' (Setoid.r x x_1) (_ : Quotient.mk'' x = Quotient.mk'' x_1 ↔ Setoid.r x x_1)

ink

instance Cycle.instDecidableMemCycleInstMembershipCycle {α : Type u_1} [inst : DecidableEq α] (x : α) (s : Cycle α) : Decidable (x ∈ s)

Equations

• Cycle.instDecidableMemCycleInstMembershipCycle x s = Quotient.recOnSubsingleton' s fun l => let_fun this := inferInstance; this

ink

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

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

Equations

• Cycle.reverse s = Quot.map List.reverse (_ : ∀ (x x_1 : List α), x ~r x_1 → List.reverse x ~r List.reverse x_1) s

ink

@[simp]

theorem Cycle.reverse_coe {α : Type u_1} (l : List α) : Cycle.reverse ↑l = ↑(List.reverse l)

ink

@[simp]

theorem Cycle.mem_reverse_iff {α : Type u_1} {a : α} {s : Cycle α} : a ∈ Cycle.reverse s ↔ a ∈ s

ink

@[simp]

theorem Cycle.reverse_reverse {α : Type u_1} (s : Cycle α) : Cycle.reverse (Cycle.reverse s) = s

ink

@[simp]

theorem Cycle.reverse_nil {α : Type u_1} : Cycle.reverse Cycle.nil = Cycle.nil

ink

def Cycle.length {α : Type u_1} (s : Cycle α) : ℕ

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

Equations

• Cycle.length s = Quot.liftOn s List.length (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → List.length x = List.length x_1)

ink

@[simp]

theorem Cycle.length_coe {α : Type u_1} (l : List α) : Cycle.length ↑l = List.length l

ink

@[simp]

theorem Cycle.length_nil {α : Type u_1} : Cycle.length Cycle.nil = 0

ink

@[simp]

theorem Cycle.length_reverse {α : Type u_1} (s : Cycle α) : Cycle.length (Cycle.reverse s) = Cycle.length s

ink

def Cycle.Subsingleton {α : Type u_1} (s : Cycle α) : Prop

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

Equations

• Cycle.Subsingleton s = (Cycle.length s ≤ 1)

ink

theorem Cycle.subsingleton_nil {α : Type u_1} : Cycle.Subsingleton Cycle.nil

ink

theorem Cycle.length_subsingleton_iff {α : Type u_1} {s : Cycle α} : Cycle.Subsingleton s ↔ Cycle.length s ≤ 1

ink

@[simp]

theorem Cycle.subsingleton_reverse_iff {α : Type u_1} {s : Cycle α} : Cycle.Subsingleton (Cycle.reverse s) ↔ Cycle.Subsingleton s

ink

theorem Cycle.Subsingleton.congr {α : Type u_1} {s : Cycle α} (h : Cycle.Subsingleton s) ⦃x : α⦄ (_hx : x ∈ s) ⦃y : α⦄ (_hy : y ∈ s) : x = y

ink

def Cycle.Nontrivial {α : Type u_1} (s : Cycle α) : Prop

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

Equations

• Cycle.Nontrivial s = ∃ x y _h, x ∈ s ∧ y ∈ s

ink

@[simp]

theorem Cycle.nontrivial_coe_nodup_iff {α : Type u_1} {l : List α} (hl : List.Nodup l) : Cycle.Nontrivial ↑l ↔ 2 ≤ List.length l

ink

@[simp]

theorem Cycle.nontrivial_reverse_iff {α : Type u_1} {s : Cycle α} : Cycle.Nontrivial (Cycle.reverse s) ↔ Cycle.Nontrivial s

ink

theorem Cycle.length_nontrivial {α : Type u_1} {s : Cycle α} (h : Cycle.Nontrivial s) : 2 ≤ Cycle.length s

ink

def Cycle.Nodup {α : Type u_1} (s : Cycle α) : Prop

The s : Cycle α contains no duplicates.

Equations

• Cycle.Nodup s = Quot.liftOn s List.Nodup (_ : ∀ (_l₁ _l₂ : List α), Setoid.r _l₁ _l₂ → List.Nodup _l₁ = List.Nodup _l₂)

ink

@[simp]

theorem Cycle.nodup_nil {α : Type u_1} : Cycle.Nodup Cycle.nil

ink

@[simp]

theorem Cycle.nodup_coe_iff {α : Type u_1} {l : List α} : Cycle.Nodup ↑l ↔ List.Nodup l

ink

@[simp]

theorem Cycle.nodup_reverse_iff {α : Type u_1} {s : Cycle α} : Cycle.Nodup (Cycle.reverse s) ↔ Cycle.Nodup s

ink

theorem Cycle.Subsingleton.nodup {α : Type u_1} {s : Cycle α} (h : Cycle.Subsingleton s) : Cycle.Nodup s

ink

theorem Cycle.Nodup.nontrivial_iff {α : Type u_1} {s : Cycle α} (h : Cycle.Nodup s) : Cycle.Nontrivial s ↔ ¬Cycle.Subsingleton s

ink

def Cycle.toMultiset {α : Type u_1} (s : Cycle α) : Multiset α

The s : Cycle α as a Multiset α.

Equations

• Cycle.toMultiset s = Quotient.liftOn' s Multiset.ofList (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → ↑x = ↑x_1)

ink

@[simp]

theorem Cycle.coe_toMultiset {α : Type u_1} (l : List α) : Cycle.toMultiset ↑l = ↑l

ink

@[simp]

theorem Cycle.nil_toMultiset {α : Type u_1} : Cycle.toMultiset Cycle.nil = 0

ink

@[simp]

theorem Cycle.card_toMultiset {α : Type u_1} (s : Cycle α) : ↑Multiset.card (Cycle.toMultiset s) = Cycle.length s

ink

@[simp]

theorem Cycle.toMultiset_eq_nil {α : Type u_1} {s : Cycle α} : Cycle.toMultiset s = 0 ↔ s = Cycle.nil

ink

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

The lift of list.map.

Equations

• Cycle.map f = Quotient.map' (List.map f) (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → List.map f x ~r List.map f x_1)

ink

@[simp]

theorem Cycle.map_nil {α : Type u_2} {β : Type u_1} (f : α → β) : Cycle.map f Cycle.nil = Cycle.nil

ink

@[simp]

theorem Cycle.map_coe {α : Type u_2} {β : Type u_1} (f : α → β) (l : List α) : Cycle.map f ↑l = ↑(List.map f l)

ink

@[simp]

theorem Cycle.map_eq_nil {α : Type u_2} {β : Type u_1} (f : α → β) (s : Cycle α) : Cycle.map f s = Cycle.nil ↔ s = Cycle.nil

ink

def Cycle.lists {α : Type u_1} (s : Cycle α) : Multiset (List α)

The Multiset of lists that can make the cycle.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Cycle.lists_coe {α : Type u_1} (l : List α) : Cycle.lists ↑l = ↑(List.cyclicPermutations l)

ink

@[simp]

theorem Cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : Cycle α} {l : List α} : l ∈ Cycle.lists s ↔ ↑l = s

ink

@[simp]

theorem Cycle.lists_nil {α : Type u_1} : Cycle.lists Cycle.nil = ↑[[]]

ink

def Cycle.decidableNontrivialCoe {α : Type u_1} [inst : DecidableEq α] (l : List α) : Decidable (Cycle.Nontrivial ↑l)

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.
• Cycle.decidableNontrivialCoe [] = isFalse (_ : ¬∃ x x_1 _h, x ∈ Cycle.nil ∧ x_1 ∈ Cycle.nil)
• Cycle.decidableNontrivialCoe [x_1] = isFalse (_ : ¬∃ x x_1 _h, x ∈ ↑[x_1] ∧ x_1 ∈ ↑[x_1])

ink

instance Cycle.instDecidableNontrivial {α : Type u_1} [inst : DecidableEq α] {s : Cycle α} : Decidable (Cycle.Nontrivial s)

Equations

• Cycle.instDecidableNontrivial = Quot.recOnSubsingleton' s Cycle.decidableNontrivialCoe

ink

instance Cycle.instDecidableNodup {α : Type u_1} [inst : DecidableEq α] {s : Cycle α} : Decidable (Cycle.Nodup s)

Equations

• Cycle.instDecidableNodup = Quot.recOnSubsingleton' s List.nodupDecidable

ink

instance Cycle.fintypeNodupCycle {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] : Fintype { s // Cycle.Nodup s }

Equations

• One or more equations did not get rendered due to their size.

ink

instance Cycle.fintypeNodupNontrivialCycle {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] : Fintype { s // Cycle.Nodup s ∧ Cycle.Nontrivial s }

Equations

• One or more equations did not get rendered due to their size.

ink

def Cycle.toFinset {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) : Finset α

The s : Cycle α as a Finset α.

Equations

• Cycle.toFinset s = Multiset.toFinset (Cycle.toMultiset s)

ink

@[simp]

theorem Cycle.toFinset_toMultiset {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) : Multiset.toFinset (Cycle.toMultiset s) = Cycle.toFinset s

ink

@[simp]

theorem Cycle.coe_toFinset {α : Type u_1} [inst : DecidableEq α] (l : List α) : Cycle.toFinset ↑l = List.toFinset l

ink

@[simp]

theorem Cycle.nil_toFinset {α : Type u_1} [inst : DecidableEq α] : Cycle.toFinset Cycle.nil = ∅

ink

@[simp]

theorem Cycle.toFinset_eq_nil {α : Type u_1} [inst : DecidableEq α] {s : Cycle α} : Cycle.toFinset s = ∅ ↔ s = Cycle.nil

ink

def Cycle.next {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s) : α

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Cycle.prev {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s) : α

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

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Cycle.prev_reverse_eq_next {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.prev (Cycle.reverse s) (_ : Cycle.Nodup (Cycle.reverse s)) x (_ : x ∈ Cycle.reverse s) = Cycle.next s hs x hx

ink

@[simp]

theorem Cycle.prev_reverse_eq_next' {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup (Cycle.reverse s)) (x : α) (hx : x ∈ Cycle.reverse s) : Cycle.prev (Cycle.reverse s) hs x hx = Cycle.next s (_ : Cycle.Nodup s) x (_ : x ∈ s)

ink

theorem Cycle.next_reverse_eq_prev {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.next (Cycle.reverse s) (_ : Cycle.Nodup (Cycle.reverse s)) x (_ : x ∈ Cycle.reverse s) = Cycle.prev s hs x hx

ink

@[simp]

theorem Cycle.next_reverse_eq_prev' {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup (Cycle.reverse s)) (x : α) (hx : x ∈ Cycle.reverse s) : Cycle.next (Cycle.reverse s) hs x hx = Cycle.prev s (_ : Cycle.Nodup s) x (_ : x ∈ s)

ink

@[simp]

theorem Cycle.next_mem {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.next s hs x hx ∈ s

ink

theorem Cycle.prev_mem {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.prev s hs x hx ∈ s

ink

@[simp]

theorem Cycle.prev_next {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.prev s hs (Cycle.next s hs x hx) (_ : Cycle.next s hs x hx ∈ s) = x

ink

@[simp]

theorem Cycle.next_prev {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : Cycle.Nodup s) (x : α) (hx : x ∈ s) : Cycle.next s hs (Cycle.prev s hs x hx) (_ : Cycle.prev s hs x hx ∈ s) = x

ink

unsafe instance Cycle.instReprCycle {α : Type u_1} [inst : Repr α] : Repr (Cycle α)

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.

Equations

• One or more equations did not get rendered due to their size.

ink

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↔ R a b ∧ R b c ∧ R c a∧ R b c ∧ R c a∧ R c a

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Cycle.Chain.nil {α : Type u_1} (r : α → α → Prop) : Cycle.Chain r Cycle.nil

ink

@[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])

ink

theorem Cycle.chain_singleton {α : Type u_1} (r : α → α → Prop) (a : α) : Cycle.Chain r ↑[a] ↔ r a a

ink

theorem Cycle.chain_ne_nil {α : Type u_1} (r : α → α → Prop) {l : List α} (hl : l ≠ []) : Cycle.Chain r ↑l ↔ List.Chain r (List.getLast l hl) l

ink

theorem Cycle.chain_map {α : Type u_2} {β : Type u_1} {r : α → α → Prop} (f : β → α) {s : Cycle β} : Cycle.Chain r (Cycle.map f s) ↔ Cycle.Chain (fun a b => r (f a) (f b)) s

ink

theorem Cycle.chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : Cycle.Chain r ↑(List.range (Nat.succ n)) ↔ r n 0 ∧ ((m : ℕ) → m < n → r m (Nat.succ m))

ink

theorem Cycle.chain_of_pairwise {α : Type u_1} {r : α → α → Prop} {s : Cycle α} : ((a : α) → a ∈ s → (b : α) → b ∈ s → r a b) → Cycle.Chain r s

ink

theorem Cycle.chain_iff_pairwise {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [inst : IsTrans α r] : Cycle.Chain r s ↔ (a : α) → a ∈ s → (b : α) → b ∈ s → r a b

ink

theorem Cycle.forall_eq_of_chain {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [inst : IsTrans α r] [inst : IsAntisymm α r] (hs : Cycle.Chain r s) {a : α} {b : α} (ha : a ∈ s) (hb : b ∈ s) : a = b