doc-next-gen

Mathlib.Data.Multiset.Pi

Module docstring

{"# The cartesian product of multisets

Main definitions

  • Multiset.pi: Cartesian product of multisets indexed by a multiset. "}
Multiset.Pi.empty definition
(δ : α → Sort*) : ∀ a ∈ (0 : Multiset α), δ a
Full source 
/-- Given `δ : α → Sort*`, `Pi.empty δ` is the trivial dependent function out of the empty
multiset. -/
def empty (δ : α → Sort*) : ∀ a ∈ (0 : Multiset α), δ a :=
  nofun
Trivial dependent function on the empty multiset
Informal description
Given a type family $\delta : \alpha \to \text{Type}$, the function $\text{Pi.empty}$ is the trivial dependent function from the empty multiset $(0 : \text{Multiset } \alpha)$ to $\delta$, i.e., for any $a$ in the empty multiset, it returns an element of $\delta a$.
Multiset.Pi.cons definition
(b : δ a) (f : ∀ a ∈ m, δ a) : ∀ a' ∈ a ::ₘ m, δ a'
Full source 
/-- Given `δ : α → Sort*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
function `f` such that `f a' : δ a'` for all `a'` in `m`, `Pi.cons m a b f` is a function `g` such
that `g a'' : δ a''` for all `a''` in `a ::ₘ m`. -/
def cons (b : δ a) (f : ∀ a ∈ m, δ a) : ∀ a' ∈ a ::ₘ m, δ a' :=
  fun a' ha' => if h : a' = a then Eq.ndrec b h.symm else f a' <| (mem_cons.1 ha').resolve_left h
Function extension for multiset cartesian product
Informal description
Given a type family $\delta : \alpha \to \text{Sort}^*$, a multiset $m$ over $\alpha$, an element $a \in \alpha$, a term $b \in \delta a$, and a function $f$ such that $f(a') \in \delta a'$ for all $a' \in m$, the function $\text{Pi.cons}(m, a, b, f)$ constructs a new function $g$ such that: - $g(a) = b$, and - $g(a') = f(a')$ for all $a' \in m$. In other words, $\text{Pi.cons}$ extends the function $f$ defined on $m$ to a function defined on $a ::ₘ m$ by setting its value at $a$ to be $b$ and keeping the other values unchanged.
Multiset.Pi.cons_same theorem
{b : δ a} {f : ∀ a ∈ m, δ a} (h : a ∈ a ::ₘ m) : cons m a b f a h = b
Full source 
theorem cons_same {b : δ a} {f : ∀ a ∈ m, δ a} (h : a ∈ a ::ₘ m) :
    cons m a b f a h = b :=
  dif_pos rfl
Consistency of Function Extension in Multiset Cartesian Product
Informal description
Given a type family $\delta : \alpha \to \text{Sort}^*$, a multiset $m$ over $\alpha$, an element $a \in \alpha$, a term $b \in \delta a$, and a function $f$ such that $f(a') \in \delta a'$ for all $a' \in m$, the function $\text{cons}(m, a, b, f)$ satisfies $\text{cons}(m, a, b, f)(a, h) = b$ for any proof $h$ that $a$ is in the multiset $a ::ₘ m$.
Multiset.Pi.cons_ne theorem
{a a' : α} {b : δ a} {f : ∀ a ∈ m, δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a) : Pi.cons m a b f a' h' = f a' ((mem_cons.1 h').resolve_left h)
Full source 
theorem cons_ne {a a' : α} {b : δ a} {f : ∀ a ∈ m, δ a} (h' : a' ∈ a ::ₘ m)
    (h : a' ≠ a) : Pi.cons m a b f a' h' = f a' ((mem_cons.1 h').resolve_left h) :=
  dif_neg h
Consistency of Extended Function at Distinct Points in Multiset Cartesian Product
Informal description
Let $\delta : \alpha \to \text{Sort}^*$ be a type family, $m$ a multiset over $\alpha$, $a \in \alpha$, $b \in \delta a$, and $f$ a function such that $f(a') \in \delta a'$ for all $a' \in m$. For any $a' \in a ::ₘ m$ with $a' \neq a$, the extended function $\text{Pi.cons}(m, a, b, f)$ satisfies $\text{Pi.cons}(m, a, b, f)(a') = f(a')$.
Multiset.Pi.cons_swap theorem
{a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a} (h : a ≠ a') : HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f)) (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f))
Full source 
theorem cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a}
    (h : a ≠ a') : HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f))
      (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f)) := by
  apply hfunext rfl
  simp only [heq_iff_eq]
  rintro a'' _ rfl
  refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_
  rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
  on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
  all_goals simp [*, Pi.cons_same, Pi.cons_ne]
Commutativity of Function Extension in Multiset Cartesian Product for Distinct Points
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Sort}^*$ a type family, $m$ a multiset over $\alpha$, and $a, a' \in \alpha$ with $a \neq a'$. Given elements $b \in \delta a$ and $b' \in \delta a'$, and a function $f$ such that $f(a'') \in \delta a''$ for all $a'' \in m$, the two extended functions constructed by: 1. First extending $f$ at $a'$ with $b'$, then extending the result at $a$ with $b$, and 2. First extending $f$ at $a$ with $b$, then extending the result at $a'$ with $b'$, are heterogeneously equal. In other words, the order of extending the function at distinct points $a$ and $a'$ does not affect the resulting function up to heterogeneous equality.
Multiset.Pi.cons_eta theorem
{m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') : (cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f
Full source 
@[simp]
theorem cons_eta {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') :
    (cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f := by
  ext a' h'
  by_cases h : a' = a
  · subst h
    rw [Pi.cons_same]
  · rw [Pi.cons_ne _ h]
Idempotence of Function Extension in Multiset Cartesian Product
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Sort}^*$ a type family, $m$ a multiset over $\alpha$, and $a \in \alpha$. For any function $f$ defined on the multiset $a ::ₘ m$ (i.e., $f(a') \in \delta a'$ for all $a' \in a ::ₘ m$), the extended function constructed by: 1. Setting its value at $a$ to be $f(a)$, and 2. Setting its value at any other $a' \in m$ to be $f(a')$, is equal to the original function $f$. In other words, the extension operation $\text{cons}$ is idempotent when applied in this manner.
Multiset.Pi.cons_map theorem
(b : δ a) (f : ∀ a' ∈ m, δ a') {δ' : α → Sort*} (φ : ∀ ⦃a'⦄, δ a' → δ' a') : Pi.cons _ _ (φ b) (fun a' ha' ↦ φ (f a' ha')) = (fun a' ha' ↦ φ ((cons _ _ b f) a' ha'))
Full source 
theorem cons_map (b : δ a) (f : ∀ a' ∈ m, δ a')
    {δ' : α → Sort*} (φ : ∀ ⦃a'⦄, δ a' → δ' a') :
    Pi.cons _ _ (φ b) (fun a' ha' ↦ φ (f a' ha')) = (fun a' ha' ↦ φ ((cons _ _ b f) a' ha')) := by
  ext a' ha'
  refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm
  ext rfl
  rfl
Commutativity of Function Extension and Mapping in Multiset Cartesian Product
Informal description
Let $\delta, \delta' : \alpha \to \text{Sort}^*$ be type families, $m$ a multiset over $\alpha$, $a \in \alpha$, $b \in \delta a$, $f$ a function such that $f(a') \in \delta a'$ for all $a' \in m$, and $\varphi$ a function mapping $\delta a'$ to $\delta' a'$ for each $a' \in \alpha$. Then the following equality holds: \[ \text{Pi.cons}(m, a, \varphi(b), \lambda a' \, ha', \varphi(f(a', ha'))) = \lambda a' \, ha', \varphi(\text{Pi.cons}(m, a, b, f)(a', ha')) \]
Multiset.Pi.forall_rel_cons_ext theorem
{r : ∀ ⦃a⦄, δ a → δ a → Prop} {b₁ b₂ : δ a} {f₁ f₂ : ∀ a' ∈ m, δ a'} (hb : r b₁ b₂) (hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)) : ∀ a ha, r (cons _ _ b₁ f₁ a ha) (cons _ _ b₂ f₂ a ha)
Full source 
theorem forall_rel_cons_ext {r : ∀ ⦃a⦄, δ a → δ a → Prop} {b₁ b₂ : δ a} {f₁ f₂ : ∀ a' ∈ m, δ a'}
    (hb : r b₁ b₂) (hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)) :
    ∀ a ha, r (cons _ _ b₁ f₁ a ha) (cons _ _ b₂ f₂ a ha) := by
  intro a ha
  dsimp [cons]
  split_ifs with H
  · cases H
    exact hb
  · exact hf _ _
Extension of Relation to Multiset Cartesian Product Functions
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Sort}^*$ a type family, $m$ a multiset over $\alpha$, and $a \in \alpha$. Given a relation $r$ on $\delta$ (i.e., for each $a \in \alpha$, $r : \delta a \to \delta a \to \text{Prop}$), elements $b_1, b_2 \in \delta a$, and functions $f_1, f_2 : \forall a' \in m, \delta a'$, if: 1. $r(b_1, b_2)$ holds, and 2. for every $a' \in m$ and $h_a : a' \in m$, $r(f_1 a' h_a, f_2 a' h_a)$ holds, then for every $a' \in a ::ₘ m$ and $h_a : a' \in a ::ₘ m$, the relation $r$ holds between the extended functions: \[ r(\text{cons}(m, a, b_1, f_1) a' h_a, \text{cons}(m, a, b_2, f_2) a' h_a). \]
Multiset.Pi.cons_injective theorem
{a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) : Function.Injective (Pi.cons s a b)
Full source 
theorem cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
    Function.Injective (Pi.cons s a b) := fun f₁ f₂ eq =>
  funext fun a' =>
    funext fun h' =>
      have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
      have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
      calc
        f₁ a' h' = Pi.cons s a b f₁ a' this := by rw [Pi.cons_ne this ne.symm]
               _ = Pi.cons s a b f₂ a' this := by rw [eq]
               _ = f₂ a' h' := by rw [Pi.cons_ne this ne.symm]
Injectivity of Multiset Cartesian Product Extension When $a \notin s$
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Sort}^*$ a type family, $a \in \alpha$, $b \in \delta a$, and $s$ a multiset over $\alpha$ such that $a \notin s$. Then the function $\text{Pi.cons}(s, a, b)$ is injective, meaning that for any two functions $f_1, f_2 : \forall a' \in s, \delta a'$, if $\text{Pi.cons}(s, a, b, f_1) = \text{Pi.cons}(s, a, b, f_2)$, then $f_1 = f_2$.
Multiset.pi definition
(m : Multiset α) (t : ∀ a, Multiset (β a)) : Multiset (∀ a ∈ m, β a)
Full source 
/-- `pi m t` constructs the Cartesian product over `t` indexed by `m`. -/
def pi (m : Multiset α) (t : ∀ a, Multiset (β a)) : Multiset (∀ a ∈ m, β a) :=
  m.recOn {Pi.empty β}
    (fun a m (p : Multiset (∀ a ∈ m, β a)) => (t a).bind fun b => p.map <| Pi.cons m a b)
    (by
      intro a a' m n
      by_cases eq : a = a'
      · subst eq; rfl
      · simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b _
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b' _
        apply map_hcongr
        · rw [cons_swap a a']
        intro f _
        exact Pi.cons_swap eq)
Cartesian product of multisets
Informal description
Given a multiset $m$ over a type $\alpha$ and for each $a \in \alpha$, a multiset $t(a)$ over a type $\beta(a)$, the cartesian product $\text{pi}(m, t)$ is a multiset consisting of all dependent functions $f$ such that for every $a \in m$, $f(a) \in t(a)$. The construction is defined recursively: 1. For the empty multiset $m = 0$, the product is the singleton multiset containing the trivial function $\text{Pi.empty}$. 2. For a multiset $a ::ₘ m$, the product is formed by taking each element $b \in t(a)$ and extending every function in $\text{pi}(m, t)$ via $\text{Pi.cons}(m, a, b)$.
Multiset.pi_zero theorem
(t : ∀ a, Multiset (β a)) : pi 0 t = {Pi.empty β}
Full source 
@[simp]
theorem pi_zero (t : ∀ a, Multiset (β a)) : pi 0 t = {Pi.empty β} :=
  rfl
Cartesian Product of Empty Multiset Yields Singleton Trivial Function
Informal description
For any family of multisets $t(a)$ indexed by elements $a$ of type $\alpha$, the cartesian product $\text{pi}(0, t)$ of the empty multiset $0$ with $t$ is the singleton multiset containing only the trivial dependent function $\text{Pi.empty}$.
Multiset.pi_cons theorem
(m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) : pi (a ::ₘ m) t = (t a).bind fun b => (pi m t).map <| Pi.cons m a b
Full source 
@[simp]
theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) :
    pi (a ::ₘ m) t = (t a).bind fun b => (pi m t).map <| Pi.cons m a b :=
  recOn_cons a m
Recursive Construction of Multiset Cartesian Product: $\text{pi}(a ::ₘ m, t) = \bigcup_{b \in t(a)} \{\text{Pi.cons}(m, a, b, f) \mid f \in \text{pi}(m, t)\}$
Informal description
Given a multiset $m$ over a type $\alpha$, a family of multisets $t(a)$ over types $\beta(a)$ for each $a \in \alpha$, and an element $a \in \alpha$, the cartesian product $\text{pi}(a ::ₘ m, t)$ is equal to the union over all $b \in t(a)$ of the multisets obtained by extending each function in $\text{pi}(m, t)$ via $\text{Pi.cons}(m, a, b)$. More precisely, for the multiset $a ::ₘ m$ (obtained by adding one occurrence of $a$ to $m$), the cartesian product is constructed by: 1. For each element $b$ in $t(a)$, 2. Taking each function $f$ in $\text{pi}(m, t)$, 3. Extending $f$ to a new function $g$ on $a ::ₘ m$ such that $g(a) = b$ and $g(a') = f(a')$ for all $a' \in m$, 4. Collecting all such extended functions $g$ into a multiset.
Multiset.card_pi theorem
(m : Multiset α) (t : ∀ a, Multiset (β a)) : card (pi m t) = prod (m.map fun a => card (t a))
Full source 
theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
    card (pi m t) = prod (m.map fun a => card (t a)) :=
  Multiset.induction_on m (by simp) (by simp +contextual [mul_comm])
Cardinality of Multiset Cartesian Product: $|\text{pi}(m, t)| = \prod_{a \in m} |t(a)|$
Informal description
For any multiset $m$ over a type $\alpha$ and any family of multisets $t(a)$ over types $\beta(a)$ for each $a \in \alpha$, the cardinality of the cartesian product $\text{pi}(m, t)$ is equal to the product of the cardinalities of the multisets $t(a)$ for all $a \in m$. That is, $$|\text{pi}(m, t)| = \prod_{a \in m} |t(a)|.$$
Multiset.Nodup.pi theorem
{s : Multiset α} {t : ∀ a, Multiset (β a)} : Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t)
Full source 
protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
    Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t) :=
  Multiset.induction_on s (fun _ _ => nodup_singleton _)
    (by
      intro a s ih hs ht
      have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
      have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
      simp only [pi_cons, nodup_bind]
      refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩
      refine (ht a <| mem_cons_self _ _).pairwise ?_
      exact fun b₁ _ b₂ _ neb =>
        disjoint_map_map.2 fun f _ g _ eq =>
          have : Pi.cons s a b₁ f a (mem_cons_self _ _) = Pi.cons s a b₂ g a (mem_cons_self _ _) :=
            by rw [eq]
          neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this)
No-Duplicates Property of Multiset Cartesian Product
Informal description
Let $s$ be a multiset over a type $\alpha$, and for each $a \in \alpha$, let $t(a)$ be a multiset over a type $\beta(a)$. If $s$ has no duplicate elements and for every $a \in s$, the multiset $t(a)$ has no duplicate elements, then the cartesian product $\text{pi}(s, t)$ also has no duplicate elements.
Multiset.mem_pi theorem
(m : Multiset α) (t : ∀ a, Multiset (β a)) : ∀ f : ∀ a ∈ m, β a, f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a
Full source 
theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
    ∀ f : ∀ a ∈ m, β a, f ∈ pi m tf ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a := by
  intro f
  induction' m using Multiset.induction_on with a m ih
  · have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
    simp only [this, pi_zero, mem_singleton, true_iff]
    intro _ h; exact (not_mem_zero _ h).elim
  simp_rw [pi_cons, mem_bind, mem_map, ih]
  constructor
  · rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
    by_cases h : a' = a
    · subst h
      rwa [Pi.cons_same]
    · rw [Pi.cons_ne _ h]
      apply hf'
  · intro hf
    refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
    rw [Pi.cons_eta]
Membership Criterion for Multiset Cartesian Product: $f \in \text{pi}(m, t) \leftrightarrow \forall a \in m, f(a) \in t(a)$
Informal description
For any multiset $m$ over a type $\alpha$ and a family of multisets $t(a)$ over types $\beta(a)$ for each $a \in \alpha$, a dependent function $f$ (where $f(a) \in \beta(a)$ for each $a \in m$) belongs to the cartesian product $\text{pi}(m, t)$ if and only if for every $a \in m$ and every proof $h$ that $a \in m$, the value $f(a, h)$ is an element of $t(a)$.