Lean not acknowledging value of term in recursor

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable (F : Type) [Field F] [DecidableEq F]

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

namespace ElemOp

variable {F} in
@[simp] def onMatrix (E : ElemOp F m) (A : Matrix (Fin m) (Fin k) F) : Matrix (Fin m) (Fin k) F :=
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)))

end ElemOp

inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m (n+1)
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm (m+1) (n+1)
deriving Repr

variable {F} in
def RowEchelonForm.toMatrix (R : RowEchelonForm F m n) : Matrix (Fin m) (Fin n) F :=
  match R with
  | nil => fun _ => ![]
  | pad R0 => FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix
  | extend R0 v => Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix)

variable {F} in
def RowEchelonForm.pivots (R : RowEchelonForm F m n) : List {(i,j) : (Fin m)×(Fin n) | R.toMatrix i j = 1} :=
  match R with
  | nil => []
  | pad M => M.pivots.map (fun ⟨(i,j),hij⟩ => ⟨(i,j.succ),by simp at hij; simp [toMatrix,hij]⟩)
  | extend M _ => ⟨(0,0),by simp [toMatrix]⟩ :: (M.pivots.map (fun ⟨(i,j),hij⟩ => ⟨(i.succ,j.succ),by simp at hij; simp [toMatrix,hij]⟩))

variable {F} in
def RowEchelonForm.zerosAtPivots (R0 : RowEchelonForm F m n) (w : Fin n → F) : Prop := (R0.pivots.all (fun ⟨(_,j),_⟩ => w j = 0))

@[instance]
def RowEchelonForm.decidable_zerosAtPivots (R : RowEchelonForm F m n) (w : Fin n → F) : Decidable (R.zerosAtPivots w) :=
  inferInstanceAs (Decidable (R.pivots.all (fun ⟨(_,j),_⟩ => w j = 0)))

def RowEchelonForm.isReduced : RowEchelonForm F m n → Prop
  | nil => True
  | pad R0 => R0.isReduced
  | extend R0 w => (R0.zerosAtPivots w) ∧ (R0.isReduced)

def RowReducedEchelonForm (m n : Nat) := {R : RowEchelonForm F m n // R.isReduced}

@[instance]
def RowEchelonForm.decidable_isReduced (R : RowEchelonForm F m n) : Decidable (R.isReduced) :=
  match R with
  | .nil => .isTrue (trivial)
  | .pad R0 => R0.decidable_isReduced
  | .extend R0 v => instDecidableAnd (dq := R0.decidable_isReduced)

variable {F} in
def RowReducedEchelonForm.extend_eltPivotColEntries (R0 : RowReducedEchelonForm F m n) (v : Fin n → F) : {w : Fin n → F // R0.1.zerosAtPivots w} :=
  R0.1.pivots.rec
  (⟨v,by dsimp [RowEchelonForm.zerosAtPivots]; simp; intro a b R h; simp at h⟩)      --error here
  (fun ⟨(i,j),_⟩ l iw =>
  let w := (iw + (-(v j))•(R0.1.toMatrix i))
  have hw : R0.1.zerosAtPivots w := by sorry
  ⟨w,hw⟩)

In this code, in the last function, how do I make Lean acknowledge that R0.1.pivots is taking the value List.nil in the first argument of the recursor?

[Giacomo Stevanato]

Vivek Rajesh Joshi said:

how do I make Lean acknowledge that R0.1.pivots is taking the value List.nil in the first argument of the recursor?

If you want this then you can't do induction. Intuitively with induction you're trying to prove something for all lists, so you can't assume that the given list (List.nil in this case) is equal to your list of interest (R0.1.pivots). Or, in other words, you're proving something for your list by proving that it holds for its tail, and that tail's tail, and so on until such tail becomes an empty list; these tails will obviously be different than your original list.

If you want such equality proof then you want to match on R0.1.pivots to distinguish its possible cases. With match you can get a proof of equality using match eq_proof : thing_to_match with ..., which you can then use in your simp. It would look something like this:

  match eh : R0.1.pivots with
  | .nil => ⟨v, by dsimp [RowEchelonForm.zerosAtPivots]; simp; intro a b R h; simp[eh] at h⟩
  | .cons ⟨(i,j),_⟩ l =>
    let w := (iw + (-(v j))•(R0.1.toMatrix i))
    have hw : R0.1.zerosAtPivots w := by sorry
    ⟨w,hw⟩

This will of course complain about iw being not defined because since you're not doing induction. That iw didn't really make sense in the first place since it was a proof for goal though.