6

I'm trying to deal with canonical structures in ssreflect. There are 2 pieces of code that I took from here.

I will bring pieces for the bool and the option types.

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.

Now, suppose I have a function f from finType to Prop.

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

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

In the last two cases I get the following error:

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

What am I doing wrong?

4

1 回答 1

8

在这些情况下，规范结构的实例搜索有点违反直觉。假设你有以下东西：

  • 一个结构类型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).

这里发生了什么？请记住，从toFinite.sort声明为强制转换，因此是真正的意思。当您将表达式应用于 时，Coq 必须为. 然后它会找到，因为它被声明为规范。所以元素 of是触发搜索的原因，但不是触发搜索的原因。finTypeTypex : Tx : Finite.sort Tfuntrue : boolFinite.sort _ = boolbool_finTypeboolbool

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

于 2017-08-23T14:35:18.737 回答