Not sure why termination works in one but not the other

Stream: lean4

[Mark Santa Clara Munro]

I was working on making a function that would turn all elements above a selected one in a Matrix, which is when I made this:

import Mathlib
variable {m n : Type*} {α R : Type*}
variable [DecidableEq m]

theorem morePrev {y : ℕ} (i : Fin y) : i - 1 < y := by
  omega

-- Operation which add x times Row j to Row i
def addMulRow [SMul R α] [Add α] (M : Matrix m n α) (i : m) (j : m) (x : R): Matrix m n α :=
  Matrix.updateRow M i (M i + x • M j)

 -- i stands for current row, j stands for specified column, y stands for the last row + 1, p stands for the row of the pivot
 -- turns all numbers on column j below row i or p into 0
 def turnAboveIntoZero [DecidableEq α] [DivisionRing α] {y : ℕ} {z : ℕ} (M : Matrix (Fin y) (Fin z) α) (i : Fin y) (j : Fin z) (p : Fin y)
   : Matrix (Fin y) (Fin z) α :=
   if (i : ℕ) - 1 = 0 then M
   else
     let iprev := (⟨i-1, morePrev i⟩ : Fin y)
     if M iprev j = 0 then turnAboveIntoZero M iprev j p
     else
       let M' := addMulRow M iprev p (-(M iprev j)/(M p j))
      turnAboveIntoZero M' iprev j p
 termination_by (i : ℕ) - 1

Unfortunately, I realized that this would end up ignoring the first row, so I changed it to:

import Mathlib
variable {m n : Type*} {α R : Type*}
variable [DecidableEq m]

theorem morePrev {y : ℕ} (i : Fin y) : i - 1 < y := by
  omega

-- Operation which add x times Row j to Row i
def addMulRow [SMul R α] [Add α] (M : Matrix m n α) (i : m) (j : m) (x : R): Matrix m n α :=
  Matrix.updateRow M i (M i + x • M j)

-- i stands for current row, j stands for specified column, y stands for the last row + 1, p stands for the row of the pivot
-- turns all numbers on column j below row i or p into 0
def turnAboveIntoZero [DecidableEq α] [DivisionRing α] {y : ℕ} {z : ℕ} (M : Matrix (Fin y) (Fin z) α) (i : Fin y) (j : Fin z) (p : Fin y)
  : Matrix (Fin y) (Fin z) α :=
  if (i : ℕ) = 0 then M
  else
    let iprev := (⟨i-1, morePrev i⟩ : Fin y)
    if M iprev j = 0 then turnAboveIntoZero M iprev j p
    else
      let M' := addMulRow M iprev p (-(M iprev j)/(M p j))
      turnAboveIntoZero M' iprev j p
termination_by (i : ℕ)

I don't understand why this wouldn't work, as i is still decreasing and will end up going to 0. I checked the bounds for Fin, to see if that was an issue, but zero is included. I don't know if I am misunderstanding termination and how it works, but as of right now I'm not sure what my issue could be.

[Edward van de Meent]

if you check the error, lean tells you why it doesn't work: it doesn't know how to prove that ⟨↑i - 1, ⋯⟩ < i (or iprev < i). particularly because the statement i-1 < i is not true for all natural numbers i.

[Edward van de Meent]

the easiest way to fix this is to add have : iprev < i := by ... right after the declaration of iprev

[Edward van de Meent]

you'll probably want to have that i isn't 0, so naming the condition is probably a good idea

[Mark Santa Clara Munro]

(deleted)

[Mark Santa Clara Munro]

Edward van de Meent said:

the easiest way to fix this is to add have : iprev < i := by ... right after the declaration of iprev

What would I use to prove that iprev < i? Even though it seems obvious I have not found a way to prove it.

[Edward van de Meent]

def turnAboveIntoZero [DecidableEq α] [DivisionRing α] {y : ℕ} {z : ℕ} (M : Matrix (Fin y) (Fin z) α) (i : Fin y) (j : Fin z) (p : Fin y)
  : Matrix (Fin y) (Fin z) α :=
  if h:(i : ℕ) = 0 then M
  else
    let iprev := (⟨i-1, morePrev i⟩ : Fin y)
    have : iprev < i := by
      unfold_let iprev
      rw [Fin.mk_lt_mk]
      exact Nat.sub_one_lt h
    if M iprev j = 0 then turnAboveIntoZero M iprev j p
    else
      let M' := addMulRow M iprev p (-(M iprev j)/(M p j))
      turnAboveIntoZero M' iprev j p
termination_by (i : ℕ)

[Edward van de Meent]

basically, it uses two key parts: naming the if-clause, making it available, and unfolding the let, to allow us to use its definition.

[Mark Santa Clara Munro]

Thank you so much for the help!! I understand it now.