diff options
27 files changed, 100 insertions, 82 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8f628df..7c0c563 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -174,7 +174,6 @@ ci-fourcolor-dev: variables: COQ_VERSION: "dev" - # The Odd Order Theorem .ci-odd-order: extends: .ci diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 200b270..96ec16c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -164,6 +164,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - The following naming inconsistencies have been fixed in `ssrnat.v`: + `homo_inj_lt(_in)` -> `inj_homo_ltn(in)` + `(inc|dec)r(_in)` -> `(inc|dev)n(_in)` +- switching long suffixes to short suffixes + + `odd_add` -> `oddD` + + `odd_sub` -> `oddB` + + `take_addn` -> `takeD` + + `rot_addn` -> `rotD` + + `nseq_addn` -> `nseqD` ### Removed diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 0725885..21730c3 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. @@ -2395,7 +2395,7 @@ rewrite (reindex (lift_perm i0 j0)); last first. by rewrite lift_perm_lift -si0 permE ulsfK. rewrite /cofactor big_distrr /=. apply: eq_big => [s | s _]; first by rewrite lift_perm_id eqxx. -rewrite -signr_odd mulrA -signr_addb odd_add -odd_lift_perm; congr (_ * _). +rewrite -signr_odd mulrA -signr_addb oddD -odd_lift_perm; congr (_ * _). case: (pickP 'I_n) => [k0 _ | n0]; last first. by rewrite !big1 // => [j /unlift_some[i] | i _]; have:= n0 i. rewrite (reindex (lift i0)). diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b39f600..a8cf94b 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -469,7 +469,7 @@ rewrite big_ord_recr big_ord_recl/= big1 ?add0r //=; last first. rewrite !mxE ?subnn -horner_coef0 /= hornerMXaddC. rewrite !(eqxx, mulr0, add0r, addr0, subr0, rmorphN, opprK)/=. rewrite mulrC /cofactor; congr (_ * 'X + _). - rewrite /cofactor -signr_odd odd_add addbb mul1r; congr (\det _). + rewrite /cofactor -signr_odd oddD addbb mul1r; congr (\det _). apply/matrixP => i j; rewrite !mxE -val_eqE coefD coefMX coefC. by rewrite /= /bump /= !add1n !eqSS addr0. rewrite /cofactor [X in \det X](_ : _ = D _). @@ -901,7 +901,10 @@ apply: integral_horner_root mon_p pu0 intRp _. by apply/integral_poly => i; rewrite coefX; apply: integral_nat. Qed. -Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core. +Let integral0_RtoK := integral0 RtoK. +Let integral1_RtoK := integral1 RtoK. +Let monicXsubC_K := @monicXsubC K. +Hint Resolve integral0_RtoK integral1_RtoK monicXsubC_K : core. Let XsubC0 (u : K) : root ('X - u%:P) u. Proof. by rewrite root_XsubC. Qed. Let intR_XsubC u : 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/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/algC.v b/mathcomp/field/algC.v index 4932148..cd0a886 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -610,7 +610,8 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (intr_inj : injective ZtoC) : core. +Let intr_inj_ZtoC := (intr_inj : injective ZtoC). +Local Hint Resolve intr_inj_ZtoC : core. (* Specialization of a few basic ssrnum order lemmas. *) diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 15d1d61..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 *) @@ -53,7 +53,8 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (intr_inj : injective ZtoC) : core. +Local Definition intr_inj_ZtoC := (intr_inj : injective ZtoC). +Local Hint Resolve intr_inj_ZtoC : core. Local Notation QtoCm := [rmorphism of QtoC]. (* Number fields and rational spans. *) diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 6e7432f..52472a6 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -116,7 +116,8 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj [numDomainType of algC]) : core. +Let intr_inj_algC := @intr_inj [numDomainType of algC]. +Local Hint Resolve intr_inj_algC : core. Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]). Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index eb5e028..aff97b0 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -452,8 +452,8 @@ Qed. Lemma odd_mul_tperm x y s : odd_perm (tperm x y * s) = (x != y) (+) odd_perm s. Proof. -rewrite addbC -addbA -[~~ _]oddb -odd_add -ncycles_mul_tperm. -by rewrite odd_add odd_double addbF. +rewrite addbC -addbA -[~~ _]oddb -oddD -ncycles_mul_tperm. +by rewrite oddD odd_double addbF. Qed. Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). @@ -490,7 +490,7 @@ Lemma odd_permM : {morph odd_perm : s1 s2 / s1 * s2 >-> s1 (+) s2}. Proof. move=> s1 s2; case: (prod_tpermP s1) => ts1 ->{s1} dts1. case: (prod_tpermP s2) => ts2 ->{s2} dts2. -by rewrite -big_cat !odd_perm_prod ?all_cat ?dts1 // size_cat odd_add. +by rewrite -big_cat !odd_perm_prod ?all_cat ?dts1 // size_cat oddD. Qed. Lemma odd_permV s : odd_perm s^-1 = odd_perm s. 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/div.v b/mathcomp/ssreflect/div.v index b366055..9047a44 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -329,7 +329,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. 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/seq.v b/mathcomp/ssreflect/seq.v index 6dc739e..dca4136 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -282,7 +282,7 @@ Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed. Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s. Proof. by elim: n => //= n ->. Qed. -Lemma nseq_addn n1 n2 x : +Lemma nseqD n1 n2 x : nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x. Proof. by rewrite cat_nseq /nseq /ncons iter_add. Qed. @@ -772,7 +772,7 @@ Qed. Lemma take_drop i j s : take i (drop j s) = drop j (take (i + j) s). Proof. by rewrite addnC; elim: s i j => // x s IHs [|i] [|j] /=. Qed. -Lemma take_addn i j s : take (i + j) s = take i s ++ take j (drop i s). +Lemma takeD i j s : take (i + j) s = take i s ++ take j (drop i s). Proof. elim: i j s => [|i IHi] [|j] [|a s] //; first by rewrite take0 addn0 cats0. by rewrite addSn /= IHi. @@ -788,12 +788,12 @@ by case: s => [|a s]//; rewrite /= ltnS. Qed. Lemma take_nseq i j x : i <= j -> take i (nseq j x) = nseq i x. -Proof. by move=>/subnKC <-; rewrite nseq_addn take_size_cat // size_nseq. Qed. +Proof. by move=>/subnKC <-; rewrite nseqD take_size_cat // size_nseq. Qed. Lemma drop_nseq i j x : drop i (nseq j x) = nseq (j - i) x. Proof. case: (leqP i j) => [/subnKC {1}<-|/ltnW j_le_i]. - by rewrite nseq_addn drop_size_cat // size_nseq. + by rewrite nseqD drop_size_cat // size_nseq. by rewrite drop_oversize ?size_nseq // (eqP j_le_i). Qed. @@ -890,7 +890,7 @@ Lemma all_rev a s : all a (rev s) = all a s. Proof. by rewrite !all_count count_rev size_rev. Qed. Lemma rev_nseq n x : rev (nseq n x) = nseq n x. -Proof. by elim: n => // n IHn; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. Qed. +Proof. by elim: n => // n IHn; rewrite -[in LHS]addn1 nseqD rev_cat IHn. Qed. End Sequences. @@ -1784,7 +1784,7 @@ Section RotCompLemmas. Variable T : Type. Implicit Type s : seq T. -Lemma rot_addn m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s). +Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s). Proof. move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n). rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop. @@ -1792,13 +1792,13 @@ by rewrite size_drop !size_takel ?leq_addl ?addnK. Qed. Lemma rotS n s : n < size s -> rot n.+1 s = rot 1 (rot n s). -Proof. exact: (@rot_addn 1). Qed. +Proof. exact: (@rotD 1). Qed. Lemma rot_add_mod m n s : n <= size s -> m <= size s -> rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s. Proof. -move=> Hn Hm; case: leqP => [/rot_addn // | /ltnW Hmn]; symmetry. -by rewrite -{2}(rotK n s) /rotr -rot_addn size_rot addnBA ?subnK ?addnK. +move=> Hn Hm; case: leqP => [/rotD // | /ltnW Hmn]; symmetry. +by rewrite -{2}(rotK n s) /rotr -rotD size_rot addnBA ?subnK ?addnK. Qed. Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s). @@ -3340,7 +3340,7 @@ have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t. pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)). have xrotK t: {in le_x t, cancel (xrot t) xrotV}. move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x]. - rewrite -rot_addn ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev. + rewrite -rotD ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev. by rewrite ifN // size_takel //= eqxx addn0. apply/uniq_perm=> [||t]; first exact: permutations_uniq. apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //. @@ -3426,6 +3426,9 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := Ltac tfae := do !apply: AllIffConj. (* Temporary backward compatibility. *) +Notation take_addn := (deprecate take_addn takeD _) (only parsing). +Notation rot_addn := (deprecate rot_addn rotD _) (only parsing). +Notation nseq_addn := (deprecate nseq_addn nseqD _) (only parsing). Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _) (only parsing). Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _) diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 7de4ad4..c2f2c52 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 *) @@ -1245,19 +1245,19 @@ Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false. Lemma oddb (b : bool) : odd b = b. Proof. by case: b. Qed. -Lemma odd_add m n : odd (m + n) = odd m (+) odd n. +Lemma oddD m n : odd (m + n) = odd m (+) odd n. Proof. by elim: m => [|m IHn] //=; rewrite -addTb IHn addbA addTb. Qed. -Lemma odd_sub m n : n <= m -> odd (m - n) = odd m (+) odd n. +Lemma oddB m n : n <= m -> odd (m - n) = odd m (+) odd n. Proof. -by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -odd_add subnK. +by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK. Qed. Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i. -Proof. by move=> oddm le_im; rewrite (odd_sub (le_im)) oddm. Qed. +Proof. by move=> oddm le_im; rewrite (oddB (le_im)) oddm. Qed. Lemma odd_mul m n : odd (m * n) = odd m && odd n. -Proof. by elim: m => //= m IHm; rewrite odd_add -addTb andb_addl -IHm. Qed. +Proof. by elim: m => //= m IHm; rewrite oddD -addTb andb_addl -IHm. Qed. Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m. Proof. by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd. Qed. @@ -1304,7 +1304,7 @@ Lemma leq_Sdouble m n : (m.*2 <= n.*2.+1) = (m <= n). Proof. by rewrite leqNgt ltn_Sdouble -leqNgt. Qed. Lemma odd_double n : odd n.*2 = false. -Proof. by rewrite -addnn odd_add addbb. Qed. +Proof. by rewrite -addnn oddD addbb. Qed. Lemma double_gt0 n : (0 < n.*2) = (0 < n). Proof. by case: n. Qed. @@ -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}. @@ -1918,3 +1918,7 @@ Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) Proof. by case: ltngtP; constructor. Qed. End mc_1_10. + +(* Temporary backward compatibility. *) +Notation odd_add := (deprecate odd_add oddD _) (only parsing). +Notation odd_sub := (deprecate odd_sub oddB _) (only parsing). 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. |