Stream: Coq users

Topic: Apply vs rewrite unification definition unfolding


view this post on Zulip Sanjit Bhat (Oct 25 2023 at 23:27):

I'm trying to understand under what situations unification unfolds a definition. Along the way, I came up with the following toy example:

Module one.
Section proof.
Parameter f : nat -> Prop.
Hypothesis f_unit : f 0.
Definition g (t : nat) := f t.

Goal (g 0).
  apply f_unit.
Qed.
End proof.
End one.

Module two.
Section proof.
Parameter f : nat -> Prop.
Hypothesis f_unit : f 0 = True.
Definition g (t : nat) := f t.

Goal (g 0 = True).
  Fail rewrite f_unit.
Abort.
End proof.
End two.

I'm struggling to understand why unification works with apply but not with rewrite. Both generate identical unification branches for f 0 ~= g0. With apply, it leaves unification with success, while with rewrite, it leaves with failure.

view this post on Zulip Paolo Giarrusso (Oct 25 2023 at 23:53):

Non-ssreflect rewrite doesn't use unification here.

view this post on Zulip Paolo Giarrusso (Oct 25 2023 at 23:55):

And that's the version of rewrite that you're using if this is complete (as it seems!).

Ssreflect rewrite uses... something more complicated that's not unification, but is father away from syntactic equality, and can unfold definitions in some cases.

view this post on Zulip Sanjit Bhat (Oct 26 2023 at 00:09):

Hm, that's good to know! I'm slightly confused, though, because when I ran the rewrite with Set Debug "tactic-unification"., I got the following output, which makes me believe unification is still happening. Note that this exact unification case resulted in a success in module one.

[tactic-unification] Starting unification: f 0 ~= g 0

[tactic-unification] Leaving unification with failure

view this post on Zulip Julio Di Egidio (Oct 26 2023 at 01:56):

Sanjit Bhat said:

I'm struggling to understand why unification works with apply but not with rewrite.

This code works for me in both Coq 8.16 and 8.17:

Module two.
  Section proof.
    Parameter f : nat -> Prop.
    Hypothesis f_unit : f 0 = True.
    Definition g (t : nat) := f t.

    Goal (g 0 = True).
    Proof.
      unfold g.
      rewrite f_unit.
      reflexivity.
    Qed.
  End proof.
End two.

IIANM, the fact is rewrite does not do unfolding of definition.

view this post on Zulip Paolo Giarrusso (Oct 26 2023 at 02:40):

@Sanjit Bhat internally, unification allows tweaking which definitions can or cannot be unfolded. AFAICT, rewrite doesn't let you configure this.

view this post on Zulip Paolo Giarrusso (Oct 26 2023 at 02:41):

actually, https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:flag.Keyed-Unification might be relevant? I'm not entirely sure (never tried)

view this post on Zulip Paolo Giarrusso (Oct 26 2023 at 02:42):

Similar options are exposed in a _different_ context, where they affect not rewrite but (typeclasses) eauto: see Hint Opaque/Transparent/Constants / Variables:

https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Opaque
https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Constants

view this post on Zulip Pierre Rousselin (Oct 26 2023 at 05:05):

Set Keyed Unification does not change the fact that rewrite does not unfold the definition of g. It works with a notation though.

Module three.
Section proof.
Parameter f : nat -> Prop.
Hypothesis f_unit : f 0 = True.
Notation g := f.

Goal (g 0 = True).
  rewrite f_unit.
  reflexivity.
Qed.
End proof.
End three.

view this post on Zulip Cyril Cohen (Oct 26 2023 at 08:19):

Using Set Keyed Unification works provided you declare f and g as equivalent keys:

Module three.
Section proof.
Parameter f : nat -> Prop.
Hypothesis f_unit : f 0 = True.
Definition g := f.

Set Keyed Unification.
Declare Equivalent Keys f g.

Goal (g 0 = True).
  rewrite f_unit.
  reflexivity.
Qed.
End proof.
End three.

view this post on Zulip Cyril Cohen (Oct 26 2023 at 08:20):

unfortunately ssreflect rewrite fails now because it does not respect equivalent keys (cc @Enrico Tassi )

view this post on Zulip Sanjit Bhat (Nov 02 2023 at 17:30):

Thanks for the responses! To summarize what I've learned, there's room for tweaking unification definition unfolding. Rewrite unification settings by default unfold fewer things, but rewrite provides the Keyed Unification flag to configure this behavior.


Last updated: Oct 13 2024 at 01:02 UTC