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