如何将set策略引入的变量添加至Hint DB？环境未找到错误求解

你遇到的问题本质是作用域不匹配：用set在证明过程中引入的变量m是当前证明上下文的局部变量，而默认的Hint命令是往全局环境的Hint数据库（比如core）里添加规则，全局环境根本看不到这个局部定义的m，所以会报找不到的错误。

可行的解决方法 #

根据你的需求，分两种场景给出方案：

场景1：只需要在当前证明中自动展开m

如果只是想在当前这个证明里让Coq自动展开m，可以把Hint限定在局部Hint数据库里：

Example foo : forall n : nat, n + n = n + n.
Proof.
intro n.
set (m := n + n).
Hint Unfold m : local.  (* 把Hint加到名为local的局部数据库 *)
autounfold with local. (* 使用这个局部数据库里的规则自动展开 *)
reflexivity.
Qed.

这里的local是一个自定义的Hint数据库名字（你也可以换成别的），它只在当前证明的上下文中生效，不会污染全局环境。

场景2：需要全局范围内使用这个m的展开规则

如果想让m的展开规则在所有证明里都能用，那得把m定义成全局的符号，而不是证明内的局部变量。比如在Proof外面定义一个带参数的Definition：

Definition m (n : nat) := n + n.  (* 全局定义m *)
Hint Unfold m.  (* 现在可以全局添加Hint了 *)

Example foo : forall n : nat, n + n = n + n.
Proof.
intro n.
rewrite <- (m n).  (* 可以直接引用全局的m *)
reflexivity.
Qed.

这种方式下的m是全局可见的，Hint自然能找到它。

补充：Section内的局部全局定义

如果不想让m完全全局，但想在一个Section的多个证明里复用，可以用Let在Section里定义：

Section MySection.
Variable n : nat.
Let m := n + n.  (* Section内的局部定义 *)
Hint Unfold m.  (* Hint在Section范围内有效 *)

Example foo : n + n = n + n.
Proof.
autounfold.  (* 会自动展开m *)
reflexivity.
Qed.
End MySection.

Section结束后，m和对应的Hint都会消失，不会影响全局环境。

总结 #

Coq8.7里确实不能直接给证明内set的局部变量加全局Hint，但通过局部Hint数据库或者调整变量的定义作用域，完全可以实现你想要的效果。

内容的提问来源于stack exchange，提问作者wkwkes