Mathlib.Data.List.Pi

List.Pi.nil definition

(α : ι → Sort*) : (∀ i ∈ ([] : List ι), α i)

Full source

/-- Given `α : ι → Sort*`, `Pi.nil α` is the trivial dependent function out of the empty list. -/
def nil (α : ι → Sort*) : (∀ i ∈ ([] : List ι), α i) :=
  nofun

Trivial dependent function on the empty list

Informal description

Given a family of types $\alpha : \iota \to \text{Type}$, the trivial dependent function $\text{Pi.nil}\, \alpha$ is the unique function from the empty list to $\alpha$, which vacuously satisfies the condition of being defined for all $i$ in the empty list.

List.Pi.head definition

(f : ∀ j ∈ i :: l, α j) : α i

Full source

/-- Given `f` a function whose domain is `i :: l`, get its value at `i`. -/
def head (f : ∀ j ∈ i :: l, α j) : α i :=
  f i mem_cons_self

Value at head of cartesian product function

Informal description

Given a function $f$ defined on the cartesian product of types indexed by a list $i :: l$, this function extracts the value of $f$ at the head element $i$.

List.Pi.tail definition

(f : ∀ j ∈ i :: l, α j) : ∀ j ∈ l, α j

Full source

/-- Given `f` a function whose domain is `i :: l`, produce a function whose domain
is restricted to `l`. -/
def tail (f : ∀ j ∈ i :: l, α j) : ∀ j ∈ l, α j :=
  fun j hj ↦ f j (mem_cons_of_mem _ hj)

Restriction of a function to the tail of a list

Informal description

Given a function $ f $ defined for all elements in the list $ i :: l $ (i.e., for the head $ i $ and the tail $ l $), the function `List.Pi.tail` restricts $ f $ to the tail $ l $, returning a function defined only for elements in $ l $. More formally, if $ f $ is a function such that for every $ j \in i :: l $, $ f(j) $ is defined, then `List.Pi.tail f` is the function that maps each $ j \in l $ to $ f(j) $.

List.Pi.cons definition

(a : α i) (f : ∀ j ∈ l, α j) : ∀ j ∈ i :: l, α j

Full source

/-- Given `α : ι → Sort*`, a list `l` and a term `i`, as well as a term `a : α i` and a
function `f` such that `f j : α j` for all `j` in `l`, `Pi.cons a f` is a function `g` such
that `g k : α k` for all `k` in `i :: l`. -/
def cons (a : α i) (f : ∀ j ∈ l, α j) : ∀ j ∈ i :: l, α j :=
  Multiset.Pi.cons (α := ι) l _ a f

Function extension for list cartesian product

Informal description

Given a type family $\alpha : \iota \to \text{Sort}^*$, a list $l$ over $\iota$, an element $i \in \iota$, a term $a \in \alpha i$, and a function $f$ such that $f(j) \in \alpha j$ for all $j \in l$, the function $\text{List.Pi.cons}(a, f)$ constructs a new function $g$ such that: - $g(i) = a$, and - $g(j) = f(j)$ for all $j \in l$. In other words, $\text{List.Pi.cons}$ extends the function $f$ defined on $l$ to a function defined on $i :: l$ by setting its value at $i$ to be $a$ and keeping the other values unchanged.

List.Pi.cons_def theorem

 (a : α i) (f : ∀ j ∈ l, α j) :
  cons _ _ a f = fun j hj ↦ if h : j = i then h.symm.rec a else f j <| (mem_cons.1 hj).resolve_left h

Full source

lemma cons_def (a : α i) (f : ∀ j ∈ l, α j) : cons _ _ a f =
    fun j hj ↦ if h : j = i then h.symm.rec a else f j <| (mem_cons.1 hj).resolve_left h :=
  rfl

Definition of List Extension Function via Case Analysis

Informal description

