The Equations examples (here for example) use a `Keyed Unification`

without which some rewrites fail (although due to a change in the behavior of `funelim`

rather). I was not aware of this flag, and the documentation is a little cryptic to me:

This flag makes higher-order unification used by rewrite rely on a set of keys to drive unification. The subterms, considered as rewriting candidates, must start with the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments are then unified up to full reduction.

Would anyone be able to expand on what it means?

Suppose that you are rewriting using `a x = _`

. Coq will look for an occurrence of `a _`

in the goal. But what if there is no `a`

in your goal, but some `b`

that has the same normal form as `a`

? That is what keyed unification is for. You tell Coq that `a`

and `b`

are the same using `Declare Equivalent Keys`

.

(In general, `a`

and `b`

are just one trivial unfolding away from the other, but that is usually sufficient to mess with `rewrite`

.)

Thanks for your answer! Declare Equivalent Keys doesn't seem to be used explicitly in Yannick's link... Curious if `Print Equivalent Keys`

would print something anyway

Thanks Guillaume!

Just to illustrate explicitly Guillaume's answer if useful to anyone else:

```
Section foo.
Variable A : Type.
Variable a b : A.
Definition c := a.
Variable EQ : a = b.
(* Declaring c and a equivalent *)
Declare Equivalent Keys c a.
(* The current list of keys declared equivalent can be checked with: *)
Print Equivalent Keys.
Goal c = b.
Fail rewrite EQ.
(* Setting on the use of keys *)
Set Keyed Unification.
rewrite EQ.
reflexivity
Qed.
End foo.
```

As Paolo mentions though Equations must be some more dirty work behind the scene. In particular in the rose_tree example the flag must be set before the definition of `map_In`

for things to work, while it does not seem to matter in vanilla coq

Note that symbols are automatically declared equivalent with themselves. So, this might just be a way to force `rewrite`

to work harder when looking for subterms. Said otherwise, `Set Keyed Unification`

has the side effect of making the vanilla `rewrite`

behave similarly to SSReflect's one.

A note which might be of interest in this context: I tend to use `setoid_rewrite`

in case I need rewrite modulo unification (in cases which otherwise wouldn't need setoid_rewrite). It handles this out of the box nicely without extra hints and also doesn't seem to be excessively slow doing so.

If you have only few instances, you can also use ssreflect rewrite with pattern selection.

```
From mathcomp Require Import ssreflect.
Section foo.
Variable A : Type.
Variable a b : A.
Definition c := a.
Variable EQ : a = b.
Goal c = b.
Fail rewrite EQ.
rewrite [c]EQ.
reflexivity.
Qed.
```

Last updated: Jun 18 2024 at 09:02 UTC