Structures canoniques dans ssreflect

Question

J'essaie de traiter des structures canoniques dans ssreflect. Il y a 2 morceaux de code que j'ai pris de here.

Je vais apporter des pièces pour le bool et les types d'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. 

Maintenant, supposons que j'ai une fonction f de finType à Prop

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

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

Dans les deux derniers cas, je reçois l'erreur suivante:.

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

Qu'est-ce que je fais mal ?

Answer 1

La recherche d'instance pour les structures canoniques est un peu contre-intuitive dans ces cas. Supposons que vous ayez les choses suivantes:

• un type de structure S, et un type T; Un champ proj : S -> T de S; Un élément x : T; et
• un élément st : S qui a été déclaré comme canonique, tel que proj st est défini comme x.

Dans votre exemple, nous aurions:

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

recherche structure Canonical déclenchée ne dans le cas suivant: lorsque l'algorithme de type vérification tente de trouver une valeur pour remplir valablement dans le trou dans l'équation proj _ = x. Ensuite, il utilisera st : S pour remplir ce trou. Dans votre exemple, vous vous attendiez à ce que l'algorithme comprenne que bool peut être utilisé comme finType, en le transformant en bool_finType, ce qui n'est pas tout à fait ce qui est décrit ci-dessus.

Pour que Coq infère ce que vous voulez, vous devez utiliser un problème d'unification de ce formulaire. Par exemple,

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

Que se passe-t-il ici? Rappelez-vous que Finite.sort est déclaré comme coercition de finType à Type, donc x : T signifie vraiment x : Finite.sort T. Lorsque vous appliquez l'expression fun à true : bool, Coq doit trouver une solution pour Finite.sort _ = bool. Il trouve ensuite bool_finType, car il a été déclaré comme canonique. Donc, l'élément de bool est ce qui déclenche la recherche, mais pas tout à fait lui-même bool.Comme l'a fait remarquer ejgallego, ce modèle est si courant que ssreflect fournit la syntaxe spéciale [finType of ...]. Mais il pourrait être utile de comprendre ce qui se passe sous le capot.