Coq：設置默認隱式參數

Question

假設我有一個包含很多模塊和部分的代碼。其中一些有多態的定義。

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. 

通常Coq可以推斷出類型，但是我經常仍然會輸入錯誤。在這種情況下，您必須使用@明確指定隱式類型，這會破壞可讀性。

無法推斷_類型爲「Type」的隱式參數_。

有沒有辦法避免這種情況？是否可以指定類似默認參數的東西，每當Coq無法猜測某個類型時會替換它們？

Answer 1

您可以使用類型類來實現這個概念默認值：

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 *)