Library Coq.setoid_ring.Ring_theory
Require Import Setoid Morphisms BinPos BinNat.
Set Implicit Arguments.
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 :
Equivalence req.
Infix "*" :=
rmul.
Infix "==" :=
req.
Hypothesis mul_ext :
Proper (
req ==> req ==> req)
rmul.
Hypothesis mul_assoc :
forall x y z,
x * (y * z) == (x * y) * z.
Fixpoint pow_pos (
x:
R) (
i:
positive) :
R :=
match i with
|
xH =>
x
|
xO i =>
let p :=
pow_pos x i in p * p
|
xI i =>
let p :=
pow_pos x i in x * (p * p)
end.
Lemma pow_pos_swap x j :
pow_pos x j * x == x * pow_pos x j.
Lemma pow_pos_succ x j :
pow_pos x (
Pos.succ j)
== x * pow_pos x j.
Lemma pow_pos_add 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 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.
Infix "==" :=
req.
Infix "+" :=
radd.
Infix "*" :=
rmul.
Infix "-" :=
rsub.
Notation "- x" := (
ropp x).
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.
Infix "+!" :=
cadd.
Infix "-!" :=
csub.
Infix "*!" :=
cmul.
Notation "-! x" := (
copp x).
Infix "?=!" :=
ceqb.
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 :
-x = x and x - y = x + y
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
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_srewrite_sr 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) ].
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)
| |-
context [(
add x ?
y)] =>
progress rewrite (
ARadd_comm ARth x y)
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)
| |-
context [(
mul x ?
y)] =>
progress rewrite (
ARmul_comm ARth x y)
end).