Library Coq.setoid_ring.Ncring
Require Import Setoid.
Require Import BinPos.
Require Import BinNat.
Require Export Morphisms Setoid Bool.
Require Export ZArith_base.
Require Export Algebra_syntax.
Set Implicit Arguments.
Class Ring_ops(
T:
Type)
{
ring0:
T}
{
ring1:
T}
{
add:
T->T->T}
{
mul:
T->T->T}
{
sub:
T->T->T}
{
opp:
T->T}
{
ring_eq:
T->T->Prop}.
Instance zero_notation(
T:
Type)`{
Ring_ops T}:
Zero T:=
ring0.
Instance one_notation(
T:
Type)`{
Ring_ops T}:
One T:=
ring1.
Instance add_notation(
T:
Type)`{
Ring_ops T}:
Addition T:=
add.
Instance mul_notation(
T:
Type)`{
Ring_ops T}:@
Multiplication T T:=
mul.
Instance sub_notation(
T:
Type)`{
Ring_ops T}:
Subtraction T:=
sub.
Instance opp_notation(
T:
Type)`{
Ring_ops T}:
Opposite T:=
opp.
Instance eq_notation(
T:
Type)`{
Ring_ops T}:@
Equality T:=
ring_eq.
Class Ring `{
Ro:
Ring_ops}:={
ring_setoid:
Equivalence _==_;
ring_plus_comp:
Proper (
_==_ ==> _==_ ==>_==_)
_+_;
ring_mult_comp:
Proper (
_==_ ==> _==_ ==>_==_)
_*_;
ring_sub_comp:
Proper (
_==_ ==> _==_ ==>_==_)
_-_;
ring_opp_comp:
Proper (
_==_==>_==_)
-_;
ring_add_0_l :
forall x, 0
+ x == x;
ring_add_comm :
forall x y,
x + y == y + x;
ring_add_assoc :
forall x y z,
x + (y + z) == (x + y) + z;
ring_mul_1_l :
forall x, 1
* x == x;
ring_mul_1_r :
forall x,
x * 1
== x;
ring_mul_assoc :
forall x y z,
x * (y * z) == (x * y) * z;
ring_distr_l :
forall x y z,
(x + y) * z == x * z + y * z;
ring_distr_r :
forall x y z,
z * ( x + y) == z * x + z * y;
ring_sub_def :
forall x y,
x - y == x + -y;
ring_opp_def :
forall x,
x + -x == 0
}.
Section Ring_power.
Context {
R:
Type}`{
Ring R}.
Fixpoint pow_pos (
x:
R) (
i:
positive) {
struct i}:
R :=
match i with
|
xH =>
x
|
xO i =>
let p :=
pow_pos x i in p * p
|
xI i =>
let p :=
pow_pos x i in x * (p * p)
end.
Definition pow_N (
x:
R) (
p:
N) :=
match p with
|
N0 => 1
|
Npos p =>
pow_pos x p
end.
End Ring_power.
Definition ZN(
x:
Z):=
match x with
Z0 =>
N0
|
Zpos p |
Zneg p =>
Npos p
end.
Instance power_ring {
R:
Type}`{
Ring R} :
Power:=
{
power x y :=
pow_N x (
ZN y)}.
Interpretation morphisms definition
Identity is a morphism
rings are almost rings
Lemma ring_mul_0_l :
forall x, 0
* x == 0.
Lemma ring_mul_0_r :
forall x,
x * 0
== 0.
Lemma ring_opp_mul_l :
forall x y,
-(x * y) == -x * y.
Lemma ring_opp_mul_r :
forall x y,
-(x * y) == x * -y.
Lemma ring_opp_add :
forall x y,
-(x + y) == -x + -y.
Lemma ring_opp_opp :
forall x,
- -x == x.
Lemma ring_sub_ext :
forall x1 x2,
x1 == x2 -> forall y1 y2,
y1 == y2 -> x1 - y1 == x2 - y2.
Ltac mrewrite :=
repeat first
[
rewrite ring_add_0_l
|
rewrite <- (
ring_add_comm 0)
|
rewrite ring_mul_1_l
|
rewrite ring_mul_0_l
|
rewrite ring_distr_l
|
reflexivity
].
Lemma ring_add_0_r :
forall x,
(x + 0
) == x.
Lemma ring_add_assoc1 :
forall x y z,
(x + y) + z == (y + z) + x.
Lemma ring_add_assoc2 :
forall x y z,
(y + x) + z == (y + z) + x.
Lemma ring_opp_zero :
-0
== 0.
End Ring.
Some simplification tactics