feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_pr…

…oduct}_cons` (#11241) While these can be proved by `simp`, they are not rejected by the simp linter.
leanprover-community · Jan 5, 2022 · b27e33a · b27e33a
1 parent 98b64f4
commit b27e33a
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/src/data/fin/vec_notation.lean b/src/data/fin/vec_notation.lean
@@ -300,6 +300,10 @@ by { ext i, refine fin.cases _ _ i; simp [vec_head, vec_tail] }
   v + vec_cons y w = vec_cons (vec_head v + y) (vec_tail v + w) :=
 by { ext i, refine fin.cases _ _ i; simp [vec_head, vec_tail] }
 
+@[simp] lemma cons_add_cons (x : α) (v : fin n → α) (y : α) (w : fin n → α) :
+  vec_cons x v + vec_cons y w = vec_cons (x + y) (v + w) :=
+by simp
+
 @[simp] lemma head_add (a b : fin n.succ → α) : vec_head (a + b) = vec_head a + vec_head b := rfl
 
 @[simp] lemma tail_add (a b : fin n.succ → α) : vec_tail (a + b) = vec_tail a + vec_tail b := rfl
@@ -320,6 +324,10 @@ by { ext i, refine fin.cases _ _ i; simp [vec_head, vec_tail] }
   v - vec_cons y w = vec_cons (vec_head v - y) (vec_tail v - w) :=
 by { ext i, refine fin.cases _ _ i; simp [vec_head, vec_tail] }
 
+@[simp] lemma cons_sub_cons (x : α) (v : fin n → α) (y : α) (w : fin n → α) :
+  vec_cons x v - vec_cons y w = vec_cons (x - y) (v - w) :=
+by simp
+
 @[simp] lemma head_sub (a b : fin n.succ → α) : vec_head (a - b) = vec_head a - vec_head b := rfl
 
 @[simp] lemma tail_sub (a b : fin n.succ → α) : vec_tail (a - b) = vec_tail a - vec_tail b := rfl

diff --git a/src/data/matrix/notation.lean b/src/data/matrix/notation.lean
@@ -71,6 +71,10 @@ by simp [dot_product, fin.sum_univ_succ, vec_head, vec_tail]
   dot_product v (vec_cons x w) = vec_head v * x + dot_product (vec_tail v) w :=
 by simp [dot_product, fin.sum_univ_succ, vec_head, vec_tail]
 
+@[simp] lemma cons_dot_product_cons (x : α) (v : fin n → α) (y : α) (w : fin n → α) :
+  dot_product (vec_cons x v) (vec_cons y w) = x * y + dot_product v w :=
+by simp
+
 end dot_product
 
 section col_row