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
.
Non-ssreflect rewrite doesn't use unification here.
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.
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
Sanjit Bhat said:
I'm struggling to understand why unification works with
apply
but not withrewrite
.
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.
@Sanjit Bhat internally, unification allows tweaking which definitions can or cannot be unfolded. AFAICT, rewrite
doesn't let you configure this.
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)
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
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.
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.
unfortunately ssreflect rewrite fails now because it does not respect equivalent keys (cc @Enrico Tassi )
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