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 #
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
FinVec.map f v = ![f (v 0), f (v 1), ...]
Equations
- FinVec.map f = FinVec.seq fun (x : Fin m) => f
Instances For
Expand v
to ![v 0, v 1, ...]
Equations
Instances For
∀
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
∃
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
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
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
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) let x : «$val» =Q FinVec.prod «$f_2» := ⋯ pure ⟨q(«$val»), q(⋯)⟩
Instances For
Creates the expression f 0 * f 1 * ... * f (n - 1)
.
Instances For
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) let x : «$val» =Q FinVec.sum «$f_2» := ⋯ pure ⟨q(«$val»), q(⋯)⟩
Instances For
Creates the expression f 0 + f 1 + ... + f (n - 1)
.
Instances For
Rewrites ∏ i : Fin n, f i
as f 0 * f 1 * ... * f (n - 1)
when n
is a numeral.
Instances For
Rewrites ∑ i : Fin n, f i
as f 0 + f 1 + ... + f (n - 1)
when n
is a numeral.