Mathlib.Data.List.Perm.Lattice

List.Perm.bagInter_right theorem

{l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) : l₁.bagInter t ~ l₂.bagInter t

Full source

theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
    l₁.bagInter t ~ l₂.bagInter t := by
  induction h generalizing t with
  | nil => simp
  | cons x => by_cases x ∈ t <;> simp [*, Perm.cons]
  | swap x y =>
    by_cases h : x = y
    · simp [h]
    by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
    · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
    · simp [xt, yt, mt mem_of_mem_erase, Perm.cons]
    · simp [xt, yt, mt mem_of_mem_erase, Perm.cons]
    · simp [xt, yt]
  | trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)

Permutation Preserves Bag Intersection on the Right

Informal description

For any lists $l₁$, $l₂$, and $t$ of elements of type $\alpha$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$), then the bag intersection of $l₁$ with $t$ is a permutation of the bag intersection of $l₂$ with $t$.

List.Perm.bagInter_left theorem

(l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) : l.bagInter t₁ = l.bagInter t₂

Full source

theorem Perm.bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) :
    l.bagInter t₁ = l.bagInter t₂ := by
  induction l generalizing t₁ t₂ p with | nil => simp | cons a l IH => ?_
  by_cases h : a ∈ t₁
  · simp [h, p.subset h, IH (p.erase _)]
  · simp [h, mt p.mem_iff.2 h, IH p]

Invariance of Bag Intersection under Permutation of Second Argument

Informal description

For any list $l$ and any two lists $t_1$ and $t_2$ that are permutations of each other (denoted $t_1 \sim t_2$), the bag intersection of $l$ with $t_1$ is equal to the bag intersection of $l$ with $t_2$. That is, $l \cap t_1 = l \cap t_2$.

List.Perm.bagInter theorem

{l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) : l₁.bagInter t₁ ~ l₂.bagInter t₂

Full source

theorem Perm.bagInter {l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) :
    l₁.bagInter t₁ ~ l₂.bagInter t₂ :=
  ht.bagInter_left l₂ ▸ hl.bagInter_right _

Permutation Invariance of Bag Intersection

Informal description

For any lists $l₁, l₂, t₁, t₂$ of elements of type $\alpha$, if $l₁$ is a permutation of $l₂$ (denoted $l₁ \sim l₂$) and $t₁$ is a permutation of $t₂$ (denoted $t₁ \sim t₂$), then the bag intersection of $l₁$ with $t₁$ is a permutation of the bag intersection of $l₂$ with $t₂$. That is, $l₁ \cap t₁ \sim l₂ \cap t₂$.

List.Perm.inter_append theorem

{l t₁ t₂ : List α} (h : Disjoint t₁ t₂) : l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂

Full source

theorem Perm.inter_append {l t₁ t₂ : List α} (h : Disjoint t₁ t₂) :
    l ∩ (t₁ ++ t₂)l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ := by
  induction l with
  | nil => simp
  | cons x xs l_ih =>
    by_cases h₁ : x ∈ t₁
    · have h₂ : x ∉ t₂ := h h₁
      simp [*]
    by_cases h₂ : x ∈ t₂
    · simp only [*, inter_cons_of_not_mem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      refine Perm.trans (Perm.cons _ l_ih) ?_
      change [x][x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ ([x] ++ xs ∩ t₂)
      rw [← List.append_assoc]
      solve_by_elim [Perm.append_right, perm_append_comm]
    · simp [*]

Permutation of List Intersection with Concatenation of Disjoint Lists

Informal description

For any lists $l$, $t₁$, $t₂$ of type $\alpha$, if $t₁$ and $t₂$ are disjoint (have no common elements), then the intersection of $l$ with the concatenation of $t₁$ and $t₂$ is permutation-equivalent to the concatenation of the intersection of $l$ with $t₁$ and the intersection of $l$ with $t₂$. In symbols: $$ l ∩ (t₁ ++ t₂) \sim (l ∩ t₁) ++ (l ∩ t₂) $$ where $∩$ denotes list intersection, $++$ denotes list concatenation, and $\sim$ denotes permutation equivalence.

List.Perm.take_inter theorem

{xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n)

Full source

theorem Perm.take_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys)
    (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n) := by
  simp only [List.inter]
  exact Perm.trans (show xs.take n ~ xs.filter (xs.take n).elem by
      conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
    (Perm.filter _ h)

Permutation of Initial Segment and Intersection for Duplicate-Free Lists

Informal description

For any two lists $xs$ and $ys$ of type $\alpha$, if $xs$ is a permutation of $ys$ (denoted $xs \sim ys$) and $ys$ has no duplicate elements, then for any natural number $n$, the first $n$ elements of $xs$ (denoted $\text{take}(n, xs)$) is a permutation of the intersection of $ys$ with the first $n$ elements of $xs$ (denoted $ys \cap \text{take}(n, xs)$).

List.Perm.drop_inter theorem

{xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) : xs.drop n ~ ys.inter (xs.drop n)

Full source

theorem Perm.drop_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) :
    xs.drop n ~ ys.inter (xs.drop n) := by
  by_cases h'' : n ≤ xs.length
  · let n' := xs.length - n
    have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
    have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]
    rw [h₁]
    apply (reverse_perm _).trans
    rw [inter_reverse]
    apply Perm.take_inter _ _ h'
    apply (reverse_perm _).trans; assumption
  · have : xs.drop n = [] := by
      apply eq_nil_of_length_eq_zero
      rw [length_drop, Nat.sub_eq_zero_iff_le]
      apply le_of_not_ge h''
    simp [this, List.inter]

Permutation of Dropped Segment and Intersection for Duplicate-Free Lists

Informal description

For any two lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a permutation of $ys$ (denoted $xs \sim ys$) and $ys$ has no duplicate elements, then for any natural number $n$, the list obtained by dropping the first $n$ elements of $xs$ (denoted $\text{drop}(n, xs)$) is a permutation of the intersection of $ys$ with the dropped segment (denoted $ys \cap \text{drop}(n, xs)$).

List.Perm.dropSlice_inter theorem

{xs ys : List α} (n m : ℕ) (h : xs ~ ys) (h' : ys.Nodup) : List.dropSlice n m xs ~ ys ∩ List.dropSlice n m xs

Full source

theorem Perm.dropSlice_inter {xs ys : List α} (n m : ℕ) (h : xs ~ ys)
    (h' : ys.Nodup) : List.dropSliceList.dropSlice n m xs ~ ys ∩ List.dropSlice n m xs := by
  simp only [dropSlice_eq]
  have : n ≤ n + m := Nat.le_add_right _ _
  have h₂ := h.nodup_iff.2 h'
  apply Perm.trans _ (Perm.inter_append _).symm
  · exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
  · exact disjoint_take_drop h₂ this

Permutation of Drop-Slice Segment and Intersection for Duplicate-Free Lists

Informal description

For any two lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a permutation of $ys$ (denoted $xs \sim ys$) and $ys$ has no duplicate elements, then for any natural numbers $n$ and $m$, the sublist obtained by dropping $n$ elements and then taking $m$ elements from $xs$ (denoted $\text{dropSlice}(n, m, xs)$) is a permutation of the intersection of $ys$ with this sublist (denoted $ys \cap \text{dropSlice}(n, m, xs)$).