Vector

This files defines Vec as an abbreviation of Fin n → α. (This is different with Vector.) A lot of definitions in this file are just encapsulations of those under Fin namespace; the reason to create a new namespace is to allow dot notation and to avoid potential naming collision.

Vec type is heavily used in this library, mainly because (Fin n → α) → α can be used in inductive definitions very naturally (while other solutions, including List α → α and mutual inductive, generate very complicated recursors).

theorem Nat.pair_le_pair_left {a₁ a₂ b : ℕ} (h : a₁ ≤ a₂) : pair a₁ b ≤ pair a₂ b

theorem Nat.pair_le_pair_right {b₁ b₂ a : ℕ} (h : b₁ ≤ b₂) : pair a b₁ ≤ pair a b₂

theorem Nat.pair_lt_pair_left' {a₁ a₂ b₁ b₂ : ℕ} (h₁ : a₁ < a₂) (h₂ : b₁ ≤ b₂) : pair a₁ b₁ < pair a₂ b₂

theorem Nat.pair_lt_pair_right' {a₁ a₂ b₁ b₂ : ℕ} (h₁ : a₁ ≤ a₂) (h₂ : b₁ < b₂) : pair a₁ b₁ < pair a₂ b₂

theorem Nat.pair_le_pair {a₁ a₂ b₁ b₂ : ℕ} (h₁ : a₁ ≤ a₂) (h₂ : b₁ ≤ b₂) : pair a₁ b₁ ≤ pair a₂ b₂

def Nat.reduceAddAdd : Lean.Meta.Simp.DSimproc

Equations

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

def Fin.mkOfNat (i : ℕ) (n : Lean.Expr) : Lean.Expr

Create an expression of OfNat.ofNat i : Fin (n + 1).

Equations

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

def Fin.succ_natLit : Lean.Meta.Simp.DSimproc

Equations

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

def Fin.cases1 {motive : Fin 1 → Sort u_1} (zero : motive 0) (i : Fin 1) : motive i

Equations

• Fin.cases1 zero i = Fin.cases zero (fun (x : Fin 0) => x.elim0) i

def Fin.cases2 {motive : Fin 2 → Sort u_1} (zero : motive 0) (one : motive 1) (i : Fin 2) : motive i

Equations

• Fin.cases2 zero one i = Fin.cases zero (fun (i : Fin 1) => Fin.cases one (fun (x : Fin 0) => x.elim0) i) i

def Fin.cases3 {motive : Fin 3 → Sort u_1} (zero : motive 0) (one : motive 1) (two : motive 2) (i : Fin 3) : motive i

Equations

• Fin.cases3 zero one two i = Fin.cases zero (fun (i : Fin 2) => Fin.cases one (fun (j : Fin 1) => Fin.cases two (fun (x : Fin 0) => x.elim0) j) i) i

def Fin.cases4 {motive : Fin 4 → Sort u_1} (zero : motive 0) (one : motive 1) (two : motive 2) (three : motive 3) (i : Fin 4) : motive i

Equations

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

@[simp]

theorem Fin.forall_fin_three {p : Fin 3 → Prop} : (∀ (i : Fin 3), p i) ↔ p 0 ∧ p 1 ∧ p 2

@[simp]

theorem Fin.forall_fin_four {p : Fin 4 → Prop} : (∀ (i : Fin 4), p i) ↔ p 0 ∧ p 1 ∧ p 2 ∧ p 3

@[simp]

theorem Fin.exists_fin_three {p : Fin 3 → Prop} : (∃ (i : Fin 3), p i) ↔ p 0 ∨ p 1 ∨ p 2

@[simp]

theorem Fin.exists_fin_four {p : Fin 4 → Prop} : (∃ (i : Fin 4), p i) ↔ p 0 ∨ p 1 ∨ p 2 ∨ p 3

def Fin.castAdd' {n : ℕ} (x : Fin n) (m : ℕ) : Fin (m + n)

castAdd' x m embeds x : Fin n in Fin (m + n). This is the converse of castAdd m i which embeds into Fin (n + m).

