Mathlib.Data.Fin.Tuple.Reflection

FinVec.seq definition

: ∀ {m}, (Fin m → α → β) → (Fin m → α) → Fin m → β

Full source

/-- Evaluate `FinVec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]` -/
def seq : ∀ {m}, (Fin m → α → β) → (Fin m → α) → Fin m → β
  | 0, _, _ => ![]
  | _ + 1, f, v => Matrix.vecCons (f 0 (v 0)) (seq (Matrix.vecTail f) (Matrix.vecTail v))

Pointwise function application on tuples

Informal description

The function `FinVec.seq` takes two tuples `f : Fin m → (α → β)` and `v : Fin m → α`, and returns a tuple `Fin m → β` where each element is obtained by applying the corresponding function in `f` to the corresponding element in `v`. Specifically, for each index `i : Fin m`, the result is `(f i) (v i)`.

FinVec.seq_eq theorem

: ∀ {m} (f : Fin m → α → β) (v : Fin m → α), seq f v = fun i => f i (v i)

Full source

@[simp]
theorem seq_eq : ∀ {m} (f : Fin m → α → β) (v : Fin m → α), seq f v = fun i => f i (v i)
  | 0, _, _ => Subsingleton.elim _ _
  | n + 1, f, v =>
    funext fun i => by
      simp_rw [seq, seq_eq]
      refine i.cases ?_ fun i => ?_
      · rfl
      · rw [Matrix.cons_val_succ]
        rfl

Pointwise Function Application on Tuples

Informal description

For any natural number $m$, functions $f : \text{Fin } m \to (\alpha \to \beta)$, and vectors $v : \text{Fin } m \to \alpha$, the pointwise application of $f$ to $v$ is equal to the vector defined by $(f\, i)\,(v\, i)$ for each $i \in \text{Fin } m$. That is, \[ \text{seq } f\, v = \lambda i, f\, i\, (v\, i). \]

FinVec.map definition

(f : α → β) {m} : (Fin m → α) → Fin m → β

Full source

/-- `FinVec.map f v = ![f (v 0), f (v 1), ...]` -/
def map (f : α → β) {m} : (Fin m → α) → Fin m → β :=
  seq fun _ => f

Pointwise mapping of a function over a tuple

Informal description

The function `FinVec.map` takes a function $f : \alpha \to \beta$ and a tuple $v : \text{Fin } m \to \alpha$, and returns a new tuple $\text{Fin } m \to \beta$ where each element is obtained by applying $f$ to the corresponding element of $v$. That is, for each index $i \in \text{Fin } m$, the result is $f(v(i))$.

FinVec.map_eq theorem

(f : α → β) {m} (v : Fin m → α) : map f v = f ∘ v

Full source

/-- This can be used to prove
```lean
example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
  (map_eq _ _).symm
```
-/
@[simp]
theorem map_eq (f : α → β) {m} (v : Fin m → α) : map f v = f ∘ v :=
  seq_eq _ _

Pointwise Mapping Equals Function Composition for Tuples

Informal description

For any function $f : \alpha \to \beta$ and any tuple $v : \text{Fin } m \to \alpha$, the pointwise mapping of $f$ over $v$ is equal to the composition of $f$ with $v$, i.e., \[ \text{map } f\, v = f \circ v. \]

FinVec.etaExpand definition

{m} (v : Fin m → α) : Fin m → α

Full source

/-- Expand `v` to `![v 0, v 1, ...]` -/
def etaExpand {m} (v : Fin m → α) : Fin m → α :=
  map id v

Tuple expansion to explicit form

Informal description

The function `FinVec.etaExpand` takes a tuple `v : Fin m → α` and returns a new tuple `Fin m → α` where each element is the same as in `v`. This is equivalent to applying the identity function to each element of `v`, effectively expanding `v` to its explicit form `![v 0, v 1, ...]`.

FinVec.etaExpand_eq theorem

{m} (v : Fin m → α) : etaExpand v = v

Full source

/-- This can be used to prove
```lean
example (a : Fin 2 → α) : a = ![a 0, a 1] :=
  (etaExpand_eq _).symm
```
-/
@[simp]
theorem etaExpand_eq {m} (v : Fin m → α) : etaExpand v = v :=
  map_eq id v

Tuple Expansion Identity: $\text{etaExpand } v = v$

