# Understand the reduction behind apply

I am working on Software Foundation, the volume of Verified Functional Algorithm. I encounter a state `Permutation [] ([] ++ [])`.
Although `[]` is not equal to `[] ++ []`, I can finish the proof by `apply Permutation_refl.` It seems that `apply` perform some reduction before matching `Permutation_refl` with the current goal.

From the Coq manual, Tactics — Coq 8.16.1 documentation, I find no information about the reduction behind `apply`.

Where could I know the mechanism of the reduction of `apply` beside the manual? The question can also be extended to other tactics that perform operations not mentioned in the Coq manual

``````Require Import List.
Eval compute in (@nil nat ++ @nil nat).
``````

As one can see, the expression computes to `nil`.
In other words, `[] ++ []` is equal to `[]`.

In general, a function applied to known arguments is “equal” to its result. (Technically we talk of “definitional equality”, equality by definition of the function. Definitionally equal terms are indistinguishable for Coq.) So `[] ++ []` is equal to `[]`, also `2 + 3` equal to `5`, etc. Troubles start when some of the arguments are “unknown” (neutral terms built from variables/parameters): `x + 0` and `0 + x` are not known to be equal-by-definition by Coq – one of them will be equal to `x`, depending on the order in which the function `(+)` inspects its arguments.

The documentation mentions that “[t]he tactic `apply` relies on first-order unification with dependent types”. While this note is quite cryptic, it actually corresponds to the “mechanism of the reduction of `apply`”. Indeed, Coq’s unification algorithm in particular knows how to evaluate expressions before attempting to unify them.

In your precise case, what happens is that `Permutation_refl` has type `Permutation ?l ?l` for some unknown `?l` (technically, an existential variable), and gets unified with your goal `Permutation [] ([]++[])`. Coq thus unifies `?l` with `[]` as the first arguments to `Permutation`, and then gets to compare `?l` (which has been solved to `[]`) and `[] ++ []`. It evaluates the second one, obtaining `[]` as LessnessR showed, which solves this second problem by reflexivity.

As far as I can tell, unification is not described in details in the manual. The closest I can think of is this paper: although it does not describe the algorithm currently used in Coq, it is close enough to it that you should get a good idea of what happens there.

1 Like