# Matching Coq Binders

## Motivation

Recently, I had some trouble trying to Ltac scripts in Coq to match function bodies. After some googling, I came across this GitHub README for useful Coq tricks that provided part of the puzzle:

If you have a second-order match (using

`@?z x`

, which bind`z`

to a function) and you want to apply the function, there’s a trick involving a seemingly useless match. See LtacGallinaApplication.v for an example.

In LtacGallinaApplication.v, we find this piece of code

```
Notation "'subst!' y 'for' x 'in' f" := (match y with x => f end) (at level 10).
Ltac app_beta f x :=
match f with
| (fun y => ?F) => constr:(subst! x for y in F)
end.
```

which helps us obtain the body of a function `f`

when applied to `x`

.

## Solution

We can use this trick to write a script^{1} that lets us “match” on the body of the function using the `ident`

of the argument:

```
Notation "'subst!' y 'for' x 'in' f" := (match y with x => f end) (at level 10).
Ltac match_body fn match_fn :=
match fn with
| (fun (i : ?t) => ?F) =>
let x := fresh i in
evar (x: t);
match goal with
| |- t => econstructor
| |- _ =>
let body := constr:(subst! x for i in F) in
match_fn x body;
clear x
end
| _ => fail "Not a unary function!"
end.
```

Let’s break it down:

- Create a temporary
`ident`

bound to`x`

for the “concrete” variable that we be substituting into`f`

’s body - Create an evar for
`x`

, which we can get rid off if the function argument`i`

has a non-empty type - Construct the body with the substitution
- Run the user-provided
`match_fn`

on this body (CPS is used here because with`evar ...`

,`match_body`

is no longer a pure function) - Clean-up code; remove the temporary
`x`

binding

## Usage

This is best illustrated by an example:

```
match_body fn ltac:(fun i body => idtac i body)
```

Note that the `ltac`

scope specifier is required. This could probably be improved using some notation hackery.

This only handles arity 1 for simplicity

^{1}but shouldn’t be hard to extend ↩︎