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}
{mul:T->T->T}
{sub:T->T->T}
{opp:T->T}
{ring_eq:T->T->Prop}.

#[global]
Instance zero_notation(T:Type)`{Ring_ops T}:Zero T:= ring0.
#[global]
Instance one_notation(T:Type)`{Ring_ops T}:One T:= ring1.
#[global]
#[global]
Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T:= mul.
#[global]
Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T:= sub.
#[global]
Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T:= opp.
#[global]
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
}.
#[global]
Existing Instance ring_setoid.
#[global]
Existing Instance ring_plus_comp.
#[global]
Existing Instance ring_mult_comp.
#[global]
Existing Instance ring_sub_comp.
#[global]
Existing Instance ring_opp_comp.

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.

#[global]
Instance power_ring {R:Type}`{Ring R} : Power:=
{power x y := pow_N x (ZN y)}.

Interpretation morphisms definition

Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= {
ring_morphism0 : [0] == 0;
ring_morphism1 : [1] == 1;
ring_morphism_add : forall x y, [x + y] == [x] + [y];
ring_morphism_sub : forall x y, [x - y] == [x] - [y];
ring_morphism_mul : forall x y, [x * y] == [x] * [y];
ring_morphism_opp : forall x, [-x] == -[x];
ring_morphism_eq : forall x y, x == y -> [x] == [y]}.

Section Ring.

Context {R:Type}`{Rr:Ring R}.

Lemma pow_pos_comm : forall x j, x * pow_pos x j == pow_pos x j * x.

Lemma pow_pos_succ : forall x j, pow_pos x (Pos.succ j) == x * pow_pos x j.

Lemma pow_pos_add : forall x i j,
pow_pos x (i + j) == pow_pos x i * pow_pos x j.

Definition id_phi_N (x:N) : N := x.

Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.

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_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
Ltac gen_reflexivity := reflexivity.

Ltac gen_rewrite :=
repeat first
[ reflexivity
| progress rewrite ring_opp_zero
| rewrite ring_mul_1_l
| rewrite ring_mul_1_r
| rewrite ring_mul_0_l
| rewrite ring_mul_0_r
| rewrite ring_distr_l
| rewrite ring_distr_r