Library Rings

Require Import EnsembleFacts.
Require Import Groups.

Require Import Setoid.


Delimit Scope ring_scope with ring.

Section Rings.

Variable U:Type.
Variable add prod:Operation U.
Infix "+" := add : ring_scope.
Infix "*" := prod: ring_scope.
Open Scope ring_scope.

Definition Distributive_left:=forall (a b c:U),
a * (b + c)=(a * b) +(a* c).
Definition Distributive_right:=forall (a b c:U),
(a + b)*c=(a * c) +(b* c).

Definition Distributive:= Distributive_left /\ Distributive_right.

Definition Ring:=
AbelianGroup U add /\
Monoid U prod /\
Distributive.

Definition CommutativeRing:=Ring /\ Commutativity U prod.

Definition Ring0 (zero:U):= Identity U add zero.
Definition Ring1 (one:U):=Identity U prod one.

Hypothesis R:Ring.
Lemma Gadd: Group U add.

Lemma Ring0_unique: exists! zero:U, Ring0 zero.

Lemma Ring1_unique: exists! one:U, Ring1 one.

Lemma Ring_distribute_left: Distributive_left.

Lemma Ring_distribute_right: Distributive_right.

Lemma Ring_add_commute: Commutativity U add.

Lemma Ring_add_associate: Associativity U add.

Lemma Ring_prod_associate: Associativity U prod.

Lemma Ring_addleft_simplify: forall a b c:U, a+b=a+c->b=c.

Lemma Ring_addright_simplify: forall a b c:U, a+c=b+c->a=b.

Lemma Ring_add_leftadd: forall a b c:U, a=b->c+a=c+b.

Lemma Ring_add_rightadd: forall a b c:U, a=b->a+c=b+c.

Variable zero:U.
Hypothesis zeroH:Ring0 zero.
Variable one:U.
Hypothesis oneH:Ring1 one.

Lemma Ring_addleft0: forall (a:U), zero+a=a.

Lemma Ring_addright0: forall (a:U), a+zero=a.

Lemma Ring_addleft_simplify0: forall a b:U, a+b=a->b=zero.

Lemma Ring_addright_simplify0: forall a b:U, a+b=b->a=zero.

Theorem Ring_prodleft0: forall (a:U), zero * a=zero.

Theorem Ring_prodright0: forall (a:U), a*zero=zero.

Lemma Ring_prodleft1: forall (a:U), one * a=a.

Lemma Ring_prodright1: forall (a:U), a*one=a.

Theorem Ring_trivial: zero=one -> forall a:U, a=zero.

Lemma minus_one: exists mone:U, Inverse U add one mone.

Variable mone:U.
Hypothesis moneH:Inverse U add one mone.

Variable minus:U->U.
Hypothesis minusH: Group_Inversion U add minus.
Notation " - a " := (minus a) : ring_scope.

Definition sub (a b:U):=a + (-b).
Notation " a - b " := (sub a b) : ring_scope.

Lemma Ring_minus_double: forall a:U, --a=a.

Lemma Ring_minus_zero: -zero=zero.

Lemma Ring_minus_simplify: forall a b:U, -a=-b->a=b.

Lemma Ring_minus_addition_t: forall a b:U, -(a+b)=(-b)+(-a).

Lemma Ring_minus_addition: forall a b:U, -(a+b)=(-a)+(-b).

Lemma mone_minus: mone=-one.

Lemma Ring_sub: forall a:U, a-a=zero.

Lemma Ring_ShiftRightTerm: forall (a b c:U), a+b=c->a=c-b.

Lemma Ring_ShiftLeftTerm: forall (a b c:U), a+b=c->b=-a+c.

Theorem Ring_minusprod_left: forall a b:U,(-a)*b=-(a*b).

Theorem Ring_minusprod_right: forall a b:U,a*(-b)=-(a*b).

Theorem Ring_prodleft_mone: forall (a:U), (-one)*a=-a.

Theorem Ring_prodright_mone: forall (a:U), a*(-one)=-a.

Lemma Ring_sub_rightadd: forall a b c:U, a=b->a-c=b-c.

Lemma Ring_subright_simplify: forall a b c:U, a-c=b-c->a=b.

Lemma Ring_subright_simplify0: forall a b:U, a-b=-b->a=zero.

Lemma Ring_sub_leftadd: forall a b c:U, a=b->c-a=c-b.

Lemma Ring_subleft_simplify: forall a b c:U, a-b=a-c->b=c.

Lemma Ring_subleft_simplify0: forall a b:U, a-b=a->b=zero.

End Rings.

Section Integers.
Require Import ZArith.
Open Scope Z_scope.
Theorem Ring_Integers: Ring Z Zplus Zmult.

Let integers_commute: forall a b:Z, a+b=b+a.

End Integers.