Канонические структуры в 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.

Теперь предположим, что у меня есть функция f от finType до Prop.

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

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

В последних двух случаях я получаю следующую ошибку:

Термин "bool /option 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 можно использовать как 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 : boolCoq должен найти решение для Finite.sort _ = bool, Затем он находит bool_finTypeпотому что он был объявлен каноническим. Таким образом, элемент bool это то, что вызывает поиск, но не совсем bool сам.

Как указал ejgallego, этот шаблон настолько распространен, что ssreflect предоставляет особый [finType of ...] синтаксис. Но все же может быть полезно понять, что происходит под капотом.