Equations

• x.castAdd' m = Fin.cast ⋯ (Fin.castAdd m x)

@[simp]

theorem Fin.castAdd'_zero {n m : ℕ} : castAdd' 0 m = 0

@[simp]

theorem Fin.castAdd'_succ {n✝ : ℕ} {x : Fin n✝} {m : ℕ} : x.succ.castAdd' m = (x.castAdd' m).succ

@[simp]

theorem Fin.castAdd'_one {n m : ℕ} : castAdd' 1 m = 1

@[simp]

theorem Fin.addNat_succ {n✝ : ℕ} {x : Fin n✝} {m : ℕ} : x.addNat (m + 1) = (x.addNat m).succ

def Fin.addCases' {m n : ℕ} {motive : Fin (m + n) → Sort u} (left : (i : Fin n) → motive (i.castAdd' m)) (right : (i : Fin m) → motive (i.addNat n)) (i : Fin (m + n)) : motive i

Equations

• Fin.addCases' left right i = if hi : ↑i < n then left ⟨↑i, hi⟩ else have hi' := ⋯; ⋯ ▸ right ⟨↑i - n, ⋯⟩

@[reducible]

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

Vec α n is an abbreviation of Fin n → α, a vector of length n.

Equations

• Vec α n = (Fin n → α)

def Vec.nil {α : Type u} : Vec α 0

Equations

• []ᵥ = Fin.elim0

def Vec.cons {α : Type u} {n : ℕ} (a : α) (v : Vec α n) : Vec α (n + 1)

Equations

• a ∷ᵥ v = Fin.cons a v

def Vec.«term_∷ᵥ_» : Lean.TrailingParserDescr

Equations

• Vec.«term_∷ᵥ_» = Lean.ParserDescr.trailingNode `Vec.«term_∷ᵥ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ᵥ ") (Lean.ParserDescr.cat `term 67))

def Vec.vec : Lean.ParserDescr

Equations

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

def Vec.unexpandNil : Lean.PrettyPrinter.Unexpander

Equations

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

def Vec.unexpandCons : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem Vec.cons_succ {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} {i : Fin n✝} : (a ∷ᵥ v) i.succ = v i

theorem Vec.cons_zero {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} : (a ∷ᵥ v) 0 = a

theorem Vec.cons_one {α : Type u} {n : ℕ} {a : α} {v : Vec α (n + 1)} : (a ∷ᵥ v) 1 = v 0

theorem Vec.cons_two {α : Type u} {n : ℕ} {a : α} {v : Vec α (n + 2)} : (a ∷ᵥ v) 2 = v 1

theorem Vec.cons_three {α : Type u} {n : ℕ} {a : α} {v : Vec α (n + 3)} : (a ∷ᵥ v) 3 = v 2

partial def Vec.matchVecConsPrefix (n e : Lean.Expr) : Lean.MetaM (List Lean.Expr × Lean.Expr × Lean.Expr)

def Vec.cons_natLit : Lean.Meta.Simp.DSimproc

Equations

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

theorem Vec.ext {α : Type u} {n : ℕ} {v₁ v₂ : Vec α n} : (∀ (i : Fin n), v₁ i = v₂ i) → v₁ = v₂

theorem Vec.ext_iff {α : Type u} {n : ℕ} {v₁ v₂ : Vec α n} : v₁ = v₂ ↔ ∀ (i : Fin n), v₁ i = v₂ i

def Vec.head {α : Type u} {n : ℕ} (v : Vec α (n + 1)) : α

Equations

• v.head = v 0

@[simp]

theorem Vec.head_cons {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} : (a ∷ᵥ v).head = a

def Vec.tail {α : Type u} {n : ℕ} (v : Vec α (n + 1)) : Vec α n

Equations

• v.tail = v ∘ Fin.succ

@[simp]

theorem Vec.tail_apply {α : Type u} {n : ℕ} {x : Fin n} {v : Vec α (n + 1)} : v.tail x = v x.succ

@[simp]

