Cannot pattern match on custom inductive type

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

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

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
  match hz:row.z with
  | none => zeroVec F n
  | some p => row.h hz ▸ (zeroVec F p).append (Vector.cons 1 row.tail)

def Vector.concat (a : α) : Vector α n → Vector α (n+1) := fun v => Vector.append v ⟨[a],rfl⟩

abbrev Vector.allZero (v : Vector F n) : Prop := v.toList.all (.=0)

inductive RowReducedEchelonForm : (R : Vector (ReducedRow F n) m) → Prop where
| nil : RowReducedEchelonForm Vector.nil
| cons : (row : ReducedRow F n) → RowReducedEchelonForm R →
         ((row.toVector F).allZero) → RowReducedEchelonForm (R.concat row)

example (l : Vector (ReducedRow F n) m) (hl' : l' = l.concat r) (h : RowReducedEchelonForm F l') : (r.toVector F).allZero := by
  -- match h with
  -- | RowReducedEchelonForm.nil => sorry
  -- | RowReducedEchelonForm.cons row _ _ => sorry
  cases h with
  | RowReducedEchelonForm.nil => sorry
  | RowReducedEchelonForm.cons row _ _ => sorry

How do I pattern match on h with .nil and .cons _ _ _ in the example above?

[Kyle Miller]

You're using the cases tactic, which doesn't do pattern matching like match. It just wants the names of the constructors as-is, and deleting RowReducedEchelonForm. from each case will do it.

[Kyle Miller]

The names come from the names of the arguments to RowReducedEchelonForm.casesOn

[Vivek Rajesh Joshi]

That doesn't fix it either. I tried the match tactic that I've commented out above, it too was complaining about the argument names.

[Kyle Miller]

It fixed it for me though:

example (l : Vector (ReducedRow F n) m) (hl' : l' = l.concat r) (h : RowReducedEchelonForm F l') : (r.toVector F).allZero := by
  cases h with
  | cons row _ _ => sorry

[Kyle Miller]

The match tactic isn't complaining about argument names, but a type mismatch:

type mismatch
  RowReducedEchelonForm.nil
has type
  RowReducedEchelonForm F Vector.nil : Prop
but is expected to have type
  RowReducedEchelonForm F l' : Prop

It turns out you can fix this by deleting the nil case.

[Vivek Rajesh Joshi]

I see, so Lean can figure out by itself that h cannot be formed from the nil constructor?

[Robert Maxton]

Vivek Rajesh Joshi said:

I see, so Lean can figure out by itself that h cannot be formed from the nil constructor?

(Belated reply) Rather than that, it doesn't even get that far: it's looking for a RowReducedEchelonForm F l', and you gave it a naively-unrelated RowReducedEchelonForm F Vector.nil, so it throws an error. Instead, precisely because that constructor can never produce values of type like that of h, you can just remove that line entirely and Lean won't be bothered.