Library Coq.ring.LegacyRing_theory

Require Export Bool.


Section Theory_of_semi_rings.

Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : 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.

Record Semi_Ring_Theory : Prop :=
  {SR_plus_comm : forall n m:A, n + m = m + n;
   SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
   SR_mult_comm : forall n m:A, n * m = m * n;
   SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
   SR_plus_zero_left : forall n:A, 0 + n = n;
   SR_mult_one_left : forall n:A, 1 * n = n;
   SR_mult_zero_left : forall n:A, 0 * n = 0;
   SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;

   SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.

Variable T : Semi_Ring_Theory.

Let plus_comm := SR_plus_comm T.
Let plus_assoc := SR_plus_assoc T.
Let mult_comm := SR_mult_comm T.
Let mult_assoc := SR_mult_assoc T.
Let plus_zero_left := SR_plus_zero_left T.
Let mult_one_left := SR_mult_one_left T.
Let mult_zero_left := SR_mult_zero_left T.
Let distr_left := SR_distr_left T.

Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
  mult_one_left mult_zero_left distr_left .

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

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

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

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

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

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

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

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

Hint Resolve SR_plus_permute SR_mult_permute.

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

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

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

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

Lemma SR_plus_zero_right : forall n:A, n + 0 = n.
Lemma SR_plus_zero_right2 : forall n:A, n = n + 0.

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

Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
End Theory_of_semi_rings.

Section Theory_of_rings.

Variable A : Type.

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).

Record Ring_Theory : Prop :=
  {Th_plus_comm : forall n m:A, n + m = m + n;
   Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
   Th_mult_comm : forall n m:A, n * m = m * n;
   Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
   Th_plus_zero_left : forall n:A, 0 + n = n;
   Th_mult_one_left : forall n:A, 1 * n = n;
   Th_opp_def : forall n:A, n + - n = 0;
   Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
   Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.

Variable T : Ring_Theory.

Let plus_comm := Th_plus_comm T.
Let plus_assoc := Th_plus_assoc T.
Let mult_comm := Th_mult_comm T.
Let mult_assoc := Th_mult_assoc T.
Let plus_zero_left := Th_plus_zero_left T.
Let mult_one_left := Th_mult_one_left T.
Let opp_def := Th_opp_def T.
Let distr_left := Th_distr_left T.

Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
  mult_one_left opp_def distr_left.

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

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

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

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

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

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

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

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

Hint Resolve Th_plus_permute Th_mult_permute.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma Th_opp_zero : - 0 = 0.
Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.

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

End Theory_of_rings.

Hint Resolve Th_mult_zero_left : core.


Definition Semi_Ring_Theory_of :
  forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A)
    (Aopp:A -> A) (Aeq:A -> A -> bool),
    Ring_Theory Aplus Amult Aone Azero Aopp Aeq ->
    Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
Defined.

Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory.

Section product_ring.

End product_ring.

Section power_ring.

End power_ring.