向Coq中的类型类实例添加引理

Question

在文件SemiRing.v中，我定义了一些类：

(** Setoids. *)

Class Setoid := {
  s_typ :> Type;
  s_eq : relation s_typ;
  s_eq_Equiv : Equivalence s_eq }.

Existing Instance s_eq_Equiv.

Module Import Setoid_Notations.
  Infix "==" := s_eq.
End Setoid_Notations.

Instance Leibniz_Setoid (A : Type) : Setoid.

Proof.
  apply Build_Setoid with (s_eq := @eq A). constructor. fo. fo.
  unfold Transitive. apply eq_trans.
Defined.


(** Setoids with decidable equivalence. *)

Class Decidable_Setoid := {
  ds_setoid :> Setoid;
  ds_eq_dec : forall x y, {s_eq x y} + {~s_eq x y} }.

 Class SemiRing := {
  sr_ds :> Decidable_Setoid;
  sr_0 : s_typ;
  sr_1 : s_typ;
  sr_add : s_typ -> s_typ -> s_typ;
  sr_add_eq : Proper (s_eq ==> s_eq ==> s_eq) sr_add;
  sr_mul : s_typ -> s_typ -> s_typ;
  sr_mul_eq : Proper (s_eq ==> s_eq ==> s_eq) sr_mul;
  sr_th : semi_ring_theory sr_0 sr_1 sr_add sr_mul s_eq }.

然后，我定义了一个NSemiRing.v是自然数的SemiRing的一个实例。

Require Import SemiRing.

Instance Nat_as_Setoid : Setoid := Leibniz_Setoid nat. (*Where A = nat *)

Instance Nat_as_DS : Decidable_Setoid.

Proof.
  apply Build_Decidable_Setoid with (ds_setoid := Nat_as_Setoid).
  apply eq_nat_dec.
Defined.

Instance Nat_as_SR : SemiRing.

Proof.
apply Build_SemiRing with (sr_ds := Nat_as_DS) (sr_0 := 0) (sr_1 := 1)
  (sr_add := plus) (sr_mul := mult).
class. class. constructor; intros; simpl; try ring. refl.
Defined.

我的问题是：

我想要一个引理，例如：

Lemma Aadd_0_r (n: nat) : n + 0 = n.

Proof. ... Qed.

如何添加或使这个引理Aadd_0_r (类型为nat )被视为SemiRing类型的Nat_as_SR的字段之一？

在另一个文件中导入NSemiRing：

Require Import NSemiRing.
Context {S: SemiRing}. Import Setoid_Notations.

例如，如果我有一个具有如下形式的引理：

Lemma add_zero_r (n: s_typ): n + 0 == n.

其中，"s_typ“被自动识别为"nat”类型，我可以调用引理Aadd_0_r来证明这个引理。

Answer 1

难道Proof. apply Aadd_0_r. Qed.不是完成了证据吗？

如果您关闭了符号和unfold，那么您的所有目标定义都会降为Aadd_0_r。