Module cring

Implicit Arguments On.

Module CRing <: Cat_Sig.

Export Misc.

Section CRing_Theory.

Variable A:Type; add:A->A->A; zero:A; opp:A->A; mul:A->A->A; one:A.

Record CRing_Theory : Prop := {
  ax_add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z);
  ax_add_commut : (x,y:A) (add x y)==(add y x);
  ax_zero_sx : (x:A) (add zero x)==x;
  ax_opp_sx : (x:A) (add (opp x) x)==zero;
  ax_mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z);
  ax_mul_commut : (x,y:A) (mul x y)==(mul y x);
  ax_one_sx : (x:A) (mul one x)==x;
  ax_distrib_sx : (x,y,z:A) (mul x (add y y))==(add (mul x y) (mul x z));
  ax_distrib_dx : (x,y,z:A) (mul (add y y) x)==(mul (mul y x) (mul z x))
 }.

End CRing_Theory.

Record Ring_Data : Type := {
  ring_carrier :> Type;
  add : ring_carrier->ring_carrier->ring_carrier;
  zero : ring_carrier;
  opp : ring_carrier->ring_carrier;
  mul : ring_carrier->ring_carrier->ring_carrier;
  one : ring_carrier
 }.

Implicits zero [1].
Implicits one [1].

Record CRing : Type := {
  ring_data :> Ring_Data;
  ring_theory :> (CRing_Theory (!add ring_data) (!zero ring_data)
     (!opp ring_data) (!mul ring_data) (!one ring_data))
 }.

Definition Obj : Type := CRing.
Coercion CRing_of_Obj [x:Obj] : CRing := x.

Section CRing_Facts.

Variable A:CRing.

Lemma add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z).
Proof.
  Intros; Apply (ax_add_assoc A).
Qed.

Lemma add_commut : (x,y:A) (add x y)==(add y x).
Proof.
  Intros; Apply (ax_add_commut A).
Qed.

Lemma zero_sx : (x:A) (add zero x)==x.
Proof.
  Intros; Apply (ax_zero_sx A).
Qed.

Lemma opp_sx : (x:A) (add (opp x) x)==zero.
Proof.
  Intros; Apply (ax_opp_sx A).
Qed.

Lemma mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z).
Proof.
  Intros; Apply (ax_mul_assoc A).
Qed.

Lemma mul_commut : (x,y:A) (mul x y)==(mul y x).
Proof.
  Intros; Apply (ax_mul_commut A).
Qed.

Lemma one_sx : (x:A) (mul one x)==x.
Proof.
  Intros; Apply (ax_one_sx A).
Qed.

Lemma distrib_sx : (x,y,z:A)
 (mul x (add y y))==(add (mul x y) (mul x z)).
Proof.
  Intros; Apply (ax_distrib_sx A).
Qed.

Lemma distrib_dx : (x,y,z:A)
 (mul (add y y) x)==(mul (mul y x) (mul z x)).
Proof.
  Intros; Apply (ax_distrib_dx A).
Qed.

End CRing_Facts.

Hints Resolve add_assoc add_commut zero_sx opp_sx mul_assoc mul_commut
one_sx distrib_sx distrib_dx.

Record Morph_Theory [A,B:CRing; f:A->B] : Prop := {
  morph_add : (x,y:A) (f (add x y))==(add (f x) (f y));
  morph_opp : (x:A) (f (opp x))==(opp (f x));
  morph_mul : (x,y:A) (f (mul x y))==(mul (f x) (f y));
  morph_one : (f one)==one
 }.

Record CRing_Morph [A,B:CRing] : Type := {
  morph_data :> A->B;
  morph_theory :> (Morph_Theory morph_data)
 }.

Definition Morph := CRing_Morph.

Lemma morph_extens : (A,B:CRing; f,g:(Morph A B))
 ((x:A)(f x)==(g x)) -> f==g.
Proof.
  NewDestruct f; NewDestruct g; Simpl; Intros.
  Assert U : morph_data0 == morph_data1.
  Apply nondep_extensionality; Assumption.
  NewDestruct U.
  Assert U : morph_theory0 == morph_theory1.
  Apply proof_irrelevance.
  NewDestruct U.
  Reflexivity.
Qed.

Section morph_comp.

Variable A,B,C:CRing.

Variable f:(Morph B C); g:(Morph A B).

Local h [x:A] : C := (f (g x)).

Remark h_th : (Morph_Theory h).
Proof.
  Unfold h; Split; Intros.
  Rewrite (morph_add g).
  Rewrite (morph_add f).
  Reflexivity.
  Rewrite (morph_opp g).
  Rewrite (morph_opp f).
  Reflexivity.
  Rewrite (morph_mul g).
  Rewrite (morph_mul f).
  Reflexivity.
  Rewrite (morph_one g).
  Rewrite (morph_one f).
  Reflexivity.
Qed.

Definition morph_comp : (Morph A C).
Proof.
  Split with h;
  Apply h_th.
Defined.

End morph_comp.

Definition morph_id [A:CRing] : (Morph A A).
Proof.
  Intros.
  Split with [x:A]x.
  Abstract Split; Auto.
Defined.

Implicits morph_id [1].

Lemma morph_comp_assoc : (A,B,C,D:CRing)
 (h:(Morph C D); g:(Morph B C); f:(Morph A B))
 (morph_comp h (morph_comp g f))==(morph_comp (morph_comp h g) f).
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.

Lemma morph_id_sx : (A,B:CRing; f:(Morph A B))
 (morph_comp morph_id f)==f.
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.

Lemma morph_id_dx : (A,B:CRing; f:(Morph A B))
 (morph_comp f morph_id)==f.
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.