Informal description

For any tuple $v : \text{Fin } m \to \alpha$, the expanded form $\text{etaExpand } v$ is equal to $v$ itself.

FinVec.Forall definition

: ∀ {m} (_ : (Fin m → α) → Prop), Prop

Full source

/-- `∀` with better defeq for `∀ x : Fin m → α, P x`. -/
def Forall : ∀ {m} (_ : (Fin m → α) → Prop), Prop
  | 0, P => P ![]
  | _ + 1, P => ∀ x : α, Forall fun v => P (Matrix.vecCons x v)

Universal quantification over tuples with optimized definitional equality

Informal description

The definition `FinVec.Forall` provides a way to express universal quantification over functions from `Fin m` to `α` (i.e., tuples of length `m` with elements in `α`) with better definitional equality properties. Specifically: - For `m = 0`, it reduces to `P ![]` (the empty tuple case). - For `m = n + 1`, it expands to `∀ x : α, Forall (fun v => P (x :: v))`, where `::` denotes prepending an element to a tuple. This is designed to work seamlessly with Lean's `![]` notation for tuples.

FinVec.forall_iff theorem

: ∀ {m} (P : (Fin m → α) → Prop), Forall P ↔ ∀ x, P x

Full source

/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∀ f, P f) ↔ ∀ a₀ a₁, P ![a₀, a₁] :=
  (forall_iff _).symm
```
-/
@[simp]
theorem forall_iff : ∀ {m} (P : (Fin m → α) → Prop), ForallForall P ↔ ∀ x, P x
  | 0, P => by
    simp only [Forall, Fin.forall_fin_zero_pi]
    rfl
  | .succ n, P => by simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

Equivalence of Universal Quantification over Finite Tuples

Informal description

For any predicate $P$ on tuples of length $m$ with elements in $\alpha$, the universal quantification `Forall P` over all such tuples is equivalent to the statement that $P$ holds for every tuple $x : \text{Fin } m \to \alpha$.

FinVec.Exists definition

: ∀ {m} (_ : (Fin m → α) → Prop), Prop

Full source

/-- `∃` with better defeq for `∃ x : Fin m → α, P x`. -/
def Exists : ∀ {m} (_ : (Fin m → α) → Prop), Prop
  | 0, P => P ![]
  | _ + 1, P => ∃ x : α, Exists fun v => P (Matrix.vecCons x v)

Existential quantifier for finite vectors with improved definitional behavior

Informal description

The existential quantifier for functions from `Fin m` to `α`, defined recursively to have better definitional equality properties. Specifically: - For `m = 0`, it evaluates to `P ![]` (the predicate applied to the empty vector) - For `m = n + 1`, it expands to `∃ x : α, ∃ v : Fin n → α, P (x :: v)` (using vector cons notation) This definition is designed to work well with Lean's definitional equality when used with the `![]` vector notation.

FinVec.exists_iff theorem

: ∀ {m} (P : (Fin m → α) → Prop), Exists P ↔ ∃ x, P x

Full source

/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∃ f, P f) ↔ ∃ a₀ a₁, P ![a₀, a₁] :=
  (exists_iff _).symm
```
-/
theorem exists_iff : ∀ {m} (P : (Fin m → α) → Prop), ExistsExists P ↔ ∃ x, P x
  | 0, P => by
    simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
    rfl
  | .succ n, P => by simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]

Equivalence of Existential Quantifiers for Finite Vectors

Informal description

For any natural number $m$ and any predicate $P$ on functions from $\text{Fin}\, m$ to $\alpha$, the existential statement $\exists f, P(f)$ is equivalent to $\exists x, P(x)$, where $x$ is a function of type $\text{Fin}\, m \to \alpha$.

FinVec.sum definition

[Add α] [Zero α] : ∀ {m} (_ : Fin m → α), α

Full source

/-- `Finset.univ.sum` with better defeq for `Fin`. -/
def sum [Add α] [Zero α] : ∀ {m} (_ : Fin m → α), α
  | 0, _ => 0
  | 1, v => v 0
  | _ + 2, v => sum (fun i => v (Fin.castSucc i)) + v (Fin.last _)

Sum of a finite tuple

Informal description

