如何在 Coq 中将部分与提示混合在一起？

Question

我正在写一些大量涉及类型类的内容，我想利用提示来轻松证明局部引理以及导出的定理。

例如，考虑

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.

Lemma chain_seq : forall {A} `{C : MyClass A} l1 l2,
    chain l1 -> chain l2 -> chain (l1 ++ l2).
Admitted.

Lemma chain_seq_seq : forall {A} `{C : MyClass A} l1 l2 l3,
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
Admitted.

(* and so on... *)

在每个引理或定义中指定

{A} {C : MyClass A}

是非常烦人的（想象一下有更多的参数和更多的类）。值得庆幸的是，我们有

Section

结构可以提供帮助：

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

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

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  Admitted.

好多了。现在我为第一个定理添加提示并用它来显示第二个定理：

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.

这有效。但是，当我退出该部分后，它就不再存在：

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

那是因为提示总是局部的，坦率地说我不喜欢这一点。我真的希望能够在每个引理定义之后使用提示，但我也想将它们导出以供外部使用。目前我看到这种情况有两种退出方式：

• 不使用节（并承受每次编写所有与类相关的内容的痛苦）
• 关闭该部分后立即保留所有提示声明的副本。额外的乐趣点：每次嵌套一个部分时都执行此操作。

还有什么我可以做的吗？

Answer 1

https://coq.inria.fr/doc/V8.19.0/refman/proofs/automatic-tropics/auto.html#creating-hints

在部分内，某些命令仅支持

local

属性。它们是

Hint Immediate

、

Hint Resolve

、

Hint Constructors

、

Hint Unfold

、

Hint Extern

和

Hint Rewrite

。

local

是部分内所有提示命令的默认设置。

似乎您可能必须在结束部分之后直接重复所有

Hint Resolve

行。 :(