# Nested dependent pattern matching

I currently have the following:

``````Inductive var {V : nat} :=
| free (name : name)
| bound (l : Fin.t V).

Definition openv a {V} (v : @var (S V)) : @var V :=
match v with
| free n => free (shift_name a n)
| bound l =>
match l in Fin.t (S V) with
| Fin.F1 => free a
| Fin.FS l => bound l
end
end.
``````

where Fin.t is the finite set type from Vectors.Fin. However, I’d like to write `openv` in a more nested manner like so:

``````Definition openv a {V} (v : @var (S V)) : @var V :=
match v with
| free n => free (shift_name a n)
| bound Fin.F1 => free a
| bound (Fin.FS l) => bound l
end.
``````

However, Coq complains that `The term "l" has type "Fin.t n" while it is expected to have type "Fin.t V".`, despite the target `v` having type `@var (S V)`. I’m guessing this is in part because `(S V)` is an index of `Fin.t`, not a parameter. This is why I have `in Fin.t (S V)` in the nested match in the first snippet.

Is there a way to write this in the nested form, but perhaps with some type or `in` annotations? Something like `| bound (Fin.FS l in Fin.t (S V)) => ...` for instance. Or is the first snippet the idiomatic way to write this?

Hi @jon,

I think your nested pattern-match is the standard way to achieve your goal, however if your goal is to have a convenient way to write such functions (and work with them) then I would recommend having a look at the Equations plugin.

Here’s what I end up with your snippet:

``````From Coq Require Import Fin.

Parameter name : Type.
Parameter shift_name : name -> name -> name.

Inductive var {V : nat} :=
| free (name : name)
| bound (l : Fin.t V).

From Equations Require Import Equations.

Derive Signature for Fin.t.

Equations openv (a : name) {V} (v : @var (S V)) : @var V :=
openv a (free n) := free (shift_name a n) ;
openv a (bound Fin.F1) := free a ;
openv a (bound (Fin.FS l)) := bound l.
``````

Note that the underlying code generated by Equations is very close to what you wrote (but you also obtain equations to work with and the `funelim` induction scheme).