Canonical structures in ssreflect

Question

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

I will give pieces for bool and types of options.

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" is of type "Set / Type", while it is expected that it will be of type "finType".

What am I doing wrong?

Answer 1

The search for instances of canonical structures in this case is an intuitive counter. Suppose you have the following things:

• structure type S and type T ;
• field proj : S -> T of S ;
• element x : T ; and
• an st : S element that was declared canonical, so proj st is defined as x .

In your example, we will have:

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

The search for the canonical structure is launched only in the following case: when the type checking algorithm tries to find the value in order to correctly fill the hole in the equation proj _ = x . He will then use st : S to fill this hole. In your example, you expected the algorithm to understand that bool can be used as finType , converting it to bool_finType , which is not quite what is described above.

To get Coq to do what you want, you need to use the join problem of this form. For instance,

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

What's going on here? Remember that Finite.sort declared as coercion from finType to Type , so x : T really means x : Finite.sort T When you apply the fun expression to true : bool , Coq should find a solution for Finite.sort _ = bool . Then it finds bool_finType because it was declared as canonical. So the bool element is what launches the search, but not quite the bool itself.

As ejgallego noted, this pattern is so common that ssreflect provides a special syntax [finType of ...] . But it may be useful to understand what is happening under the hood.