Library Coq.ring.Setoid_ring_theory



Require Export Bool.
Require Export Setoid.


Section Setoid_rings.

Variable A : Type.
Variable Aequiv : A -> A -> Prop.

Infix Local "==" := Aequiv (at level 70, no associativity).

Variable S : Setoid_Theory A Aequiv.

Add Setoid A Aequiv S as Asetoid.

Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.

Infix "+" := Aplus (at level 50, left associativity).
Infix "*" := Amult (at level 40, left associativity).
Notation "0" := Azero.
Notation "1" := Aone.
Notation "- x" := (Aopp x).

Variable plus_morph :
 forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2.
Variable mult_morph :
  forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2.
Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0.

Add Morphism Aplus : Aplus_ext.
Qed.

Add Morphism Amult : Amult_ext.
Qed.

Add Morphism Aopp : Aopp_ext.
Qed.

Section Theory_of_semi_setoid_rings.

Record Semi_Setoid_Ring_Theory : Prop :=
  {SSR_plus_comm : forall n m:A, n + m == m + n;
   SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
   SSR_mult_comm : forall n m:A, n * m == m * n;
   SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
   SSR_plus_zero_left : forall n:A, 0 + n == n;
   SSR_mult_one_left : forall n:A, 1 * n == n;
   SSR_mult_zero_left : forall n:A, 0 * n == 0;
   SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
   SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p;
   SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.

Variable T : Semi_Setoid_Ring_Theory.

Let plus_comm := SSR_plus_comm T.
Let plus_assoc := SSR_plus_assoc T.
Let mult_comm := SSR_mult_comm T.
Let mult_assoc := SSR_mult_assoc T.
Let plus_zero_left := SSR_plus_zero_left T.
Let mult_one_left := SSR_mult_one_left T.
Let mult_zero_left := SSR_mult_zero_left T.
Let distr_left := SSR_distr_left T.
Let plus_reg_left := SSR_plus_reg_left T.
Let equiv_refl := Seq_refl A Aequiv S.
Let equiv_sym := Seq_sym A Aequiv S.
Let equiv_trans := Seq_trans A Aequiv S.

Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
  mult_one_left mult_zero_left distr_left plus_reg_left
  equiv_refl .
Hint Immediate equiv_sym.

Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).

Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).

Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n.

Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n.

Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n.

Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.

Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).

Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).

Hint Resolve SSR_plus_permute SSR_mult_permute.

Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.

Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).

Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0.

Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0.

Lemma SSR_plus_zero_right : forall n:A, n + 0 == n.

Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0.

Lemma SSR_mult_one_right : forall n:A, n * 1 == n.

Lemma SSR_mult_one_right2 : forall n:A, n == n * 1.

Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.

End Theory_of_semi_setoid_rings.

Section Theory_of_setoid_rings.

Record Setoid_Ring_Theory : Prop :=
  {STh_plus_comm : forall n m:A, n + m == m + n;
   STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
   STh_mult_comm : forall n m:A, n * m == m * n;
   STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
   STh_plus_zero_left : forall n:A, 0 + n == n;
   STh_mult_one_left : forall n:A, 1 * n == n;
   STh_opp_def : forall n:A, n + - n == 0;
   STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
   STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.

Variable T : Setoid_Ring_Theory.

Let plus_comm := STh_plus_comm T.
Let plus_assoc := STh_plus_assoc T.
Let mult_comm := STh_mult_comm T.
Let mult_assoc := STh_mult_assoc T.
Let plus_zero_left := STh_plus_zero_left T.
Let mult_one_left := STh_mult_one_left T.
Let opp_def := STh_opp_def T.
Let distr_left := STh_distr_left T.
Let equiv_refl := Seq_refl A Aequiv S.
Let equiv_sym := Seq_sym A Aequiv S.
Let equiv_trans := Seq_trans A Aequiv S.

Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
  mult_one_left opp_def distr_left equiv_refl equiv_sym.


Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).

Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).

Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n.

Lemma STh_mult_one_left2 : forall n:A, n == 1 * n.

Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.

Lemma STh_opp_def2 : forall n:A, 0 == n + - n.

Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).

Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).

Hint Resolve STh_plus_permute STh_mult_permute.

Lemma Saux1 : forall a:A, a + a == a -> a == 0.

Lemma STh_mult_zero_left : forall n:A, 0 * n == 0.
Hint Resolve STh_mult_zero_left.

Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n.

Lemma Saux2 : forall x y z:A, x + y == 0 -> x + z == 0 -> y == z.

Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y.
Hint Resolve STh_opp_mult_left.

Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y).

Lemma STh_mult_zero_right : forall n:A, n * 0 == 0.

Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0.

Lemma STh_plus_zero_right : forall n:A, n + 0 == n.

Lemma STh_plus_zero_right2 : forall n:A, n == n + 0.

Lemma STh_mult_one_right : forall n:A, n * 1 == n.

Lemma STh_mult_one_right2 : forall n:A, n == n * 1.

Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y.

Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y).

Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y).

Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p).

Lemma STh_opp_opp : forall n:A, - - n == n.
Hint Resolve STh_opp_opp.

Lemma STh_opp_opp2 : forall n:A, n == - - n.

Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y.

Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y.

Lemma STh_opp_zero : - 0 == 0.

Lemma STh_plus_reg_left : forall n m p:A, n + m == n + p -> m == p.

Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.

Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.

Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).

End Theory_of_setoid_rings.

Hint Resolve STh_mult_zero_left STh_plus_reg_left: core.


Definition Semi_Setoid_Ring_Theory_of :
  Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
Defined.

Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >->
 Semi_Setoid_Ring_Theory.

Section product_ring.

End product_ring.

Section power_ring.

End power_ring.

End Setoid_rings.