# Lemmas for tuples `Fin m → α` #

This file contains alternative definitions of common operators on vectors which expand definitionally to the expected expression when evaluated on `![]` notation.

This allows "proof by reflection", where we prove `f = ![f 0, f 1]` by defining `FinVec.etaExpand f` to be equal to the RHS definitionally, and then prove that `f = etaExpand f`.

The definitions in this file should normally not be used directly; the intent is for the corresponding `*_eq` lemmas to be used in a place where they are definitionally unfolded.

## Main definitions #

- `FinVec.seq`
- `FinVec.map`
- `FinVec.sum`
- `FinVec.etaExpand`

source
def FinVec.seq {α : Type u_1} {β : Type u_2} {m : ℕ} :
(Fin m → α → β) → (Fin m → α) → Fin m → β

Evaluate `FinVec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]`

Equations

- FinVec.seq x_3 x_4 = ![]
- FinVec.seq f v = Matrix.vecCons (f 0 (v 0)) (FinVec.seq (Matrix.vecTail f) (Matrix.vecTail v))

Instances For

source
@[simp]
theorem FinVec.seq_eq {α : Type u_1} {β : Type u_2} {m : ℕ} (f : Fin m → α → β) (v : Fin m → α) :
seq f v = fun (i : Fin m) => f i (v i)
source
def FinVec.map {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} :
(Fin m → α) → Fin m → β

`FinVec.map f v = ![f (v 0), f (v 1), ...]`

Equations

- FinVec.map f = FinVec.seq fun (x : Fin m) => f

Instances For

source
@[simp]
theorem FinVec.map_eq {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} (v : Fin m → α) :
map f v = f ∘ v

This can be used to prove

    example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
      (map_eq _ _).symm

source
def FinVec.etaExpand {α : Type u_1} {m : ℕ} (v : Fin m → α) :
Fin m → α

Expand `v` to `![v 0, v 1, ...]`

Equations

- FinVec.etaExpand v = FinVec.map id v

Instances For

source
@[simp]
theorem FinVec.etaExpand_eq {α : Type u_1} {m : ℕ} (v : Fin m → α) :
etaExpand v = v

This can be used to prove

    example (a : Fin 2 → α) : a = ![a 0, a 1] :=
      (etaExpand_eq _).symm

source
def FinVec.Forall {α : Type u_1} {m : ℕ} :
((Fin m → α) → Prop) → Prop

`∀` with better defeq for `∀ x : Fin m → α, P x`.

Equations

- FinVec.Forall P = P ![]
- FinVec.Forall P = ∀ (x : α), FinVec.Forall fun (v : Fin n → α) => P (Matrix.vecCons x v)

Instances For

source
@[simp]
theorem FinVec.forall_iff {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop) :
Forall P ↔ ∀ (x : Fin m → α), P x

This can be used to prove

    example (P : (Fin 2 → α) → Prop) : (∀ f, P f) ↔ ∀ a₀ a₁, P ![a₀, a₁] :=
      (forall_iff _).symm

source
def FinVec.Exists {α : Type u_1} {m : ℕ} :
((Fin m → α) → Prop) → Prop

`∃` with better defeq for `∃ x : Fin m → α, P x`.

Equations

- FinVec.Exists P = P ![]
- FinVec.Exists P = ∃ (x : α), FinVec.Exists fun (v : Fin n → α) => P (Matrix.vecCons x v)

Instances For

source
theorem FinVec.exists_iff {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop) :
Exists P ↔ ∃ (x : Fin m → α), P x

This can be used to prove

    example (P : (Fin 2 → α) → Prop) : (∃ f, P f) ↔ ∃ a₀ a₁, P ![a₀, a₁] :=
      (exists_iff _).symm

source
def FinVec.sum {α : Type u_1} [Add α] [Zero α] {m : ℕ} :
(Fin m → α) → α

`Finset.univ.sum` with better defeq for `Fin`.

Equations

- FinVec.sum x_2 = 0
- FinVec.sum v = v 0
- FinVec.sum v = (FinVec.sum fun (i : Fin (n + 1)) => v i.castSucc) + v (Fin.last (n + 1))

Instances For

source
def FinVec.prod {α : Type u_1} [Mul α] [One α] {m : ℕ} :
(Fin m → α) → α

`Finset.univ.prod` with better defeq for `Fin`.

Equations

- FinVec.prod x_2 = 1
- FinVec.prod v = v 0
- FinVec.prod v = (FinVec.prod fun (i : Fin (n + 1)) => v i.castSucc) * v (Fin.last (n + 1))

Instances For