theorem Vec.tail_cons {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} : (a ∷ᵥ v).tail = v

@[simp]

theorem Vec.cons_eq_iff {α✝ : Type u_1} {a₁ : α✝} {n✝ : ℕ} {v₁ : Vec α✝ n✝} {a₂ : α✝} {v₂ : Vec α✝ n✝} : a₁ ∷ᵥ v₁ = a₂ ∷ᵥ v₂ ↔ a₁ = a₂ ∧ v₁ = v₂

theorem Vec.eq_nil {α : Type u} (v : Vec α 0) : v = []ᵥ

theorem Vec.eq_cons {α : Type u} {n : ℕ} (v : Vec α (n + 1)) : v = v.head ∷ᵥ v.tail

theorem Vec.eq_one {α : Type u} (v : Vec α 1) : v = [v 0]ᵥ

theorem Vec.eq_two {α : Type u} (v : Vec α 2) : v = [v 0, v 1]ᵥ

theorem Vec.eq_three {α : Type u} (v : Vec α 3) : v = [v 0, v 1, v 2]ᵥ

theorem Vec.eq_four {α : Type u} (v : Vec α 4) : v = [v 0, v 1, v 2, v 3]ᵥ

def Vec.tacticSimp_vec_ : Lean.ParserDescr

Equations

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

theorem Vec.exists_vec_succ {α : Type u} {n : ℕ} {p : Vec α (n + 1) → Prop} : (∃ (v : Vec α (n + 1)), p v) ↔ ∃ (a : α) (v : Vec α n), p (a ∷ᵥ v)

@[simp]

theorem Vec.exists_vec0 {α : Type u} {p : Vec α 0 → Prop} : (∃ (v : Vec α 0), p v) ↔ p []ᵥ

@[simp]

theorem Vec.exists_vec1 {α : Type u} {p : Vec α 1 → Prop} : (∃ (v : Vec α 1), p v) ↔ ∃ (x : α), p [x]ᵥ

@[simp]

theorem Vec.exists_vec2 {α : Type u} {p : Vec α 2 → Prop} : (∃ (v : Vec α 2), p v) ↔ ∃ (x : α) (y : α), p [x, y]ᵥ

@[simp]

theorem Vec.exists_vec3 {α : Type u} {p : Vec α 3 → Prop} : (∃ (v : Vec α 3), p v) ↔ ∃ (x : α) (y : α) (z : α), p [x, y, z]ᵥ

def Vec.rec {α : Type u} {motive : {n : ℕ} → Vec α n → Sort v} (nil : motive []ᵥ) (cons : {n : ℕ} → (a : α) → (v : Vec α n) → motive v → motive (a ∷ᵥ v)) {n : ℕ} (v : Vec α n) : motive v

Equations

• Vec.rec nil cons v = ⋯ ▸ nil
• Vec.rec nil cons v = ⋯ ▸ cons v.head v.tail (Vec.rec nil cons v.tail)

@[simp]

theorem Vec.rec_nil {α : Type u} {motive : {n : ℕ} → Vec α n → Sort v} (nil : motive []ᵥ) (cons : {n : ℕ} → (a : α) → (v : Vec α n) → motive v → motive (a ∷ᵥ v)) : rec nil (fun {n : ℕ} => cons) []ᵥ = nil

@[simp]

theorem Vec.rec_cons {α : Type u} {motive : {n : ℕ} → Vec α n → Sort v} (nil : motive []ᵥ) (cons : {n : ℕ} → (a : α) → (v : Vec α n) → motive v → motive (a ∷ᵥ v)) {a : α} {n✝ : ℕ} {v : Vec α n✝} : rec nil (fun {n : ℕ} => cons) (a ∷ᵥ v) = cons a v (rec nil (fun {n : ℕ} => cons) v)

theorem Vec.comp_cons {α✝ : Type u_1} {δ✝ : Type u_2} {f : α✝ → δ✝} {a : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} : f ∘ (a ∷ᵥ v) = f a ∷ᵥ f ∘ v

