CODEWITHSUNDEEP
coq
wkwkes
wkwkes

Reputation: 23

How to add variables introduced by set tactic to a Hint DB?

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.

Upvotes: 2

Views: 115

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

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.

Upvotes: 2

Related Questions