Dependent Pattern Matching

Stream: lean4

[Reed Mullanix]

I'm messing around with everyone's favorite toy example, length indexed vectors, and I can't figure out how to get pattern matching to do what I would expect.

inductive Vec (A : Type) : Nat → Type where
| vnil : Vec A 0
| vcons : {n : Nat} → A → Vec A n → Vec A (Nat.succ n)


def traverse_ {n : Nat} {A : Type} (v : Vec A n) (f : A → IO Unit) : IO Unit :=
  match v with
  | Vec.vnil => return ()
  | (Vec.vcons a v') => f a *> traverse v' f

This fails with the following message:

 test.lean     9   3 error           type mismatch
   Vec.vnil
 has type
   Vec A 0
 but is expected to have type
   Vec A n (lsp)

I would expect that matching on vnil would force us to unify n with 0. I also attempted to match on both n and v simultaneously, but that didn't seem to do much of anything.

[Kyle Miller]

Matching on both seems to work:

inductive Vec (A : Type) : Nat → Type where
| vnil : Vec A 0
| vcons : {n : Nat} → A → Vec A n → Vec A (Nat.succ n)


def traverse {n : Nat} {A : Type} (v : Vec A n) (f : A → IO Unit) : IO Unit :=
  match n, v with
  | 0, Vec.vnil => return ()
  | n+1, (Vec.vcons a v') => f a *> traverse v' f

[Reed Mullanix]

Weird! Yours works, but when I add parens around (n, v) in the match it breaks

[Kyle Miller]

I'm guessing it's because (n, v) is creating a term of Prod Nat (Vec A n), which is then being matched, and the product has no dependence between the two components.

[Reed Mullanix]

Ah, that would make sense. Thanks for the help :)

[Kyle Miller]

This typechecks, but it fails the termination check:

def traverse {A : Type} (v : Vec A n) (f : A → IO Unit) : IO Unit :=
  match Sigma.mk n v with
  | ⟨0, Vec.vnil⟩ => return ()
  | ⟨_, Vec.vcons a v'⟩ => f a *> traverse v' f

[Liang-Ting Chen]

Hi, I am also playing with the typical example Vec, trying to define a type-safe head function as follows:

inductive Vec (α : Type) : Nat → Type where
  | nil  :               Vec α 0
  | cons : α → Vec α n → Vec α (1 + n)

namespace Vec
  def head (xs : Vec α (1 + n)) : α :=
    match xs with
    | cons x xs => x

But Lean4 complains

dependent elimination failed, stuck at auxiliary equation
Nat.add 1 n = 0

which I don't see how to tell Lean that nil is an absurd case. The Lean3 manual has exactly the same example, but that impossible case can just be ignored.

[Sebastian Ullrich]

Nat.add is defined by recursion on the second parameter. Are you sure it's not n + 1 in the Lean 3 example?

[Daniel Fabian]

using n.succ circumvents the problem, too, btw.

[Liang-Ting Chen]

Ooops!! Thanks for solving my problem so quickly!

[Liang-Ting Chen]

Sebastian Ullrich said:

Nat.add is defined by recursion on the second parameter. Are you sure it's not n + 1 in the Lean 3 example?

Yes, you're right. It is n + 1 in the Lean 3 manual. I wasn't copying the example directly, but typed manually. I am more used to defining these operations by recursion on the first parameter.