diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 293 |
1 files changed, 130 insertions, 163 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index ab992552..42ce4edc 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Setoid. -Require Import BinPos. -Require Import BinNat. +Require Import Setoid Morphisms BinPos BinNat. Set Implicit Arguments. @@ -35,48 +33,42 @@ Section Power. 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). + Variable Rsth : Equivalence req. + Infix "*" := rmul. + Infix "==" := req. - 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_ext : Proper (req ==> req ==> req) rmul. 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. exact mul_ext. Qed. - - Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + Fixpoint pow_pos (x:R) (i:positive) : 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) + | 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_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j. Proof. - induction j;simpl. - rewrite IHj. - rewrite (mul_comm x (pow_pos x j *pow_pos x j)). - setoid_rewrite (mul_comm x (pow_pos x j)) at 2. - repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - apply (Seq_refl _ _ Rsth). + induction j; simpl; rewrite <- ?mul_assoc. + - f_equiv. now do 2 (rewrite IHj, mul_assoc). + - now do 2 (rewrite IHj, mul_assoc). + - reflexivity. Qed. - Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Lemma pow_pos_succ x j : + pow_pos x (Pos.succ j) == x * pow_pos x j. Proof. - intro x;induction i;intros. - rewrite xI_succ_xO;rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. - simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc; - simpl. apply (Seq_refl _ _ Rsth). + induction j; simpl; try reflexivity. + rewrite IHj, <- mul_assoc; f_equiv. + now rewrite mul_assoc, pow_pos_swap, mul_assoc. + Qed. + + Lemma pow_pos_add x i j : + pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Proof. + induction i using Pos.peano_ind. + - now rewrite Pos.add_1_l, pow_pos_succ. + - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc. Qed. Definition pow_N (x:R) (p:N) := @@ -87,9 +79,9 @@ Section Power. 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. + Lemma pow_N_pow_N x n : pow_N x (id_phi_N n) == pow_N x n. Proof. - intros; apply (Seq_refl _ _ Rsth). + reflexivity. Qed. End Power. @@ -98,19 +90,18 @@ 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). + 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_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_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 }. @@ -119,11 +110,11 @@ Section DEFINITIONS. (*Almost ring are no ring : Ropp_def is missing **) 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_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_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; @@ -134,10 +125,10 @@ Section DEFINITIONS. (** 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_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_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; @@ -148,19 +139,15 @@ Section DEFINITIONS. Record sring_eq_ext : Prop := mk_seqe { (* SRing operators are compatible with equality *) - SRadd_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; - SRmul_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2 + SRadd_ext : Proper (req ==> req ==> req) radd; + SRmul_ext : Proper (req ==> req ==> req) rmul }. Record ring_eq_ext : Prop := mk_reqe { (* Ring operators are compatible with equality *) - Radd_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; - Rmul_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2; - Ropp_ext : forall x1 x2, x1 == x2 -> -x1 == -x2 + Radd_ext : Proper (req ==> req ==> req) radd; + Rmul_ext : Proper (req ==> req ==> req) rmul; + Ropp_ext : Proper (req ==> req) ropp }. (** Interpretation morphisms definition*) @@ -170,9 +157,9 @@ Section DEFINITIONS. Variable ceqb : C->C->bool. (* [phi] est un morphisme de [C] dans [R] *) 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). + Infix "+!" := cadd. Infix "-!" := csub. + Infix "*!" := cmul. Notation "-! x" := (copp x). + Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (*for semi rings*) Record semi_morph : Prop := mkRmorph { @@ -216,15 +203,13 @@ Section DEFINITIONS. End MORPHISM. (** Identity is a morphism *) - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid1. + 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. Proof. - apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi);intros;unfold IDphi; - try apply (Seq_refl _ _ Rsth);auto. + now apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi). Qed. (** Specification of the power function *) @@ -239,35 +224,31 @@ Section DEFINITIONS. End POWER. - Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + 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. - 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). + Notation "0" := rO. Notation "1" := rI. + Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. + Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) - Lemma Eqsth : Setoid_Theory R (@eq R). - Proof. constructor;red;intros;subst;trivial. Qed. + Lemma Eqsth : Equivalence (@eq R). + Proof. exact eq_equivalence. Qed. Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;solve_proper. Qed. Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;solve_proper. Qed. - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid2. - Ltac sreflexivity := apply (Seq_refl _ _ Rsth). + Variable Rsth : Equivalence req. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. @@ -282,23 +263,24 @@ Section ALMOST_RING. Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). Lemma SRopp_ext : forall x y, x == y -> -x == -y. - Proof. intros x y H;exact H. Qed. + Proof. intros x y H; exact H. Qed. Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req. Proof. - constructor. exact (SRadd_ext SReqe). exact (SRmul_ext SReqe). - exact SRopp_ext. + constructor. + - exact (SRadd_ext SReqe). + - exact (SRmul_ext SReqe). + - exact SRopp_ext. Qed. Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y. - Proof. intros;sreflexivity. Qed. + Proof. reflexivity. Qed. Lemma SRopp_add : forall x y, -(x + y) == -x + -y. - Proof. intros;sreflexivity. Qed. - + Proof. reflexivity. Qed. Lemma SRsub_def : forall x y, x - y == x + -y. - Proof. intros;sreflexivity. Qed. + Proof. reflexivity. Qed. Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. Proof (mk_art 0 1 radd rmul SRsub SRopp req @@ -315,7 +297,7 @@ Section ALMOST_RING. Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req 0 1 radd rmul SRsub SRopp reqb (@IDphi R). Proof. - apply mkmorph;intros;try sreflexivity. unfold IDphi;auto. + now apply mkmorph. Qed. (* a semi_morph can be extended to a ring_morph for the almost_ring derived @@ -331,9 +313,7 @@ Section ALMOST_RING. ring_morph rO rI radd rmul SRsub SRopp req cO cI cadd cmul cadd (fun x => x) ceqb phi. Proof. - case Smorph; intros; constructor; auto. - unfold SRopp in |- *; intros. - setoid_reflexivity. + case Smorph; now constructor. Qed. End SEMI_RING. @@ -347,31 +327,28 @@ Section ALMOST_RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. (** Rings are almost rings*) - Lemma Rmul_0_l : forall x, 0 * x == 0. + Lemma Rmul_0_l x : 0 * x == 0. Proof. - intro x; setoid_replace (0*x) with ((0+1)*x + -x). - rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth). - rewrite (Ropp_def Rth);sreflexivity. + setoid_replace (0*x) with ((0+1)*x + -x). + now rewrite (Radd_0_l Rth), (Rmul_1_l Rth), (Ropp_def Rth). - rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). - rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity. + rewrite (Rdistr_l Rth), (Rmul_1_l Rth). + rewrite <- (Radd_assoc Rth), (Ropp_def Rth). + now rewrite (Radd_comm Rth), (Radd_0_l Rth). Qed. - Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. + Lemma Ropp_mul_l x y : -(x * y) == -x * y. Proof. - intros x y;rewrite <-(Radd_0_l Rth (- x * y)). - rewrite (Radd_comm Rth). - rewrite <-(Ropp_def Rth (x*y)). - rewrite (Radd_assoc Rth). - rewrite <- (Rdistr_l Rth). - rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). - rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. + rewrite <-(Radd_0_l Rth (- x * y)). + rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)). + rewrite (Radd_assoc Rth), <- (Rdistr_l Rth). + rewrite (Rth.(Radd_comm) (-x)), (Ropp_def Rth). + now rewrite Rmul_0_l, (Radd_0_l Rth). Qed. - Lemma Ropp_add : forall x y, -(x + y) == -x + -y. + Lemma Ropp_add x y : -(x + y) == -x + -y. Proof. - intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))). + rewrite <- ((Radd_0_l Rth) (-(x+y))). rewrite <- ((Ropp_def Rth) x). rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). rewrite <- ((Ropp_def Rth) y). @@ -383,17 +360,17 @@ Section ALMOST_RING. rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth). - rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). - apply (Radd_comm Rth). + rewrite ((Radd_comm Rth) y), (Ropp_def Rth). + rewrite ((Radd_comm Rth) (-x) 0), (Radd_0_l Rth). + now apply (Radd_comm Rth). Qed. - Lemma Ropp_opp : forall x, - -x == x. + Lemma Ropp_opp x : - -x == x. Proof. - intros x; rewrite <- (Radd_0_l Rth (- -x)). + rewrite <- (Radd_0_l Rth (- -x)). rewrite <- (Ropp_def Rth x). - rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth). + rewrite <- (Radd_assoc Rth), (Ropp_def Rth). + rewrite ((Radd_comm Rth) x); now apply (Radd_0_l Rth). Qed. Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. @@ -407,10 +384,10 @@ Section ALMOST_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. - Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y). - Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). - Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). - Variable Csth : Setoid_Theory C ceq. + 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 Setoid C ceq Csth as C_setoid. Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. @@ -420,9 +397,9 @@ Section ALMOST_RING. 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 : phi_ext1. exact phi_ext. Qed. - Lemma Smorph_opp : forall x, [-!x] == -[x]. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. - intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). + rewrite <- (Rth.(Radd_0_l) [-!x]). rewrite <- ((Ropp_def Rth) [x]). rewrite ((Radd_comm Rth) [x]). rewrite <- (Radd_assoc Rth). @@ -430,17 +407,18 @@ Section ALMOST_RING. rewrite (Ropp_def Cth). rewrite (Smorph0 Smorph). rewrite (Radd_comm Rth (-[x])). - apply (Radd_0_l Rth);sreflexivity. + now apply (Radd_0_l Rth). Qed. - Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y]. + Lemma Smorph_sub x y : [x -! y] == [x] - [y]. Proof. - intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth). - rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity. + rewrite (Rsub_def Cth), (Rsub_def Rth). + now rewrite (Smorph_add Smorph), Smorph_opp. Qed. - Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req - cO cI cadd cmul csub copp ceqb phi. + Lemma Smorph_morph : + ring_morph 0 1 radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. Proof (mkmorph 0 1 radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi (Smorph0 Smorph) (Smorph1 Smorph) @@ -458,17 +436,11 @@ elim ARth; intros. constructor; trivial. Qed. - Lemma ARsub_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Instance ARsub_ext : Proper (req ==> req ==> req) rsub. Proof. - intros. - setoid_replace (x1 - y1) with (x1 + -y1). - setoid_replace (x2 - y2) with (x2 + -y2). - rewrite H;rewrite H0;sreflexivity. - apply (ARsub_def ARth). - apply (ARsub_def ARth). + intros x1 x2 Ex y1 y2 Ey. + now rewrite !(ARsub_def ARth), Ex, Ey. Qed. - Add Morphism rsub : rsub_ext. exact ARsub_ext. Qed. Ltac mrewrite := repeat first @@ -479,64 +451,56 @@ Qed. | rewrite (ARmul_0_l ARth) | rewrite <- ((ARmul_comm ARth) 0) | rewrite (ARdistr_l ARth) - | sreflexivity + | reflexivity | match goal with | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y)) end]. - Lemma ARadd_0_r : forall x, (x + 0) == x. - Proof. intros; mrewrite. Qed. + Lemma ARadd_0_r x : x + 0 == x. + Proof. mrewrite. Qed. - Lemma ARmul_1_r : forall x, x * 1 == x. - Proof. intros;mrewrite. Qed. + Lemma ARmul_1_r x : x * 1 == x. + Proof. mrewrite. Qed. - Lemma ARmul_0_r : forall x, x * 0 == 0. - Proof. intros;mrewrite. Qed. + Lemma ARmul_0_r x : x * 0 == 0. + Proof. mrewrite. Qed. - Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. + Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y. Proof. - intros;mrewrite. - repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. + mrewrite. now rewrite !(ARth.(ARmul_comm) z). Qed. - Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x. Proof. - intros;rewrite <-(ARth.(ARadd_assoc) x). - rewrite (ARth.(ARadd_comm) x);sreflexivity. + now rewrite <-(ARth.(ARadd_assoc) x), (ARth.(ARadd_comm) x). Qed. - Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x. Proof. - intros; repeat rewrite <- (ARadd_assoc ARth); - rewrite ((ARadd_comm ARth) x); sreflexivity. + now rewrite <- !(ARadd_assoc ARth), ((ARadd_comm ARth) x). Qed. - Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. + Lemma ARmul_assoc1 x y z : (x * y) * z == (y * z) * x. Proof. - intros;rewrite <-((ARmul_assoc ARth) x). - rewrite ((ARmul_comm ARth) x);sreflexivity. + now rewrite <- ((ARmul_assoc ARth) x), ((ARmul_comm ARth) x). Qed. - Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. + Lemma ARmul_assoc2 x y z : (y * x) * z == (y * z) * x. Proof. - intros; repeat rewrite <- (ARmul_assoc ARth); - rewrite ((ARmul_comm ARth) x); sreflexivity. + now rewrite <- !(ARmul_assoc ARth), ((ARmul_comm ARth) x). Qed. - Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. + Lemma ARopp_mul_r x y : - (x * y) == x * -y. Proof. - intros;rewrite ((ARmul_comm ARth) x y); - rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth). + rewrite ((ARmul_comm ARth) x y), (ARopp_mul_l ARth). + now apply (ARmul_comm ARth). Qed. Lemma ARopp_zero : -0 == 0. Proof. - rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth). - repeat rewrite ARmul_0_r; sreflexivity. + now rewrite <- (ARmul_0_r 0), (ARopp_mul_l ARth), !ARmul_0_r. Qed. - - End ALMOST_RING. @@ -611,6 +575,8 @@ Ltac gen_add_push add Rsth Reqe ARth x := 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 := @@ -619,5 +585,6 @@ Ltac gen_mul_push mul Rsth Reqe ARth x := 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). - |