diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/Make | 1 | ||||
| -rw-r--r-- | mathcomp/Make.test-suite | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/all_ssreflect.v | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrAC.v | 241 | ||||
| -rw-r--r-- | mathcomp/test_suite/test_ssrAC.v | 100 |
7 files changed, 350 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e184d44..200b270 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -29,6 +29,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added lemmas `foldr_rcons`, `foldl_rcons`, `scanl_rcons` and `nth_cons_scanl` in `seq` +- ssrAC tactics, see header of `ssreflect/ssrAC.v` for documentation + of `(AC patternshape reordering)`, `(ACl reordering)` `(ACof + reordering reordering)`, `op.[AC patternshape reordering]`, `op.[ACl + reordering]` and `op.[ACof reordering reordering]`. + ### Changed - Reorganized the algebraic hierarchy and the theory of `ssrnum.v`. 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/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..151e8ae --- /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 0, left associativity). +Notation "op .[ 'AC' p s ]" := (opAC op p s) + (at level 2, p at level 0, 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 |