Library Coq.setoid_ring.Ring_theory
Require Import Setoid.
Require Import BinPos.
Require Import BinNat.
Module RingSyntax.
Reserved Notation "x ?=! y" (
at level 70,
no associativity).
Reserved Notation "x +! y " (
at level 50,
left associativity).
Reserved Notation "x -! y" (
at level 50,
left associativity).
Reserved Notation "x *! y" (
at level 40,
left associativity).
Reserved Notation "-! x" (
at level 35,
right associativity).
Reserved Notation "[ x ]" (
at level 0).
Reserved Notation "x ?== y" (
at level 70,
no associativity).
Reserved Notation "x -- y" (
at level 50,
left associativity).
Reserved Notation "x ** y" (
at level 40,
left associativity).
Reserved Notation "-- x" (
at level 35,
right associativity).
Reserved Notation "x == y" (
at level 70,
no associativity).
End RingSyntax.
Import RingSyntax.
Section Power.
Variable R:
Type.
Variable rI :
R.
Variable rmul :
R ->
R ->
R.
Variable req :
R ->
R ->
Prop.
Variable Rsth :
Setoid_Theory R req.
Notation "x * y " := (
rmul x y).
Notation "x == y" := (
req x y).
Hypothesis mul_ext :
forall x1 x2,
x1 == x2 ->
forall y1 y2,
y1 == y2 ->
x1 * y1 == x2 * y2.
Hypothesis mul_comm :
forall x y,
x * y == y * x.
Hypothesis mul_assoc :
forall x y z,
x * (y * z) == (x * y) * z.
Add Setoid R req Rsth as R_set_Power.
Add Morphism rmul :
rmul_ext_Power.
Fixpoint pow_pos (
x:
R) (
i:
positive) {
struct i}:
R :=
match i with
|
xH =>
x
|
xO i =>
let p :=
pow_pos x i in rmul p p
|
xI i =>
let p :=
pow_pos x i in rmul x (
rmul p p)
end.
Lemma pow_pos_Psucc :
forall x j,
pow_pos x (
Psucc j)
== x * pow_pos x j.
Lemma pow_pos_Pplus :
forall x i j,
pow_pos x (
i + j)
== pow_pos x i * pow_pos x j.
Definition pow_N (
x:
R) (
p:
N) :=
match p with
|
N0 =>
rI
|
Npos p =>
pow_pos x p
end.
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.
End Power.
Section DEFINITIONS.
Variable R :
Type.
Variable (
rO rI :
R) (
radd rmul rsub:
R->
R->
R) (
ropp :
R ->
R).
Variable req :
R ->
R ->
Prop.
Notation "0" :=
rO.
Notation "1" :=
rI.
Notation "x + y" := (
radd x y).
Notation "x * y " := (
rmul x y).
Notation "x - y " := (
rsub x y).
Notation "- x" := (
ropp x).
Notation "x == y" := (
req x y).
Semi Ring
Almost Ring
Record almost_ring_theory :
Prop :=
mk_art {
ARadd_0_l :
forall x, 0
+ x == x;
ARadd_comm :
forall x y,
x + y == y + x;
ARadd_assoc :
forall x y z,
x + (y + z) == (x + y) + z;
ARmul_1_l :
forall x, 1
* x == x;
ARmul_0_l :
forall x, 0
* x == 0;
ARmul_comm :
forall x y,
x * y == y * x;
ARmul_assoc :
forall x y z,
x * (y * z) == (x * y) * z;
ARdistr_l :
forall x y z,
(x + y) * z == (x * z) + (y * z);
ARopp_mul_l :
forall x y,
-(x * y) == -x * y;
ARopp_add :
forall x y,
-(x + y) == -x + -y;
ARsub_def :
forall x y,
x - y == x + -y
}.
Ring
Equality is extensional
Interpretation morphisms definition
Section MORPHISM.
Variable C:
Type.
Variable (
cO cI :
C) (
cadd cmul csub :
C->
C->
C) (
copp :
C->
C).
Variable ceqb :
C->
C->
bool.
Variable phi :
C ->
R.
Notation "x +! y" := (
cadd x y).
Notation "x -! y " := (
csub x y).
Notation "x *! y " := (
cmul x y).
Notation "-! x" := (
copp x).
Notation "x ?=! y" := (
ceqb x y).
Notation "[ x ]" := (
phi x).
Record semi_morph :
Prop :=
mkRmorph {
Smorph0 :
[cO] == 0;
Smorph1 :
[cI] == 1;
Smorph_add :
forall x y,
[x +! y] == [x]+[y];
Smorph_mul :
forall x y,
[x *! y] == [x]*[y];
Smorph_eq :
forall x y,
x?=!y = true ->
[x] == [y]
}.
Record ring_morph :
Prop :=
mkmorph {
morph0 :
[cO] == 0;
morph1 :
[cI] == 1;
morph_add :
forall x y,
[x +! y] == [x]+[y];
morph_sub :
forall x y,
[x -! y] == [x]-[y];
morph_mul :
forall x y,
[x *! y] == [x]*[y];
morph_opp :
forall x,
[-!x] == -[x];
morph_eq :
forall x y,
x?=!y = true ->
[x] == [y]
}.
Section SIGN.
Variable get_sign :
C ->
option C.
Record sign_theory :
Prop :=
mksign_th {
sign_spec :
forall c c',
get_sign c = Some c' ->
c ?=! -! c' = true
}.
End SIGN.
Definition get_sign_None (
c:
C) := @
None C.
Lemma get_sign_None_th :
sign_theory get_sign_None.
Section DIV.
Variable cdiv:
C ->
C ->
C*C.
Record div_theory :
Prop :=
mkdiv_th {
div_eucl_th :
forall a b,
let (
q,
r) :=
cdiv a b in [a] == [b *! q +! r]
}.
End DIV.
End MORPHISM.
Identity is a morphism
Specification of the power function
Leibniz equality leads to a setoid theory and is extensional
Every semi ring can be seen as an almost ring, by taking :
Identity morphism for semi-ring equipped with their almost-ring structure
Rings are almost rings
Every semi morphism between two rings is a morphism
Useful lemmas on almost ring
Variable ARth :
almost_ring_theory 0 1
radd rmul rsub ropp req.
Lemma ARth_SRth :
semi_ring_theory 0 1
radd rmul req.
Lemma ARsub_ext :
forall x1 x2,
x1 == x2 ->
forall y1 y2,
y1 == y2 ->
x1 - y1 == x2 - y2.
Add Morphism rsub :
rsub_ext.
Ltac mrewrite :=
repeat first
[
rewrite (
ARadd_0_l ARth)
|
rewrite <- ((
ARadd_comm ARth) 0)
|
rewrite (
ARmul_1_l ARth)
|
rewrite <- ((
ARmul_comm ARth) 1)
|
rewrite (
ARmul_0_l ARth)
|
rewrite <- ((
ARmul_comm ARth) 0)
|
rewrite (
ARdistr_l ARth)
|
sreflexivity
|
match goal with
| |-
context [?
z * (?x + ?y)] =>
rewrite ((
ARmul_comm ARth)
z (
x+y))
end].
Lemma ARadd_0_r :
forall x,
(x + 0
) == x.
Lemma ARmul_1_r :
forall x,
x * 1
== x.
Lemma ARmul_0_r :
forall x,
x * 0
== 0.
Lemma ARdistr_r :
forall x y z,
z * (x + y) == z*x + z*y.
Lemma ARadd_assoc1 :
forall x y z,
(x + y) + z == (y + z) + x.
Lemma ARadd_assoc2 :
forall x y z,
(y + x) + z == (y + z) + x.
Lemma ARmul_assoc1 :
forall x y z,
(x * y) * z == (y * z) * x.
Lemma ARmul_assoc2 :
forall x y z,
(y * x) * z == (y * z) * x.
Lemma ARopp_mul_r :
forall x y,
- (x * y) == x * -y.
Lemma ARopp_zero :
-0
== 0.
End ALMOST_RING.
Section AddRing.
Inductive ring_kind :
Type :=
|
Abstract
|
Computational
(
R:
Type)
(
req :
R ->
R ->
Prop)
(
reqb :
R ->
R ->
bool)
(
_ :
forall x y,
(reqb x y) = true ->
req x y)
|
Morphism
(
R :
Type)
(
rO rI :
R) (
radd rmul rsub:
R->
R->
R) (
ropp :
R ->
R)
(
req :
R ->
R ->
Prop)
(
C :
Type)
(
cO cI :
C) (
cadd cmul csub :
C->
C->
C) (
copp :
C->
C)
(
ceqb :
C->
C->
bool)
phi
(
_ :
ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi).
End AddRing.
Some simplification tactics
Ltac gen_reflexivity Rsth :=
apply (
Seq_refl _ _ Rsth).
Ltac gen_srewrite Rsth Reqe ARth :=
repeat first
[
gen_reflexivity Rsth
|
progress rewrite (
ARopp_zero Rsth Reqe ARth)
|
rewrite (
ARadd_0_l ARth)
|
rewrite (
ARadd_0_r Rsth ARth)
|
rewrite (
ARmul_1_l ARth)
|
rewrite (
ARmul_1_r Rsth ARth)
|
rewrite (
ARmul_0_l ARth)
|
rewrite (
ARmul_0_r Rsth ARth)
|
rewrite (
ARdistr_l ARth)
|
rewrite (
ARdistr_r Rsth Reqe ARth)
|
rewrite (
ARadd_assoc ARth)
|
rewrite (
ARmul_assoc ARth)
|
progress rewrite (
ARopp_add ARth)
|
progress rewrite (
ARsub_def ARth)
|
progress rewrite <- (
ARopp_mul_l ARth)
|
progress rewrite <- (
ARopp_mul_r Rsth Reqe ARth) ].
Ltac gen_add_push add Rsth Reqe ARth x :=
repeat (
match goal with
| |-
context [
add (
add ?
y x) ?
z] =>
progress rewrite (
ARadd_assoc2 Rsth Reqe ARth x y z)
| |-
context [
add (
add x ?
y) ?
z] =>
progress rewrite (
ARadd_assoc1 Rsth ARth x y z)
end).
Ltac gen_mul_push mul Rsth Reqe ARth x :=
repeat (
match goal with
| |-
context [
mul (
mul ?
y x) ?
z] =>
progress rewrite (
ARmul_assoc2 Rsth Reqe ARth x y z)
| |-
context [
mul (
mul x ?
y) ?
z] =>
progress rewrite (
ARmul_assoc1 Rsth ARth x y z)
end).