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: Apr 19 2024 at 06:02 UTC