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.