Solving induction proof without dependent induction

Stream: new members

[Vivek Rajesh Joshi]

The only thing left to show in the proof below is E \in elimColBelow_ij M i j. Can this be done without induction' hl : elimColBelow_ij M i j? As far as my experience goes with dependent induction (not much but still), it makes the inductive hypothesis pretty much useless. If someone found out how to make it useful, that would also be appreciated.

import Mathlib.Data.Matrix.Notation
import Mathlib.Tactic.Linarith

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

inductive ElemOp : Type where
| scalarMul (c : Rat) (hc : c≠0) (i : Fin m) : ElemOp
| rowSwap (i : Fin m) (j : Fin m) : ElemOp
| rowMulAdd (c : Rat) (i : Fin m) (j : Fin m) : ElemOp

namespace ElemOp

def ElemOpOnMatrix  (E : ElemOp (m:=m)) (A : Matrix (Fin m) (Fin n) Rat) : Matrix (Fin m) (Fin n) Rat :=
match E with
| scalarMul c _ i => A.updateRow i (c • (A i))
| rowSwap i j => let newr := (A i)
    Matrix.updateRow (Matrix.updateRow A i (A j)) j newr
| rowMulAdd c i j => A.updateRow i (A i + (c • (A j)))

def elemMat (E : ElemOp (m:=m)) := ElemOpOnMatrix E (1:Matrix (Fin m) (Fin m) Rat)

def List.eraseAll [DecidableEq α] : List α → α → List α
  | [],    _ => []
  | a::as, b =>
    if a = b then List.eraseAll as b
    else a :: List.eraseAll as b

def list_mat_of_ElemOp : List (ElemOp (m:=m)) → List (Matrix (Fin m) (Fin m) Rat)
  | [] => []
  | a::as => elemMat a :: list_mat_of_ElemOp as

def elimColBelow_ij (i:Fin m) (j:Fin n) : List (ElemOp (m:=m)) :=
  List.ofFn fun r : Fin (m-i-1) =>
  have h : r.val+(i.val+1)<m := (Nat.add_lt_of_lt_sub (Eq.subst (Nat.sub_sub m i.1 1) (r.2)))
  rowMulAdd (-M ⟨r+i+1,h⟩ j) ⟨r+i+1,h⟩ i

lemma rval_ival_lt (i : Fin m) (r : Fin (m-i-1)) : r.1+i.1+1 < m :=
  Nat.add_assoc _ _ _ ▸ (Nat.add_lt_of_lt_sub (Eq.subst (Nat.sub_sub m i.1 1) (r.2)))

example : (List.eraseAll (list_mat_of_ElemOp (elimColBelow_ij M i j)) (rowMulAdd (-M ⟨↑r+↑i+1,rval_ival_lt i r⟩ j) ⟨↑r+↑i+1,rval_ival_lt i r⟩ i).elemMat).prod*M = M := by
  induction' elimColBelow_ij M i j with E as ih
  · rw [list_mat_of_ElemOp,List.eraseAll,List.prod_nil, Matrix.one_mul]
  · by_cases hE : E = rowMulAdd (-M ⟨↑r + ↑i + 1,rval_ival_lt i r⟩ j) ⟨↑r + ↑i + 1,rval_ival_lt i r⟩ i
    · rw [list_mat_of_ElemOp,hE,List.eraseAll]
      simp [ih]
    · rw [list_mat_of_ElemOp,List.eraseAll,if_neg,List.prod_cons,Matrix.mul_assoc,ih]