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
.
@[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
theorem
Vector3.cons_head_tail
{α : Type u_1}
{n : ℕ}
(v : Vector3 α (Nat.succ n))
:
Vector3.cons (Vector3.head v) (Vector3.tail v) = 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 0 [])
(Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C n w → C (Nat.succ n) (Vector3.cons a w))
:
C n 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 => Hs n_2 a t (Vector3.recOn t H0 fun {n} => Hs n)) v_2
Instances For
@[simp]
theorem
Vector3.recOn_nil
{α : Type u_1}
{C : {n : ℕ} → Vector3 α n → Sort u_2}
{H0 : C 0 []}
{Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C n w → C (Nat.succ n) (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 0 []}
{Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C n w → C (Nat.succ n) (Vector3.cons a w)}
{n : ℕ}
{a : α}
{v : Vector3 α n}
:
Vector3.recOn (Vector3.cons a v) H0 Hs = Hs n a v (Vector3.recOn v H0 Hs)
@[simp]
@[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.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))
theorem
exists_vector_succ
{α : Type u_1}
{n : ℕ}
(f : Vector3 α (Nat.succ n) → Prop)
:
Exists f ↔ ∃ x v, f (Vector3.cons x v)
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
.
Instances For
@[simp]
@[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