I want to use a Hint DB with variables introduced by set
. For example,
Example foo : forall n : nat, n + n = n + n.
Proof.
intro.
set (m := n + n).
Hint Unfold m.
but, Coq says:
Error: The reference
m
was not found in the current environment.
Is there any way to achieve this, or is it impossible?
I'm using Coq 8.7.
It's not possible to do this like you suggested because after you finish foo
with Qed
the local variable m
will be out of scope, but hints go straight into some global database.
However, you can use the Section
mechanism, as the hints declared inside a section are local to that section:
Section LocalHints.
Variable n : nat.
Let m := n + n.
Hint Unfold m.
Example bar : m = m.
Proof.
autounfold with core.
reflexivity.
Qed.
End LocalHints.