Mathlib.Data.List.ProdSigma

Module docstring

{"# Lists in product and sigma types

This file proves basic properties of List.product and List.sigma, which are list constructions living in Prod and Sigma types respectively. Their definitions can be found in Data.List.Defs. Beware, this is not about List.prod, the multiplicative product. ","### product ","### sigma ","### Miscellaneous lemmas "}

List.nil_product theorem

(l : List β) : (@nil α) ×ˢ l = []

Full source

@[simp]
theorem nil_product (l : List β) : (@nil α) ×ˢ l = [] :=
  rfl

Empty List Product Yields Empty List

Informal description

For any list $l$ of elements of type $\beta$, the product of the empty list of type $\alpha$ with $l$ is the empty list, i.e., $[] \timesˢ l = []$.

List.product_cons theorem

(a : α) (l₁ : List α) (l₂ : List β) : (a :: l₁) ×ˢ l₂ = map (fun b => (a, b)) l₂ ++ (l₁ ×ˢ l₂)

Full source

@[simp]
theorem product_cons (a : α) (l₁ : List α) (l₂ : List β) :
    (a :: l₁) ×ˢ l₂ = map (fun b => (a, b)) l₂ ++ (l₁ ×ˢ l₂) :=
  rfl

Product of Cons List with Another List

Informal description

For any element $a$ of type $\alpha$, list $l₁$ of elements of type $\alpha$, and list $l₂$ of elements of type $\beta$, the product of the list $a :: l₁$ with $l₂$ is equal to the concatenation of the list obtained by mapping each element $b$ of $l₂$ to the pair $(a, b)$ and the product of $l₁$ with $l₂$. In symbols: $$(a :: l₁) \timesˢ l₂ = \mathrm{map} (λb, (a, b))\, l₂ +\!\!+ (l₁ \timesˢ l₂)$$

List.product_nil theorem

: ∀ l : List α, l ×ˢ (@nil β) = []

Full source

@[simp]
theorem product_nil : ∀ l : List α, l ×ˢ (@nil β) = []
  | [] => rfl
  | _ :: l => by simp [product_cons, product_nil l]

Product with Empty List Yields Empty List

Informal description

For any list $l$ of elements of type $\alpha$, the product of $l$ with the empty list of type $\beta$ is the empty list, i.e., $l \timesˢ [] = []$.

List.mem_product theorem

{l₁ : List α} {l₂ : List β} {a : α} {b : β} : (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Full source

@[simp]
theorem mem_product {l₁ : List α} {l₂ : List β} {a : α} {b : β} :
    (a, b)(a, b) ∈ l₁ ×ˢ l₂(a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ := by
  simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, exists_prop, and_left_comm,
    exists_and_left, exists_eq_left, exists_eq_right]

Membership in List Product is Component-wise Membership

Informal description

For any lists $l_1$ of elements of type $\alpha$ and $l_2$ of elements of type $\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, the pair $(a, b)$ is an element of the product list $l_1 \timesˢ l_2$ if and only if $a$ is an element of $l_1$ and $b$ is an element of $l_2$. In symbols: $$(a, b) \in l_1 \timesˢ l_2 \leftrightarrow a \in l_1 \land b \in l_2$$

List.length_product theorem

(l₁ : List α) (l₂ : List β) : length (l₁ ×ˢ l₂) = length l₁ * length l₂

Full source

theorem length_product (l₁ : List α) (l₂ : List β) :
    length (l₁ ×ˢ l₂) = length l₁ * length l₂ := by
  induction' l₁ with x l₁ IH
  · exact (Nat.zero_mul _).symm
  · simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]

Length of List Product Equals Product of Lengths

Informal description

For any lists $l_1$ of elements of type $\alpha$ and $l_2$ of elements of type $\beta$, the length of their product list $l_1 \timesˢ l_2$ is equal to the product of the lengths of $l_1$ and $l_2$, i.e., $$\text{length}(l_1 \timesˢ l_2) = \text{length}(l_1) \times \text{length}(l_2).$$

List.nil_sigma theorem

(l : ∀ a, List (σ a)) : (@nil α).sigma l = []

Full source

@[simp]
theorem nil_sigma (l : ∀ a, List (σ a)) : (@nil α).sigma l = [] :=
  rfl

Sigma Product of Empty List is Empty

Informal description

For any family of lists $l : \forall a, \text{List}(\sigma a)$, the sigma product of the empty list with $l$ is the empty list, i.e., $\text{nil.sigma}\, l = []$.

List.sigma_cons theorem

 (a : α) (l₁ : List α) (l₂ : ∀ a, List (σ a)) : (a :: l₁).sigma l₂ = map (Sigma.mk a) (l₂ a) ++ l₁.sigma l₂

Full source

@[simp]
theorem sigma_cons (a : α) (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    (a :: l₁).sigma l₂ = map (Sigma.mk a) (l₂ a) ++ l₁.sigma l₂ :=
  rfl

Sigma Product of Cons List Equals Map Concatenated with Sigma Product

Informal description

For any element $a$ of type $\alpha$, any list $l_1$ of elements of type $\alpha$, and any family of lists $l_2$ where for each $a$, $l_2(a)$ is a list of elements of type $\sigma(a)$, the sigma product of the list $a :: l_1$ with $l_2$ is equal to the concatenation of the list obtained by mapping $\Sigma.mk\,a$ over $l_2(a)$ and the sigma product of $l_1$ with $l_2$. In symbols: $$(a :: l_1).\mathrm{sigma}\,l_2 = \mathrm{map}\,(\Sigma.mk\,a)\,(l_2\,a) \mathbin{+\!\!+} l_1.\mathrm{sigma}\,l_2$$

List.sigma_nil theorem

: ∀ l : List α, (l.sigma fun a => @nil (σ a)) = []

Full source

@[simp]
theorem sigma_nil : ∀ l : List α, (l.sigma fun a => @nil (σ a)) = []
  | [] => rfl
  | _ :: l => by simp [sigma_cons, sigma_nil l]

Sigma Product with Empty Lists Yields Empty List

Informal description

For any list `l` of elements of type `α`, the sigma product of `l` with the function that always returns the empty list is the empty list. In other words, if for every element `a` in `l` we pair it with an empty list of elements of type `σ a`, the resulting sigma list is empty.

List.mem_sigma theorem

 {l₁ : List α} {l₂ : ∀ a, List (σ a)} {a : α} {b : σ a} : Sigma.mk a b ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Full source

@[simp]
theorem mem_sigma {l₁ : List α} {l₂ : ∀ a, List (σ a)} {a : α} {b : σ a} :
    Sigma.mkSigma.mk a b ∈ l₁.sigma l₂Sigma.mk a b ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a := by
  simp [List.sigma, mem_flatMap, mem_map, exists_prop, exists_and_left, and_left_comm,
    exists_eq_left, heq_iff_eq, exists_eq_right]

Membership in Sigma Product of Lists

Informal description

For any list $l_1$ of elements of type $\alpha$, any family of lists $l_2$ where for each $a \in \alpha$, $l_2(a)$ is a list of elements of type $\sigma(a)$, and any pair $(a, b)$ where $b \in \sigma(a)$, the pair $(a, b)$ belongs to the sigma product of $l_1$ and $l_2$ if and only if $a$ is an element of $l_1$ and $b$ is an element of $l_2(a)$. In symbols: $$(a, b) \in l_1.\mathrm{sigma}\,l_2 \leftrightarrow a \in l_1 \land b \in l_2(a)$$

List.mem_map_swap theorem

(x : α) (y : β) (xs : List (α × β)) : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Full source

@[simp 1100]
theorem mem_map_swap (x : α) (y : β) (xs : List (α × β)) :
    (y, x)(y, x) ∈ map Prod.swap xs(y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs := by
  induction' xs with x xs xs_ih
  · simp only [not_mem_nil, map_nil]
  · obtain ⟨a, b⟩ := x
    simp only [mem_cons, Prod.mk_inj, map, Prod.swap_prod_mk, Prod.exists, xs_ih, and_comm]

Membership Preservation under Pair Swapping in Lists

Informal description

For any elements $x \in \alpha$, $y \in \beta$, and a list $xs$ of pairs in $\alpha \times \beta$, the pair $(y, x)$ is in the list obtained by mapping the swap function over $xs$ if and only if the pair $(x, y)$ is in $xs$.