The function computes the sum of a tuple of elements of type $\alpha$ indexed by $\text{Fin}\, m$, where $\alpha$ is equipped with an addition operation and a zero element. For $m = 0$, the sum is $0$. For $m = 1$, the sum is the single element $v(0)$. For $m \geq 2$, the sum is defined recursively as the sum of the first $m-1$ elements plus the last element $v(\text{last}\, m)$.

FinVec.prod definition

[Mul α] [One α] : ∀ {m} (_ : Fin m → α), α

Full source

/-- `Finset.univ.prod` with better defeq for `Fin`. -/
@[to_additive existing]
def prod [Mul α] [One α] : ∀ {m} (_ : Fin m → α), α
  | 0, _ => 1
  | 1, v => v 0
  | _ + 2, v => prod (fun i => v (Fin.castSucc i)) * v (Fin.last _)

Product of a finite tuple

Informal description

The product of a tuple of elements $(v_0, \ldots, v_{m-1})$ in a type $\alpha$ equipped with multiplication and a multiplicative identity, defined recursively as: - $1$ when $m = 0$, - $v_0$ when $m = 1$, - $\prod_{i=0}^{m-2} v_i \cdot v_{m-1}$ when $m \geq 2$.

FinVec.prod_eq theorem

[CommMonoid α] : ∀ {m} (a : Fin m → α), prod a = ∏ i, a i

Full source

