diff options
Diffstat (limited to 'mathcomp')
27 files changed, 417 insertions, 82 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/matrix.v b/mathcomp/algebra/matrix.v index 0725885..f49473f 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -100,7 +100,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* \adj A == the adjugate matrix of A (\adj A i j = cofactor j i A). *) (* A \in unitmx == A is invertible (R must be a comUnitRingType). *) (* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *) -(* The following operations provide a correspondance between linear functions *) +(* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) (* a (linear) function f : 'rV_m -> 'rV_n on ROW VECTORS *) @@ -129,7 +129,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* - The Cramer rule : mul_mx_adj & mul_adj_mx. *) (* Finally, as an example of the use of block products, we program and prove *) (* the correctness of a classical linear algebra algorithm: *) -(* cormenLUP A == the triangular decomposition (L, U, P) of a nontrivial *) +(* cormen_lup A == the triangular decomposition (L, U, P) of a nontrivial *) (* square matrix A into a lower triagular matrix L with 1s *) (* on the main diagonal, an upper matrix U, and a *) (* permutation matrix P, such that P * A = L * U. *) @@ -1837,7 +1837,7 @@ Lemma mulmx_block m1 m2 n1 n2 p1 p2 (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2)) (Adl *m Bul + Adr *m Bdl) (Adl *m Bur + Adr *m Bdr). Proof. by rewrite mul_col_mx !mul_row_block. Qed. -(* Correspondance between matrices and linear function on row vectors. *) +(* Correspondence between matrices and linear function on row vectors. *) Section LinRowVector. Variables m n : nat. @@ -1856,7 +1856,7 @@ Qed. End LinRowVector. -(* Correspondance between matrices and linear function on matrices. *) +(* Correspondence between matrices and linear function on matrices. *) Section LinMatrix. Variables m1 n1 m2 n2 : nat. @@ -1959,7 +1959,7 @@ by congr (_ + _); apply: eq_bigr => i _; rewrite (block_mxEul, block_mxEdr). Qed. (* The matrix ring structure requires a strutural condition (dimension of the *) -(* form n.+1) to statisfy the nontriviality condition we have imposed. *) +(* form n.+1) to satisfy the nontriviality condition we have imposed. *) Section MatrixRing. Variable n' : nat. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e25d7c0..d21e690 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -10,7 +10,7 @@ From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple. (* *) (* {poly R} == the type of polynomials with coefficients of type R, *) (* represented as lists with a non zero last element *) -(* (big endian representation); the coeficient type R *) +(* (big endian representation); the coefficient type R *) (* must have a canonical ringType structure cR. In fact *) (* {poly R} denotes the concrete type polynomial cR; R *) (* is just a phantom argument that lets type inference *) 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/character/integral_char.v b/mathcomp/character/integral_char.v index 7e470b2..2b886a6 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -83,7 +83,7 @@ Qed. Section GenericClassSums. (* This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with *) -(* the combinatorial definition of the coeficients exposed. *) +(* the combinatorial definition of the coefficients exposed. *) (* This part could move to mxrepresentation.*) Variable (gT : finGroupType) (G : {group gT}) (F : fieldType). diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 1c3fe0b..92470d9 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -11,7 +11,7 @@ From mathcomp Require Import mxalgebra mxrepresentation. (******************************************************************************) (* This file completes the theory developed in mxrepresentation.v with the *) (* construction and properties of linear representations over finite fields, *) -(* and in particular the correspondance between internal action on a (normal) *) +(* and in particular the correspondence between internal action on a (normal) *) (* elementary abelian p-subgroup and a linear representation on an Fp-module. *) (* We provide the following next constructions for a finite field F: *) (* 'Zm%act == the action of {unit F} on 'M[F]_(m, n). *) diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index c87b55c..997255b 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -17,7 +17,7 @@ From mathcomp Require Import cyclotomic. (* x \in Cint_span X <=> x is a Z-linear combination of elements of *) (* X : seq algC. *) (* x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) *) -(* polynomial of x over Q has integer coeficients. *) +(* polynomial of x over Q has integer coefficients. *) (* (e %| a)%A <=> e divides a with respect to algebraic integers, *) (* (e %| a)%Ax i.e., a is in the algebraic integer ideal generated *) (* by e. This is is notation for a \in dvdA e, where *) 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/bigop.v b/mathcomp/ssreflect/bigop.v index 633bb36..601dfb3 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -5,12 +5,12 @@ From mathcomp Require Import div fintype tuple finfun. (******************************************************************************) (* This file provides a generic definition for iterating an operator over a *) -(* set of indices (bigop); this big operator is parametrized by the return *) +(* set of indices (bigop); this big operator is parameterized by the return *) (* type (R), the type of indices (I), the operator (op), the default value on *) (* empty lists (idx), the range of indices (r), the filter applied on this *) (* range (P) and the expression we are iterating (F). The definition is not *) (* to be used directly, but via the wide range of notations provided and *) -(* and which support a natural use of big operators. *) +(* which support a natural use of big operators. *) (* To improve performance of the Coq typechecker on large expressions, the *) (* bigop constant is OPAQUE. It can however be unlocked to reveal the *) (* transparent constant reducebig, to let Coq expand summation on an explicit *) @@ -27,7 +27,7 @@ From mathcomp Require Import div fintype tuple finfun. (* 2. Results depending on the properties of the operator: *) (* We distinguish: monoid laws (op is associative, idx is an identity *) (* element), abelian monoid laws (op is also commutative), and laws with *) -(* a distributive operation (semi-rings). Examples of such results are *) +(* a distributive operation (semirings). Examples of such results are *) (* splitting, permuting, and exchanging bigops. *) (* A special section is dedicated to big operators on natural numbers. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 3a484a1..aef8e27 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -5,10 +5,10 @@ From mathcomp Require Import div fintype tuple finfun bigop prime finset. (******************************************************************************) (* This files contains the definition of: *) -(* 'C(n, m) == the binomial coeficient n choose m. *) +(* 'C(n, m) == the binomial coefficient n choose m. *) (* n ^_ m == the falling (or lower) factorial of n with m terms, i.e., *) (* the product n * (n - 1) * ... * (n - m + 1). *) -(* Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m/!. *) +(* Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m`!. *) (* *) (* In additions to the properties of these functions, we prove a few seminal *) (* results such as triangular_sum, Wilson and Pascal; their proofs are good *) diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index f5d95e8..12b0601 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -38,7 +38,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* x != y :> T <=> x and y compare unequal at type T. *) (* x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces *) (* to x == y -> x = y. *) -(* eq_op == the boolean relation behing the == notation. *) +(* eq_op == the boolean relation behind the == notation. *) (* pred1 a == the singleton predicate [pred x | x == a]. *) (* pred2, pred3, pred4 == pair, triple, quad predicates. *) (* predC1 a == [pred x | x != a]. *) @@ -47,7 +47,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* predU1 a P, predD1 P a == applicative versions of the above. *) (* frel f == the relation associated with f : T -> T. *) (* := [rel x y | f x == y]. *) -(* invariant k f == elements of T whose k-class is f-invariant. *) +(* invariant f k == elements of T whose k-class is f-invariant. *) (* := [pred x | k (f x) == k x] with f : T -> T. *) (* [fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n] *) (* [eta f with a1 |-> e1, .., a_n |-> e_n] == *) @@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* insub x = Some u with val u = x if P x, *) (* None if ~~ P x *) (* The insubP lemma encapsulates this dichotomy. *) -(* P should be infered from the expected return type. *) +(* P should be inferred from the expected return type. *) (* innew x == total (non-option) variant of insub when P = predT. *) (* {? x | P} == option {x | P} (syntax for casting insub x). *) (* insubd u0 x == the generic projection with default value u0. *) @@ -92,7 +92,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. (* [subType for S_val by Srect], [newType for S_val by Srect] *) (* variants of the above where the eliminator is explicitly provided. *) (* Here S no longer needs to be syntactically identical to {x | P x} or *) -(* wrapped T, but it must have a derived constructor S_Sub statisfying an *) +(* wrapped T, but it must have a derived constructor S_Sub satisfying an *) (* eliminator Srect identical to the one the Coq Inductive command would *) (* have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the *) (* newType form) must be convertible to x. *) @@ -437,7 +437,7 @@ End Endo. Variable aT : Type. -(* The invariant of an function f wrt a projection k is the pred of points *) +(* The invariant of a function f wrt a projection k is the pred of points *) (* that have the same projection as their image. *) Definition invariant (rT : eqType) f (k : aT -> rT) := diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 749f5e2..0218f6a 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -39,7 +39,7 @@ From mathcomp Require Import fintype tuple. (* limitations referred to above. *) (* ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. *) (* f \in family F == f belongs to the family F (f x \in F x for all x) *) -(* There are addidional operations for non-dependent finite functions, *) +(* There are additional operations for non-dependent finite functions, *) (* i.e., f in {ffun aT -> rT}. *) (* [ffun x => E] := finfun (fun x => E). *) (* The type of E must not depend on x; this restriction *) @@ -155,7 +155,7 @@ Proof. by fix IHt 2 => n [st]; apply/Kstep=> i; apply: IHt. Defined. Set Elimination Schemes. (* End example. *) *) -(* The correspondance between finfun_of and CiC dependent functions. *) +(* The correspondence between finfun_of and CiC dependent functions. *) Section DepPlainTheory. Variables (aT : finType) (rT : aT -> Type). Notation fT := {ffun finPi aT rT}. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index afd43df..09ca95f 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -776,7 +776,7 @@ Qed. (* has to apply it to the natural numbers corresponding to the line, e.g. *) (* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`. *) (* examples of this are in order_id_cycle and fconnnect_f. *) -(* One may also use lemma all_iffLR to get a one sided impliciation, as in *) +(* One may also use lemma all_iffLR to get a one sided implication, as in *) (* orderPcycle. *) (*****************************************************************************) Lemma orbitPcycle {x} : [<-> diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index cd1a1bb..9953c0d 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -43,7 +43,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* is_transversal X P D <=> X is a transversal of the partition P of D. *) (* transversal P D == a transversal of P, provided P is a partition of D. *) (* transversal_repr x0 X B == a representative of B \in P selected by the *) -(* tranversal X of P, or else x0. *) +(* transversal X of P, or else x0. *) (* powerset A == the set of all subset of the set A. *) (* P ::&: A == those sets in P that are subsets of the set A. *) (* f @^-1: A == the preimage of the collective predicate A under f. *) @@ -56,7 +56,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* [set E | x in A, y in B] == the set of values of E for x drawn from A and *) (* and y drawn from B; B may depend on x. *) (* [set E | x <- A, y <- B & P] == the set of values of E for x drawn from A *) -(* y drawn from B, such that P is trye. *) +(* y drawn from B, such that P is true. *) (* [set E | x : T] == the set of all values of E, with x in type T. *) (* [set E | x : T & P] == the set of values of E for x : T s.t. P is true. *) (* [set E | x : T, y : U in B], [set E | x : T, y : U in B & P], *) @@ -102,7 +102,7 @@ From mathcomp Require Import choice fintype finfun bigop. (* These suffixes are sometimes preceded with an `s' to distinguish them from *) (* their basic ssrbool interpretation, e.g., *) (* card1 : #|pred1 x| = 1 and cards1 : #|[set x]| = 1 *) -(* We also use a trailling `r' to distinguish a right-hand complement from *) +(* We also use a trailing `r' to distinguish a right-hand complement from *) (* commutativity, e.g., *) (* setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0. *) (******************************************************************************) @@ -146,7 +146,7 @@ Notation "{ 'set' T }" := (set_of (Phant T)) (* preferable to state equalities at the {set _} level, even when comparing *) (* subtype values, because the primitive "injection" tactic tends to diverge *) (* on complex types (e.g., quotient groups). We provide some parse-only *) -(* notation to make this technicality less obstrusive. *) +(* notation to make this technicality less obstructive. *) Notation "A :=: B" := (A = B :> {set _}) (at level 70, no associativity, only parsing) : set_scope. Notation "A :<>: B" := (A <> B :> {set _}) @@ -2128,7 +2128,7 @@ Qed. (**********************************************************************) (* *) -(* Maximum and minimun (sub)set with respect to a given pred *) +(* Maximum and minimum (sub)set with respect to a given pred *) (* *) (**********************************************************************) diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 6c27b73..432c30f 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -108,7 +108,7 @@ From mathcomp Require Import path. (* invF inj_f y == the x such that f x = y, for inj_j : injective f with *) (* f : T -> T. *) (* dinjectiveb A f <=> the restriction of f : T -> R to A is injective *) -(* (this is a bolean predicate, R must be an eqType). *) +(* (this is a boolean predicate, R must be an eqType). *) (* injectiveb f <=> f : T -> R is injective (boolean predicate). *) (* pred0b A <=> no x : T satisfies x \in A. *) (* [forall x, P] <=> P (in which x can appear) is true for all values of x *) diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index f572a51..4eeada9 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -10,7 +10,7 @@ From mathcomp Require Import seq fintype. (* provide a helper to quotient T by a decidable equivalence relation (e *) (* : rel T) if T is a choiceType (or encodable as a choiceType modulo e). *) (* *) -(* See "Pragamatic Quotient Types in Coq", proceedings of ITP2013, *) +(* See "Pragmatic Quotient Types in Coq", proceedings of ITP2013, *) (* by Cyril Cohen. *) (* *) (* *** Generic Quotienting *** *) @@ -263,7 +263,7 @@ Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}. Hypothesis pi_h : forall (x : T), \pi_qU (h x) = hq (\pi_qT x). Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)). -(* Internal Lemmmas : do not use directly *) +(* Internal Lemmas : do not use directly *) Lemma pi_morph1 : \pi (f a) = fq (equal_val x). Proof. by rewrite !piE. Qed. Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y). Proof. by rewrite !piE. Qed. Lemma pi_mono1 : p a = pq (equal_val x). Proof. by rewrite !piE. Qed. @@ -294,7 +294,7 @@ Notation PiMono2 pi_r := Notation PiMorph11 pi_f := (fun a (x : {pi a}) => EqualTo (pi_morph11 pi_f a x)). -(* lifiting helpers *) +(* lifting helpers *) Notation lift_op1 Q f := (locked (fun x : Q => \pi_Q (f (repr x)) : Q)). Notation lift_op2 Q g := (locked (fun x y : Q => \pi_Q (g (repr x) (repr y)) : Q)). diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 8f3efaf..38ee13d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -46,7 +46,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* they operate on and then the operands. Here is the exhaustive list of all *) (* such symbols for partial orders and lattices together with their default *) (* display (as displayed by Check). We document their meaning in the *) -(* paragraph adter the next. *) +(* paragraph after the next. *) (* *) (* For porderType T *) (* @Order.le disp T == <=%O (in fun_scope) *) @@ -118,7 +118,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).` *) (* Non overloaded notations will default to the default display. *) (* *) -(* One may use displays either for convenience or to desambiguate between *) +(* One may use displays either for convenience or to disambiguate between *) (* different structures defined on "copies" of a type (as explained below.) *) (* We provide the following "copies" of types, *) (* the first one is a *documented example* *) @@ -182,7 +182,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* the structures that fits the display one mentioned, but will rather *) (* determine which canonical structure and display to use depending on the *) (* copy of the type one provided. In this sense they are merely displays *) -(* to inform the user of what the inferrence did, rather than additional *) +(* to inform the user of what the inference did, rather than additional *) (* input for the inference. *) (* *) (* Existing displays are either dual_display d (where d is a display), *) @@ -4546,7 +4546,7 @@ Import SubOrder.Exports. (* i.e. without creating a "copy". We use the predefined total_display, which *) (* is designed to parse and print meet and join as minn and maxn. This looks *) (* like standard canonical structure declaration, except we use a display. *) -(* We also use a single factory LeOrderMixin to instanciate three different *) +(* We also use a single factory LeOrderMixin to instantiate three different *) (* canonical declarations porderType, distrLatticeType, orderType *) (* We finish by providing theorems to convert the operations of ordered and *) (* lattice types to their definition without structure abstraction. *) @@ -4692,8 +4692,8 @@ End DvdSyntax. (* we declare it on a "copy" of the type. *) (* We first recover structures that are common to both nat and natdiv *) (* (eqType, choiceType, countType) through the clone mechanisms, then we use *) -(* a single factory MeetJoinMixin to instanciate both porderType and *) -(* distrLatticeType canonical structures,and end with top and bottom. *) +(* a single factory MeetJoinMixin to instantiate both porderType and *) +(* distrLatticeType canonical structures, and end with top and bottom. *) (* We finish by providing theorems to convert the operations of ordered and *) (* lattice types to their definition without structure abstraction. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index bccafa8..9327a2f 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -6,7 +6,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* The basic theory of paths over an eqType; this file is essentially a *) (* complement to seq.v. Paths are non-empty sequences that obey a progression *) (* relation. They are passed around in three parts: the head and tail of the *) -(* sequence, and a proof of (boolean) predicate asserting the progression. *) +(* sequence, and a proof of a (boolean) predicate asserting the progression. *) (* This "exploded" view is rarely embarrassing, as the first two parameters *) (* are usually inferred from the type of the third; on the contrary, it saves *) (* the hassle of constantly constructing and destructing a dependent record. *) @@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* We allow duplicates; uniqueness, if desired (as is the case for several *) (* geometric constructions), must be asserted separately. We do provide *) (* shorthand, but only for cycles, because the equational properties of *) -(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) +(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) (* We define notations for the common cases of function paths, where the *) (* progress relation is actually a function. In detail: *) (* path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we *) @@ -26,7 +26,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* the form [:: f x; f (f x); ...]. This is just a notation *) (* for path (frel f) x p. *) (* sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p *) -(* is an e-path (this is oten used with e = leq or ltn). *) +(* is an e-path (this is often used with e = leq or ltn). *) (* cycle e c == c is an e-cycle: either c = [::], or c = x :: p with *) (* x :: (rcons p x) an e-path. *) (* fcycle f c == c is an f-cycle, for a function f. *) @@ -47,9 +47,9 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* c (viewed as a cycle), or x if x \notin c. *) (* prev c x == the predecessor of the first occurrence of x in the *) (* sequence c (viewed as a cycle), or x if x \notin c. *) -(* arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting *) +(* arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting *) (* at the first occurrence of x in c, and ending just before *) -(* the next ocurrence of y (in cycle order); arc c x y *) +(* the next occurrence of y (in cycle order); arc c x y *) (* returns an unspecified sub-arc of c if x and y do not both *) (* occur in c. *) (* ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) *) @@ -73,12 +73,12 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* of splitP will also simultaneously replace take (index x p) with p1 and *) (* drop (index x p).+1 p with p2. *) (* - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and *) -(* simulaneously generates an equation x = last x0 p. *) +(* simultaneously generates an equation x = last x0 p. *) (* - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x *) (* appears explicitly at the start of the right part. *) (* The parts p1 and p2 are computed using index/take/drop in all cases, but *) -(* only splitP attemps to subsitute the explicit values. The substitution of *) -(* p can be deferred using the dependent equation generation feature of *) +(* only splitP attempts to substitute the explicit values. The substitution *) +(* of p can be deferred using the dependent equation generation feature of *) (* ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates *) (* the equation p = p1 ++ p2 instead of performing the substitution outright. *) (* Similarly, eliminating the loop removal lemma shortenP simultaneously *) @@ -86,7 +86,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* last x p'. *) (* Note that although all "path" functions actually operate on the *) (* underlying sequence, we provide a series of lemmas that define their *) -(* interaction with thepath and cycle predicates, e.g., the cat_path equation *) +(* interaction with the path and cycle predicates, e.g., the cat_path equation*) (* can be used to split the path predicate after splitting the underlying *) (* sequence. *) (******************************************************************************) diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index b71f5e7..02d3cda 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -47,7 +47,7 @@ Unset Printing Implicit Defensive. (* The complexity of any arithmetic operation with the Peano representation *) (* is pretty dreadful, so using algorithms for "harder" problems such as *) -(* factoring, that are geared for efficient artihmetic leads to dismal *) +(* factoring, that are geared for efficient arithmetic leads to dismal *) (* performance -- it takes a significant time, for instance, to compute the *) (* divisors of just a two-digit number. On the other hand, for Peano *) (* integers, prime factoring (and testing) is linear-time with a small *) 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/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 7de4ad4..fb6a030 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -90,7 +90,7 @@ Require Export Ring. (* V (infix) -- disjunction, as in *) (* leq_eqVlt : (m <= n) = (m == n) || (m < n). *) (* X - exponentiation, as in lognX : logn p (m ^ n) = logn p m * n in *) -(* file prime.v (the suffix is not used in ths file). *) +(* file prime.v (the suffix is not used in this file). *) (* Suffixes that abbreviate operations (D, B, M and X) are used to abbreviate *) (* second-rank operations in equational lemma names that describe left-hand *) (* sides (e.g., mulnDl); they are not used to abbreviate the main operation *) @@ -1542,7 +1542,7 @@ Section NatToNat. Variable (f : nat -> nat). (****************************************************************************) -(* This listing of "Let"s factor out the required premices for the *) +(* This listing of "Let"s factor out the required premises for the *) (* subsequent lemmas, putting them in the context so that "done" solves the *) (* goals quickly *) (****************************************************************************) @@ -1645,7 +1645,7 @@ Module NatTrec. (* Usage: *) (* Import NatTrec. *) -(* in section definining functions, rebinds all *) +(* in section defining functions, rebinds all *) (* non-tail recursive operators. *) (* rewrite !trecE. *) (* in the correctness proof, restores operators *) @@ -1793,7 +1793,7 @@ End NumberInterpretation. (* Num 1 072 399 *) (* to create large numbers for test cases *) (* Eval compute in [Num of some expression] *) -(* to display the resut of an expression that *) +(* to display the result of an expression that *) (* returns a larger integer. *) Record number : Type := Num {bin_of_number :> N}. diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index dbc7f3d..d85fdf8 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -52,7 +52,7 @@ Reserved Notation "x ^- n" (at level 29, left associativity). Reserved Notation "x *: A" (at level 40). Reserved Notation "A :* x" (at level 40). -(* Reserved notation for set-theretic operations. *) +(* Reserved notation for set-theoretic operations. *) Reserved Notation "A :&: B" (at level 48, left associativity). Reserved Notation "A :|: B" (at level 52, left associativity). Reserved Notation "a |: A" (at level 52, left associativity). diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 10d54f0..551dc77 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -13,12 +13,12 @@ Unset Printing Implicit Defensive. (* [tuple of s] == the tuple whose underlying sequence (value) is s. *) (* The size of s must be known: specifically, Coq must *) (* be able to infer a Canonical tuple projecting on s. *) -(* in_tuple s == the (size s)-tuple with value s. *) +(* in_tuple s == the (size s).-tuple with value s. *) (* [tuple] == the empty tuple. *) (* [tuple x1; ..; xn] == the explicit n.-tuple <x1; ..; xn>. *) (* [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound *) (* in E). *) -(* tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n. *) +(* tcast Emn t == the m.-tuple t cast as an n.-tuple using Emn : m = n.*) (* As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be *) (* applied to t : n.-tuple T; we provide a few specialized instances when *) (* avoids the need for a default value. *) @@ -373,7 +373,7 @@ Variables (n : nat) (T : finType). (* tuple_finMixin could, in principle, be made Canonical to allow for folding *) (* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), *) (* but in practice it will not work because the mixin_enum projector *) -(* has been burried under an opaque alias, to avoid some performance issues *) +(* has been buried under an opaque alias, to avoid some performance issues *) (* during type inference. *) Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T). Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin. 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 |