Coq类型类方法默认实现支持情况及模拟方案问询

Coq的类型类系统不直接支持Haskell那种在类定义时给方法指定默认实现的特性——也就是让实例可以按需覆盖、不写就用默认逻辑的机制，官方文档里确实没提这个功能，这是两者类型类设计的核心差异之一。

如果需要模拟这种行为，有几种通用的模式：

1. 提前定义全局默认函数 #

先写好通用的默认实现函数，在类型类定义里不指定默认，但实例可以直接引用这个函数来快速实现，省去重复写代码的麻烦。

(* 先定义通用默认实现 *)
Definition default_eq {A} (x y : A) : bool := false.

(* 定义类型类 *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool
}.

(* 用默认实现的实例 *)
Instance eq_bool : Eq bool := { eqb := default_eq }.

(* 自定义实现的实例 *)
Instance eq_nat : Eq nat := { eqb := Nat.eqb }.

2. 用辅助引理封装依赖型默认逻辑 #

如果默认实现需要依赖类型类的其他方法，可以把这个逻辑封装成辅助引理，实例需要时直接调用即可。

Class Monoid (M : Type) := {
  op : M -> M -> M;
  e : M
}.

(* 基于Monoid的默认幂运算逻辑 *)
Definition default_pow {M} `{Monoid M} (x : M) (n : nat) : M :=
  match n with
  | O => e
  | S n' => op x (default_pow x n')
  end.

(* 带幂运算的类型类 *)
Class MonoidWithPow (M : Type) := {
  monoid :> Monoid M;
  pow : M -> nat -> M
}.

(* 复用默认pow的实例 *)
Instance monoid_nat_pow : MonoidWithPow nat := {
  monoid := { op := Nat.add; e := O };
  pow := default_pow
}.

3. 复用基础实例实现默认逻辑 #

如果多个实例共享相同的默认行为，可以先定义一个包含通用逻辑的基础实例，新实例直接引用它的方法，只修改需要自定义的部分。

(* 基础List Monoid实例 *)
Instance monoid_list {A} : Monoid (list A) := {
  op := app;
  e := nil
}.

(* 给List加上默认幂运算 *)
Instance monoid_list_pow {A} : MonoidWithPow (list A) := {
  monoid := monoid_list;
  pow := default_pow
}.

4. 用记录类型做中间层 #

先定义一个带默认值的记录类型，再通过这个记录生成类型类实例，实例可以选择性修改记录字段来覆盖默认。

Record DefaultEq (A : Type) := {
  default_eqb : A -> A -> bool := default_eq
}.

Class Eq (A : Type) := {
  eqb : A -> A -> bool
}.

(* 从DefaultEq生成Eq实例，默认用记录里的default_eqb *)
Definition eq_from_default {A} (d : DefaultEq A) : Eq A := {
  eqb := default_eqb d
}.

(* 完全用默认的实例 *)
Instance eq_unit : Eq unit := eq_from_default {| |}.

(* 覆盖默认的实例 *)
Instance eq_bool : Eq bool := eq_from_default {| default_eqb := Bool.eqb |}.

内容的提问来源于stack exchange，提问作者Zak Kent