## Stream: lean4

### Topic: Dependent Pattern Matching

#### Reed Mullanix (Jan 13 2021 at 02:20):

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 (Jan 13 2021 at 02:23):

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 (Jan 13 2021 at 02:28):

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

#### Kyle Miller (Jan 13 2021 at 02:30):

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 (Jan 13 2021 at 02:30):

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

#### Kyle Miller (Jan 13 2021 at 02:31):

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 (Apr 20 2021 at 08:15):

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

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 (Apr 20 2021 at 08:20):

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 (Apr 20 2021 at 08:27):

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

#### Liang-Ting Chen (Apr 20 2021 at 08:28):

Ooops!! Thanks for solving my problem so quickly!

#### Liang-Ting Chen (Apr 20 2021 at 08:34):

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.

Last updated: May 07 2021 at 11:09 UTC