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；
S 的字段 proj : S -> T；
一个元素x : T；和
已声明为规范的元素 st : S，例如 proj st 定义为 x。

在您的示例中，我们将：

S = finType
T = Type
proj = Finite.sort
x = bool
st = bool_finType.

规范结构搜索仅在以下情况下触发：当类型检查算法试图找到一个值以有效填充方程中的空洞时proj _ = x.然后，它将使用 st : S 来填补这个洞。在您的示例中，您希望算法通过将 bool 转换为 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 ...] 语法。但了解幕后发生的事情可能仍然有用。

ssreflect 中的规范结构

Canonical structures in ssreflect

coq

ssreflect