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

@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: Jun 22 2024 at 16:02 UTC