Some proof scripts made better using ssrAC.

math-comp · Mar 25, 2020 · 8714cfd · 8714cfd
1 parent 01253f8
commit 8714cfd
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 27 deletions.
diff --git 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) (3*1*2*4)) (AC (2*2) (3*2*1*4))/= !equivf_l.
+by rewrite (ACl ((2*3)*(1*4))) (ACl ((2*3)*(4*1)))/=.
 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)) (4*2*7*((1*3)*(6*5))))/=.
+by rewrite [X in _ + X](AC (3*(2*2)) (4*6*7*((1*3)*(2*5))))/=.
 Qed.
 
 Lemma nonzero1 : 1%:F != 0%:F :> type.

diff --git 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.
 
 (******************************************************************************)
@@ -4082,7 +4082,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) (1*(2*3)*4))/= -invfM -exprMn.
 by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //.
 Qed.
 
@@ -4331,12 +4331,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) (1*4*(2*3)))/= mulrACA -expr2 sqrCi mulN1r.
+by rewrite -!mulrA [_ * ('i * _)]mulrCA [_ * y1]mulrC.
 Qed.
 
 Lemma normC2_rect :
@@ -4653,7 +4652,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) (1*4*(3*2))] -!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.