Library Stdlib.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
Record semi_ring_theory : Prop := mk_srt {
SRadd_0_l : forall n, 0 + n == n;
SRadd_comm : forall n m, n + m == m + n ;
SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
SRmul_1_l : forall n, 1*n == n;
SRmul_0_l : forall n, 0*n == 0;
SRmul_comm : forall n m, n*m == m*n;
SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
SRdistr_l : forall n m p, (n + m)*p == n*p + m*p
}.
SRadd_0_l : forall n, 0 + n == n;
SRadd_comm : forall n m, n + m == m + n ;
SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
SRmul_1_l : forall n, 1*n == n;
SRmul_0_l : forall n, 0*n == 0;
SRmul_comm : forall n m, n*m == m*n;
SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
SRdistr_l : forall n m p, (n + m)*p == n*p + m*p
}.
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
}.
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
Record ring_theory : Prop := mk_rt {
Radd_0_l : forall x, 0 + x == x;
Radd_comm : forall x y, x + y == y + x;
Radd_assoc : forall x y z, x + (y + z) == (x + y) + z;
Rmul_1_l : forall x, 1 * x == x;
Rmul_comm : forall x y, x * y == y * x;
Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z;
Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z);
Rsub_def : forall x y, x - y == x + -y;
Ropp_def : forall x, x + (- x) == 0
}.
Radd_0_l : forall x, 0 + x == x;
Radd_comm : forall x y, x + y == y + x;
Radd_assoc : forall x y z, x + (y + z) == (x + y) + z;
Rmul_1_l : forall x, 1 * x == x;
Rmul_comm : forall x y, x * y == y * x;
Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z;
Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z);
Rsub_def : forall x y, x - y == x + -y;
Ropp_def : forall x, x + (- x) == 0
}.
Equality is extensional
Record sring_eq_ext : Prop := mk_seqe {
SRadd_ext : Proper (req ==> req ==> req) radd;
SRmul_ext : Proper (req ==> req ==> req) rmul
}.
Record ring_eq_ext : Prop := mk_reqe {
Radd_ext : Proper (req ==> req ==> req) radd;
Rmul_ext : Proper (req ==> req ==> req) rmul;
Ropp_ext : Proper (req ==> req) ropp
}.
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.
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
Variable Rsth : Equivalence req.
Variable reqb : R->R->bool.
Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y.
Definition IDphi (x:R) := x.
Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi.
Variable reqb : R->R->bool.
Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y.
Definition IDphi (x:R) := x.
Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi.
Specification of the power function
Section POWER.
Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Record power_theory : Prop := mkpow_th {
rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
}.
End POWER.
Definition pow_N_th :=
mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
End DEFINITIONS.
Section ALMOST_RING.
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.
Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Record power_theory : Prop := mkpow_th {
rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
}.
End POWER.
Definition pow_N_th :=
mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
End DEFINITIONS.
Section ALMOST_RING.
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.
Leibniz equality leads to a setoid theory and is extensional
Lemma Eqsth : Equivalence (@eq R).
Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R).
Variable Rsth : Equivalence req.
Section SEMI_RING.
Variable SReqe : sring_eq_ext radd rmul req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext1.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1.
Variable SRth : semi_ring_theory 0 1 radd rmul req.
Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R).
Variable Rsth : Equivalence req.
Section SEMI_RING.
Variable SReqe : sring_eq_ext radd rmul req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext1.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1.
Variable SRth : semi_ring_theory 0 1 radd rmul req.
Every semi ring can be seen as an almost ring, by taking :
-x = x and x - y = x + y
Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
Definition SRsub x y := x + -y. Infix "-" := SRsub.
Lemma SRopp_ext : forall x y, x == y -> -x == -y.
Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req.
Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y.
Lemma SRopp_add : forall x y, -(x + y) == -x + -y.
Lemma SRsub_def : forall x y, x - y == x + -y.
Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req.
Definition SRsub x y := x + -y. Infix "-" := SRsub.
Lemma SRopp_ext : forall x y, x == y -> -x == -y.
Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req.
Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y.
Lemma SRopp_add : forall x y, -(x + y) == -x + -y.
Lemma SRsub_def : forall x y, x - y == x + -y.
Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req.
Identity morphism for semi-ring equipped with their almost-ring structure
Variable reqb : R->R->bool.
Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y.
Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req
0 1 radd rmul SRsub SRopp reqb (@IDphi R).
Variable C : Type.
Variable (cO cI : C) (cadd cmul: C->C->C).
Variable (ceqb : C -> C -> bool).
Variable phi : C -> R.
Variable Smorph : semi_morph rO rI radd rmul req cO cI cadd cmul ceqb phi.
Lemma SRmorph_Rmorph :
ring_morph rO rI radd rmul SRsub SRopp req
cO cI cadd cmul cadd (fun x => x) ceqb phi.
End SEMI_RING.
Infix "-" := rsub.
Notation "- x" := (ropp x).
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext2.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2.
Add Morphism ropp with signature (req ==> req) as ropp_ext2.
Section RING.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y.
Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req
0 1 radd rmul SRsub SRopp reqb (@IDphi R).
Variable C : Type.
Variable (cO cI : C) (cadd cmul: C->C->C).
Variable (ceqb : C -> C -> bool).
Variable phi : C -> R.
Variable Smorph : semi_morph rO rI radd rmul req cO cI cadd cmul ceqb phi.
Lemma SRmorph_Rmorph :
ring_morph rO rI radd rmul SRsub SRopp req
cO cI cadd cmul cadd (fun x => x) ceqb phi.
End SEMI_RING.
Infix "-" := rsub.
Notation "- x" := (ropp x).
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext2.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2.
Add Morphism ropp with signature (req ==> req) as ropp_ext2.
Section RING.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Rings are almost rings
Lemma Rmul_0_l x : 0 * x == 0.
Lemma Ropp_mul_l x y : -(x * y) == -x * y.
Lemma Ropp_add x y : -(x + y) == -x + -y.
Lemma Ropp_opp x : - -x == x.
Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Lemma Ropp_mul_l x y : -(x * y) == -x * y.
Lemma Ropp_add x y : -(x + y) == -x + -y.
Lemma Ropp_opp x : - -x == x.
Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Every semi morphism between two rings is a morphism
Variable C : Type.
Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C).
Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool).
Variable phi : C -> R.
Infix "+!" := cadd. Infix "*!" := cmul.
Infix "-!" := csub. Notation "-! x" := (copp x).
Notation "?=!" := ceqb. Notation "[ x ]" := (phi x).
Variable Csth : Equivalence ceq.
Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
Add Parametric Relation : C ceq
reflexivity proved by (@Equivalence_Reflexive _ _ Csth)
symmetry proved by (@Equivalence_Symmetric _ _ Csth)
transitivity proved by (@Equivalence_Transitive _ _ Csth)
as C_setoid.
Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext.
Add Morphism copp with signature (ceq ==> ceq) as copp_ext.
Variable Cth : ring_theory cO cI cadd cmul csub copp ceq.
Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi.
Variable phi_ext : forall x y, ceq x y -> [x] == [y].
Add Morphism phi with signature (ceq ==> req) as phi_ext1.
Lemma Smorph_opp x : [-!x] == -[x].
Lemma Smorph_sub x y : [x -! y] == [x] - [y].
Lemma Smorph_morph :
ring_morph 0 1 radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
End RING.
Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C).
Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool).
Variable phi : C -> R.
Infix "+!" := cadd. Infix "*!" := cmul.
Infix "-!" := csub. Notation "-! x" := (copp x).
Notation "?=!" := ceqb. Notation "[ x ]" := (phi x).
Variable Csth : Equivalence ceq.
Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
Add Parametric Relation : C ceq
reflexivity proved by (@Equivalence_Reflexive _ _ Csth)
symmetry proved by (@Equivalence_Symmetric _ _ Csth)
transitivity proved by (@Equivalence_Transitive _ _ Csth)
as C_setoid.
Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext.
Add Morphism copp with signature (ceq ==> ceq) as copp_ext.
Variable Cth : ring_theory cO cI cadd cmul csub copp ceq.
Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi.
Variable phi_ext : forall x y, ceq x y -> [x] == [y].
Add Morphism phi with signature (ceq ==> req) as phi_ext1.
Lemma Smorph_opp x : [-!x] == -[x].
Lemma Smorph_sub x y : [x -! y] == [x] - [y].
Lemma Smorph_morph :
ring_morph 0 1 radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
End RING.
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.
Instance ARsub_ext : Proper (req ==> req ==> req) rsub.
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)
| reflexivity
| match goal with
| |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y))
end].
Lemma ARadd_0_r x : x + 0 == x.
Lemma ARmul_1_r x : x * 1 == x.
Lemma ARmul_0_r x : x * 0 == 0.
Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y.
Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x.
Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x.
Lemma ARmul_assoc1 x y z : (x * y) * z == (y * z) * x.
Lemma ARmul_assoc2 x y z : (y * x) * z == (y * z) * x.
Lemma ARopp_mul_r 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.
Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req.
Instance ARsub_ext : Proper (req ==> req ==> req) rsub.
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)
| reflexivity
| match goal with
| |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y))
end].
Lemma ARadd_0_r x : x + 0 == x.
Lemma ARmul_1_r x : x * 1 == x.
Lemma ARmul_0_r x : x * 0 == 0.
Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y.
Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x.
Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x.
Lemma ARmul_assoc1 x y z : (x * y) * z == (y * z) * x.
Lemma ARmul_assoc2 x y z : (y * x) * z == (y * z) * x.
Lemma ARopp_mul_r 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_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).
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).