Mathlib.GroupTheory.Perm.List

List.formPerm definition

: Equiv.Perm α

Full source

/-- A list `l : List α` can be interpreted as an `Equiv.Perm α` where each element in the list
is permuted to the next one, defined as `formPerm`. When we have that `Nodup l`,
we prove that `Equiv.Perm.support (formPerm l) = l.toFinset`, and that
`formPerm l` is rotationally invariant, in `formPerm_rotate`.
-/
def formPerm : Equiv.Perm α :=
  (zipWith Equiv.swap l l.tail).prod

Permutation from a list via adjacent transpositions

Informal description

Given a list `l : List α`, the permutation `formPerm l` is defined as the product of transpositions swapping each element in the list with its next element. Specifically, for a list `[x₁, x₂, ..., xₙ]`, the permutation is the composition of swaps `(x₁ x₂) ∘ (x₂ x₃) ∘ ... ∘ (xₙ₋₁ xₙ)`. When the list has no duplicates (`Nodup l`), the support of the permutation `formPerm l` is exactly the set of elements in `l`, and the permutation is invariant under rotation of the list. For lists with duplicates, the permutation depends on the arrangement of duplicates. Adjacent duplicates (e.g., `[..., x, x, ...]`) do not affect the resulting permutation, as the corresponding swap would be the identity. This definition is primarily intended for use with duplicate-free lists, where the resulting permutation is cyclic (provided the list has at least two elements). The presence of duplicates in certain arrangements can lead to non-cyclic permutations.

List.formPerm_nil theorem

: formPerm ([] : List α) = 1

Full source

@[simp]
theorem formPerm_nil : formPerm ([] : List α) = 1 :=
  rfl

Empty List Yields Identity Permutation

Informal description

The permutation formed from the empty list is the identity permutation, i.e., $\text{formPerm}([]) = 1$.

List.formPerm_singleton theorem

(x : α) : formPerm [x] = 1

Full source

@[simp]
theorem formPerm_singleton (x : α) : formPerm [x] = 1 :=
  rfl

Identity Permutation from Singleton List

Informal description

For any element $x$ of type $\alpha$, the permutation formed from the singleton list $[x]$ is the identity permutation.

List.formPerm_cons_cons theorem

(x y : α) (l : List α) : formPerm (x :: y :: l) = swap x y * formPerm (y :: l)

Full source

@[simp]
theorem formPerm_cons_cons (x y : α) (l : List α) :
    formPerm (x :: y :: l) = swap x y * formPerm (y :: l) :=
  prod_cons

Recursive construction of permutation from a list with head and next element

Informal description

For any elements $x, y$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the permutation formed from the list $x :: y :: l$ is equal to the composition of the transposition swapping $x$ and $y$ with the permutation formed from the list $y :: l$. In other words, \[ \text{formPerm}(x :: y :: l) = (x\ y) \circ \text{formPerm}(y :: l). \]

List.formPerm_pair theorem

(x y : α) : formPerm [x, y] = swap x y

Full source

theorem formPerm_pair (x y : α) : formPerm [x, y] = swap x y :=
  rfl

Permutation of a Two-Element List is a Transposition

Informal description

For any two elements $x$ and $y$ of type $\alpha$, the permutation formed from the list $[x, y]$ is equal to the transposition swapping $x$ and $y$, i.e., $\text{formPerm}([x, y]) = \text{swap}(x, y)$.

List.mem_or_mem_of_zipWith_swap_prod_ne theorem

