Nested dependent pattern matching

Using Coq
1

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?

2

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).

1 Like