Cleaning up linalg proof

Stream: new members

[Yakov Pechersky]

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],
          rw <-eq_neg_iff_add_eq_zero at hAB''',
          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]

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

[Yakov Pechersky]

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],
          rw <-eq_neg_iff_add_eq_zero at hBA'''',
          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]

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]

We have the other direction too, nonsing_inv

[Yakov Pechersky]

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

[Yakov Pechersky]

(deleted)