Merge pull request #211 from CohenCyril/ssrAC

Rewriting with AC (not modulo AC), using a small scale command.

8 files changed, 362 insertions, 27 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index 0a2c4a4..1d837c1 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -81,6 +81,7 @@ ssreflect/order.v
 ssreflect/path.v
 ssreflect/prime.v
 ssreflect/seq.v
+ssreflect/ssrAC.v
 ssreflect/ssrbool.v
 ssreflect/ssreflect.v
 ssreflect/ssrfun.v
diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
index bca6ed9..99d8289 100644
--- a/mathcomp/Make.test-suite
+++ b/mathcomp/Make.test-suite
@@ -1,4 +1,5 @@
 test_suite/hierarchy_test.v
+test_suite/test_ssrAC.v
 
 -I .
 -R . mathcomp
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.
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 108f545..f8c640d 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -1,6 +1,7 @@
 all_ssreflect.v
 eqtype.v
 seq.v
+ssrAC.v
 ssrbool.v
 ssreflect.v
 ssrfun.v
diff --git a/mathcomp/ssreflect/all_ssreflect.v b/mathcomp/ssreflect/all_ssreflect.v
index 318d5ef..a73f073 100644
--- a/mathcomp/ssreflect/all_ssreflect.v
+++ b/mathcomp/ssreflect/all_ssreflect.v
@@ -17,3 +17,4 @@ Require Export finset.
 Require Export order.
 Require Export binomial.
 Require Export generic_quotient.