Given a type family $\alpha$ indexed by elements of a list, an element $a \in \alpha_i$ for some index $i$, and a function $f$ defined for all indices $j$ in a list $l$ such that $f(j) \in \alpha_j$, the function $\text{cons}(a, f)$ is defined as follows: for any index $j$ in the extended list $i :: l$ and proof $hj$ that $j$ is in this list, we have \[ \text{cons}(a, f)(j, hj) = \begin{cases} a & \text{if } j = i, \\ f(j, h'j) & \text{otherwise, where } h'j \text{ is the proof that } j \in l. \end{cases} \]

Multiset.Pi.cons_coe theorem

{l : List ι} (a : α i) (f : ∀ j ∈ l, α j) : Multiset.Pi.cons l _ a f = cons _ _ a f

Full source

@[simp] lemma _root_.Multiset.Pi.cons_coe {l : List ι} (a : α i) (f : ∀ j ∈ l, α j) :
    Multiset.Pi.cons l _ a f = cons _ _ a f :=
  rfl

Equality of Multiset and List Extension Functions for Cartesian Products

Informal description

For any list $l$ over an index type $\iota$, any element $a$ of type $\alpha_i$ (where $\alpha : \iota \to \text{Type}$ is a type family), and any function $f$ such that $f(j) \in \alpha_j$ for all $j \in l$, the multiset extension function $\text{Multiset.Pi.cons}(l, a, f)$ is equal to the list extension function $\text{List.Pi.cons}(a, f)$.

List.Pi.cons_eta theorem

(f : ∀ j ∈ i :: l, α j) : cons _ _ (head f) (tail f) = f

Full source

@[simp] lemma cons_eta (f : ∀ j ∈ i :: l, α j) :
    cons _ _ (head f) (tail f) = f :=
  Multiset.Pi.cons_eta (α := ι) (m := l) f

Idempotence of Function Extension in List Cartesian Product

Informal description

For any function $f$ defined on the cartesian product of types indexed by a list $i :: l$, the extension of $f$ constructed by: 1. Setting its value at the head $i$ to be $\text{head}(f)$, and 2. Setting its values on the tail $l$ to be $\text{tail}(f)$, is equal to the original function $f$. In other words, the extension operation $\text{cons}$ is idempotent when applied to $f$ in this manner.

List.Pi.cons_map theorem

 (a : α i) (f : ∀ j ∈ l, α j) {α' : ι → Sort*} (φ : ∀ ⦃j⦄, α j → α' j) :
  cons _ _ (φ a) (fun j hj ↦ φ (f j hj)) = (fun j hj ↦ φ ((cons _ _ a f) j hj))

Full source

lemma cons_map (a : α i) (f : ∀ j ∈ l, α j)
    {α' : ι → Sort*} (φ : ∀ ⦃j⦄, α j → α' j) :
    cons _ _ (φ a) (fun j hj ↦ φ (f j hj)) = (fun j hj ↦ φ ((cons _ _ a f) j hj)) :=
  Multiset.Pi.cons_map _ _ _

Commutativity of Function Extension and Mapping in List Cartesian Product

Informal description

Let $\alpha, \alpha' : \iota \to \text{Type}$ be type families, $l$ a list over $\iota$, $i \in \iota$, $a \in \alpha i$, and $f$ a function such that $f(j) \in \alpha j$ for all $j \in l$. Given a function $\varphi : \forall j, \alpha j \to \alpha' j$, the following equality holds: \[ \text{cons}(a, f) \circ \varphi = \text{cons}(\varphi(a), \varphi \circ f) \] where $\text{cons}$ extends a function defined on $l$ to $i :: l$ by setting its value at $i$ to be the given element and preserving the other values.

List.Pi.forall_rel_cons_ext theorem

 {r : ∀ ⦃i⦄, α i → α i → Prop} {a₁ a₂ : α i} {f₁ f₂ : ∀ j ∈ l, α j} (ha : r a₁ a₂)
  (hf : ∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)) : ∀ j hj, r (cons _ _ a₁ f₁ j hj) (cons _ _ a₂ f₂ j hj)

Full source

lemma forall_rel_cons_ext {r : ∀ ⦃i⦄, α i → α i → Prop} {a₁ a₂ : α i} {f₁ f₂ : ∀ j ∈ l, α j}
    (ha : r a₁ a₂) (hf : ∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)) :
    ∀ j hj, r (cons _ _ a₁ f₁ j hj) (cons _ _ a₂ f₂ j hj) :=
  Multiset.Pi.forall_rel_cons_ext (α := ι) (m := l) ha hf

Extension of Relation to List Cartesian Product Functions

Informal description

Let $\alpha : \iota \to \text{Type}$ be a type family, $l$ a list over $\iota$, and $i \in \iota$. Given a relation $r$ on $\alpha$ (i.e., for each $i \in \iota$, $r : \alpha i \to \alpha i \to \text{Prop}$), elements $a_1, a_2 \in \alpha i$, and functions $f_1, f_2 : \forall j \in l, \alpha j$, if: 1. $r(a_1, a_2)$ holds, and 2. for every $j \in l$ and $h_j : j \in l$, $r(f_1 j h_j, f_2 j h_j)$ holds, then for every $j \in i :: l$ and $h_j : j \in i :: l$, the relation $r$ holds between the extended functions: \[ r(\text{cons}(a_1, f_1) j h_j, \text{cons}(a_2, f_2) j h_j), \] where $\text{cons}(a, f)$ extends $f$ to $i :: l$ by setting its value at $i$ to be $a$ and preserving the other values.

List.pi definition

: ∀ l : List ι, (∀ i, List (α i)) → List (∀ i, i ∈ l → α i)

Full source

/-- `pi xs f` creates the list of functions `g` such that, for `x ∈ xs`, `g x ∈ f x` -/
def pi : ∀ l : List ι, (∀ i, List (α i)) → List (∀ i, i ∈ l → α i)
  |     [],  _ => [List.Pi.nil α]
  | i :: l, fs => (fs i).flatMap (fun b ↦ (pi l fs).map (List.Pi.cons _ _ b))

Cartesian product of indexed lists

Informal description

