coq - ssreflect 中的规范结构

Question

我正在尝试处理 ssreflect 中的规范结构。我从 here 中提取了 2 段代码.

我将为 bool 和选项类型带来作品。

Section BoolFinType.

  Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed.
  Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
  Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
  Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed.

End BoolFinType.

Section OptionFinType.

  Variable T : finType.
  Notation some := (@Some _) (only parsing).

  Local Notation enumF T := (Finite.enum T).

  Definition option_enum := None :: map some (enumF T).

  Lemma option_enumP : Finite.axiom option_enum.
  Proof. by case => [x|]; rewrite /= count_map (count_pred0, enumP). Qed.

  Definition option_finMixin := Eval hnf in FinMixin option_enumP.
  Canonical option_finType := Eval hnf in FinType (option T) option_finMixin.

  Lemma card_option : #|{: option T}| = #|T|.+1.
  Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed.

End OptionFinType.

现在，假设我有一个从 finType 到 Prop 的函数 f。

Variable T: finType.
Variable f: finType -> Prop.

Goal f T. (* Ok *)
Goal f bool. (* Not ok *)
Goal f (option T). (* Not ok *)

在最后两种情况下，我收到以下错误:

The term "bool/option T" has type "Set/Type" while it is expected to have type "finType".

我究竟做错了什么？

Answer 1

在这些情况下，对规范结构的实例搜索有点反直觉。假设你有以下几点:

一种结构类型S , 和类型 T ;

一个字段proj : S -> T的 S ;

一个元素 x : T ;和

一个元素 st : S已被声明为规范的，例如 proj st定义为 x .

在您的示例中，我们将有:

S = finType

T = Type

proj = Finite.sort

x = bool

st = bool_finType .

规范结构搜索仅在以下情况下触发:当类型检查算法试图找到一个值以有效填充方程 proj _ = x 中的空洞时。 .然后，它将使用 st : S来填补这个空洞。在您的示例中，您希望算法能够理解 bool可以用作 finType ，通过将其转换为 bool_finType ，这与上面描述的不太一样。

为了让 Coq 推断出你想要什么，你需要使用这种形式的统一问题。例如，

Variable P : finType -> Prop.
Check ((fun (T : finType) (x : T) => P T) _ true).

这里发生了什么？请记住 Finite.sort被声明为来自 finType 的强制转换至 Type , 所以 x : T真正的意思是 x : Finite.sort T .当您申请时 fun表达到 true : bool , Coq 不得不为 Finite.sort _ = bool 寻找解决方案.然后它找到 bool_finType ，因为它被声明为规范的。所以 bool的元素是触发搜索的原因，但不完全是 bool本身。

正如 ejgallego 所指出的，这种模式非常普遍，以至于 ssreflect 提供了特殊的 [finType of ...]句法。但了解幕后发生的事情可能仍然有用。