Coq: définir les paramètres implicites par défaut

Question

Supposons que j'ai un code avec beaucoup de modules et de sections. Dans certains d'entre eux, il existe des définitions polymorphes.

Module MyModule. 

    Section MyDefs. 

     (* Implicit. *) 
     Context {T: Type}. 

     Inductive myIndType: Type := 
     | C : T -> myIndType. 

    End MyDefs. 

End MyModule. 

Module AnotherModule. 

    Section AnotherSection. 

     Context {T: Type}. 
     Variable P: Type -> Prop. 

     (*    ↓↓   ↓↓ - It's pretty annoying. *) 
     Lemma lemma: P (@myIndType T). 

    End AnotherSection. 

End AnotherModule. 

Habituellement, Coq peut déduire le type, mais souvent je reçois toujours une erreur de frappe. Dans de tels cas, vous devez spécifier explicitement le type implicite avec @, ce qui gâche la lisibilité.

Impossible de déduire le paramètre implicite _ de _ dont le type est "Type".

Y at-il un moyen d'éviter cela? Est-il possible de spécifier quelque chose comme les paramètres par défaut, qui seront substitués chaque fois que Coq ne peut pas deviner un type?

Answer 1

Vous pouvez utiliser une classe de types pour mettre en œuvre cette notion de valeur par défaut:

Class Default (A : Type) (a : A) := 
    withDefault { value : A }. 

Arguments withDefault {_} {_}. 
Arguments value {_} {_}. 

Instance default (A : Type) (a : A) : Default A a := 
    withDefault a. 

Definition myNat `{dft : Default nat 3} : nat := 
    value dft. 

Eval cbv in myNat. 
(* = 3 : nat *) 
Eval cbv in (@myNat (withDefault 5)). 
(* = 5 : nat *)