## Stream: new members

### Topic: Cleaning up linalg proof

#### Yakov Pechersky (Jul 09 2020 at 18:52):

I'm finding proving simple high school / college results a bit difficult. For the following result about matrix inverses, how could I clean this up further? I've already been able to make a lot of headway with field_simp. Is there some fin_cases which would populate all my let := hypotheses?

import data.matrix.notation
import tactic

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (A B : matrix (fin n) (fin n) R)

@[reducible] def mat_invertible : Prop := A * B = 1 ∧ B * A = 1

variables {α : Type u} [semiring α]
variables {m o : ℕ} {m' n' o' : Type} [fintype m'] [fintype n']

open_locale matrix

lemma mul_cons {o : ℕ} {α} [comm_semiring α]
(A : matrix (fin m.succ) (fin n.succ) α) (B : matrix (fin n.succ) (fin o.succ) α) :
A ⬝ B = (matrix.vec_cons (matrix.mul_vec A (matrix.vec_head Bᵀ)) (A ⬝ (matrix.vec_tail Bᵀ)ᵀ)ᵀ)ᵀ :=
begin
ext i j,
refine fin.cases _ _ i;
induction j with kj hkj;
induction kj with nj hnj;
{ intros, simp, refl },
end

example (A : matrix (fin 2) (fin 2) R) {a b c d : R} (hA : A = ![![a, b], ![c, d]]) :
a * d - b * c ≠ 0 ↔ ∃ B, mat_invertible A B :=
begin
split,
{ intros h,
use (1 / (a * d - b * c)) • ![![d, -b], ![-c, a]],
split;
{ ext i j,
fin_cases i;
fin_cases j;
field_simp [hA, h];
ring } },
{ intros h H,
rcases h with ⟨B, hAB, hBA⟩,
rw [<-matrix.ext_iff, hA, matrix.mul_eq_mul] at hAB hBA,
simp [mul_cons, matrix.vec_head, matrix.vec_tail] at hAB hBA,
let hAB' := hAB 0 0,
let hAB'''' := hAB 0 1,
let hAB''' := hAB 1 0,
let hAB'' := hAB 1 1,
let hBA' := hBA 0 0,
let hBA'''' := hBA 0 1,
let hBA''' := hBA 1 0,
let hBA'' := hBA 1 1,
have finne : ((0 : fin 2) ≠ 1) := fin.ne_of_vne zero_ne_one,
simp [finne] at hAB' hAB'' hAB''' hAB'''' hBA' hBA'' hBA''' hBA'''',
classical,
by_cases ha : a = 0;
by_cases hb : b = 0;
by_cases hc : c = 0;
by_cases hd : d = 0,
-- at least one element of A is zero
any_goals
{ simp [ha, hb, hc, hd, mul_zero, sub_zero, mul_eq_zero] at H,
cases H;
simp * at * },
-- all elements of A nonzero
{ have ha' : a = b * c / d,
by { rw eq_div_iff hd, rw <-sub_eq_zero, exact H },
change (a * B 0 0 + b * B 1 0 = 1) at hAB',
change (c * B 0 0 + d * B 1 0 = 0) at hAB''',
have hBv': B 1 0 = - c / d * B 0 0,
{ field_simp [hc, hd],
simp [hAB''', mul_comm] },
have hd' : d = 0,
{ field_simp [ha', ha, hb, hc, hd, hBv'] at hAB',
rw <-hAB',
ring },
exact absurd hd' hd } }
end


#### Yakov Pechersky (Jul 09 2020 at 18:53):

Additionally, something like mul_cons is not in matrix.notation. Should it be? It's a bit clunky with all the transposes.

#### Yakov Pechersky (Jul 09 2020 at 19:22):

I'm able to remove all the hAB' hypotheses. It's too bad the pretty printer doesn't have a way to flip the notation for the transposes, which makes hAB pretty ugly if simplified.

import data.matrix.notation
import tactic

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (A B : matrix (fin n) (fin n) R)

@[reducible] def mat_invertible : Prop := A * B = 1 ∧ B * A = 1

variables {α : Type u} [semiring α]
variables {m o : ℕ} {m' n' o' : Type} [fintype m'] [fintype n']

open_locale matrix

lemma mul_cons {o : ℕ} {α} [comm_semiring α]
(A : matrix (fin m.succ) (fin n.succ) α) (B : matrix (fin n.succ) (fin o.succ) α) :
A ⬝ B = (matrix.vec_cons (matrix.mul_vec A (matrix.vec_head Bᵀ)) (A ⬝ (matrix.vec_tail Bᵀ)ᵀ)ᵀ)ᵀ :=
begin
ext i j,
refine fin.cases _ _ i;
induction j with kj hkj;
induction kj with nj hnj;
{ intros, simp, refl },
end

example (A : matrix (fin 2) (fin 2) R) {a b c d : R} (hA : A = ![![a, b], ![c, d]]) :
a * d - b * c ≠ 0 ↔ ∃ B, mat_invertible A B :=
begin
split,
{ intros h,
use (1 / (a * d - b * c)) • ![![d, -b], ![-c, a]],
split;
{ ext i j,
fin_cases i;
fin_cases j;
field_simp [hA, h];
ring } },
{ intros h H,
rcases h with ⟨B, hAB, hBA⟩,
rw [<-matrix.ext_iff, hA, matrix.mul_eq_mul] at hBA,
simp [mul_cons, matrix.vec_head, matrix.vec_tail] at hBA,
let hBA' := hBA 0 0,
let hBA'''' := hBA 0 1,
let hBA''' := hBA 1 0,
let hBA'' := hBA 1 1,
have finne : ((0 : fin 2) ≠ 1) := fin.ne_of_vne zero_ne_one,
simp [finne] at hBA' hBA'' hBA''' hBA'''',
classical,
by_cases ha : a = 0;
by_cases hb : b = 0;
by_cases hc : c = 0;
by_cases hd : d = 0,
-- at least one element of A is zero
any_goals
{ simp [ha, hb, hc, hd, mul_zero, sub_zero, mul_eq_zero] at H,
cases H;
simp * at * },
-- all elements of A nonzero
{ have ha' : a = b * c / d,
by { rw eq_div_iff hd, rw <-sub_eq_zero, exact H },
change (a * B 0 0 + c * B 0 1 = 1) at hBA',
change (b * B 0 0 + d * B 0 1 = 0) at hBA'''',
have hBv : B 0 1 = - b / d * B 0 0,
{ field_simp [hb, hd],
simp [hBA'''', mul_comm] },
have hd' : d = 0,
{ field_simp [ha', ha, hb, hc, hd, hBv] at hBA',
rw <-hBA',
ring },
exact absurd hd' hd } }
end


#### Kevin Buzzard (Jul 11 2020 at 17:12):

For the "has inverse -> det isn't zero" I would use det(AB)=det(A)det(B). In fact I'd prove that det!=0 iff exists inverse for n x n matrices, prove that det(A)=ad-bc if n=2 (which was done in another thread) and then put it together. This seems like a more natural approach. I'm pretty sure we have det(AB)=det(A)det(B). You can use it to prove that if A has an inverse then det(A) is a unit, over an arbitrary commutative semiring I should think.

#### Reid Barton (Jul 11 2020 at 17:16):

We have the other direction too, nonsing_inv

#### Yakov Pechersky (Jul 12 2020 at 03:22):

I was hoping to avoid the definition of det for this particular proof

#### Yakov Pechersky (Jul 12 2020 at 03:23):

(deleted)

Last updated: May 13 2021 at 05:21 UTC