# Zulip Chat Archive

## 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

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 (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