Documentation

Init.Data.List.Perm

List Permutations #

This file introduces the List.Perm relation, which is true if two lists are permutations of one another.

Notation #

The notation ~ is used for permutation equivalence.

@[simp]
theorem List.Perm.refl {α : Type u_1} (l : List α) :
l.Perm l
theorem List.Perm.rfl {α : Type u_1} {l : List α} :
l.Perm l
theorem List.Perm.of_eq {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ = l₂) :
l₁.Perm l₂
theorem List.Perm.symm {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) :
l₂.Perm l₁
instance List.instTransPerm {α : Type u_1} :
Equations
    theorem List.perm_comm {α : Type u_1} {l₁ l₂ : List α} :
    l₁.Perm l₂ l₂.Perm l₁
    theorem List.Perm.congr_left {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) (l₃ : List α) :
    l₁.Perm l₃ l₂.Perm l₃
    theorem List.Perm.congr_right {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) (l₃ : List α) :
    l₃.Perm l₁ l₃.Perm l₂
    theorem List.Perm.swap' {α : Type u_1} (x y : α) {l₁ l₂ : List α} (p : l₁.Perm l₂) :
    (y :: x :: l₁).Perm (x :: y :: l₂)
    theorem List.Perm.recOnSwap' {α : Type u_1} {motive : (l₁ l₂ : List α) → l₁.Perm l₂Prop} {l₁ l₂ : List α} (p : l₁.Perm l₂) (nil : motive [] [] ) (cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ hmotive (x :: l₁) (x :: l₂) ) (swap' : ∀ (x y : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ hmotive (y :: x :: l₁) (x :: y :: l₂) ) (trans : ∀ {l₁ l₂ l₃ : List α} (h₁ : l₁.Perm l₂) (h₂ : l₂.Perm l₃), motive l₁ l₂ h₁motive l₂ l₃ h₂motive l₁ l₃ ) :
    motive l₁ l₂ p

    Similar to Perm.recOn, but the swap case is generalized to Perm.swap', where the tail of the lists are not necessarily the same.

    instance List.isSetoid (α : Type u_1) :
    Equations
      theorem List.Perm.mem_iff {α : Type u_1} {a : α} {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      a l₁ a l₂
      theorem List.Perm.subset {α : Type u_1} {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      l₁ l₂
      theorem List.Perm.append_right {α : Type u_1} {l₁ l₂ : List α} (t₁ : List α) (p : l₁.Perm l₂) :
      (l₁ ++ t₁).Perm (l₂ ++ t₁)
      theorem List.Perm.append_left {α : Type u_1} {t₁ t₂ : List α} (l : List α) :
      t₁.Perm t₂(l ++ t₁).Perm (l ++ t₂)
      theorem List.Perm.append {α : Type u_1} {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) :
      (l₁ ++ t₁).Perm (l₂ ++ t₂)
      theorem List.Perm.append_cons {α : Type u_1} (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : r₁.Perm r₂) :
      (l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂)
      @[simp]
      theorem List.perm_middle {α : Type u_1} {a : α} {l₁ l₂ : List α} :
      (l₁ ++ a :: l₂).Perm (a :: (l₁ ++ l₂))
      @[simp]
      theorem List.perm_append_singleton {α : Type u_1} (a : α) (l : List α) :
      (l ++ [a]).Perm (a :: l)
      theorem List.perm_append_comm {α : Type u_1} {l₁ l₂ : List α} :
      (l₁ ++ l₂).Perm (l₂ ++ l₁)
      theorem List.perm_append_comm_assoc {α : Type u_1} (l₁ l₂ l₃ : List α) :
      (l₁ ++ (l₂ ++ l₃)).Perm (l₂ ++ (l₁ ++ l₃))
      theorem List.concat_perm {α : Type u_1} (l : List α) (a : α) :
      (l.concat a).Perm (a :: l)
      theorem List.Perm.length_eq {α : Type u_1} {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      l₁.length = l₂.length
      theorem List.Perm.contains_eq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁.Perm l₂) {a : α} :
      l₁.contains a = l₂.contains a
      theorem List.Perm.eq_nil {α : Type u_1} {l : List α} (p : l.Perm []) :
      l = []
      theorem List.Perm.nil_eq {α : Type u_1} {l : List α} (p : [].Perm l) :
      [] = l
      @[simp]
      theorem List.perm_nil {α : Type u_1} {l₁ : List α} :
      l₁.Perm [] l₁ = []
      @[simp]
      theorem List.nil_perm {α : Type u_1} {l₁ : List α} :
      [].Perm l₁ l₁ = []
      theorem List.not_perm_nil_cons {α : Type u_1} (x : α) (l : List α) :
      ¬[].Perm (x :: l)
      theorem List.not_perm_cons_nil {α : Type u_1} {l : List α} {a : α} :
      ¬(a :: l).Perm []
      theorem List.Perm.isEmpty_eq {α : Type u_1} {l l' : List α} (h : l.Perm l') :
      @[simp]
      theorem List.reverse_perm {α : Type u_1} (l : List α) :
      theorem List.perm_cons_append_cons {α : Type u_1} {l l₁ l₂ : List α} (a : α) (p : l.Perm (l₁ ++ l₂)) :
      (a :: l).Perm (l₁ ++ a :: l₂)
      @[simp]
      theorem List.perm_replicate {α : Type u_1} {n : Nat} {a : α} {l : List α} :
      l.Perm (replicate n a) l = replicate n a
      @[simp]
      theorem List.replicate_perm {α : Type u_1} {n : Nat} {a : α} {l : List α} :
      (replicate n a).Perm l replicate n a = l
      @[simp]
      theorem List.perm_singleton {α : Type u_1} {a : α} {l : List α} :
      l.Perm [a] l = [a]
      @[simp]
      theorem List.singleton_perm {α : Type u_1} {a : α} {l : List α} :
      [a].Perm l [a] = l
      theorem List.Perm.eq_singleton {α✝ : Type u_1} {l : List α✝} {a : α✝} (h : l.Perm [a]) :
      l = [a]
      theorem List.Perm.singleton_eq {α✝ : Type u_1} {a : α✝} {l : List α✝} (h : [a].Perm l) :
      [a] = l
      theorem List.singleton_perm_singleton {α : Type u_1} {a b : α} :
      [a].Perm [b] a = b
      theorem List.perm_cons_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a l) :
      l.Perm (a :: l.erase a)
      theorem List.Perm.filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      theorem List.Perm.map {α : Type u_1} {β : Type u_2} (f : αβ) {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      (List.map f l₁).Perm (List.map f l₂)
      theorem List.Perm.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {l₁ l₂ : List α} :
      l₁.Perm l₂∀ {H₁ : ∀ (a : α), a l₁p a} {H₂ : ∀ (a : α), a l₂p a}, (List.pmap f l₁ H₁).Perm (List.pmap f l₂ H₂)
      theorem List.Perm.unattach {α : Type u} {p : αProp} {l₁ l₂ : List { x : α // p x }} (h : l₁.Perm l₂) :
      theorem List.Perm.filter {α : Type u_1} (p : αBool) {l₁ l₂ : List α} (s : l₁.Perm l₂) :
      (List.filter p l₁).Perm (List.filter p l₂)
      theorem List.filter_append_perm {α : Type u_1} (p : αBool) (l : List α) :
      (filter p l ++ filter (fun (x : α) => !p x) l).Perm l
      theorem List.exists_perm_sublist {α : Type u_1} {l₁ l₂ l₂' : List α} (s : l₁.Sublist l₂) (p : l₂.Perm l₂') :
      (l₁' : List α), l₁'.Perm l₁ l₁'.Sublist l₂'
      theorem List.Perm.sizeOf_eq_sizeOf {α : Type u_1} [SizeOf α] {l₁ l₂ : List α} (h : l₁.Perm l₂) :
      sizeOf l₁ = sizeOf l₂
      theorem List.Sublist.exists_perm_append {α : Type u_1} {l₁ l₂ : List α} :
      l₁.Sublist l₂ (l : List α), l₂.Perm (l₁ ++ l)
      theorem List.Perm.countP_eq {α : Type u_1} (p : αBool) {l₁ l₂ : List α} (s : l₁.Perm l₂) :
      countP p l₁ = countP p l₂
      theorem List.Perm.countP_congr {α : Type u_1} {l₁ l₂ : List α} (s : l₁.Perm l₂) {p p' : αBool} (hp : ∀ (x : α), x l₁p x = p' x) :
      countP p l₁ = countP p' l₂
      theorem List.countP_eq_countP_filter_add {α : Type u_1} (l : List α) (p q : αBool) :
      countP p l = countP p (filter q l) + countP p (filter (fun (a : α) => !q a) l)
      theorem List.Perm.count_eq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (p : l₁.Perm l₂) (a : α) :
      count a l₁ = count a l₂
      theorem List.Perm.foldl_eq' {β : Type u_1} {α : Type u_2} {f : βαβ} {l₁ l₂ : List α} (p : l₁.Perm l₂) (comm : ∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f (f z x) y = f (f z y) x) (init : β) :
      foldl f init l₁ = foldl f init l₂
      theorem List.Perm.foldr_eq' {α : Type u_1} {β : Type u_2} {f : αββ} {l₁ l₂ : List α} (p : l₁.Perm l₂) (comm : ∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f y (f x z) = f x (f y z)) (init : β) :
      foldr f init l₁ = foldr f init l₂
      theorem List.Perm.rec_heq {α : Type u_1} {β : List αSort u_2} {f : (a : α) → (l : List α) → β lβ (a :: l)} {b : β []} {l l' : List α} (hl : l.Perm l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l.Perm l'b b'f a l b f a l' b') (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, f a (a' :: l) (f a' l b) f a' (a :: l) (f a l b)) :
      List.rec b f l List.rec b f l'
      theorem List.perm_inv_core {α : Type u_1} {a : α} {l₁ l₂ r₁ r₂ : List α} :
      (l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂)(l₁ ++ r₁).Perm (l₂ ++ r₂)

      Lemma used to destruct perms element by element.

      theorem List.Perm.cons_inv {α : Type u_1} {a : α} {l₁ l₂ : List α} :
      (a :: l₁).Perm (a :: l₂)l₁.Perm l₂
      @[simp]
      theorem List.perm_cons {α : Type u_1} (a : α) {l₁ l₂ : List α} :
      (a :: l₁).Perm (a :: l₂) l₁.Perm l₂
      theorem List.perm_append_left_iff {α : Type u_1} {l₁ l₂ : List α} (l : List α) :
      (l ++ l₁).Perm (l ++ l₂) l₁.Perm l₂
      theorem List.perm_append_right_iff {α : Type u_1} {l₁ l₂ : List α} (l : List α) :
      (l₁ ++ l).Perm (l₂ ++ l) l₁.Perm l₂
      theorem List.Perm.erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α} (p : l₁.Perm l₂) :
      (l₁.erase a).Perm (l₂.erase a)
      theorem List.cons_perm_iff_perm_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
      (a :: l₁).Perm l₂ a l₂ l₁.Perm (l₂.erase a)
      theorem List.perm_iff_count {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
      l₁.Perm l₂ ∀ (a : α), count a l₁ = count a l₂
      theorem List.isPerm_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
      l₁.isPerm l₂ = true l₁.Perm l₂
      instance List.decidablePerm {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
      Decidable (l₁.Perm l₂)
      Equations
        theorem List.Perm.insert {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α} (p : l₁.Perm l₂) :
        (List.insert a l₁).Perm (List.insert a l₂)
        theorem List.perm_insert_swap {α : Type u_1} [BEq α] [LawfulBEq α] (x y : α) (l : List α) :
        theorem List.Perm.pairwise_iff {α : Type u_1} {R : ααProp} (S : ∀ {x y : α}, R x yR y x) {l₁ l₂ : List α} (_p : l₁.Perm l₂) :
        Pairwise R l₁ Pairwise R l₂
        theorem List.Pairwise.perm {α : Type u_1} {R : ααProp} {l l' : List α} (hR : Pairwise R l) (hl : l.Perm l') (hsymm : ∀ {x y : α}, R x yR y x) :
        theorem List.Perm.pairwise {α : Type u_1} {R : ααProp} {l l' : List α} (hl : l.Perm l') (hR : Pairwise R l) (hsymm : ∀ {x y : α}, R x yR y x) :
        theorem List.Perm.eq_of_sorted {α : Type u_1} {le : ααProp} {l₁ l₂ : List α} :
        (∀ (a b : α), a l₁b l₂le a ble b aa = b)Pairwise le l₁Pairwise le l₂l₁.Perm l₂l₁ = l₂

        If two lists are sorted by an antisymmetric relation, and permutations of each other, they must be equal.

        theorem List.Nodup.perm {α : Type u_1} {l l' : List α} (hR : l.Nodup) (hl : l.Perm l') :
        theorem List.Perm.nodup {α : Type u_1} {l l' : List α} (hl : l.Perm l') (hR : l.Nodup) :
        theorem List.Perm.nodup_iff {α : Type u_1} {l₁ l₂ : List α} :
        l₁.Perm l₂ → (l₁.Nodup l₂.Nodup)
        theorem List.Perm.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁.Perm l₂) :
        l₁.flatten.Perm l₂.flatten
        theorem List.cons_append_cons_perm {α : Type u_1} {a b : α} {as bs : List α} :
        (a :: as ++ b :: bs).Perm (b :: as ++ a :: bs)
        theorem List.Perm.flatMap_right {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : αList β) (p : l₁.Perm l₂) :
        (flatMap f l₁).Perm (flatMap f l₂)
        theorem List.Perm.eraseP {α : Type u_1} (f : αBool) {l₁ l₂ : List α} (H : Pairwise (fun (a b : α) => f a = truef b = trueFalse) l₁) (p : l₁.Perm l₂) :
        (List.eraseP f l₁).Perm (List.eraseP f l₂)
        theorem List.perm_insertIdx {α : Type u_1} (x : α) (l : List α) {i : Nat} (h : i l.length) :
        (l.insertIdx i x).Perm (x :: l)
        theorem List.Perm.take {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {n : Nat} (w : (List.drop n l₁).Perm (List.drop n l₂)) :
        (List.take n l₁).Perm (List.take n l₂)
        theorem List.Perm.drop {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {n : Nat} (w : (List.take n l₁).Perm (List.take n l₂)) :
        (List.drop n l₁).Perm (List.drop n l₂)