+Require Export ssrAC.
diff --git a/mathcomp/ssreflect/ssrAC.v b/mathcomp/ssreflect/ssrAC.v
new file mode 100644
index 0000000..8483f71
--- /dev/null
+++ b/mathcomp/ssreflect/ssrAC.v
@@ -0,0 +1,241 @@
+Require Import BinPos BinNat.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq bigop.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(************************************************************************)
+(* Small Scale Rewriting using Associatity and Commutativity            *)
+(*                                                                      *)
+(* Rewriting with AC (not modulo AC), using a small scale command.      *)
+(* Replaces opA, opC, opAC, opCA, ... and any combinations of them      *)
+(*                                                                      *)
+(* Usage :                                                              *)
+(*   rewrite [pattern](AC patternshape reordering)                      *)
+(*   rewrite [pattern](ACl reordering)                                  *)
+(*   rewrite [pattern](ACof reordering reordering)                      *)
+(*   rewrite [pattern]op.[AC patternshape reordering]                   *)
+(*   rewrite [pattern]op.[ACl reordering]                               *)
+(*   rewrite [pattern]op.[ACof reordering reordering]                   *)
+(*                                                                      *)
+(* - if op is specified, the rule is specialized to op                  *)
+(*   otherwise,          the head symbol is a generic comm_law          *)
+(*                       and the rewrite might be less efficient        *)
+(*   NOTE because of a bug in Coq's notations coq/coq#8190              *)
+(*        op must not contain any hole.                                 *)
+(*        *%R.[AC p s] currently does not work because of that          *)
+(*        (@GRing.mul R).[AC p s] must be used instead                  *)
+(*                                                                      *)
+(* - pattern is optional, as usual, but must be used to select the      *)
+(*   appropriate operator in case of ambiguity such an operator must    *)
+(*   have a canonical Monoid.com_law structure                          *)
+(*   (additions, multiplications, conjuction and disjunction do)        *)
+(*                                                                      *)
+(* - patternshape is expressed using the syntax                         *)
+(*      p := n | p * p'                                                 *)
+(*      where "*" is purely formal                                      *)
+(*        and n > 0 is number of left associated symbols                *)
+(*   examples of pattern shapes:                                        *)
+(*   + 4 represents (n * m * p * q)                                     *)
+(*   + (1*2) represents (n * (m * p))                                   *)
+(*                                                                      *)
+(* - reordering is expressed using the syntax                           *)
+(*     s := n | s * s'                                                  *)
+(*   where "*" is purely formal and n > 0 is the position in the LHS    *)
+(*   positions start at 1 !                                             *)
+(*                                                                      *)
+(* If the ACl variant is used, the patternshape defaults to the         *)
+(* pattern fully associated to the left i.e. n i.e (x * y * ...)        *)
+(*                                                                      *)
+(* Examples of reorderings:                                             *)
+(* - ACl ((1*2)*3) is the identity (and will fail with error message)   *)
+(* - opAC == op.[ACl (1*3)*2] == op.[AC 3 ((1*3)*2)]                    *)
+(* - opCA == op.[AC (2*1) (1*2*3)]                                      *)
+(* - opACA == op.[AC (2*2) ((1*3)*(2*4))]                               *)
+(* - rewrite opAC -opA == rewrite op.[ACl 1*(3*2)]                      *)
+(* ...                                                                  *)
+(************************************************************************)
+
+
+Delimit Scope AC_scope with AC.
+
+Definition change_type ty ty' (x : ty) (strategy : ty = ty') : ty' :=
+ ecast ty ty strategy x.
+Notation simplrefl := (ltac: (simpl; reflexivity)).
+Notation cbvrefl := (ltac: (cbv; reflexivity)).
+Notation vmrefl := (ltac: (vm_compute; reflexivity)).
+
+Module AC.
+
+Canonical positive_eqType := EqType positive
+   (EqMixin (fun _ _ => equivP idP (Pos.eqb_eq _ _))).
+(* Should be replaced by (EqMixin Pos.eqb_spec) for coq >= 8.7 *)
+
+Inductive syntax := Leaf of positive | Op of syntax & syntax.
+Coercion serial := (fix loop (acc : seq positive) (s : syntax) :=
+   match s with
+   | Leaf n => n :: acc
+   | Op s s' => (loop^~ s (loop^~ s' acc))
+   end) [::].
+
+Lemma serial_Op s1 s2 : Op s1 s2 = s1 ++ s2 :> seq _.
+Proof.
+rewrite /serial; set loop := (X in X [::]); rewrite -/loop.
+elim: s1 (loop [::] s2) => [n|s11 IHs1 s12 IHs2] //= l.
+by rewrite IHs1 [in RHS]IHs1 IHs2 catA.
+Qed.
+
+Definition Leaf_of_nat n := Leaf ((pos_of_nat n n) - 1)%positive.
+
+Module Import Syntax.
+Bind Scope AC_scope with syntax.
+Coercion Leaf : positive >-> syntax.
+Coercion Leaf_of_nat : nat >-> syntax.
+Notation "1" := 1%positive : AC_scope.
+Notation "x * y" := (Op x%AC y%AC) : AC_scope.
+End Syntax.
+
+Definition pattern (s : syntax) := ((fix loop n s :=
+  match s with
+  | Leaf 1%positive => (Leaf n, Pos.succ n)
+  | Leaf m => Pos.iter (fun oi => (Op oi.1 (Leaf oi.2), Pos.succ oi.2))
+                       (Leaf n, Pos.succ n) (m - 1)%positive
+  | Op s s' => let: (p, n') := loop n s in
+               let: (p', n'') := loop n' s' in
+               (Op p p', n'')
+  end) 1%positive s).1.
+
+Section eval.
+Variables (T : Type) (idx : T) (op : T -> T -> T).
+Inductive env := Empty | ENode of T & env & env.
+Definition pos := fix loop (e : env) p {struct e} :=
+  match e, p with
+ | ENode t _ _, 1%positive => t
+ | ENode t e _, (p~0)%positive => loop e p
+ | ENode t _ e, (p~1)%positive => loop e p
+ | _, _ => idx
+end.
+
+Definition set_pos (f : T -> T) := fix loop e p {struct p} :=
+  match e, p with
+ | ENode t e e', 1%positive => ENode (f t) e e'
+ | ENode t e e', (p~0)%positive => ENode t (loop e p) e'
+ | ENode t e e', (p~1)%positive => ENode t e (loop e' p)
+ | Empty, 1%positive => ENode (f idx) Empty Empty
+ | Empty, (p~0)%positive => ENode idx (loop Empty p) Empty
+ | Empty, (p~1)%positive => ENode idx Empty (loop Empty p)
+ end.
+
+Lemma pos_set_pos (f : T -> T) e (p p' : positive) :
+  pos (set_pos f e p) p' = if p == p' then f (pos e p) else pos e p'.
+Proof. by elim: p e p' => [p IHp|p IHp|] [|???] [?|?|]//=; rewrite IHp. Qed.
+
+Fixpoint unzip z (e : env) : env := match z with
+ | [::] => e
+ | (x, inl e') :: z' => unzip z' (ENode x e' e)
+ | (x, inr e') :: z' => unzip z' (ENode x e e')
+end.
+
+Definition set_pos_trec (f : T -> T) := fix loop z e p {struct p} :=
+  match e, p with
+ | ENode t e e', 1%positive => unzip z (ENode (f t) e e')
+ | ENode t e e', (p~0)%positive => loop ((t, inr e') :: z) e p
+ | ENode t e e', (p~1)%positive => loop ((t, inl e) :: z) e' p
+ | Empty, 1%positive => unzip z (ENode (f idx) Empty Empty)
+ | Empty, (p~0)%positive => loop ((idx, (inr Empty)) :: z) Empty p
+ | Empty, (p~1)%positive => loop ((idx, (inl Empty)) :: z) Empty p
+ end.
+
+Lemma set_pos_trecE f z e p : set_pos_trec f z e p = unzip z (set_pos f e p).
+Proof. by elim: p e z => [p IHp|p IHp|] [|???] [|[??]?] //=; rewrite ?IHp. Qed.
+
+Definition eval (e : env) := fix loop (s : syntax) :=
+match s with
+  | Leaf n => pos e n
+  | Op s s' => op (loop s) (loop s')
+end.
+End eval.
+Arguments Empty {T}.
+
+Definition content := (fix loop (acc : env N) s :=
+  match s with
+  | Leaf n => set_pos_trec 0%num N.succ [::] acc n
+  | Op s s' => loop (loop acc s') s
+  end) Empty.
+
+Lemma count_memE x (t : syntax) : count_mem x t = pos 0%num (content t) x.
+Proof.
+rewrite /content; set loop := (X in X Empty); rewrite -/loop.
+rewrite -[LHS]addn0; have <- : pos 0%num Empty x = 0 :> nat by elim: x.
+elim: t Empty => [n|s IHs s' IHs'] e //=; last first.
+  by rewrite serial_Op count_cat -addnA IHs' IHs.
+rewrite ?addn0 set_pos_trecE pos_set_pos; case: (altP eqP) => [->|] //=.
+by rewrite -N.add_1_l nat_of_add_bin //=.
+Qed.
+
+Definition cforall N T : env N -> (env T -> Type) -> Type := env_rect (@^~ Empty)
+  (fun _ e IHe e' IHe' R => forall x, IHe (fun xe => IHe' (R \o ENode x xe))).
+
+Lemma cforallP N T R : (forall e : env T, R e) -> forall (e : env N), cforall e R.
+Proof.
+move=> Re e; elim: e R Re => [|? e /= IHe e' IHe' ?? x] //=.
+by apply: IHe => ?; apply: IHe' => /=.
+Qed.
+
+Section eq_eval.
+Variables (T : Type) (idx : T) (op : Monoid.com_law idx).
+
+Lemma proof (p s : syntax) : content p = content s ->
+  forall env, eval idx op env p = eval idx op env s.
+Proof.
+suff evalE env t : eval idx op env t = \big[op/idx]_(i <- t) (pos idx env i).
+  move=> cps e; rewrite !evalE; apply: perm_big.
+  by apply/allP => x _ /=; rewrite !count_memE cps.
+elim: t => //= [n|t -> t' ->]; last by rewrite serial_Op big_cat.
+by rewrite big_cons big_nil Monoid.mulm1.
+Qed.
+
+Definition direct p s ps := cforallP (@proof p s ps) (content p).
+
+End eq_eval.
+
+Module Exports.
+Export AC.Syntax.
+End Exports.
+End AC.
+Export AC.Exports.
+
+Notation AC_check_pattern :=
+  (ltac: (match goal with
+    |- AC.content ?pat = AC.content ?ord =>
+      let pat' := fresh "pat" in let pat' := eval compute in pat in
+      tryif unify pat' ord then
+           fail 1 "AC: equality between" pat
+                  "and" ord "is trivial, cannot progress"
+      else tryif vm_compute; reflexivity then idtac
+      else fail 2 "AC: mismatch between shape" pat "=" pat' "and reordering" ord
+    | |- ?G => fail 3 "AC: no pattern to check" G
+  end)).
+
+Notation opACof law p s :=
+((fun T idx op assoc lid rid comm => (change_type (@AC.direct T idx
+   (@Monoid.ComLaw _ _ (@Monoid.Law _ idx op assoc lid rid) comm)
+   p%AC s%AC AC_check_pattern) cbvrefl)) _ _ law
+(Monoid.mulmA _) (Monoid.mul1m _) (Monoid.mulm1 _) (Monoid.mulmC _)).
+
+Notation opAC op  p s := (opACof op (AC.pattern p%AC) s%AC).
+Notation opACl op s := (opAC op (AC.Leaf_of_nat (size (AC.serial s%AC))) s%AC).
+
+Notation "op .[ 'ACof' p s ]" := (opACof op p s)
+  (at level 2, p at level 1, left associativity).
+Notation "op .[ 'AC' p s ]" := (opAC op p s)
+  (at level 2, p at level 1, left associativity).
+Notation "op .[ 'ACl' s ]" := (opACl op s)
+  (at level 2, left associativity).
+
+Notation AC_strategy :=
+  (ltac: (cbv -[Monoid.com_operator Monoid.operator]; reflexivity)).
+Notation ACof p s := (change_type
+  (@AC.direct _ _ _  p%AC s%AC AC_check_pattern) AC_strategy).
+Notation AC p s := (ACof (AC.pattern p%AC) s%AC).
+Notation ACl s := (AC (AC.Leaf_of_nat (size (AC.serial s%AC))) s%AC).
diff --git a/mathcomp/test_suite/test_ssrAC.v b/mathcomp/test_suite/test_ssrAC.v
new file mode 100644
index 0000000..92dd101
--- /dev/null
+++ b/mathcomp/test_suite/test_ssrAC.v
@@ -0,0 +1,100 @@
+From mathcomp Require Import all_ssreflect ssralg.
+
+Section Tests.
+Lemma test_orb (a b c d : bool) : (a || b) || (c || d) = (a || c) || (b || d).
+Proof. time by rewrite orbACA. Restart.
+Proof. time by rewrite (AC (2*2) ((1*3)*(2*4))). Restart.
+Proof. time by rewrite orb.[AC (2*2) ((1*3)*(2*4))]. Qed.
+
+Lemma test_addn (a b c d : nat) : a + b + c + d = a + c + b + d.
+Proof. time by rewrite -addnA addnAC addnA addnAC. Restart.
+Proof. time by rewrite (ACl (1*3*2*4)). Restart.
+Proof. time by rewrite addn.[ACl 1*3*2*4]. Qed.
+
+Lemma test_addr (R : comRingType) (a b c d : R) : (a + b + c + d = a + c + b + d)%R.
+Proof. time by rewrite -GRing.addrA GRing.addrAC GRing.addrA GRing.addrAC. Restart.
+Proof. time by rewrite (ACl (1*3*2*4)). Restart.
+Proof. time by rewrite (@GRing.add R).[ACl 1*3*2*4]. Qed.
+
+Local Open Scope ring_scope.
+Import GRing.Theory.
+
+Lemma test_mulr (R : comRingType) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : R)
+    (x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 : R) :
+    (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) =
+    (x0 * x2 * x4 * x9) * (x1 * x3 * x5 * x7) * x6 * x8 *
+    (x10 * x12 * x14 * x19) * (x11 * x13 * x15 * x17) * x16 * x18 * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9)*
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) * (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19)
+   *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *(x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) *
+    (x10 * x11) * (x12 * x13) * (x14 * x15) * (x16 * x17 * x18 * x19) *
+ (x0 * x1) * (x2 * x3) * (x4 * x5) * (x6 * x7 * x8 * x9) .
+Proof.
+pose s := ((2 * 4 * 9 * 1 * 3 * 5 * 7 * 6 * 8 * 20 * 21 * 22 * 23) * 25 * 26 * 27 * 28
+             * (29 * 30 * 31) * 32 * 33 * 34 * 35 * 36 * 37 *  38 * 39 * 40 * 41
+             * (10 * 12 * 14 * 19 * 11 * 13 * 15 * 17 * 16 * 18 * 24)
+                  * (42 * 43 * 44 * 45 * 46 * 47 *  48 * 49) * 50
+                  * 52 * 53 * 54 * 55 * 56 * 57 *  58 * 59 * 51* 60
+                  * 62 * 63 * 64 * 65 * 66 * 67 *  68 * 69 * 61* 70
+                  * 72 * 73 * 74 * 75 * 76 * 77 *  78 * 79 * 71 * 80
+                  * 82 * 83 * 84 * 85 * 86 * 87 *  88 * 89 * 81* 90
+                  * 92 * 93 * 94 * 95 * 96 * 97 *  98 * 99 * 91 * 100 *
+((102 * 104 * 109 * 101 * 103 * 105 * 107 * 106 * 108 * 120 * 121 * 122 * 123) * 125 * 126 * 127 * 128
+             * (129 * 130 * 131) * 132 * 133 * 134 * 135 * 136 * 137 *  138 * 139 * 140 * 141
+             * (110 * 112 * 114 * 119 * 111 * 113 * 115 * 117 * 116 * 118 * 124)
+                  * (142 * 143 * 144 * 145 * 146 * 147 *  148 * 149) * 150
+                  * 152 * 153 * 154 * 155 * 156 * 157 *  158 * 159 * 151* 160
+                  * 162 * 163 * 164 * 165 * 166 * 167 *  168 * 169 * 161* 170
+                  * 172 * 173 * 174 * 175 * 176 * 177 *  178 * 179 * 171 * 180
+                  * 182 * 183 * 184 * 185 * 186 * 187 *  188 * 189 * 181* 190
+                  * 192 * 193 * 194 * 195 * 196 * 197 *  198 * 199 * 191)
+
+)%AC.
+time have := (@GRing.mul R).[ACl s].
+time rewrite (@GRing.mul R).[ACl s].
+Abort.
+End Tests.
\ No newline at end of file