Zulip Chat Archive

Stream: lean4

Topic: Dependent Pattern Matching


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reed Mullanix (Jan 13 2021 at 02:28):

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

view this post on Zulip 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.

view this post on Zulip Reed Mullanix (Jan 13 2021 at 02:30):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Daniel Fabian (Apr 20 2021 at 08:27):

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

view this post on Zulip Liang-Ting Chen (Apr 20 2021 at 08:28):

Ooops!! Thanks for solving my problem so quickly!

view this post on Zulip 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