def Vec.rcons {α : Type u} {n : ℕ} (v : Vec α n) (x : α) : Vec α (n + 1)

Equations

• v.rcons x = Fin.snoc v x

@[simp]

theorem Vec.rcons_nil {α✝ : Type u_1} {x : α✝} : []ᵥ.rcons x = [x]ᵥ

@[simp]

theorem Vec.rcons_cons {α✝ : Type u_1} {x : α✝} {n✝ : ℕ} {v : Vec α✝ n✝} {y : α✝} : (x ∷ᵥ v).rcons y = x ∷ᵥ v.rcons y

@[simp]

theorem Vec.rcons_last {α✝ : Type u_1} {n✝ : ℕ} {v : Vec α✝ n✝} {a : α✝} : v.rcons a (Fin.last n✝) = a

@[simp]

theorem Vec.rcons_castSucc {α✝ : Type u_1} {n✝ : ℕ} {v : Vec α✝ n✝} {a : α✝} {x : Fin n✝} : v.rcons a x.castSucc = v x

def Vec.append {α : Type u} {n m : ℕ} (v₁ : Vec α n) (v₂ : Vec α m) : Vec α (m + n)

append v₁ v₂ adds elements in v₁ : Vec α n before elements in v₂ : Vec α m, but returns a vector of length m + n. This is the converse of Fin.append which returns vector of n + m.

Equations

• v ++ᵥ v₂ = v₂
• v ++ᵥ v₂ = v.head ∷ᵥ (v.tail ++ᵥ v₂)

def Vec.«term_++ᵥ_» : Lean.TrailingParserDescr

append v₁ v₂ adds elements in v₁ : Vec α n before elements in v₂ : Vec α m, but returns a vector of length m + n. This is the converse of Fin.append which returns vector of n + m.

Equations

