ssreflect中的规范结构

Question

我正在尝试处理ssreflect中的规范结构.我从这里获取了 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 *)

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

术语"bool /选项T"具有类型"Set/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为可以用作的理解,这与上面描述的不完全相同.finTypebool_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 ...]语法.但是,了解幕后发生的事情可能仍然有用.