matching on inductives with indices

Stream: lean4

[Jovan Gerbscheid]

Is the following code expected to fail?

inductive A : Nat → Type where
| a {n} : A n
| b : A 10

def foo (n : Nat) (x : A n) (y : A 10) : A n :=
  match x with
  | .a => x
  | .b => y

It gives the error

Type mismatch
  x
has type
  A n✝
but is expected to have type
  A n

Because for some reason the match has introduced another variable n that shadows the previous n, and these ns are not defEq to eachother.

This comes up in the implementation of the ring tactic. A possible workaround is to write

def foo (n : Nat) (x : A n) (y : A 10) : A n :=
  match x with
  | x@(.a) => x
  | .b => y

[Floris van Doorn]

This is not unexpected. Since this is an inductive family, you have to always generalize n before doing induction. This also fails:

def bar (n : Nat) (x : A n) (y : A 10) : A n :=
  A.rec (@fun n' ↦ x) y x

There is probably a small trick to get this definition to work...

[Floris van Doorn]

Yeah, your workaround is equivalent to

def foo (n : Nat) (x : A n) (y : A 10) : A n :=
  match x with
  | .a => .a
  | .b => y

which of course works.

[Floris van Doorn]

I guess match could get a feature that it clears the old x (and n) from the environment, and adds a new x that corresponds to each of the cases. However, I think this is undesirable in other situations (and I'm not sure how this would interact with catch-all patterns and other features of match)

[Aaron Liu]

I would expect that x would also be shadowed

[Jovan Gerbscheid]

Indeed, looking at the type of the recursor the behaviour makes more sense:

{motive : (a : Nat) → A a → Sort u}
  (a : {n : Nat} → motive n A.a) (b : motive 10 A.b)
  {x : Nat} (t : A x) : motive x t

In my head the recursor looked more like

{motive : (a : Nat) → A a → Sort u} {x : Nat}
  (a : motive x A.a) (b : motive 10 A.b)
  (t : A x) : motive x t

[Jovan Gerbscheid]

I have some more unexpected behaviour when matching on inductives with indices. The following throws an error, but if we replace the type A x by A y or A z, it succeeds. In other words, the order of the (x y z : Nat) arguments in the definition ofA makes a difference.

inductive A : Nat → Type where
| a (x y z : Nat) : A x

def foo {n} (a : A n) : A n :=
  match a with
  | .a x y z => .a x y z
/-
Type mismatch
  A.a x y z
has type
  A x
but is expected to have type
  A n
-/

[Aaron Liu]

I have also encountered this problem with my types with lots of indices, the solution is to just rope in the indices into the match

inductive A : Nat → Type where
| a (x y z : Nat) : A x

def foo {n} (a : A n) : A n :=
  match n, a with
  | _, .a x y z => .a x y z