Given a list $l$ of indices and a family of lists $\{ \alpha_i \}_{i \in l}$, the cartesian product $\text{List.pi}\, l\, \alpha$ is the list of all functions $g$ such that for each index $i \in l$, the value $g(i)$ belongs to the corresponding list $\alpha_i$. More formally, for each $i \in l$, $\alpha_i$ is a list of possible values, and $\text{List.pi}\, l\, \alpha$ constructs all possible functions that select one element from each $\alpha_i$.

List.pi_nil theorem

(t : ∀ i, List (α i)) : pi [] t = [Pi.nil α]

Full source

@[simp] lemma pi_nil (t : ∀ i, List (α i)) :
    pi [] t = [Pi.nil α] :=
  rfl

Cartesian Product of Empty List Yields Trivial Function

Informal description

For any family of lists $t : \forall i, \text{List}(\alpha i)$, the cartesian product $\text{pi}\, []\, t$ of the empty list is the singleton list containing the trivial dependent function $\text{Pi.nil}\, \alpha$.

List.pi_cons theorem

 (i : ι) (l : List ι) (t : ∀ j, List (α j)) : pi (i :: l) t = ((t i).flatMap fun b ↦ (pi l t).map <| Pi.cons _ _ b)

Full source

@[simp] lemma pi_cons (i : ι) (l : List ι) (t : ∀ j, List (α j)) :
    pi (i :: l) t = ((t i).flatMap fun b ↦ (pi l t).map <| Pi.cons _ _ b) :=
  rfl

Recursive Construction of Cartesian Product for Cons List

Informal description

Given an index $i$, a list of indices $l$, and a family of lists $\{ \alpha_j \}_{j \in i::l}$, the cartesian product $\text{pi}\, (i :: l)\, t$ is equal to the concatenation of the results obtained by: 1. For each element $b$ in the list $\alpha_i$, 2. Extending every function in $\text{pi}\, l\, t$ by setting its value at $i$ to be $b$. In other words, $\text{pi}\, (i :: l)\, t = \bigcup_{b \in \alpha_i} \{ \text{Pi.cons}\, b\, f \mid f \in \text{pi}\, l\, t \}$.

Multiset.pi_coe theorem

(l : List ι) (fs : ∀ i, List (α i)) : (l : Multiset ι).pi (fs ·) = (↑(pi l fs) : Multiset (∀ i ∈ l, α i))

Full source

lemma _root_.Multiset.pi_coe (l : List ι) (fs : ∀ i, List (α i)) :
    (l : Multiset ι).pi (fs ·) = (↑(pi l fs) : Multiset (∀ i ∈ l, α i)) := by
  induction' l with i l ih
  · change Multiset.pi 0 _ = _
    simp only [Multiset.coe_singleton, Multiset.pi_zero, pi_nil, Multiset.singleton_inj]
    ext i hi
    simp at hi
  · change Multiset.pi (i ::ₘ ↑l) _ = _
    simp [ih, Multiset.coe_bind, - Multiset.cons_coe]

Multiset-Lift Equivalence of Cartesian Products: $\text{pi}(l, \alpha) = \text{List.pi}\, l\, \alpha$ as multisets

Informal description

Given a list $l$ of indices and a family of lists $\{ \alpha_i \}_{i \in l}$, the multiset cartesian product of $l$ (viewed as a multiset) with $\alpha$ is equal to the multiset obtained by lifting the list cartesian product of $l$ with $\alpha$ to a multiset. More precisely, for any list $l$ and family of lists $\alpha_i$, we have: $$\text{pi}((l : \text{Multiset } \iota), \alpha) = (\text{List.pi}\, l\, \alpha : \text{Multiset } (\forall i \in l, \alpha_i))$$

List.mem_pi theorem

 {l : List ι} (fs : ∀ i, List (α i)) : ∀ f : ∀ i ∈ l, α i, (f ∈ pi l fs) ↔ (∀ i (hi : i ∈ l), f i hi ∈ fs i)

Full source

lemma mem_pi {l : List ι} (fs : ∀ i, List (α i)) :
    ∀ f : ∀ i ∈ l, α i, (f ∈ pi l fs) ↔ (∀ i (hi : i ∈ l), f i hi ∈ fs i) := by
  intros f
  convert @Multiset.mem_pi ι _ α ↑l (fs ·) f using 1
  rw [Multiset.pi_coe]
  rfl

Membership Criterion for List Cartesian Product: $f \in \text{pi}(l, \alpha) \leftrightarrow \forall i \in l, f(i) \in \alpha_i$

Informal description

Given a list $l$ of indices and a family of lists $\{ \alpha_i \}_{i \in l}$, a dependent function $f$ (where $f(i) \in \alpha_i$ for each $i \in l$) belongs to the cartesian product $\text{List.pi}\, l\, \alpha$ if and only if for every $i \in l$ and every proof $h$ that $i \in l$, the value $f(i, h)$ is an element of $\alpha_i$. In other words, $f \in \text{List.pi}\, l\, \alpha \leftrightarrow \forall i \in l, f(i) \in \alpha_i$.

Main definitions