Coq：导入有关实例的信息

Question

Section Definitions.

  Definition eq_dec X := forall x y : X, {x=y} + {x <> y}.
  Existing Class eq_dec.

  (* Any function that uses eq_dec. Doesn't matter -- ↓ ↓ ↓ *)
  Definition f {X: Type} {DecX: eq_dec X} (x y: X) := x = y.

End Definitions.

Section MySection.

  Context {T: Type}.
  Hypothesis TEqDec: eq_dec T.

  Inductive myType :=
  | C: T -> myType.

  Instance myTypeEqDec : eq_dec myType.
  Proof. ... Defined.

  (* Everything is ok *)
  Example example1: forall (t1 t2: myType), f t1 t2.
  Proof. ... Qed.

End MySection.

Section AnotherSection.

  Context {T: Type}.
  Hypothesis TEqDec: eq_dec T.

  (*          Now I must explicitly specify this -- ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ 
  Example example2: forall (t1 t2: @myType T), @f _ (@myTypeEqDec _ TEqDec) t1 t2.
  Proof. ... Qed.

End AnotherSection.

如您在示例 1 中所见，Coq 能够找到有关 myType 的实例信息。但是在我更改该部分之后，有关实例的所有信息都消失了，我必须明确指定它。所以，当我有很多 type-类和实例时，代码很快就会变得混乱。显然，我应该以某种方式将该信息返回到上下文中。这样做的正确方法是什么？

Answer 1

只需将 Global 修饰符添加到您的实例声明中，如下所示：

Global Instance myTypeEqDec : eq_dec myType.
(* ... *)

如 reference manual、

中所述

One can use the Global modifier on instances declared in a section so that their generalization is automatically redeclared after the section is closed.

Coq：导入有关实例的信息

Coq: import information about instances

typeclass

implicit

coq