source
@[simp]
theorem FinVec.prod_eq {α : Type u_1} [CommMonoid α] {m : ℕ} (a : Fin m → α) :
prod a = ∏ i : Fin m, a i

This can be used to prove

    example [CommMonoid α] (a : Fin 3 → α) : ∏ i, a i = a 0 * a 1 * a 2 :=
      (prod_eq _).symm

source
@[simp]
theorem FinVec.sum_eq {α : Type u_1} [AddCommMonoid α] {m : ℕ} (a : Fin m → α) :
sum a = ∑ i : Fin m, a i

This can be used to prove

    example [AddCommMonoid α] (a : Fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
      (sum_eq _).symm

source
def FinVec.mkProdEqQ {u : Lean.Level} {α : Q(Type u)} (inst : Q(CommMonoid «$α»)) (n : ℕ) (f : Q(Fin «$n» → «$α»)) :
Lean.MetaM ((val : Q(«$α»)) × Q(∏ i : Fin «$n», «$f» i = «$val»))

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`.

Equations

- FinVec.mkProdEqQ inst 0 f_2 = pure ⟨q(1), q(⋯)⟩
- FinVec.mkProdEqQ inst m.succ f_2 = do let val ← FinVec.mkProdEqQ.makeRHS inst (m + 1) f_2 q(⋯) (m + 1) have x : «$val» =Q FinVec.prod «$f_2» := ⋯ pure ⟨q(«$val»), q(⋯)⟩

Instances For

source
def FinVec.mkProdEqQ.makeRHS {u : Lean.Level} {α : Q(Type u)} (inst : Q(CommMonoid «$α»)) (n : ℕ) (f : Q(Fin «$n» → «$α»)) (nezero : Q(NeZero «$n»)) (k : ℕ) :
Lean.MetaM Q(«$α»)

Creates the expression `f 0 * f 1 * ... * f (n - 1)`.

Equations

- FinVec.mkProdEqQ.makeRHS inst n f nezero 0 = failure
- FinVec.mkProdEqQ.makeRHS inst n f nezero 1 = pure q(«$f» 0)
- FinVec.mkProdEqQ.makeRHS inst n f nezero m.succ = do let pre ← FinVec.mkProdEqQ.makeRHS inst n f nezero m have mRaw : Q(ℕ) := Lean.mkRawNatLit m pure q(«$pre» * «$f» (OfNat.ofNat «$mRaw»))

Instances For

source
def FinVec.mkSumEqQ {u : Lean.Level} {α : Q(Type u)} (inst : Q(AddCommMonoid «$α»)) (n : ℕ) (f : Q(Fin «$n» → «$α»)) :
Lean.MetaM ((val : Q(«$α»)) × Q(∑ i : Fin «$n», «$f» i = «$val»))

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`.

Equations

- FinVec.mkSumEqQ inst 0 f_2 = pure ⟨q(0), q(⋯)⟩
- FinVec.mkSumEqQ inst m.succ f_2 = do let val ← FinVec.mkSumEqQ.makeRHS inst (m + 1) f_2 q(⋯) (m + 1) have x : «$val» =Q FinVec.sum «$f_2» := ⋯ pure ⟨q(«$val»), q(⋯)⟩

Instances For

source
def FinVec.mkSumEqQ.makeRHS {u : Lean.Level} {α : Q(Type u)} (inst : Q(AddCommMonoid «$α»)) (n : ℕ) (f : Q(Fin «$n» → «$α»)) (nezero : Q(NeZero «$n»)) (k : ℕ) :
Lean.MetaM Q(«$α»)

Creates the expression `f 0 + f 1 + ... + f (n - 1)`.

Equations

- FinVec.mkSumEqQ.makeRHS inst n f nezero 0 = failure
- FinVec.mkSumEqQ.makeRHS inst n f nezero 1 = pure q(«$f» 0)
- FinVec.mkSumEqQ.makeRHS inst n f nezero m.succ = do let pre ← FinVec.mkSumEqQ.makeRHS inst n f nezero m have mRaw : Q(ℕ) := Lean.mkRawNatLit m pure q(«$pre» + «$f» (OfNat.ofNat «$mRaw»))

Instances For

source
def Fin.prod_univ_ofNat :
Lean.Meta.Simp.Simproc

Rewrites `∏ i : Fin n, f i` as `f 0 * f 1 * ... * f (n - 1)` when `n` is a numeral.

Instances For

source
def Fin.sum_univ_ofNat :
Lean.Meta.Simp.Simproc

Rewrites `∑ i : Fin n, f i` as `f 0 + f 1 + ... + f (n - 1)` when `n` is a numeral.

Instances For