Gallina function application in Ltac

Using Rocq
1

Suppose I have a second-order match such as

match H with
| let x : nat := ?y in @?z x => (* ... *)
end

and I want to get the application z 0. (Preferably beta-reduced once so that I actually get the body of the let with 0 substituted for x.) How can I do this?

Similarly, is it possible to get the body of the let with the free variable x in it? (As if I had matched it as ?z instead of @?z x.) How about if I want to rename the free variable to y instead?

(IIRC this is the trick involving a seemingly useless match f with | f' => ... end but I can’t remember or find the details.)

2

The standard trick is

Notation "'subst!' y 'for' x 'in' f" := (match y with x => f end) (at level 10).

because match statements with only a default case get erased/inlined at interpretation time.

So then you can write:

Ltac app_beta f x :=
  match f with
  | (fun y => ?F) => constr:(subst! x for y in F)
  end.

Then you can do either

match H with
| let x : nat := ?y in @?z x => app_beta z 0
end

or else

match H with
| let x : nat := ?y in ?z => constr:(subst! 0 for x in z)
end
3 Likes