diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/fraction.v | 29 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 15 |
2 files changed, 17 insertions, 27 deletions
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index b9aa3ca..41c6117 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq. -From mathcomp Require Import choice tuple bigop ssralg poly polydiv. +From mathcomp Require Import ssrAC choice tuple bigop ssralg poly polydiv. From mathcomp Require Import generic_quotient. (* This file builds the field of fraction of any integral domain. *) @@ -157,13 +157,10 @@ Definition add := lift_op2 {fraction R} addf. Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}. Proof. -move=> x y; unlock add; apply/eqmodP; rewrite /= equivfE. -rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP //. -rewrite mulrDr mulrDl eq_sym; apply/eqP. -rewrite !mulrA ![_ * \n__]mulrC !mulrA equivf_l. -congr (_ + _); first by rewrite -mulrA mulrCA !mulrA. -rewrite -!mulrA [X in _ * X]mulrCA !mulrA equivf_l. -by rewrite mulrC !mulrA -mulrA mulrC mulrA. +move=> x y; unlock add; apply/eqmodP; rewrite /= equivfE /addf /=. +rewrite !numden_Ratio ?mulf_neq0 ?domP // mulrDr mulrDl; apply/eqP. +symmetry; rewrite (AC (2*2)%AC (3*1*2*4)%AC) (AC (2*2)%AC (3*2*1*4)%AC)/=. +by rewrite !equivf_l (ACl ((2*3)*(1*4))%AC) (ACl ((2*3)*(4*1))%AC)/=. Qed. Canonical pi_add_morph := PiMorph2 pi_add. @@ -183,8 +180,7 @@ Lemma pi_mul : {morph \pi : x y / mulf x y >-> mul x y}. Proof. move=> x y; unlock mul; apply/eqmodP=> /=. rewrite equivfE /= /addf /= !numden_Ratio ?mulf_neq0 ?domP //. -rewrite mulrAC !mulrA -mulrA equivf_r -equivf_l. -by rewrite mulrA ![_ * \d_y]mulrC !mulrA. +by rewrite mulrACA !equivf_r mulrACA. Qed. Canonical pi_mul_morph := PiMorph2 pi_mul. @@ -204,8 +200,8 @@ Canonical pi_inv_morph := PiMorph1 pi_inv. Lemma addA : associative add. Proof. elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE. -rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP // !mulrDl !mulrA !addrA. -by congr (\pi (Ratio (_ + _ + _) _)); rewrite mulrAC. +rewrite /addf /= !numden_Ratio ?mulf_neq0 ?domP // !mulrDl. +by rewrite !mulrA !addrA ![_ * _ * \d_x]mulrAC. Qed. Lemma addC : commutative add. @@ -252,13 +248,8 @@ Lemma mul_addl : left_distributive mul add. Proof. elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. rewrite !piE /equivf /mulf /addf !numden_Ratio ?mulf_neq0 ?domP //; apply/eqP. -rewrite !(mulrDr, mulrDl) !mulrA; congr (_ * _ + _ * _). - rewrite ![_ * \n_z]mulrC -!mulrA; congr (_ * _). - rewrite ![\d_y * _]mulrC !mulrA; congr (_ * _ * _). - by rewrite [X in _ = X]mulrC mulrA. -rewrite ![_ * \n_z]mulrC -!mulrA; congr (_ * _). -rewrite ![\d_x * _]mulrC !mulrA; congr (_ * _ * _). -by rewrite -mulrA mulrC [X in X * _] mulrC. +rewrite !(mulrDr, mulrDl) (AC (3*(2*2))%AC (4*2*7*((1*3)*(6*5)))%AC)/=. +by rewrite [X in _ + X](AC (3*(2*2))%AC (4*6*7*((1*3)*(2*5)))%AC)/=. Qed. Lemma nonzero1 : 1%:F != 0%:F :> type. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 21578bc..e1e5992 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. -From mathcomp Require Import div fintype path bigop order finset fingroup. +From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup. From mathcomp Require Import ssralg poly. (******************************************************************************) @@ -4078,7 +4078,7 @@ have JE x : x^* = `|x|^+2 / x. by apply: (canRL (mulfK _)) => //; rewrite mulrC -normCK. move=> x; have [->|x_neq0] := eqVneq x 0; first by rewrite !rmorph0. rewrite !JE normrM normfV exprMn normrX normr_id. -rewrite invfM exprVn mulrA -[X in X * _]mulrA -invfM -exprMn. +rewrite invfM exprVn (AC (2*2)%AC (1*(2*3)*4)%AC)/= -invfM -exprMn. by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //. Qed. @@ -4327,12 +4327,11 @@ Lemma subC_rect x1 y1 x2 y2 : (x1 + 'i * y1) - (x2 + 'i * y2) = x1 - x2 + 'i * (y1 - y2). Proof. by rewrite oppC_rect addC_rect. Qed. -Lemma mulC_rect x1 y1 x2 y2 : - (x1 + 'i * y1) * (x2 + 'i * y2) - = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1). +Lemma mulC_rect x1 y1 x2 y2 : (x1 + 'i * y1) * (x2 + 'i * y2) = + x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1). Proof. -rewrite mulrDl !mulrDr mulrCA -!addrA mulrAC -mulrA; congr (_ + _). -by rewrite mulrACA -expr2 sqrCi mulN1r addrA addrC. +rewrite mulrDl !mulrDr (AC (2*2)%AC (1*4*(2*3))%AC)/= mulrACA. +by rewrite -expr2 sqrCi mulN1r -!mulrA [_ * ('i * _)]mulrCA [_ * y1]mulrC. Qed. Lemma normC2_rect : @@ -4649,7 +4648,7 @@ have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*. have def_xy: x * y^* = y * x^*. apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2). rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn. - by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr. + by rewrite mulrN (@GRing.mul C).[AC (2*2)%AC (1*4*(3*2))%AC] -!normCK mulNrn addNr. have{def_xy def2xy} def_yx: `|y * x| = y * x^*. by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy. rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM. |