Unable to rewrite, despite being identical

Stream: new members

[Vivek Rajesh Joshi]

I'm unable to rewrite an expression that shows up in the goal, despite it having the exact same terms and type. Could someone please point out what's going wrong here?

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

variable {F : Type} [Field F] [DecidableEq F]

variable (F) in
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

def Matrix.append_row (M : Matrix (Fin m) (Fin n) α) (v : (Fin n) → α) : Matrix (Fin (m+1)) (Fin n) α :=
  Fin.snoc M v

abbrev Matrix.append_k_zeroRows (M : Matrix (Fin m) (Fin n) F) (k : Nat) : Matrix (Fin (m+k)) (Fin n) F :=
  match k with
  | 0 => M
  | p+1 => append_row (append_k_zeroRows M p) 0

abbrev Matrix.cast (h1 : m = k) (h2 : n = l) : Matrix (Fin m) (Fin n) α → Matrix (Fin k) (Fin l) α :=
  match h1,h2 with
  | rfl,rfl => id

namespace RowEchelonForm

def 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)

def 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]⟩))

def truncation (R : RowEchelonForm F m n) : (m' : Nat) × RowEchelonForm F m' n :=
  match R with
  | nil => ⟨0,nil⟩
  | pad R =>
    let ⟨m, R'⟩ := truncation R
    ⟨m,pad R'⟩
  | extend R v =>
    let ⟨m,R'⟩ := truncation R
    ⟨m+1,extend R' v⟩

lemma nonzeroRows_l1 (R : RowEchelonForm F m n) : R.truncation.1 ≤ m := by
  induction R with
  | nil => simp [truncation]
  | pad R0 ih =>
    dsimp [truncation]; exact ih
  | extend R0 w ih =>
    dsimp [truncation]; exact Nat.add_le_add_right ih 1

lemma nonzeroRows_l2 (R : RowEchelonForm F m n) :
  R.toMatrix = (Matrix.append_k_zeroRows R.truncation.2.toMatrix (m - R.truncation.1)).cast (Nat.add_sub_of_le (nonzeroRows_l1 R)) (rfl) := by
  induction R with
  | @nil k => sorry
  | @pad k l R0 ih =>
    induction k with
    | zero =>
      simp [truncation]
      rw [Nat.zero_sub R0.truncation.fst]
  | extend R0 w ih => sorry

[Matt Diamond]

I think this has something to do with the fact that Lean sees Fin (j + 0) and Fin (j + (0 - k)) as two different types

[Matt Diamond]

I'm not sure how to deal with this, though... there's docs#Fin.cast but I don't think it will help with re-writing

[Etienne Marion]

There you go:

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

variable {F : Type} [Field F] [DecidableEq F]

variable (F) in
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

def Matrix.append_row (M : Matrix (Fin m) (Fin n) α) (v : (Fin n) → α) : Matrix (Fin (m+1)) (Fin n) α :=
  Fin.snoc M v

abbrev Matrix.append_k_zeroRows (M : Matrix (Fin m) (Fin n) F) (k : Nat) : Matrix (Fin (m+k)) (Fin n) F :=
  match k with
  | 0 => M
  | p+1 => append_row (append_k_zeroRows M p) 0

abbrev Matrix.cast (h1 : m = k) (h2 : n = l) : Matrix (Fin m) (Fin n) α → Matrix (Fin k) (Fin l) α :=
  match h1,h2 with
  | rfl,rfl => id

namespace RowEchelonForm

def 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)

def 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]⟩))

def truncation (R : RowEchelonForm F m n) : (m' : Nat) × RowEchelonForm F m' n :=
  match R with
  | nil => ⟨0,nil⟩
  | pad R =>
    let ⟨m, R'⟩ := truncation R
    ⟨m,pad R'⟩
  | extend R v =>
    let ⟨m,R'⟩ := truncation R
    ⟨m+1,extend R' v⟩

lemma nonzeroRows_l1 (R : RowEchelonForm F m n) : R.truncation.1 ≤ m := by
  induction R with
  | nil => simp [truncation]
  | pad R0 ih =>
    dsimp [truncation]; exact ih
  | extend R0 w ih =>
    dsimp [truncation]; exact Nat.add_le_add_right ih 1

lemma nonzeroRows_l2 (R : RowEchelonForm F m n) :
  R.toMatrix = (Matrix.append_k_zeroRows R.truncation.2.toMatrix (m - R.truncation.1)).cast (Nat.add_sub_of_le (nonzeroRows_l1 R)) (rfl) := by
  induction R with
  | @nil k => sorry
  | @pad k l R0 ih =>
    induction k with
    | zero =>
      simp [truncation]
      have := Nat.zero_sub R0.truncation.fst
      cases this
  | extend R0 w ih => sorry

[Etienne Marion]

The issue is that you can't rewrite because it will change the type of the term where you rewrite so the cast function would be applied to a term with the wrong type, which cannot happen. As Matt said Fin n and Fin (n + (0 - k)) are not definitionally equal, though they are propositionally equal. The cases tactic applied to an equality will "rewrite" the equality everywhere at the same time, even in places which rw can't reach, solving the issue. This is the best solution I know when encountering troubles with cast.