• Vec.«term_++ᵥ_» = Lean.ParserDescr.trailingNode `Vec.«term_++ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ᵥ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem Vec.nil_append {α✝ : Type u_1} {n✝ : ℕ} {v : Vec α✝ n✝} : []ᵥ ++ᵥ v = v

@[simp]

theorem Vec.cons_append {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {v₁ : Vec α✝ n✝} {n✝¹ : ℕ} {v₂ : Vec α✝ n✝¹} : a ∷ᵥ v₁ ++ᵥ v₂ = a ∷ᵥ (v₁ ++ᵥ v₂)

@[simp]

theorem Vec.append_left {α : Type u} {m n✝ : ℕ} {v₁ : Vec α n✝} {x : Fin n✝} {v₂ : Vec α m} : (v₁ ++ᵥ v₂) (x.castAdd' m) = v₁ x

@[simp]

theorem Vec.append_right {α : Type u} {n n✝ : ℕ} {v₂ : Vec α n✝} {x : Fin n✝} {v₁ : Vec α n} : (v₁ ++ᵥ v₂) (x.addNat n) = v₂ x

theorem Vec.eq_append {α : Type u} {m n : ℕ} (v : Vec α (m + n)) : v = (fun (i : Fin n) => v (i.castAdd' m)) ++ᵥ fun (i : Fin m) => v (i.addNat n)

def Vec.append_natLit_left : Lean.Meta.Simp.DSimproc

Equations

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

instance Vec.decEq {α : Type u} {n : ℕ} [DecidableEq α] : DecidableEq (Vec α n)

Equations

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

def Vec.max {n : ℕ} : Vec ℕ n → ℕ

Equations

• x_2.max = 0
• v.max = v.head.max v.tail.max

theorem Vec.le_max {n : ℕ} {v : Vec ℕ n} (i : Fin n) : v i ≤ v.max

theorem Vec.max_le {n m : ℕ} {v : Vec ℕ n} : (∀ (i : Fin n), v i ≤ m) → v.max ≤ m

theorem Vec.max_le_iff {n m : ℕ} {v : Vec ℕ n} : v.max ≤ m ↔ ∀ (i : Fin n), v i ≤ m

@[simp]

theorem Vec.max_zero {n : ℕ} : (max fun (x : Fin n) => 0) = 0

theorem Vec.max_eq_nth {n : ℕ} (v : Vec ℕ (n + 1)) : ∃ (i : Fin (n + 1)), v.max = v i

theorem Vec.le_max_iff {n m : ℕ} {v : Vec ℕ (n + 1)} : m ≤ v.max ↔ ∃ (i : Fin (n + 1)), m ≤ v i

theorem Vec.max_pos_iff {n : ℕ} {v : Vec ℕ n} : v.max > 0 ↔ ∃ (i : Fin n), v i > 0

theorem Vec.max_zero_iff {n : ℕ} {v : Vec ℕ n} : v.max = 0 ↔ ∀ (i : Fin n), v i = 0

def Vec.paired {n : ℕ} : Vec ℕ n → ℕ

paired [a₁, ⋯, aₙ]ᵥ is ⟪a₁, ⟪a₂, ⟪⋯, ⟪aₙ, 0⟫⟫⟫ where ⟪x, y⟫ is Nat.pair.

Equations

• x_2.paired = 0
• v.paired = Nat.pair v.head v.tail.paired

theorem Vec.le_paired {n : ℕ} {i : Fin n} {v : Vec ℕ n} : v i ≤ v.paired

theorem Vec.paired_le_paired {n : ℕ} {v₁ v₂ : Vec ℕ n} : (∀ (i : Fin n), v₁ i ≤ v₂ i) → v₁.paired ≤ v₂.paired

@[simp]

theorem Vec.paired_nil {v : Vec ℕ 0} : v.paired = 0

@[simp]

theorem Vec.unpair_paired {n : ℕ} {v : Vec ℕ (n + 1)} : Nat.unpair v.paired = (v.head, v.tail.paired)

def Vec.encode {α : Type u} [Encodable α] {n : ℕ} (v : Vec α n) : ℕ

Equations

• v.encode = Vec.paired fun (i : Fin n) => Encodable.encode (v i)

def Vec.decode {α : Type u} [Encodable α] (n k : ℕ) : Option (Vec α n)

Equations

• Vec.decode 0 x✝ = if x✝ = 0 then some []ᵥ else none
• Vec.decode n.succ x✝ = do let a ← Encodable.decode (Nat.unpair x✝).1 let v ← Vec.decode n (Nat.unpair x✝).2 some (a ∷ᵥ v)

theorem Vec.encode_decode {α : Type u} [Encodable α] {n : ℕ} {v : Vec α n} : decode n v.encode = some v

instance Vec.encodable {α : Type u} [Encodable α] {n : ℕ} : Encodable (Vec α n)

Equations

• Vec.encodable = { encode := fun (v : Vec α n) => v.encode, decode := fun (k : ℕ) => Vec.decode n k, encodek := ⋯ }

@[simp]

theorem Vec.encode_nil {α : Type u} [Encodable α] {v : Vec α 0} : Encodable.encode v = 0

@[simp]

theorem Vec.encode_cons {α : Type u} [Encodable α] {n : ℕ} {a : α} {v : Vec α n} : Encodable.encode (a ∷ᵥ v) = Nat.pair (Encodable.encode a) (Encodable.encode v)

theorem Vec.encode_eq {α : Type u} [Encodable α] {n : ℕ} {v : Vec α n} : Encodable.encode v = paired fun (i : Fin n) => Encodable.encode (v i)

instance Vec.instCountable {α : Type u} {n : ℕ} [Countable α] : Countable (Vec α n)

def Vec.toList {α : Type u} {n : ℕ} (v : Vec α n) : List α

Equations

• v_1.toList = []
• v_1.toList = v_1.head :: v_1.tail.toList

instance Vec.instRepr {α : Type u} {n : ℕ} [Repr α] : Repr (Vec α n)

Equations

• Vec.instRepr = { reprPrec := fun (v : Vec α n) (x : ℕ) => Std.Format.bracketFill "[" (Std.Format.joinSep (Vec.toList (repr ∘ v)) (Std.Format.text ", ")) "]ᵥ" }