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

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), ...]

@[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)

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), ...]

@[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

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

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

@[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

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

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

@[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

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

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

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

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

Finset.univ.sum with better defeq for Fin.

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

Finset.univ.prod with better defeq for Fin.

@[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

@[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

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.

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.

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.

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.