/-- This can be used to prove
```lean
example [CommMonoid α] (a : Fin 3 → α) : ∏ i, a i = a 0 * a 1 * a 2 :=
  (prod_eq _).symm
```
-/
@[to_additive (attr := simp)
"This can be used to prove
```lean
example [AddCommMonoid α] (a : Fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
  (sum_eq _).symm
```"]
theorem prod_eq [CommMonoid α] : ∀ {m} (a : Fin m → α), prod a = ∏ i, a i
  | 0, _ => rfl
  | 1, a => (Fintype.prod_unique a).symm
  | n + 2, a => by rw [Fin.prod_univ_castSucc, prod, prod_eq]

Product of Tuple Equals Indexed Product in Commutative Monoid

Informal description

For any commutative monoid $\alpha$ and any tuple $a : \text{Fin}\, m \to \alpha$, the product $\text{prod}\, a$ is equal to the product $\prod_{i} a\, i$ over all indices $i \in \text{Fin}\, m$.

FinVec.mkProdEqQ definition

{u : Level} {α : Q(Type u)} (inst : Q(CommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
    MetaM <| (val : Q($α)) × Q(∏ i, $f i = $val)

Full source

/-- Produce a term of the form `f 0 * f 1 * ... * f (n - 1)` and an application of `FinVec.prod_eq`
that shows it is equal to `∏ i, f i`. -/
def mkProdEqQ {u : Level} {α : Q(Type u)} (inst : Q(CommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
    MetaM <| (val : Q($α)) × Q(∏ i, $f i = $val) := do
  match n with
  | 0 => return ⟨q((1 : $α)), q(Fin.prod_univ_zero $f)⟩
  | m + 1 =>
    let nezero : Q(NeZero ($m + 1)) := q(⟨Nat.succ_ne_zero _⟩)
    let val ← makeRHS (m + 1) f nezero (m + 1)
    let _ : $val =Q FinVec.prod $f := ⟨⟩
    return ⟨q($val), q(FinVec.prod_eq $f |>.symm)⟩
where
  /-- Creates the expression `f 0 * f 1 * ... * f (n - 1)`. -/
  makeRHS (n : ℕ) (f : Q(Fin $n → $α)) (nezero : Q(NeZero $n)) (k : ℕ) : MetaM Q($α) := do
  match k with
  | 0 => failure
  | 1 => pure q($f 0)
  | m + 1 =>
    let pre ← makeRHS n f nezero m
    let mRaw : Q(ℕ) := mkRawNatLit m
    pure q($pre * $f (OfNat.ofNat $mRaw))

Product of a finite tuple in a commutative monoid

Informal description

Given a commutative monoid $\alpha$ and a natural number $n$, the function constructs a term of the form $f(0) * f(1) * \cdots * f(n-1)$ along with a proof that this product is equal to $\prod_{i} f(i)$ for a given function $f : \text{Fin } n \to \alpha$.

FinVec.mkSumEqQ definition

{u : Level} {α : Q(Type u)} (inst : Q(AddCommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
    MetaM <| (val : Q($α)) × Q(∑ i, $f i = $val)

Full source

/-- Produce a term of the form `f 0 + f 1 + ... + f (n - 1)` and an application of `FinVec.sum_eq`
that shows it is equal to `∑ i, f i`. -/
def mkSumEqQ {u : Level} {α : Q(Type u)} (inst : Q(AddCommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
    MetaM <| (val : Q($α)) × Q(∑ i, $f i = $val) := do
  match n with
  | 0 => return ⟨q((0 : $α)), q(Fin.sum_univ_zero $f)⟩
  | m + 1 =>
    let nezero : Q(NeZero ($m + 1)) := q(⟨Nat.succ_ne_zero _⟩)
    let val ← makeRHS (m + 1) f nezero (m + 1)
    let _ : $val =Q FinVec.sum $f := ⟨⟩
    return ⟨q($val), q(FinVec.sum_eq $f |>.symm)⟩
where
  /-- Creates the expression `f 0 + f 1 + ... + f (n - 1)`. -/
  makeRHS (n : ℕ) (f : Q(Fin $n → $α)) (nezero : Q(NeZero $n)) (k : ℕ) : MetaM Q($α) := do
  match k with
  | 0 => failure
  | 1 => pure q($f 0)
  | m + 1 =>
    let pre ← makeRHS n f nezero m
    let mRaw : Q(ℕ) := mkRawNatLit m
    pure q($pre + $f (OfNat.ofNat $mRaw))

Sum of a finite tuple in an additively commutative monoid

Informal description

Given an additively commutative monoid $\alpha$ and a natural number $n$, the function constructs a term of the form $f(0) + f(1) + \cdots + f(n-1)$ along with a proof that this sum is equal to $\sum_{i} f(i)$ for a given function $f : \text{Fin } n \to \alpha$.

Fin.prod_univ_ofNat definition

: Lean.Meta.Simp.Simproc

Full source

/-- Rewrites `∏ i : Fin n, f i` as `f 0 * f 1 * ... * f (n - 1)` when `n` is a numeral. -/
simproc_decl prod_univ_ofNat (∏ _ : Fin _, _) := .ofQ fun u _ e => do
  match u, e with
  | .succ _, ~q(@Finset.prod (Fin $n) _ $inst (@Finset.univ _ $instF) $f) => do
    match (generalizing := false) n.nat? with
    | .none =>
      return .continue
    | .some nVal =>
      let ⟨res, pf⟩ ← mkProdEqQ inst nVal f
      let ⟨_⟩ ← assertDefEqQ q($instF) q(Fin.fintype _)
      have _ : $n =Q $nVal := ⟨⟩
      return .visit <| .mk q($res) <| some q($pf)
  | _, _ => return .continue

Product expansion for finite tuples with numeral indices

Informal description

The definition rewrites the product $\prod_{i : \text{Fin } n} f(i)$ as $f(0) * f(1) * \cdots * f(n-1)$ when $n$ is a numeral. This allows for definitional expansion when working with concrete values of $n$.

Fin.sum_univ_ofNat definition

: Lean.Meta.Simp.Simproc

Full source

/-- Rewrites `∑ i : Fin n, f i` as `f 0 + f 1 + ... + f (n - 1)` when `n` is a numeral. -/
simproc_decl sum_univ_ofNat (∑ _ : Fin _, _) := .ofQ fun u _ e => do
  match u, e with
  | .succ _, ~q(@Finset.sum (Fin $n) _ $inst (@Finset.univ _ $instF) $f) => do
    match n.nat? with
    | .none =>
      return .continue
    | .some nVal =>
      let ⟨res, pf⟩ ← mkSumEqQ inst nVal f
      let ⟨_⟩ ← assertDefEqQ q($instF) q(Fin.fintype _)
      have _ : $n =Q $nVal := ⟨⟩
      return .visit <| .mk q($res) <| some q($pf)
  | _, _ => return .continue

Sum expansion for finite tuples with numeral indices

Informal description

The definition rewrites the sum $\sum_{i : \text{Fin } n} f(i)$ as $f(0) + f(1) + \cdots + f(n-1)$ when $n$ is a numeral. This allows for definitional expansion when working with concrete values of $n$.

Main definitions