CODEWITHSUNDEEP
coq
Quyen
Quyen

Reputation: 1373

Adding a lemma to an Instance of type Class in Coq

In file SemiRing.v I defined some classes:

(** 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 }.

Then I define a NSemiRing.v is an instance of SemiRing for natural numbers.

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.

My question is:

I want to have a lemma for example:

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

Proof. ... Qed.

How can I add or make this lemma Aadd_0_r of type nat see as one of the field of Nat_as_SR of type SemiRing?

That in another file I import NSemiRing: 

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

For example, if I have a lemma that have the form of : 

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

Where I want "s_typ" is automatically recognize as type "nat" and I can call the Lemma Aadd_0_r to prove this lemma.

Upvotes: 0

Views: 348

Answers (1)

user1861759
user1861759

Reputation:

Doesn't just Proof. apply Aadd_0_r. Qed. finish the proof?

If you turn off notations and unfold all the definitions your goal reduces to Aadd_0_r.

Upvotes: 1

Related Questions