: ∀ {l l' : List α} {x : α}, (zipWith swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'

Full source

theorem mem_or_mem_of_zipWith_swap_prod_ne : ∀ {l l' : List α} {x : α},
    (zipWith swap l l').prod x ≠ x → x ∈ lx ∈ l ∨ x ∈ l'
  | [], _, _ => by simp
  | _, [], _ => by simp
  | a::l, b::l', x => fun hx ↦
    if h : (zipWith swap l l').prod x = x then
      (eq_or_eq_of_swap_apply_ne_self (a := a) (b := b) (x := x) (by simpa [h] using hx)).imp
        (by rintro rfl; exact .head _) (by rintro rfl; exact .head _)
    else
     (mem_or_mem_of_zipWith_swap_prod_ne h).imp (.tail _) (.tail _)

Non-fixed Point in Permutation Product Implies Membership in One of the Lists

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$ and any element $x \in \alpha$, if the permutation obtained as the product of transpositions formed by `zipWith swap l l'` does not fix $x$ (i.e., $( \text{zipWith swap } l\ l' ).\text{prod}\ x \neq x$), then $x$ must belong to either $l$ or $l'$.

List.zipWith_swap_prod_support' theorem

(l l' : List α) : {x | (zipWith swap l l').prod x ≠ x} ≤ l.toFinset ⊔ l'.toFinset

Full source

theorem zipWith_swap_prod_support' (l l' : List α) :
    { x | (zipWith swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := fun _ h ↦ by
  simpa using mem_or_mem_of_zipWith_swap_prod_ne h

Support of Permutation Product from Zipped Transpositions is Contained in List Union

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the set of elements $x$ that are not fixed by the permutation obtained as the product of transpositions formed by `zipWith swap l l'` is contained in the union of the sets of elements from $l$ and $l'$. In other words, $\{x \mid (\text{zipWith swap } l\ l').\text{prod}\ x \neq x\} \subseteq l.\text{toFinset} \cup l'.\text{toFinset}$.

List.zipWith_swap_prod_support theorem

[Fintype α] (l l' : List α) : (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset

Full source

theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) :
    (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset := by
  intro x hx
  have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
  simpa using zipWith_swap_prod_support' _ _ hx'

Support of Permutation Product from Zipped Transpositions is Contained in List Union (Finite Case)

Informal description

For any two lists $l$ and $l'$ of elements of a finite type $\alpha$, the support of the permutation obtained as the product of transpositions formed by `zipWith swap l l'` is contained in the union of the sets of elements from $l$ and $l'$. In other words, $\text{support}((\text{zipWith swap } l\ l').\text{prod}) \subseteq l.\text{toFinset} \cup l'.\text{toFinset}$.

List.support_formPerm_le' theorem

: {x | formPerm l x ≠ x} ≤ l.toFinset

Full source

theorem support_formPerm_le' : { x | formPerm l x ≠ x } ≤ l.toFinset := by
  refine (zipWith_swap_prod_support' l l.tail).trans ?_
  simpa [Finset.subset_iff] using tail_subset l

Support of `formPerm` is Contained in List Elements

Informal description

For any list $l$ of elements of type $\alpha$, the set of elements not fixed by the permutation $\text{formPerm } l$ is contained in the set of elements of $l$. In other words, $\{x \mid \text{formPerm } l\ x \neq x\} \subseteq l.\text{toFinset}$.

List.support_formPerm_le theorem

[Fintype α] : support (formPerm l) ≤ l.toFinset

Full source

theorem support_formPerm_le [Fintype α] : support (formPerm l) ≤ l.toFinset := by
  intro x hx
  have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
  simpa using support_formPerm_le' _ hx'

Support of Permutation from List is Contained in List Elements (Finite Case)

Informal description

For any list $l$ of elements of a finite type $\alpha$, the support of the permutation $\text{formPerm } l$ is contained in the set of elements of $l$. In other words, $\text{support}(\text{formPerm } l) \subseteq l.\text{toFinset}$.

List.mem_of_formPerm_apply_ne theorem

(h : l.formPerm x ≠ x) : x ∈ l

Full source

theorem mem_of_formPerm_apply_ne (h : l.formPerm x ≠ x) : x ∈ l := by
  simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

Non-fixed Point in `formPerm` Implies Membership in List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if the permutation `formPerm l` does not fix $x$ (i.e., $\text{formPerm } l\ x \neq x$), then $x$ must belong to $l$.

List.formPerm_apply_of_not_mem theorem

(h : x ∉ l) : formPerm l x = x

Full source

theorem formPerm_apply_of_not_mem (h : x ∉ l) : formPerm l x = x :=
  not_imp_comm.1 mem_of_formPerm_apply_ne h

Fixed Points of `formPerm` Outside the List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if $x$ does not belong to $l$, then the permutation $\text{formPerm } l$ fixes $x$, i.e., $\text{formPerm } l\ x = x$.

List.formPerm_apply_mem_of_mem theorem

(h : x ∈ l) : formPerm l x ∈ l

Full source

theorem formPerm_apply_mem_of_mem (h : x ∈ l) : formPermformPerm l x ∈ l := by
  rcases l with - | ⟨y, l⟩
  · simp at h
  induction' l with z l IH generalizing x y
  · simpa using h
  · by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp [IH _ hx]
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_not_mem hx, ← h]

Permutation $\text{formPerm } l$ Preserves Membership in $l$

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if $x$ belongs to $l$, then the image of $x$ under the permutation $\text{formPerm } l$ also belongs to $l$. In other words, $\text{formPerm } l\ x \in l$ whenever $x \in l$.

List.mem_of_formPerm_apply_mem theorem

(h : l.formPerm x ∈ l) : x ∈ l

Full source

theorem mem_of_formPerm_apply_mem (h : l.formPerm x ∈ l) : x ∈ l := by
  contrapose h
  rwa [formPerm_apply_of_not_mem h]

Preimage of List under `formPerm` is Contained in List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if the permutation $\text{formPerm } l$ maps $x$ to an element in $l$, then $x$ must belong to $l$. In other words, if $\text{formPerm } l(x) \in l$, then $x \in l$.

List.formPerm_mem_iff_mem theorem

: l.formPerm x ∈ l ↔ x ∈ l

Full source

@[simp]
theorem formPerm_mem_iff_mem : l.formPerm x ∈ ll.formPerm x ∈ l ↔ x ∈ l :=
  ⟨l.mem_of_formPerm_apply_mem, l.formPerm_apply_mem_of_mem⟩

Membership Equivalence under List Permutation: $\text{formPerm } l(x) \in l \leftrightarrow x \in l$

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, the image of $x$ under the permutation $\text{formPerm } l$ belongs to $l$ if and only if $x$ belongs to $l$. In other words, $\text{formPerm } l(x) \in l \leftrightarrow x \in l$.

List.formPerm_cons_concat_apply_last theorem

(x y : α) (xs : List α) : formPerm (x :: (xs ++ [y])) y = x

Full source

@[simp]
theorem formPerm_cons_concat_apply_last (x y : α) (xs : List α) :
    formPerm (x :: (xs ++ [y])) y = x := by
  induction' xs with z xs IH generalizing x y
  · simp
  · simp [IH]

Permutation of Extended List Maps Last Element to First

Informal description

For any elements $x, y$ of type $\alpha$ and any list $xs$ of elements of type $\alpha$, the permutation `formPerm` applied to the list $x :: (xs ++ [y])$ maps the last element $y$ back to the first element $x$. That is, $\text{formPerm}(x :: (xs ++ [y]))(y) = x$.

List.formPerm_apply_getLast theorem

(x : α) (xs : List α) : formPerm (x :: xs) ((x :: xs).getLast (cons_ne_nil x xs)) = x

Full source

@[simp]
theorem formPerm_apply_getLast (x : α) (xs : List α) :
    formPerm (x :: xs) ((x :: xs).getLast (cons_ne_nil x xs)) = x := by
  induction' xs using List.reverseRecOn with xs y _ generalizing x <;> simp

Permutation Maps Last Element to First in Extended List

Informal description

For any element $x$ of type $\alpha$ and any list $xs$ of elements of type $\alpha$, the permutation $\text{formPerm}(x :: xs)$ maps the last element of the list $x :: xs$ back to the first element $x$. That is, $\text{formPerm}(x :: xs)(\text{last}(x :: xs)) = x$, where $\text{last}(x :: xs)$ denotes the last element of the list $x :: xs$.

List.formPerm_apply_getElem_length theorem

(x : α) (xs : List α) : formPerm (x :: xs) (x :: xs)[xs.length] = x

Full source

@[simp]
theorem formPerm_apply_getElem_length (x : α) (xs : List α) :
    formPerm (x :: xs) (x :: xs)[xs.length] = x := by
  rw [getElem_cons_length rfl, formPerm_apply_getLast]

Permutation Maps Last Element to First via Index Access

Informal description

For any element $x$ of type $\alpha$ and any list $xs$ of elements of type $\alpha$, the permutation $\text{formPerm}(x :: xs)$ maps the element at index $\text{length}(xs)$ (i.e., the last element) of the list $x :: xs$ back to the first element $x$. That is, $\text{formPerm}(x :: xs)((x :: xs)[\text{length}(xs)]) = x$.

List.formPerm_apply_head theorem

(x y : α) (xs : List α) (h : Nodup (x :: y :: xs)) : formPerm (x :: y :: xs) x = y

Full source

theorem formPerm_apply_head (x y : α) (xs : List α) (h : Nodup (x :: y :: xs)) :
    formPerm (x :: y :: xs) x = y := by simp [formPerm_apply_of_not_mem h.not_mem]

Permutation Maps First Element to Second in Duplicate-Free List

Informal description

For any distinct elements $x, y$ of type $\alpha$ and any list $xs$ of elements of type $\alpha$, if the list $x :: y :: xs$ has no duplicates, then the permutation $\text{formPerm}(x :: y :: xs)$ maps $x$ to $y$. That is, $\text{formPerm}(x :: y :: xs)(x) = y$.

List.formPerm_apply_getElem_zero theorem

(l : List α) (h : Nodup l) (hl : 1 < l.length) : formPerm l l[0] = l[1]

Full source

theorem formPerm_apply_getElem_zero (l : List α) (h : Nodup l) (hl : 1 < l.length) :
    formPerm l l[0] = l[1] := by
  rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
  · simp at hl
  · simp at hl
  · rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

Permutation Maps First to Second Element in Duplicate-Free List

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$ with length at least 2, the permutation $\text{formPerm}(l)$ maps the first element $l[0]$ to the second element $l[1]$. That is, $\text{formPerm}(l)(l[0]) = l[1]$.

List.formPerm_eq_head_iff_eq_getLast theorem

(x y : α) : formPerm (y :: l) x = y ↔ x = getLast (y :: l) (cons_ne_nil _ _)

Full source

theorem formPerm_eq_head_iff_eq_getLast (x y : α) :
    formPermformPerm (y :: l) x = y ↔ x = getLast (y :: l) (cons_ne_nil _ _) :=
  Iff.trans (by rw [formPerm_apply_getLast]) (formPerm (y :: l)).injective.eq_iff

Permutation Maps to Head if and only if Input is Last Element

Informal description

For any elements $x, y$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the permutation $\text{formPerm}(y :: l)$ maps $x$ to $y$ if and only if $x$ is the last element of the list $y :: l$. That is, $\text{formPerm}(y :: l)(x) = y \leftrightarrow x = \text{last}(y :: l)$, where $\text{last}(y :: l)$ denotes the last element of the list $y :: l$.

List.formPerm_apply_lt_getElem theorem

(xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) : formPerm xs xs[n] = xs[n + 1]

Full source

theorem formPerm_apply_lt_getElem (xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) :
    formPerm xs xs[n] = xs[n + 1] := by
  induction' n with n IH generalizing xs
  · simpa using formPerm_apply_getElem_zero _ h _
  · rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
    · simp at hn
    · rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
    · specialize IH (y :: l) h.of_cons _
      · simpa [Nat.succ_lt_succ_iff] using hn
      simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]
      simp only [getElem_cons_succ] at *
      rw [← IH, swap_apply_of_ne_of_ne] <;>
      · intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

Permutation Maps $n$-th Element to $(n+1)$-th Element in Duplicate-Free List

Informal description

For any duplicate-free list $xs$ of elements of type $\alpha$, and any natural number $n$ such that $n + 1$ is less than the length of $xs$, the permutation $\text{formPerm}(xs)$ maps the $n$-th element $xs[n]$ to the $(n+1)$-th element $xs[n+1]$. That is, $\text{formPerm}(xs)(xs[n]) = xs[n+1]$.

List.formPerm_apply_getElem theorem

 (xs : List α) (w : Nodup xs) (i : ℕ) (h : i < xs.length) :
  formPerm xs xs[i] = xs[(i + 1) % xs.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h))

Full source

theorem formPerm_apply_getElem (xs : List α) (w : Nodup xs) (i : ℕ) (h : i < xs.length) :
    formPerm xs xs[i] =
      xs[(i + 1) % xs.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h)) := by
  rcases xs with - | ⟨x, xs⟩
  · simp at h
  · have : i ≤ xs.length := by
      refine Nat.le_of_lt_succ ?_
      simpa using h
    rcases this.eq_or_lt with (rfl | hn')
    · simp
    · rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]
      congr
      rw [Nat.mod_eq_of_lt]; simpa [Nat.succ_eq_add_one]

Cyclic Permutation Action on Duplicate-Free List Elements

Informal description

For any duplicate-free list $xs$ of elements of type $\alpha$, and any natural number $i$ such that $i$ is less than the length of $xs$, the permutation $\text{formPerm}(xs)$ maps the $i$-th element $xs[i]$ to the element at index $(i + 1) \bmod \text{length}(xs)$. That is, $\text{formPerm}(xs)(xs[i]) = xs[(i + 1) \bmod \text{length}(xs)]$.

List.support_formPerm_of_nodup' theorem

(l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) : {x | formPerm l x ≠ x} = l.toFinset

Full source

theorem support_formPerm_of_nodup' (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
    { x | formPerm l x ≠ x } = l.toFinset := by
  apply _root_.le_antisymm
  · exact support_formPerm_le' l
  · intro x hx
    simp only [Finset.mem_coe, mem_toFinset] at hx
    obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
    rw [Set.mem_setOf_eq, formPerm_apply_getElem _ h]
    intro H
    rw [nodup_iff_injective_get, Function.Injective] at h
    specialize h H
    rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
    · simp only [← hn', Nat.mod_self] at h
      refine not_exists.mpr h' ?_
      rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
    · simp [Nat.mod_eq_of_lt hn'] at h

Support of `formPerm` Equals List Elements for Nontrivial Duplicate-Free Lists

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$ that is not a singleton (i.e., $l \neq [x]$ for any $x \in \alpha$), the set of elements moved by the permutation $\text{formPerm}(l)$ is exactly the set of elements in $l$. That is, $\{x \mid \text{formPerm}(l)(x) \neq x\} = l.\text{toFinset}$.

List.support_formPerm_of_nodup theorem

[Fintype α] (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) : support (formPerm l) = l.toFinset

Full source

theorem support_formPerm_of_nodup [Fintype α] (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
    support (formPerm l) = l.toFinset := by
  rw [← Finset.coe_inj]
  convert support_formPerm_of_nodup' _ h h'
  simp [Set.ext_iff]

Support of Permutation from Duplicate-Free List Equals Its Elements

Informal description

For any duplicate-free list $l$ of elements in a finite type $\alpha$, where $l$ is not a singleton list (i.e., $l \neq [x]$ for any $x \in \alpha$), the support of the permutation $\text{formPerm}(l)$ is equal to the set of elements in $l$. That is, $\text{support}(\text{formPerm}(l)) = l.\text{toFinset}$.

List.formPerm_rotate_one theorem

(l : List α) (h : Nodup l) : formPerm (l.rotate 1) = formPerm l

Full source

theorem formPerm_rotate_one (l : List α) (h : Nodup l) : formPerm (l.rotate 1) = formPerm l := by
  have h' : Nodup (l.rotate 1) := by simpa using h
  ext x
  by_cases hx : x ∈ l.rotate 1
  · obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]
    simp
  · rw [formPerm_apply_of_not_mem hx, formPerm_apply_of_not_mem]
    simpa using hx

Rotational Invariance of `formPerm` for Duplicate-Free Lists

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$, the permutation formed by rotating $l$ by one position is equal to the permutation formed by $l$ itself, i.e., $\text{formPerm}(l.\text{rotate } 1) = \text{formPerm } l$.

List.formPerm_rotate theorem

(l : List α) (h : Nodup l) (n : ℕ) : formPerm (l.rotate n) = formPerm l

Full source

theorem formPerm_rotate (l : List α) (h : Nodup l) (n : ℕ) :
    formPerm (l.rotate n) = formPerm l := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n

Rotational Invariance of `formPerm` for Duplicate-Free Lists under Arbitrary Rotation

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$ and any natural number $n$, the permutation formed by rotating $l$ by $n$ positions is equal to the permutation formed by $l$ itself, i.e., $\text{formPerm}(l.\text{rotate } n) = \text{formPerm } l$.

List.formPerm_eq_of_isRotated theorem

{l l' : List α} (hd : Nodup l) (h : l ~r l') : formPerm l = formPerm l'

Full source

theorem formPerm_eq_of_isRotated {l l' : List α} (hd : Nodup l) (h : l ~r l') :
    formPerm l = formPerm l' := by
  obtain ⟨n, rfl⟩ := h
  exact (formPerm_rotate l hd n).symm

Equality of `formPerm` for Rotated Duplicate-Free Lists

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ has no duplicates and $l$ is a rotation of $l'$ (denoted $l \sim_r l'$), then the permutations formed from $l$ and $l'$ are equal, i.e., $\text{formPerm}(l) = \text{formPerm}(l')$.

List.formPerm_append_pair theorem

: ∀ (l : List α) (a b : α), formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b

Full source

theorem formPerm_append_pair : ∀ (l : List α) (a b : α),
    formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b
  | [], _, _ => rfl
  | [_], _, _ => rfl
  | x::y::l, a, b => by
    simpa [mul_assoc] using formPerm_append_pair (y::l) a b

Permutation from List Concatenation with Pair Equals Composition with Swap

Informal description

For any list $l$ of elements of type $\alpha$ and any two elements $a, b \in \alpha$, the permutation formed from the list $l \mathbin{+\kern-1.5ex+} [a, b]$ (i.e., $l$ concatenated with $[a, b]$) is equal to the composition of the permutation formed from $l \mathbin{+\kern-1.5ex+} [a]$ with the transposition swapping $a$ and $b$. In other words, \[ \text{formPerm}(l \mathbin{+\kern-1.5ex+} [a, b]) = \text{formPerm}(l \mathbin{+\kern-1.5ex+} [a]) \circ (a\ b). \]

List.formPerm_reverse theorem

: ∀ l : List α, formPerm l.reverse = (formPerm l)⁻¹

Full source

theorem formPerm_reverse : ∀ l : List α, formPerm l.reverse = (formPerm l)⁻¹
  | [] => rfl
  | [_] => rfl
  | a::b::l => by
    simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)]

Permutation from Reversed List Equals Inverse Permutation

Informal description

For any list $l$ of elements of type $\alpha$, the permutation formed from the reversed list $l^{\text{reverse}}$ is equal to the inverse of the permutation formed from $l$. That is, \[ \text{formPerm}(l^{\text{reverse}}) = (\text{formPerm}(l))^{-1}. \]

List.formPerm_pow_apply_getElem theorem

 (l : List α) (w : Nodup l) (n : ℕ) (i : ℕ) (h : i < l.length) :
  (formPerm l ^ n) l[i] = l[(i + n) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h))

Full source

theorem formPerm_pow_apply_getElem (l : List α) (w : Nodup l) (n : ℕ) (i : ℕ) (h : i < l.length) :
    (formPerm l ^ n) l[i] =
      l[(i + n) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h)) := by
  induction n with
  | zero => simp [Nat.mod_eq_of_lt h]
  | succ n hn =>
    simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w, Nat.succ_eq_add_one,
      ← Nat.add_assoc]

Cyclic Permutation Power Action on List Elements: $(\text{formPerm}(l))^n(l[i]) = l[(i + n) \bmod \text{length}(l)]$

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$, any natural number $n$, and any index $i$ such that $i < \text{length}(l)$, the $n$-th power of the permutation $\text{formPerm}(l)$ maps the $i$-th element $l[i]$ to the element at index $(i + n) \bmod \text{length}(l)$. That is, \[ (\text{formPerm}(l))^n(l[i]) = l[(i + n) \bmod \text{length}(l)]. \]

List.formPerm_pow_apply_head theorem

 (x : α) (l : List α) (h : Nodup (x :: l)) (n : ℕ) :
  (formPerm (x :: l) ^ n) x = (x :: l)[(n % (x :: l).length)]'(Nat.mod_lt _ (Nat.zero_lt_succ _))

Full source

theorem formPerm_pow_apply_head (x : α) (l : List α) (h : Nodup (x :: l)) (n : ℕ) :
    (formPerm (x :: l) ^ n) x =
      (x :: l)[(n % (x :: l).length)]'(Nat.mod_lt _ (Nat.zero_lt_succ _)) := by
  convert formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)
  simp

Cyclic Permutation Power Action on Head Element: $(\text{formPerm}(x :: l))^n(x) = (x :: l)[n \bmod \text{length}(x :: l)]$

Informal description

For any element $x$ of type $\alpha$, any list $l$ of elements of type $\alpha$ such that the list $x :: l$ has no duplicates, and any natural number $n$, the $n$-th power of the permutation $\text{formPerm}(x :: l)$ maps $x$ to the element at index $n \bmod \text{length}(x :: l)$ in the list $x :: l$. That is, \[ (\text{formPerm}(x :: l))^n(x) = (x :: l)[n \bmod \text{length}(x :: l)]. \]

List.formPerm_ext_iff theorem

 {x y x' y' : α} {l l' : List α} (hd : Nodup (x :: y :: l)) (hd' : Nodup (x' :: y' :: l')) :
  formPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l')

Full source

theorem formPerm_ext_iff {x y x' y' : α} {l l' : List α} (hd : Nodup (x :: y :: l))
    (hd' : Nodup (x' :: y' :: l')) :
    formPermformPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l') := by
  refine ⟨fun h => ?_, fun hr => formPerm_eq_of_isRotated hd hr⟩
  rw [Equiv.Perm.ext_iff] at h
  have hx : x' ∈ x :: y :: l := by
    have : x' ∈ { z | formPerm (x :: y :: l) z ≠ z } := by
      rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
      simp only [mem_cons, nodup_cons] at hd'
      push_neg at hd'
      exact hd'.left.left.symm
    simpa using support_formPerm_le' _ this
  obtain ⟨⟨n, hn⟩, hx'⟩ := get_of_mem hx
  have hl : (x :: y :: l).length = (x' :: y' :: l').length := by
    rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
    refine congr_arg Finset.card ?_
    rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
      support_formPerm_of_nodup' _ hd' (by simp)]
    simp only [h]
  use n
  apply List.ext_getElem
  · rw [length_rotate, hl]
  · intro k hk hk'
    rw [getElem_rotate]
    induction' k with k IH
    · refine Eq.trans ?_ hx'
      congr
      simpa using hn
    · conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
      rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]
      congr 1
      rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
      apply Nat.add_mod

Equality of `formPerm` for Duplicate-Free Lists is Equivalent to Rotational Equivalence

Informal description

For any elements $x, y, x', y'$ of type $\alpha$ and any lists $l, l'$ of elements of type $\alpha$, if both lists $x :: y :: l$ and $x' :: y' :: l'$ are duplicate-free, then the permutations $\text{formPerm}(x :: y :: l)$ and $\text{formPerm}(x' :: y' :: l')$ are equal if and only if the two lists are rotations of each other, i.e., $x :: y :: l \sim_r x' :: y' :: l'$.

List.formPerm_apply_mem_eq_self_iff theorem

(hl : Nodup l) (x : α) (hx : x ∈ l) : formPerm l x = x ↔ length l ≤ 1

Full source

theorem formPerm_apply_mem_eq_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) :
    formPermformPerm l x = x ↔ length l ≤ 1 := by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]
  cases hn : l.length
  · exact absurd k.zero_le (hk.trans_le hn.le).not_le
  · rw [hn] at hk
    rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
    · simp [← hk', Nat.succ_le_succ_iff, eq_comm]
    · simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
        (k.zero_le.trans_lt hk').ne.symm

Fixed Points of `formPerm` on Duplicate-Free Lists

Informal description

For a duplicate-free list $l$ of elements of type $\alpha$ and an element $x \in l$, the permutation $\text{formPerm}(l)$ fixes $x$ (i.e., $\text{formPerm}(l)(x) = x$) if and only if the length of $l$ is at most 1.

List.formPerm_apply_mem_ne_self_iff theorem

(hl : Nodup l) (x : α) (hx : x ∈ l) : formPerm l x ≠ x ↔ 2 ≤ l.length

Full source

theorem formPerm_apply_mem_ne_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) :
    formPermformPerm l x ≠ xformPerm l x ≠ x ↔ 2 ≤ l.length := by
  rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
  exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

Non-fixed Points Condition for `formPerm` on Duplicate-Free Lists

Informal description

For a duplicate-free list $l$ of elements of type $\alpha$ and an element $x \in l$, the permutation $\text{formPerm}(l)$ does not fix $x$ (i.e., $\text{formPerm}(l)(x) \neq x$) if and only if the length of $l$ is at least 2.

List.mem_of_formPerm_ne_self theorem

(l : List α) (x : α) (h : formPerm l x ≠ x) : x ∈ l

Full source

theorem mem_of_formPerm_ne_self (l : List α) (x : α) (h : formPermformPerm l x ≠ x) : x ∈ l := by
  suffices x ∈ { y | formPerm l y ≠ y } by
    rw [← mem_toFinset]
    exact support_formPerm_le' _ this
  simpa using h

Non-fixed Points of `formPerm` Belong to the List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if the permutation $\text{formPerm } l$ does not fix $x$ (i.e., $\text{formPerm } l\ x \neq x$), then $x$ must be an element of $l$.

List.formPerm_eq_self_of_not_mem theorem

(l : List α) (x : α) (h : x ∉ l) : formPerm l x = x

Full source

theorem formPerm_eq_self_of_not_mem (l : List α) (x : α) (h : x ∉ l) : formPerm l x = x :=
  by_contra fun H => h <| mem_of_formPerm_ne_self _ _ H

`formPerm` Fixes Elements Outside the List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, if $x$ does not belong to $l$, then the permutation $\text{formPerm } l$ fixes $x$, i.e., $\text{formPerm } l\ x = x$.

List.formPerm_eq_one_iff theorem

(hl : Nodup l) : formPerm l = 1 ↔ l.length ≤ 1

Full source

theorem formPerm_eq_one_iff (hl : Nodup l) : formPermformPerm l = 1 ↔ l.length ≤ 1 := by
  rcases l with - | ⟨hd, tl⟩
  · simp
  · rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]
    constructor
    · simp +contextual
    · intro h
      simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h
      simp [h]

Identity Condition for `formPerm` on Duplicate-Free Lists: $\text{formPerm}(l) = 1 \leftrightarrow |l| \leq 1$

Informal description

For a duplicate-free list $l$ of elements of type $\alpha$, the permutation $\text{formPerm}(l)$ is the identity permutation if and only if the length of $l$ is at most 1.

List.formPerm_eq_formPerm_iff theorem

 {l l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) : l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

Full source

theorem formPerm_eq_formPerm_iff {l l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) :
    l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1 := by
  rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
  · suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]
    refine ⟨fun h => Or.inr h, ?_⟩
    rintro (rfl | h)
    · simp
    · exact h
  · suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]
    refine ⟨fun h => Or.inr h, ?_⟩
    rintro (h | h)
    · simp [← h.perm.length_eq]
    · exact h
  · rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
    · simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
    · simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
    · simp [-formPerm_cons_cons, formPerm_ext_iff hl hl', Nat.succ_le_succ_iff]

Equality of `formPerm` for Duplicate-Free Lists is Equivalent to Rotational Equivalence or Triviality

Informal description

For any two duplicate-free lists $l$ and $l'$ of elements of type $\alpha$, the permutations $\text{formPerm}(l)$ and $\text{formPerm}(l')$ are equal if and only if either: 1. $l$ and $l'$ are rotations of each other (i.e., $l \sim_r l'$), or 2. Both lists have length at most 1 (i.e., $|l| \leq 1$ and $|l'| \leq 1$).

List.form_perm_zpow_apply_mem_imp_mem theorem

(l : List α) (x : α) (hx : x ∈ l) (n : ℤ) : (formPerm l ^ n) x ∈ l

Full source

theorem form_perm_zpow_apply_mem_imp_mem (l : List α) (x : α) (hx : x ∈ l) (n : ℤ) :
    (formPerm l ^ n) x ∈ l := by
  by_cases h : (l.formPerm ^ n) x = x
  · simpa [h] using hx
  · have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
    rw [← set_support_apply_mem] at h
    replace h := set_support_zpow_subset _ _ h
    simpa using support_formPerm_le' _ h

Invariance of List Elements under Powers of `formPerm`

Informal description

For any list $l$ of elements of type $\alpha$, if an element $x$ is in $l$, then for any integer power $n$, the element obtained by applying the $n$-th power of the permutation $\text{formPerm } l$ to $x$ is also in $l$. In other words, $(\text{formPerm } l)^n(x) \in l$ for all $x \in l$ and $n \in \mathbb{Z}$.

List.formPerm_pow_length_eq_one_of_nodup theorem

(hl : Nodup l) : formPerm l ^ length l = 1

Full source

theorem formPerm_pow_length_eq_one_of_nodup (hl : Nodup l) : formPerm l ^ length l = 1 := by
  ext x
  by_cases hx : x ∈ l
  · obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]
  · have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
    simpa using this

Order of Permutation from Duplicate-Free List Equals List Length

Informal description

For any duplicate-free list $l$ of elements of type $\alpha$, the permutation $\text{formPerm}(l)$ raised to the power of the length of $l$ is the identity permutation, i.e., \[ (\text{formPerm}(l))^{\text{length}(l)} = 1. \]