## Stream: Coq users

### Topic: Keyed Unification

#### Yannick Zakowski (Apr 28 2023 at 08:02):

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?

#### Guillaume Melquiond (Apr 28 2023 at 08:16):

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

#### Guillaume Melquiond (Apr 28 2023 at 08:19):

(In general, `a` and `b` are just one trivial unfolding away from the other, but that is usually sufficient to mess with `rewrite`.)

#### Paolo Giarrusso (Apr 28 2023 at 10:24):

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

#### Yannick Zakowski (Apr 28 2023 at 11:55):

Thanks Guillaume!

#### Yannick Zakowski (Apr 28 2023 at 12:00):

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

#### Yannick Zakowski (Apr 28 2023 at 12:01):

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

#### Guillaume Melquiond (Apr 28 2023 at 12:33):

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.

#### Michael Soegtrop (Apr 28 2023 at 13:06):

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.

#### Laurent Théry (Apr 28 2023 at 13:14):

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