Alternate definition of Vector in terms of Fin2

This file provides a locale Vector3 which overrides the [a, b, c] notation to create a Vector3 instead of a List.

The :: notation is also overloaded by this file to mean Vector3.cons.

def Vector3 (α : Type u) (n : ℕ) : Type u

Alternate definition of Vector based on Fin2.

Equations

• Vector3 α n = (Fin2 n → α)

instance instInhabitedVector3 {α : Type u_1} {n : ℕ} [Inhabited α] : Inhabited (Vector3 α n)

Equations

• instInhabitedVector3 = { default := fun (x : Fin2 n) => default }

@[match_pattern]

def Vector3.nil {α : Type u_1} : Vector3 α 0

The empty vector

Equations

• [] = nomatch a

@[match_pattern]

def Vector3.cons {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) : Vector3 α (Nat.succ n)

The vector cons operation

Equations

• Vector3.cons a v i = Fin2.cases' a v i

def Vector3.unexpandNil : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Vector3.unexpandCons : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Vector3.«term_::_» : Lean.TrailingParserDescr

The vector cons operation

Equations

• Vector3.«term_::_» = Lean.ParserDescr.trailingNode `Vector3.term_::_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 0))

@[simp]

theorem Vector3.cons_fz {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) : Vector3.cons a v Fin2.fz = a

@[simp]

theorem Vector3.cons_fs {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) (i : Fin2 n) : Vector3.cons a v (Fin2.fs i) = v i

@[reducible]

def Vector3.nth {α : Type u_1} {n : ℕ} (i : Fin2 n) (v : Vector3 α n) : α

Get the ith element of a vector

Equations

• Vector3.nth i v = v i

@[reducible]

def Vector3.ofFn {α : Type u_1} {n : ℕ} (f : Fin2 n → α) : Vector3 α n

Construct a vector from a function on Fin2.

Equations

• Vector3.ofFn f = f

def Vector3.head {α : Type u_1} {n : ℕ} (v : Vector3 α (Nat.succ n)) : α

Get the head of a nonempty vector.

Equations

• Vector3.head v = v Fin2.fz

def Vector3.tail {α : Type u_1} {n : ℕ} (v : Vector3 α (Nat.succ n)) : Vector3 α n

Get the tail of a nonempty vector.

Equations

• Vector3.tail v i = v (Fin2.fs i)

theorem Vector3.eq_nil {α : Type u_1} (v : Vector3 α 0) : v = []

theorem Vector3.cons_head_tail {α : Type u_1} {n : ℕ} (v : Vector3 α (Nat.succ n)) : Vector3.cons (Vector3.head v) (Vector3.tail v) = v

def Vector3.nilElim {α : Type u_1} {C : Vector3 α 0 → Sort u} (H : C []) (v : Vector3 α 0) : C v

Eliminator for an empty vector.

Equations

• Vector3.nilElim H v = Eq.mpr (_ : C v = C []) H

def Vector3.consElim {α : Type u_1} {n : ℕ} {C : Vector3 α (Nat.succ n) → Sort u} (H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)) (v : Vector3 α (Nat.succ n)) : C v

Recursion principle for a nonempty vector.

Equations

• Vector3.consElim H v = Eq.mpr (_ : C v = C (Vector3.cons (Vector3.head v) (Vector3.tail v))) (H (Vector3.head v) (Vector3.tail v))

@[simp]

theorem Vector3.consElim_cons {α : Type u_1} {n : ℕ} {C : Vector3 α (Nat.succ n) → Sort u_2} {H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)} {a : α} {t : Vector3 α n} : Vector3.consElim H (Vector3.cons a t) = H a t

def Vector3.recOn {α : Type u_1} {C : {n : ℕ} → Vector3 α n → Sort u} {n : ℕ} (v : Vector3 α n) (H0 : C []) (Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)) : C v

Recursion principle with the vector as first argument.

Equations

• Vector3.recOn v_2 H0 Hs = Vector3.nilElim H0 v_2
• Vector3.recOn v_2 H0 Hs = Vector3.consElim (fun (a : α) (t : Vector3 α n_2) => Hs a t (Vector3.recOn t H0 fun {n : ℕ} => Hs)) v_2

@[simp]

theorem Vector3.recOn_nil {α : Type u_1} {C : {n : ℕ} → Vector3 α n → Sort u_2} {H0 : C []} {Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)} : Vector3.recOn [] H0 Hs = H0

@[simp]

theorem Vector3.recOn_cons {α : Type u_1} {C : {n : ℕ} → Vector3 α n → Sort u_2} {H0 : C []} {Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)} {n : ℕ} {a : α} {v : Vector3 α n} : Vector3.recOn (Vector3.cons a v) H0 Hs = Hs a v (Vector3.recOn v H0 Hs)

def Vector3.append {α : Type u_1} {m : ℕ} {n : ℕ} (v : Vector3 α m) (w : Vector3 α n) : Vector3 α (n + m)

Append two vectors

Equations

• Vector3.append v w = Vector3.recOn v w fun {n_1 : ℕ} (a : α) (x : Vector3 α n_1) (IH : Vector3 α (n + n_1)) => Vector3.cons a IH

@[simp]

theorem Vector3.append_nil {α : Type u_1} {n : ℕ} (w : Vector3 α n) : Vector3.append [] w = w

@[simp]

theorem Vector3.append_cons {α : Type u_1} {m : ℕ} {n : ℕ} (a : α) (v : Vector3 α m) (w : Vector3 α n) : Vector3.append (Vector3.cons a v) w = Vector3.cons a (Vector3.append v w)

@[simp]

theorem Vector3.append_left {α : Type u_1} {m : ℕ} (i : Fin2 m) (v : Vector3 α m) {n : ℕ} (w : Vector3 α n) : Vector3.append v w (Fin2.left n i) = v i

@[simp]

theorem Vector3.append_add {α : Type u_1} {m : ℕ} (v : Vector3 α m) {n : ℕ} (w : Vector3 α n) (i : Fin2 n) : Vector3.append v w (Fin2.add i m) = w i

def Vector3.insert {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) : Vector3 α (Nat.succ n)

Insert a into v at index i.

Equations

• Vector3.insert a v i j = Vector3.cons a v (Fin2.insertPerm i j)

@[simp]

theorem Vector3.insert_fz {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) : Vector3.insert a v Fin2.fz = Vector3.cons a v

@[simp]

theorem Vector3.insert_fs {α : Type u_1} {n : ℕ} (a : α) (b : α) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) : Vector3.insert a (Vector3.cons b v) (Fin2.fs i) = Vector3.cons b (Vector3.insert a v i)

theorem Vector3.append_insert {α : Type u_1} {m : ℕ} {n : ℕ} (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (Nat.succ n)) (e : Nat.succ n + m = Nat.succ (n + m)) : Vector3.insert a (Vector3.append t v) (Eq.recOn e (Fin2.add i m)) = Eq.recOn e (Vector3.append t (Vector3.insert a v i))

def VectorEx {α : Type u_1} (k : ℕ) : (Vector3 α k → Prop) → Prop

"Curried" exists, i.e. ∃ x₁ ... xₙ, f [x₁, ..., xₙ].

Equations

• VectorEx 0 f = f []
• VectorEx (Nat.succ k) f = ∃ (x : α), VectorEx k fun (v : Vector3 α k) => f (Vector3.cons x v)

def VectorAll {α : Type u_1} (k : ℕ) : (Vector3 α k → Prop) → Prop

"Curried" forall, i.e. ∀ x₁ ... xₙ, f [x₁, ..., xₙ].

Equations

• VectorAll 0 f = f []
• VectorAll (Nat.succ k) f = ∀ (x : α), VectorAll k fun (v : Vector3 α k) => f (Vector3.cons x v)

theorem exists_vector_zero {α : Type u_1} (f : Vector3 α 0 → Prop) : Exists f ↔ f []

theorem exists_vector_succ {α : Type u_1} {n : ℕ} (f : Vector3 α (Nat.succ n) → Prop) : Exists f ↔ ∃ (x : α), ∃ (v : Vector3 α n), f (Vector3.cons x v)

theorem vectorEx_iff_exists {α : Type u_1} {n : ℕ} (f : Vector3 α n → Prop) : VectorEx n f ↔ Exists f

theorem vectorAll_iff_forall {α : Type u_1} {n : ℕ} (f : Vector3 α n → Prop) : VectorAll n f ↔ ∀ (v : Vector3 α n), f v

def VectorAllP {α : Type u_1} {n : ℕ} (p : α → Prop) (v : Vector3 α n) : Prop

VectorAllP p v is equivalent to ∀ i, p (v i), but unfolds directly to a conjunction, i.e. VectorAllP p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations

• VectorAllP p v = Vector3.recOn v True fun {n : ℕ} (a : α) (v : Vector3 α n) (IH : Prop) => Vector3.recOn v (p a) fun {n : ℕ} (x : α) (x : Vector3 α n) (x : Prop) => p a ∧ IH

@[simp]

theorem vectorAllP_nil {α : Type u_1} (p : α → Prop) : VectorAllP p [] = True

@[simp]

theorem vectorAllP_singleton {α : Type u_1} (p : α → Prop) (x : α) : VectorAllP p [x] = p x

@[simp]

theorem vectorAllP_cons {α : Type u_1} {n : ℕ} (p : α → Prop) (x : α) (v : Vector3 α n) : VectorAllP p (Vector3.cons x v) ↔ p x ∧ VectorAllP p v

theorem vectorAllP_iff_forall {α : Type u_1} {n : ℕ} (p : α → Prop) (v : Vector3 α n) : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

theorem VectorAllP.imp {α : Type u_1} {n : ℕ} {p : α → Prop} {q : α → Prop} (h : ∀ (x : α), p x → q x) {v : Vector3 α n} (al : VectorAllP p v) : VectorAllP q v