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.