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