Library Stdlib.setoid_ring.Ncring

From Stdlib Require Import Setoid.
From Stdlib Require Import BinPos.
From Stdlib Require Import BinNat.
From Stdlib Require Export Morphisms Setoid Bool.
From Stdlib Require Export BinInt.
From Stdlib 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}.

#[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]
Instance add_notation(T:Type)`{Ring_ops T}:Addition T:= add.
#[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)}.

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.

 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.

Ltac gen_reflexivity := reflexivity.

Ltac gen_rewrite :=
  repeat first
     [ reflexivity
     | progress rewrite ring_opp_zero
     | rewrite ring_add_0_l
     | rewrite ring_add_0_r
     | 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
     | rewrite ring_add_assoc
     | rewrite ring_mul_assoc
     | progress rewrite ring_opp_add
     | progress rewrite ring_sub_def
     | progress rewrite <- ring_opp_mul_l
     | progress rewrite <- ring_opp_mul_r ].

Ltac gen_add_push x :=
repeat (match goal with
  | |- context [(?y + x) + ?z] =>
     progress rewrite (ring_add_assoc2 x y z)
  | |- context [(x + ?y) + ?z] =>
     progress rewrite (ring_add_assoc1 x y z)
  end).