Redundant alternative

Stream: new members

[Vivek Rajesh Joshi]

I'm trying to define a recursive function to run the back substitution part of the Gaussian elimination algorithm. I'm recursing over a list of the row vectors of a matrix. For the head::tail case, Lean is giving me the error "redundant alternative". Why is it appearing, and what can I do to rectify it?

import Mathlib.Data.Matrix.Notation

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

def I : Matrix (Fin m) (Fin m) Rat := Matrix.diagonal (fun _ => (1:Rat))

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)) : Matrix (Fin m) (Fin n) Rat :=
match E with
| scalarMul c _ i => M.updateRow i (c • (M i))
| rowSwap i j => let newr := (M i)
    Matrix.updateRow (Matrix.updateRow M i (M j)) j newr
| rowMulAdd c i j => M.updateRow i (M i + (c • (M j)))

def elemMat (E : ElemOp (m:=m)) := ElemOpOnMatrix I E

#eval elemMat (scalarMul 3 (by norm_num) 0 (m:=3))
#eval elemMat (rowSwap 1 2 (m:=4))
#eval elemMat (rowMulAdd 9 0 2 (m:=3))

def elimColAbove_ij (i : Fin m) (j : Fin n) : List (Matrix (Fin m) (Fin m) Rat) :=
  List.ofFn fun r : Fin i => elemMat (rowMulAdd (-M ⟨r,Fin.val_lt_of_le r (le_of_lt i.2)⟩ j) ⟨r,Fin.val_lt_of_le r (le_of_lt i.2)⟩ i)

def backSubstitutionAux (rows_rev : List (Vector Rat n)) (hr : rows_rev.length ≤ m) : List (Matrix (Fin m) (Fin m) Rat) :=
  match h : rows_rev with
  | nil => []
  | a::as => -- redundant alternative
    if h' : a.toList.findIdx (fun x => x≠0) = n then []
    else
      elimColAbove_ij M ⟨rows_rev.indexOf a,_⟩ ⟨a.toList.findIdx (fun x => x≠0),_⟩ ++ (backSubstitutionAux as (Nat.le_of_succ_le hr))

(Ignore the _'s, I'll fill them in later, unless they are contributing to the error.

[Joachim Breitner]

Try writing [] or List.nil or .nil instead of nil; I'd wager lean is treating nil as a variable (which is then catch-all)

[Kyle Miller]

If there's a redundant alternative error, maybe we should look for catch-all patterns that match constructor names and add those into the error message?

[Vivek Rajesh Joshi]

Thanks! It got fixed when I changed nil to List.nil
Although I don't fully understand what the error was, when I hovered over nil it showed its type as List (Vector Rat n), so how does changing it to List.nil make it any different?

[Kevin Buzzard]

The point is that nil was also a term of this type, it was just a general term of this type.

[Kevin Buzzard]

It's exactly the same problem as this.

[Kyle Miller]

For example, if you change nil to x, it would mean the same thing and give the same error

[Vivek Rajesh Joshi]

Oh I see now, thanks!