Unreachable code

Stream: new members

[Vivek Rajesh Joshi]

This is a function that's supposed to eliminate all the entries below the (i,j)th entry of a matrix. Every time I try to execute it, Lean shows me this error:
Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: unreachable code
And then stops processing this file.
Can anyone tell me why this is happening, and how to fix it? I suspect it is because of an infinite recursion happening somewhere in the function, but I can't figure out where.

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

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

variable {F} in
def Matrix.rowRec {motive : {m : Nat} → Matrix (Fin m) α F → Sort _}
  (zero : (M : Matrix (Fin 0) α F) → motive M)
  (succ : {m : Nat} → (ih : (M : Matrix (Fin m) α F) → motive M) → ((M : Matrix (Fin m.succ) α F) → motive M)) :
  {m : Nat} → (M : Matrix (Fin m) α F) → motive M :=
  fun {m} ↦
  match m with
  | 0 => zero
  | _+1 => succ (Matrix.rowRec zero succ)

variable {F} in
def Matrix.firstkRows (M : Matrix (Fin m) (Fin n) F) (k : ℕ) (hk : k ≤ m) : Matrix (Fin k) (Fin n) F :=
  M.submatrix (fun i => i.castLE hk) (fun j => j)

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

@[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

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

variable {F} in
def Matrix.eltColBelow (M : Matrix (Fin m) (Fin n) F) (hij : M i j = 1) : Matrix (Fin m) (Fin n) F :=
  Matrix.rowRec (motive := fun {m} M => {i : Fin m} → M i j = 1 → Matrix (Fin m) (Fin n) F)
    (zero := fun M {i} hij => M)
    (succ := fun {k} ih A {i} hij =>
      let B := A.firstkRows k (Nat.le_succ k)
      have hi : i.val < k := by sorry
      have hb : B ⟨i,hi⟩ j = 1 := by sorry
      let C := ih B hb
      let D := (ElemOp.rowMulAdd (B ⟨i,hi⟩ j)⁻¹ i ⟨m,sorry⟩ (sorry)).onMatrix F A
      let r := D (m-1)
      append_row C r)
    M hij

def matr := !![(1:Rat),0;2,0]
-- #eval matr.eltColBelow (i:=0) (j:=0) (rfl)

[Markus Himmel]

Have you made sure that all of your sorrys are actually true? For example, hi already looks dubious to me.

In modern Lean versions, trying the #eval prints

aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.

To attempt to evaluate anyway despite the risks, use the '#eval!' command.

If you use sorry to prove something like that an array index is in bounds even though it's not, then executing the code will perform the out-of-bounds access and the program will crash. This might be the case in your code as well.

[Vivek Rajesh Joshi]

Ohh right, didn't notice that. Thanks!