Understand the reduction behind apply

Using Coq
1

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

2 
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 [].

3

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.

4

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.

2 Likes