如何在Coq中结合Section与Hint实现全局可用的提示？

问题背景 #

编写大量依赖Typeclass的Coq代码时，Section结构能避免重复声明{A} {C : MyClass A}这类参数，但Section内添加的Hint在退出Section后会失效，导致外部无法通过auto调用这些Hint来简化证明。

问题复现代码 #

首先定义基础类与函数：

Class MyClass (A : Type) :=
  connect : A -> A -> Prop.

Fixpoint chain [A] [C : MyClass A] (l : list A) {struct l} : Prop :=
  match l with
  | [] | [_] => True
  | a0 :: (a1 :: _ as rest) => connect a0 a1 /\ chain rest
  end.

使用Section简化参数声明后，Section内的Hint能正常辅助证明，但退出后Hint失效：

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  Hint Resolve chain_seq.

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto.
  Qed.
End ChainFacts.

#[export] Instance nat_connect : MyClass nat := eq.

Lemma chain_seq_seq_out : forall [l1 l2 l3 : list nat],
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  intros. now auto. (* 报错：Tactic failure: Cannot solve this goal. *)

现有两种方案存在明显缺陷：

• 放弃使用Section：需重复编写类相关参数声明，代码冗余度高
• Section结束后重新声明所有Hint：嵌套Section场景下操作繁琐，维护成本高

可行替代方案 #

1. 用Global修饰Hint #

在Section内给Hint添加Global关键字，将其提升至全局环境，Section结束后依然有效。注意Section内定义的引理会自动带上Section变量作为参数，全局Hint可以正常匹配这些参数：

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  Global Hint Resolve chain_seq. (* 添加Global关键字 *)

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto.
  Qed.
End ChainFacts.

#[export] Instance nat_connect : MyClass nat := eq.

Lemma chain_seq_seq_out : forall [l1 l2 l3 : list nat],
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  intros. now auto. (* 可正常通过auto解决 *)

2. 用#[export]属性标记Hint #

符合现代Coq风格的写法，通过#[export]属性直接导出Hint，效果与Global一致：

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  #[export] Hint Resolve chain_seq. (* 使用#[export]属性 *)

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto.
  Qed.
End ChainFacts.

3. 自定义Hint数据库 #

创建专属Hint数据库，将Section内的Hint归类到该数据库，外部使用时指定数据库即可。这种方式不会污染全局Hint环境，适合大型项目：

(* 先定义自定义Hint数据库 *)
Create HintDb chain_hints.

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  Hint Resolve chain_seq : chain_hints. (* 添加到自定义数据库 *)

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto with chain_hints. (* Section内指定数据库 *)
  Qed.
End ChainFacts.

#[export] Instance nat_connect : MyClass nat := eq.

Lemma chain_seq_seq_out : forall [l1 l2 l3 : list nat],
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  intros. now auto with chain_hints. (* 外部指定数据库 *)

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