Coq:设置默认隐式参数

假设我有一个包含很多模块和部分的代码.在其中一些中有多态定义.

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可以推断出类型,但我经常会输入错误.在这种情况下,您必须使用@显式指定隐式类型,这会破坏可读性.

Cannot infer the implicit parameter _ of _ whose type is “Type”.

有办法避免这种情况吗?是否可以指定默认参数之类的东西,每次Coq无法猜出类型时都会替换它们?

最佳答案 您可以使用类型类来实现默认值的概念:

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