在Coq中使用类型类的公理重用

(* 定义一个类型类 Eq，表示类型的相等性 *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool;
  eqb_refl : forall x, eqb x x = true;
  eqb_sym : forall x y, eqb x y = eqb y x;
  eqb_trans : forall x y z, eqb x y = true -> eqb y z = true -> eqb x z = true
}.

(* 定义一个整数类型 *)
Inductive Nat := O | S (n : Nat).

(* 为Nat类型实现Eq类型类 *)
Instance EqNat : Eq Nat := {
  eqb := fun n m =>
    match n, m with
    | O, O => true
    | S n', S m' => eqb n' m'
    | _, _ => false
    end;
  eqb_refl := fun n => match n with O => eq_refl | S n' => eq_refl end;
  eqb_sym := fun n m => match n, m with O, O => eq_refl | S n', S m' => eqb_sym n' m' | _, _ => eq_refl end;
  eqb_trans := fun n m z H1 H2 =>
    match n, m, z with
    | O, O, O => eq_refl
    | S n', S m', S z' => eqb_trans n' m' z' H1 H2
    | _, _, _ => eq_refl
    end
}.

(* 使用Eq类型类 *)
Lemma example : EqNat.(eqb) (S (S O)) (S (S O)) = true.
Proof. reflexivity. Qed.

(* 定义两个不同的Eq实例，会导致冲突 *)
Instance EqNat1 : Eq Nat := { ... }.
Instance EqNat2 : Eq Nat := { ... }. (* 冲突 *)

(* 解决方法：明确指定实例 *)
Lemma example : EqNat1.(eqb) (S (S O)) (S (S O)) = true.
Proof. reflexivity. Qed.