CHANGELOG.md

Changelog

All notable changes to this project will be documented in this file.

Last releases: [2.4.0] - 2025-04-14, [2.3.0] - 2024-11-28, [2.2.0] - 2024-01-17

The format is based on Keep a Changelog.

[2.4.0] - 2025-04-14

This release is compatible with Coq versions 8.19, 8.20 and Rocq version 9.0.

The contributors to this version are:

Alessandro Bruni, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Kazuhiko Sakaguchi, Kimaya Bedarkar, Laurent Théry, Pierre Pomeret-Coquot, Pierre Roux, Quentin Vermande, Reynald Affeldt, Mitsuharu Yamamoto, Yves Bertot

Added

• in ssralg.v

  • Semimodule and semialgebra structures lSemiModType, lSemiAlgType, semiAlgType, comSemiAlgType, subLSemiModType, subLSemiAlgType, and subSemiAlgType.
  • Scaling-morphism structures GRing.Scale.preLaw and GRing.Scale.semiLaw.
  • Mixins Nmodule_isLSemiModule, LSemiModule_isLSemiAlgebra, GRing.Scale.isPreLaw, GRing.Scale.isSemiLaw, LSemiAlgebra_isSemiAlgebra, isSubLSemiModule
  • Factories LSemiModule_isLmodule, isSemilinear, LSemiAlgebra_isComSemiAlgebra, SubNmodule_isSubLSemiModule, SubNzSemiRing_SubLSemiModule_isSubLSemiAlgebra, SubLSemiAlgebra_isSubSemiAlgebra, SubChoice_isSubLSemiModule
  • Definitions semilinear_for, subsemimod_closed
  • Notations semilinear, semiscalar, [SubNmodule_isSubLSemiModule of V by <:], [SubChoice_isSubLSemiModule of V by <:], [SubSemiRing_SubLSemiModule_isSubLSemiAlgebra of V by <:], [SubLSemiAlgebra_isSubSemiAlgebra of V by <:]
  • Lemmas subsemimod_closedD, subsemimod_closedZ, submod_closed_semi, additive_semilinear, scalable_semilinear, semilinear_linear, semilinearP, semilinearPZ, can2_semilinear, semiscalarP, subsemimodClosedP (#1125).
  • mixin Nmodule_isPzSemiRing
  • definition pzSemiRingType
  • factory isPzSemiRing
  • mixin PzSemiRing_isNonZero
  • definition pzRingType
  • factories Zmodule_isPzRing, isPzRing
  • mixin PzSemiRing_hasCommutativeMul
  • definition comPzSemiRingType
  • factory Nmodule_isComPzSemiRing
  • definition comPzRingType
  • factories PzRing_hasCommutativeMul, Zmodule_isComPzRing
  • mixin isSubPzSemiRing
  • definition subPzSemiRingType
  • factory SubNmodule_isSubPzSemiRing
  • definition subComPzSemiRingType
  • factory SubPzSemiRing_isSubComPzSemiRing
  • definition subPzRingType
  • factory subZmodule_isSubPzRing
  • definition subComPzRingType
  • factories SubPzRing_isSubComPzRing, SubChoice_isSubPzSemiRing, SubChoice_isSubComPzSemiRing, SubChoice_isSubPzRing, SubChoice_isSubComPzRing (#1319).

• in zmodp.v

  • lemmas gen_tperm_step, perm_addr1X, gen_tpermn_circular_shift (#1198).

• in cyclic.v

  • lemmas eq_expg_ord, expgD_Zp (#1198).

• in nilpotent.v

  • lemma setXn_sol (#1198).

• in alt.v

  • lemmas gen_tperm_circular_shift, solvable_AltF, solvable_SymF (#1198).

• in algC.v

  • record algR with projections algRval, algRvalP
  • lemmas total_algR, algRval_is_additive, algRval_is_multiplicative,
  • definition algR_norm
  • lemmas algR_ler_normD, algR_normr0_eq0, algR_normrMn, algR_normrN, algR_addr_gt0, algR_ger_leVge, algR_normrM, algR_ler_def, algR_archiFieldMixin
  • definition algR_pfactor
  • notation algC_pfactor
  • lemmas algR_pfactorRE, algC_pfactorRE, algR_pfactorCE, algC_pfactorCE, algC_pfactorE, size_algC_pfactor, size_algR_pfactor, algC_pfactor_eq0, algR_pfactor_eq0, algC_pfactorCgt0, algR_pfactorR_mul_gt0, monic_algC_pfactor, monic_algR_pfactor, poly_algR_pfactor, algR_rcfMixin (#1199).

• in archimedean.v

  • lemmas floorNceil, ceilNfloor, truncEfloor, intrP
  • mixin Num.NumDomain_hasFloorCeilTruncn (#1250).
  • lemmas real_floor_ge_int_tmp, real_ceil_le_int_tmp, floor_ge_int_tmp and ceil_le_int_tmp
  • lemmas truncn_le, real_truncnS_gt, truncn_ge_nat, truncn_gt_nat, truncn_lt_nat, real_truncn_le_nat, truncn_eq, le_truncn, natrEtruncn real_floor_lt_int, real_floor_eq, real_floor_ge0, floor_lt0, real_floor_le0, floor_gt0, floor_neq0, real_ceil_gt_int, real_ceil_eq, real_ceil_ge0, ceil_lt0, real_ceil_le0, ceil_gt0, ceil_neq0, floor_lt_int, floor_eq, floor_ge0, floor_le0, ceil_gt_int, ceil_eq, ceil_ge0, ceil_le0, truncnS_gt, truncn_le_nat and natr_int (#1359).

• in order.v

  • notations \min_<range> e, \max_<range> e, \min^d_<range> e, \max^d_<range> e, \min^p_<range> e, \max^p_<range> e, \min^sp_<range> e, \max^sp_<range> e, \meet^l_<range> e, \join^l_<range> e, \min^l_<range> e, \max^l_<range> e (#1298).
  • lemmas comparable_le_min2, comparable_le_max2, le_min2 and le_max2 (backport from math-comp/analysis#1410 ) (#1351).
  • export le_val in Order.SubPOrderTheory (included in Order.Theory) to avoid being forced to type Order.le_val (#1353).

• in seq.v,

  • new lemmas odflt_onth, onthE, onth_nth, onth0n, onth1P, onthTE, onthNE, onth_default, onth_cat, onth_nseq, eq_onthP, eq_from_onth, eq_from_onth_le, onth_map, inj_onth_map, onthP, onthPn, and onth_inj. (#1318).

• in tuple.v

  • new lemma tnth_onth (#1318).

• in ssrnum.v

  • Mixin Zmodule_isSemiNormed and class SemiNormedZmodule with associated structure semiNormedZmodType.
  • lemmas gtr0_norm_neq0, and gtr0_norm_eq0F (#1333).
  • lemmas natr_min, natr_max and sqrtC_real (backport from math-comp/analysis#1410 ) (#1351).

• in ssrnat.v

  • definition N_eqb (#1343).

• in interval.v

  • lemmas comparable_BSide_min, comparable_BSide_max, BSide_min, BSide_max, real_BSide_min and real_BSide_max (backport from #1410 ) (#1351).
  • lemma subset_itv_bound, matching previous subset_itv (#1380).
  • lemma subset_itv has been generalized (previous version is now subset_itv_bound) (#1380).

• new file interval_inference.v added to all_algebra.v, this can solve automatically a few more goals, making some proofs fail (with subgoals no longer existing) (backported from #1410 ) (#1352).

• in interval_inference.v

  • definitions map_iv_bound, map_itv, Itv.t, Itv.sub, Itv.spec, Itv.mk, Itv.from, fromP, Itv.num_sem, Itv.nat_sem, Itv.posnum, Itv.nonneg, Itv.real1, Itv.real2, empty_itv, widen_itv, ItvNum, ItvReal, Itv01, PosNum, NngNum, posnum_spec, nonneg_spec
  • module IntItv with
    • definitions opp_bound, opp, add_boundl, add_boundr, add, signb, sign_boundl, sign_boundr, signi, sign, mul_boundl, mul_boundr, mul, min, max, keep_nonneg_bound, keep_pos_bound, keep_nonpos_bound, keep_neg_bound, inv, exprn_le1_bound, exprn, keep_sign, keep_nonpos, keep_nonneg
    • lemmas opp_bound_ge0, opp_bound_gt0, mul_boundrC, mul_boundr_gt0
  • module Instances with
    • definitions sign_spec, Instances.sqrt_itv, Instances.sqrtC_itv
    • lemmas num_spec_zero, num_spec_one, opp_boundr, opp_boundl, num_spec_opp, num_itv_add_boundl, num_itv_add_boundr, num_spec_add, signP, num_itv_mul_boundl, num_itv_mul_boundr, BRight_le_mul_boundr, comparable_num_itv_bound, num_itv_bound_min, num_itv_bound_max, num_spec_mul, num_spec_min, num_spec_max, nat_num_spec, num_spec_natmul, num_spec_int, num_spec_intmul, num_itv_bound_keep_pos, num_itv_bound_keep_neg, num_spec_inv, num_itv_bound_exprn_le1, num_spec_exprn, num_spec_norm, num_spec_sqrt, num_spec_sqrtC, nat_spec_zero, nat_spec_succ, nat_spec_add, nat_spec_double, nat_spec_mul, nat_spec_exp, nat_spec_min, nat_spec_max, num_spec_Posz, num_spec_Negz
    • canonical instances zero_inum, one_inum, opp_inum, add_inum, mul_inum, min_typ_inum, max_typ_inum, num_min_max_typ, natmul_inum, intmul_inum, inv_inum, exprn_inum, norm_inum, sqrt_inum, sqrtC_inum, zeron_inum, succn_inum, addn_inum, double_inum, muln_inum, expn_inum, minn_inum, maxn_inum, nat_min_max_typ, Posz_inum, Negz_inum
  • lemmas map_itv_bound_comp, map_itv_comp, Itv.spec_real1, Itv.spec_real2, itv_le_total_subproof, TypInstances.top_typ_spec, TypInstances.real_domain_typ_spec, TypInstances.real_field_typ_spec, TypInstances.nat_typ_spec, TypInstances.typ_inum_spec, le_num_itv_bound, num_itv_bound_le_BLeft, BRight_le_num_itv_bound, num_spec_sub, bottom, gt0, le0F, lt0, ge0F, ge0, lt0F, le0, gt0F, cmp0, neq0, eq0F, lt1, ge1F, le1, gt1F, widen_itv_subproof, widen_itvE, posE, nngE, num_eq, num_le, num_lt, num_min, num_max, num_abs_eq0, num_le_max, num_ge_max, num_le_min, num_ge_min, num_lt_max, num_gt_max, num_lt_min, num_gt_min, num_abs_le, num_abs_lt, itvnum_subdef, itvreal_subdef, itv01_subdef, Itv01., posnum_subdef, nngnum_subdef, posnumP, nonnegP
  • canonical instances TypInstances.top_typ, TypInstances.real_domain_typ, TypInstances.real_field, TypInstances.nat_typ, TypInstances.typ_inum
  • notations {itv R & i}, {i01 R}, {posnum R}, {nonneg R}, x%:itv, [itv of x], num, x%:inum, x%:num, x%:posnum, x%:nngnum, unify_itv, [gt0 of x], [lt0 of x], [ge0 of x], [le0 of x], [cmp0 of x], [neq0 of x], x%:i01, x%:pos, x%:nng (backported from #1410 ) (#1352).
  • definition Instances.natmul_itv and IntItv.exprz
  • lemmas Instances.num_spec_exprz and Instances.nat_spec_factorial
  • instances Instances.exprz_inum and Instances.facorial_inum (#1368).

• in rat.v

  • lemma solve_Qint_span (#1191).
  • definition inIntSpan (from intdiv.v)
  • lemmas Qint_dvdz, Qnat_dvd, size_rat_int_poly, rat_poly_scale, dvdp_rat_int, dvdpP_rat_int, irreductible_rat_int, solve_QInt_span, dec_Qint_span, eisenstein_crit (from intdiv.v)
  • lemmas floorErat, ceilErat (#1381).

• in ssrfun.v

  • lemmas inr_inj, inl_inj (#1397).
  • lemmas taggedK, swap_pair and swap_pairK (#931).

• in bigop.v

  • lemmas big_sup_cond, big_sub, gt0_prodn_seq and gt0_prodn (#931).

• in eqtype.v

  • definitions etagged, untag, tagged_with, tag_with and untag_with
  • lemmas eq_from_Tagged, etaggedK, untagE, untag_dflt, untag_cst, tag_withK, untag_withK, tag_with_bij and untag_with_bij (#931).

• in finfun.v

  • definition fprod (a record with projections fprod_fun and fprod_prod)
  • definitions fun_of_fprod, fprod_of_fun, dffun_of_fprod, fprod_of_dffun, to_family_tagged_with and of_family_tagged_with
  • lemmas tag_fprod_fun, fprodK, fprodE, fprodP, etaggedE, dffun_of_fprodK, fprod_of_dffunK, dffun_of_fprod_bij, fprod_of_dffun_bij, to_family_tagged_withK, of_family_tagged_withK, to_family_tagged_with_bij and of_family_tagged_with_bij (#931).

• in finset.v

  • definitions unset1, fprod_pick and ftagged
  • lemmas set0_Nexists, eq0_subset, subsetC_disjoint, pick_set1, set1K, omap_unset1K, unset10, unset1N1, unset1K, big_cards1, card_fprod, ftaggedE, big_tag_cond, big_tag, big_fprod_dep and big_fprod (#931).

• in fintype.v

  • lemmas existsbWl and existsbWr (#931).

Changed

• in ssralg.v

  • {linear U -> V | s} and {linear U -> V}, generalized from modules to semimodules, now represent semilinear and linear functions
  • {scalar U}, generalized from rings and modules to semirings and semimodules, now represents semiscalar and scalar functions
  • {lrmorphism A -> B | s} and {lrmorphism A -> B}, generalized from algebras to semialgebras, now represent semialgebra and algebra morphisms
  • Mixins Zmodule_isLmodule, Lmodule_isLalgebra, Lalgebra_isAlgebra, isSubLmodule are now factories
  • GRing.scale, scalerA, scale0r, scale1r, scalerDr, scalerDl, scaler0, scaler_nat, scalerMnl, scalerMnr, scaler_suml, scaler_sumr, scaler_closed, scale_fun, raddfZnat, scalable_for, isScalable, linear_for, rpredZnat, submodClosed generalized to lSemiModType
  • linear0, linearD, linearMn, linear_sum, linearZ_LR, linearP, linearZ, linearZZ, linearPZ, can2_scalable, can2_linear, scalarZ, scalarP generalized to lSemiModType and semilinear functions
  • scalerAl, mulr_algl, in_alg, subalgClosed generalized to lSemiAlgType
  • rmorph_alg generalized to lSemiAlgType and semialgebra morphisms (#1125).
  • Nmodule_isNzSemiRing is now a factory
  • char, mulr_sumr, mulrnAl, mulrnAr, mulr_natl, mulr_natr, natrD, natr1, nat1r, natr_sum, natrM, expr0, expr1, expr2, exprS, expr0n, expr1n, exprD, exprSr, expr_sum, commr_sym, commr_refl, commr0, commr1, commrD, commr_sum, commrMn, commrM, commr_prod, commr_nat, commrX, exprMn_comm, exprMn_n, exprM, exprAC, expr_mod, expr_dvd, natrX, mulrI_eq0, lreg1, lregM, lregMl, rregMr, lregX, iter_mulr, iter_mulr_1, prodr_const, prodr_const_nat, prodrXr, prodrM_comm, prodrMl_comm, prodrMr_comm, prodrMn, prodrMn_const, natr_prod, exprDn_comm, exprD1n, sqrrD1, Frobenius_aut, mulr_2closed, mulr_closed, semiring_closed, semiring_closedD, semiring_closedM, rev_prodr, mulIr_eq0, rreg1, rregM, revrX, rregX, mull_fun, mulr_fun, mul_fun, raddfMnat, mull_fun_is_semi_additive, mulr_fun_is_semi_additive, multiplicative, isMultiplicative, RMorphism.type, rmorph0, rmorphD, rmorphMn, rmorph_sum, rmorphismMP, rmorph1, rmorphM, rmorph_prod, rmorphXn, rmorph_nat, rmorph_char, rmorph_eq_nat, rmorph_eq1, can2_rmorphism, idfun_is_multiplicative, comp_is_multiplicative, isMul2Closed, isMul2Closed, mulr2Closed, mulrClosed, semiring2Closed, semiringClosed, isMulClosed, isSemiringClosed, rpred1M, rpred_prod, rpredX, rpred_nat, semiringClosedP, val1, valM, valM1, ffun_one, ffun_mul, ffun_mulA, ffun_mul_1l, ffun_mul_1r, ffun_mul_addl, ffun_mul_addr, ffun_mul_0l, ffun_mul_0r, mul_pair, pair_mulA, pair_mul1l, pair_mul1r, pair_mulDl, pair_mulDr, pair_mul0r, pair_mulr0, fst_is_multiplicative, snd_is_multiplicative generalized to pzSemiRingType
  • mulrN, mulNr, mulrNN, mulN1r, mulrN1, mulrBl, mulrBr, natrB, commrN, commrN1, commrB, commr_sign, signr_add, mulr_sign, signr_addb, signrE, signrN, mulr_signM, exprNn, sqrrN, sqrr_sign, signrMK, mulrI0_lreg, lregN, lreg_sign, prodrN, exprBn_comm, subrXX_comm, subrX1, sqrrB1, subr_sqr_1, smulr_closed, subring_closed, smulr_closedM, smulr_closedN, subring_closedB, subring_closedM, subring_closed_semi, mulIr0_rreg, rregN, Zmodule_isLmodule, lmodType, scale0r, scaler0, scaleNr, scaleN1r, scalerN, scalerBl, scalerBr, scaler_nat, scaler_sign, signrZK, scalerMnl, scalerMnr, scaler_suml, scaler_sumr, scalr_closed, linear_closed, submod_closed, linear_closedB, submod_closedB, submod_closedZ, mulr_algl, subalg_closed, subalg_closedZ, subalg_closedBM, scale_fun, in_alg, raddfMsign, raddfZnat, raddfZsign, rmorphN, rmorphB, rmorphMNn, rmorphMsign, in_alg_is_additive, in_alg_is_rmorphism, isLaw, Law.type, N1op, compN1op, scalable_for, isScalable, Linear.type, linear_for, additive_linear, scalable_linear, isLinear, scalable, linear, scalar, linear0, linearN, linearD, linearB, linearMn, linearMNn, linear_sum, linearZ_LR, linearP, linearZ, linearZZ, linearPZ, can2_scalable, can2_linear, scalarZ, scalarP, idfun_is_scalable, opp_is_scalable, comp_is_scalable, null_fun_is_scalable, add_fun_is_scalable, sub_fun_is_scalable, opp_fun_is_scalable, mulr_fun_is_scalable, LRMorphism.type, rmorph_alg, Lalgebra_isAlgebra, Lalgebra_isComAlgebra, scaleAr, lalgebra_is_algebra, comAlgType, scalerCA, mulr_algr, comm_alg, exprZn, scaler_prod, scaler_prodl, scaler_prodr, mull_fun_is_scalable, integral_domain_axiom, closed_field_axiom, lalgMixin, algMixin, isScaleClosed, smulClosed, subringClosed, submodClosed, subalgClosed, divalgClosed, isSmulClosed, isSubringClosed, isSubmodClosed, isSubalgClosed, rpredMsign, rpredN1, rpred_sign, subringClosedP, rpredZsign, rpredZnat, submodClosedP, subalgClosedP, SubZmodule_isSubLmodule, subLalgType, SubNzRing_SubLmodule_isSubLalgebra, subAlgType, SubLalgebra_isSubAlgebra, SubChoice_isSubLalgebra, SubChoice_isSubAlgebra, ffun_scale, ffun_scaleA, ffun_scale1, ffun_scale_addr, ffun_scale_addl, scale_pair, pair_scaleA, pair_scale1, pair_scaleDr, pair_scaleDl, fst_is_scalable, snd_is_scalable, pair_scaleAl generalized to pzRingType
  • exprMn, prodrXl, prodr_undup_exp_count, prodrMl, prodrMr, exprDn, sqrrD generalized to comPzSemiRingType
  • exprBn, subrXX, sqrrB, subr_sqr, subr_sqrDB, scale_is_scalable, scale_fun_is_scalable, comRingMixin, ffun_mulC, pair_mulC generalized to comPzRingType (#1319).

• in archimedean.v

  • the definition of archimedean structures now include Num.floor and Num.ceil
  • as its consequence, Num.ceil x = - Num.floor (- x) does not hold definitionally anymore (use lemma ceilNfloor instead) (#1250).

• in bigop.v

  • change the implicit arguments of lemmas big_cat_nat_idem and big_cat_nat (#1261).
  • change the implicit arguments of lemmas leq_prod, prodn_cond_gt0 and prodn_gt0 (#931).

• in sesquilinear.v

  • notations _ ^ _ and _ ^t _ are now in the dedicated scope sesquilinear_scope. (#1314).
  • move notation ``_ to spectral.v and make it local (#1363).

• in spectral.v

  • notations _ ^t* is now in the dedicated scope sesquilinear_scope. (#1314).

• in ssrint.v

  • mulrzAl, mulrzAr, mulrzl, mulrzr, mulNrNz, mulrbz, intrN, intrD, intrB, intrM, intmul1_is_multiplicative, mulr2z, scaler_int, scalerMzl, scalerMzr, rmorphMz, rmorph_int, linearMn, commrMz, commr_int, sumMz, prodMz, intr_sign, rpred_int, rpredZint generalized to pzRingType (#1319).
  • lemmas exprz_ge0, exprz_gt0, exprz_gte0, ler_wpiXz2l, ler_wpeXz2l, pexprz_eq1 and ler_wpXz2r generalized from realFieldType to numDomainType (#1367).

• in ssrnum.v

  • Mixin Zmodule_isNormed is now a factory building a SemiNormedZmodule and a SemiNormedZmodule_isPositiveDefinite. (#1333).
  • Generalized lemmas from the theory of normedZmodType to semiNormedZmodType: normr0, distrC, normr_id, and normr_ge0, normr_real, ler_norm_sum, ler_normB, ler_distD, lerB_normD, lerB_dist, ler_dist_dist, ler_dist_normD, ler_nnorml, ltr_nnorml, lter_nnormr. (#1333).

• in ssrnat.v

  • lemma eq_binP changed from Stdlib's N.eqb to new N_eqb
  • eqtype instance on nat changed from Stdlib's N.eqb to new N_eqb (#1343).

• in rat.v

  • Num.floor, Num.ceil and Num.truncn on rat now compute (#1381).

• in matrix.v

  • Definitions mulmx, perm_mx, tperm_mx, is_perm_mx, pid_mx, lift0_perm, lift0_mx, comm_mx, comm_mxb generalized to pzSemiRingType
  • Definitions copid_mx, lin1_mx, lin_mx, mulmxr, lin_mulmxr, mxtrace, determinant, cofactor, adjugate, Vandermonde generalized to pzRingType
  • Definition lin_mul_row generalized to comPzRingType
  • The pzSemiRingType and pzRingType instances on square matrices generalized to the case where the size is potentially zero
  • The lmodType instance on matrices generalized to pzRingType
  • The ring morphism instances on scalar_mx and map_mx generalized to pzSemiRingType and the case where the size is potentially zero
  • The linear function instances on swizzle_mx, trmx, row, col, row', col', mxsub, row_perm, col_perm, xrow, xcol, lsubmx, rsubmx, usubmx, dsubmx, vec_mx, mxvec, diag_mx, mxtrace generalized to pzRingType
  • The additive function instances on mulmx, mulmxr, lin_mulmxr generalized to pzRingType
  • The linear function instances on mulmx, lin_mulmx, lin_mul_row generalized to comPzRingType
  • The semiringClosed instance on mxOver generalized to pzRingType
  • Lemmas trmx_delta, delta_mx_lshift, delta_mx_rshift, delta_mx_ushift, delta_mx_dshift, vec_mx_delta, mxvec_delta, trmx1, row1, col1, mulmxA, mul0mx, mulmx0, mulmxDl, mulmxDr, mulmx_suml, mulmx_sumr, rowE, colE, mul_rVP, row_mul, mxsub_mul, mul_rowsub_mx, mulmx_colsub, mul_delta_mx_cond, mul_delta_mx, mul_delta_mx_0, mul_diag_mx, mul_mx_diag, mulmx_diag, scalar_mxM, mul1mx, mulmx1, rowsubE, mul_col_perm, mul_row_perm, mul_xcol, col_permE, row_permE, xcolE, xrowE, perm_mxEsub, tperm_mxEsub, tr_perm_mx, tr_tperm_mx, perm_mx1, perm_mxM, is_perm_mxP, perm_mx_is_perm, is_perm_mx1, is_perm_mxMl, is_perm_mx_tr, is_perm_mxMr, pid_mx_0, pid_mx_1, pid_mx_row, pid_mx_col, pid_mx_block, tr_pid_mx, pid_mx_minv, pid_mx_minh, mul_pid_mx, pid_mx_id, pid_mxErow, pid_mxEcol, mul_mx_row, mul_col_mx, mul_row_col, mul_col_row, mul_row_block, mul_block_col, mulmx_block, mulmx_lsub, mulmx_rsub, mul_usub_mx, mul_dsub_mx, mxtrace1, mulmxE, idmxE, lift0_perm0, lift0_perm_lift, lift0_permK, lift0_perm_eq0, lift0_mx_perm, lift0_mx_is_perm, exp_block_diag_mx, trmx_mul_rev, map_mxM, map_delta_mx, map_diag_mx, map_scalar_mx, map_mx1, map_perm_mx, map_tperm_mx, map_pid_mx, trace_map_mx, comm_mx_sym, comm_mx_refl, comm_mx0, comm0mx, comm_mx1, comm1mx, comm_mxD, comm_mxM, comm_mx_sum, comm_mxP, all_comm_mxP, all_comm_mx1, all_comm_mx2P, all_comm_mx_cons, comm_mxE generalized to pzSemiRingType
  • Lemmas trmx_mul, diag_mxC, diag_mx_comm, scalar_mxC, comm_mx_scalar, comm_scalar_mx, mxtrace_mulC generalized to comPzSemiRingType
  • Lemams scalemx_const, matrix_sum_delta, row_sum_delta, scale_row_mx, scale_col_mx, scale_block_mx, diag_mx_sum_delta, row_diag_mx, scale_scalar_mx, scalemx1, scalar_mx_sum_delta, mx1_sum_delta, mulmxN, mulNmx, mulmxBl, mulmxBr, scalemxAl, mulmx_sum_row, mul_scalar_mx, mul_copid_mx_pid, mul_pid_mx_copid, copid_mx_id, mul_rV_lin1, mul_rV_lin, mul_vec_lin, mx_rV_lin, mx_vec_lin, mxtraceZ, map_mxZ, det_map_mx, cofactor_map_mx, map_mx_adj, map_copid_mx, map_lin1_mx, map_lin_mx, comm_mxN, comm_mxN1, comm_mxB, mul_mxrow, mul_submxrow, mxcol_mul, submxcol_mul, mul_mxrow_mxcol, mul_mxcol_mxrow, mul_mxrow_mxblock, mul_mxblock_mxrow, mul_mxblock, mxtrace_mxblock, mxdiagZ, diag_mxrow, mxtrace_mxdiag, mul_mxdiag_mxcol, mul_mxrow_mxdiag, mul_mxblock_mxdiag, mul_mxdiag_mxblock generalized to pzRingType
  • Lemmas scalemxAr, mul_vec_lin_row, mxvec_dotmul, mul_mx_scalar, determinant_multilinear, determinant_alternate, det_tr, det_perm, det1, det_mx00, detZ, det0, det_scalar, det_scalar1, det_mx11, det_mulmx, detM, expand_cofactor, expand_det_row, cofactor_tr, cofactorZ, expand_det_col, trmx_adj, adjZ, mul_mx_adj, mul_adj_mx, adj1, mulmx1C, det_ublock, det_lblock, det_trig, det_diag, mxOver_scalar, mxOver_scalarE, mxOverZ, mxOver_diag, mxOver_diagE, mxOverM, det_Vandermonde generalized to comPzRingType (#1385).

Renamed

• in archimedean.v

  • NumDomain_isArchimedean.Build -> NumDomain_hasTruncn.Build (#1250).
  • real_ge_floor -> real_floor_le
  • real_lt_succ_floor -> real_floorD1_gt
  • real_gt_pred_ceil -> real_ceilB1_lt
  • real_le_ceil -> real_ceil_ge
  • ge_floor -> floor_le_tmp
  • lt_succ_floor -> floorD1_gt
  • gt_pred_ceil -> ceilB1_lt
  • le_ceil -> ceil_ge
  • floor_le -> le_floor
  • ceil_le -> le_ceil_tmp
  • natrE -> natrEtruncn (#1359).

• in ssrfun.v

  • eqfun now has type forall [B] [A : B -> Type] (f g : forall b, A b), Prop
  • eqrel now has type forall [C] [B : C -> Type] [A : forall c, B c -> Type] (f g : forall c b, A c b), Prop (#1300).

• in ssralg.v

  • Nmodule_isSemiRing -> Nmodule_isNzSemiRing
  • isSemiRing -> isNzSemiRing
  • Zmodule_isRing -> Zmodule_isNzRing
  • isRing -> isNzRing
  • SemiRing_hasCommutativeMul -> SemiRing_hasCommutativeMul
  • Nmodule_isComSemiRing -> Nmodule_isComNzSemiRing
  • Ring_hasCommutativeMul -> NzRing_hasCommutativeMul
  • Zmodule_isComRing -> Zmodule_isComNzRing
  • Ring_hasMulInverse -> NzRing_hasMulInverse
  • ComRing_hasMulInverse -> ComNzRing_hasMulInverse
  • ComRing_isField -> ComNzRing_isField
  • isSubSemiRing -> isSubNzSemiRing
  • SubNmodule_isSubSemiRing -> SubNmodule_isSubNzSemiRing
  • SubSemiRing_isSubComSemiRing -> SubNzSemiRing_isSubComNzSemiRing
  • SubZmodule_isSubRing -> SubZmodule_isSubNzRing
  • SubRing_isSubComRing -> SubNzRing_isSubComNzRing
  • SubRing_SubLmodule_isSubLalgebra -> SubNzRing_SubLmodule_isSubLalgebra
  • SubChoice_isSubSemiRing -> SubChoice_isSubNzSemiRing
  • SubChoice_isSubComSemiRing -> SubChoice_isSubComNzSemiRing
  • SubChoice_isSubRing -> SubChoice_isSubNzRing
  • SubChoice_isSubComRing -> SubChoice_isSubComNzRing
  • semiRingType -> nzSemiRingType
  • ringType -> nzRingType
  • comSemiRingType -> comNzSemiRingType
  • comRingType -> comNzRingType
  • subSemiRingType -> subNzSemiRingType
  • subComSemiRingType -> subComNzSemiRingType
  • subRingType -> subNzRingType
  • subComNzRingType -> subComNzRingType (#1306).
  • char -> pchar
  • [char _] -> [pchar _]
  • has_char0 -> has_pchar0
  • Frobenius_aut -> pFrobenius_aut
  • charf0 -> pcharf0
  • charf_prime -> pcharf_prime
  • mulrn_char -> mulrn_pchar
  • natr_mod_char -> natr_mod_pchar
  • dvdn_charf -> dvdn_pcharf
  • charf_eq -> pcharf_eq
  • bin_lt_charf_0 -> bin_lt_pcharf_0
  • Frobenius_autE -> pFrobenius_autE
  • Frobenius_aut0 -> pFrobenius_aut0
  • Frobenius_aut1 -> pFrobenius_aut1
  • Frobenius_autMn -> pFrobenius_autMn
  • Frobenius_aut_nat -> pFrobenius_aut_nat
  • Frobenius_autM_comm -> pFrobenius_autM_comm
  • Frobenius_autX -> pFrobenius_autX
  • addrr_char2 -> addrr_pchar2
  • Frobenius_autN -> pFrobenius_autN
  • Frobenius_autB_comm -> pFrobenius_autB_comm
  • exprNn_char -> exprNn_pchar
  • oppr_char2 -> oppr_pchar2
  • subr_char2 -> subr_pchar2
  • addrK_char2 -> addrK_pchar2
  • rmorph_char -> rmorph_pchar
  • Frobenius_aut_is_semi_additive -> pFrobenius_aut_is_semi_additive
  • Frobenius_aut_is_multiplicative -> pFrobenius_aut_is_multiplicative
  • exprDn_char -> exprDn_pchar
  • natf_neq0 -> natf_neq0_pchar
  • natf0_char -> natf0_pchar
  • charf'_nat -> pcharf'_nat
  • charf0P -> pcharf0P
  • char0_natf_div -> pchar0_natf_div
  • fmorph_char -> fmorph_pchar
  • char_lalg -> pchar_lalg

• in ring_quotient.v

  • isRingQuotient -> isNzRingQuotient
  • ringQuotType -> nzRingQuotType (#1306).

• in finalg.v

  • isRing -> isNzRing
  • finSemiRingType-> finNzSemiRingType
  • finRingType -> finNzRingType
  • finComSemiRingType -> finComNzSemiRingType
  • finComRingType -> finComNzRingType
  • card_finRing_gt1 -> card_finNzRing_gt1 (#1306).

• in countalg.v

  • countSemiRingType-> countNzSemiRingType
  • countRingType -> countNzRingType
  • countComSemiRingType -> countComNzSemiRingType
  • countComRingType -> countComNzRingType (#1306).

• in intdiv.v

  • dvdz_charf -> dvdz_pcharf

• in poly.v

  • char_poly -> pchar_poly
  • prim_root_charF -> prim_root_pcharF
  • char_prim_root -> pchar_prim_root
  • size_opp -> size_polyN
  • size_add -> size_polyD
  • size_addl -> size_polyDl
  • size_mul_leq -> size_polyM_leq (#1315).

• in qpoly.v

  • char_qpoly -> pchar_qpoly

• in sesquilinear.v

  • is_symplectic -> is_psymplectic
  • is_orthogonal -> is_porthogonal

• in ssrint.v

  • Frobenius_autMz -> pFrobenius_autMz
  • Frobenius_aut_int -> pFrobenius_aut_int

• in ssrnum.v

  • char_num -> pchar_num

• in zmodp.v

  • char_Zp -> pchar_Zp
  • char_Fp -> pchar_Fp
  • char_Fp_0 -> pchar_Fp_0

• in classfun.v

  • algC'G -> algC'G_pchar

• in mxabelem.v

  • rfix_pgroup_char -> rfix_pgroup_pchar
  • pcore_sub_rstab_mxsimple -> pcore_sub_rstab_mxsimple_pchar
  • pcore_sub_rker_mx_irr -> pcore_sub_rker_mx_irr_pchar
  • pcore_faithful_mx_irr -> pcore_faithful_mx_irr_pchar
  • extraspecial_repr_structure -> extraspecial_repr_structure_pchar
  • faithful_repr_extraspecial -> faithful_repr_extraspecial_pchar

• in mxrepresentation.v

  • mx_Maschke -> mx_Maschke_pchar
  • rsim_regular_submod -> rsim_regular_submod_pchar
  • irr_mx_sum -> irr_mx_sum_pchar
  • Wedderburn_sum -> Wedderburn_sum_pchar
  • Wedderburn_sum_id -> Wedderburn_sum_id_pchar
  • Wedderburn_is_id -> Wedderburn_is_id_pchar
  • Wedderburn_closed -> Wedderburn_closed_pchar
  • Wedderburn_is_ring -> Wedderburn_is_ring_pchar
  • Wedderburn_min_ideal -> Wedderburn_min_ideal_pchar
  • not_rsim_op0 -> not_rsim_op0_pchar
  • rsim_irr_comp -> rsim_irr_comp_pchar
  • irr_comp'_op0 -> irr_comp'_op0_pchar
  • irr_comp_envelop -> irr_comp_envelop_pchar
  • ker_irr_comp_op -> ker_irr_comp_op_pchar
  • regular_op_inj -> regular_op_inj_pchar
  • rank_irr_comp -> rank_irr_comp_pchar
  • irr_comp_rsim -> irr_comp_rsim_pchar
  • irr_reprK -> irr_reprK_pchar
  • irr_repr'_op0 -> irr_repr'_op0_pchar
  • op_Wedderburn_id -> op_Wedderburn_id_pchar
  • irr_comp_id -> irr_comp_id_pchar
  • rank_Wedderburn_subring -> rank_Wedderburn_subring_pchar
  • sum_irr_degree -> sum_irr_degree_pchar
  • irr_mx_mult -> irr_mx_mult_pchar
  • mxtrace_regular -> mxtrace_regular_pchar
  • linear_irr_comp -> linear_irr_comp_pchar
  • Wedderburn_subring_center -> Wedderburn_subring_center_pchar
  • Wedderburn_center -> Wedderburn_center_pchar
  • card_irr -> card_irr_pchar
  • cycle_repr_structure -> cycle_repr_structure_pchar
  • splitting_cyclic_primitive_root -> splitting_cyclic_primitive_root_pchar

• in algC.v

  • Cchar -> Cpchar

• in finfield.v

  • finCharP -> finPcharP
  • card_finCharP -> card_finPcharP
  • PrimeCharType -> pPrimeCharType
  • primeChar_scale -> pprimeChar_scale
  • primeChar_scaleA -> pprimeChar_scaleA
  • primeChar_scale1 -> pprimeChar_scale1
  • primeChar_scaleDr -> pprimeChar_scaleDr
  • primeChar_scaleDl -> pprimeChar_scaleDl
  • primeChar_scaleAl -> pprimeChar_scaleAl
  • primeChar_scaleAr -> pprimeChar_scaleAr
  • primeChar_abelem -> pprimeChar_abelem
  • primeChar_pgroup -> pprimeChar_pgroup
  • order_primeChar -> order_pprimeChar
  • card_primeChar -> card_pprimeChar
  • primeChar_vectAxiom -> pprimeChar_vectAxiom
  • primeChar_dimf -> pprimeChar_dimf
  • PrimePowerField -> pPrimePowerField
  • FinDomainSplittingFieldType -> FinDomainSplittingFieldType_pchar

• in separable.v

  • char0_PET -> pchar0_PET
  • separablePn -> separablePn_pchar
  • separable_exponent -> separable_exponent_pchar
  • charf0_separable -> pcharf0_separable
  • charf_p_separable -> pcharf_p_separable
  • charf_n_separable -> pcharf_n_separable
  • purely_inseparable_elementP -> purely_inseparable_elementP_pchar

• in abelian.v

  • fin_lmod_char_abelem -> fin_lmod_pchar_abelem
  • fin_lmod_char_abelem -> fin_lmod_pchar_abelem (#1311).

Removed

• in ssralg.v

  • mixin NzSemiRing_hasCommutativeMul
  • factory NzRing_hasCommutativeMul (#1319).

• in ssrnat.v

  • requirements for BinNat, Ndec and Ring from Stdlib. You may need to add some explicit requirements, the most common one being From Coq Require Setoid, but we also observed BinPos, Pnat, Ring_theory, RelationClasses, Wf_nat and List
  • lemmas nat_of_add_bin, nat_of_mul_bin, nat_of_exp_bin, nat_semi_ring, nat_semi_morph and nat_power_theory
  • definition extend_number (was a coercion)
  • tactic nat_litteral
  • ring instance for nat (use algebra-tactics instead) (#1343).

• in rat.v

  • lemmas rat_ring_theory and rat_field_theory
  • ring and field instances for rat (use algebra-tactics instead) (#1343).
  • definition inIntSpan (moved to rat.v)
  • lemmas Qint_dvdz, Qnat_dvd, size_rat_int_poly, rat_poly_scale, dvdp_rat_int, dvdpP_rat_int, irreductible_rat_int, solve_QInt_span, dec_Qint_span, eisenstein_crit (moved to rat.v) (#1381).

Deprecated

• in ssrnum.v

  • lemma pmulrn_rgt0 (#1324).

• in archimedean.v

  • lemma real_floor_ge_int (use real_floor_ge_int_tmp instead)
  • lemma real_ceil_le_int (use real_ceil_le_int_tmp instead)
  • lemma floor_ge_int (use floor_ge_int_tmp instead)
  • lemma ceil_le_int (use ceil_le_int_tmp instead) (#1359).

• in interval.v

  • lemma subset_itv_bound, use subset_itv instead (#1380).

[2.3.0] - 2024-11-28

Added

• in ssrnat.v

  • lemmas ltn_mull, ltn_mulr

• in ssrint.v

  • lemmas intrN, intrB

• in ssrnum.v

  • lemma invf_pgt, invf_pge, invf_ngt, invf_nge
  • lemma invf_plt, invf_ple, invf_nlt, invf_nle

• in bigop.v

  • lemma big_ord1, big_ord1_cond, big_rcons_op, big_change_idx, big_rcons, big_only1, big_mknat
  • lemmas big_rev, rev_big_rev and big_morph_in

• in eqtype.v

  • definition dfwith
  • lemmas dfwith_in, dfwith_out, dfwithP

• in seq.v

  • lemmas has_undup, all_undup, zip_uniql, zip_uniqr, index_nth

• in finset.v

  • definition setXn
  • lemmas in_setXn, setXnP, cardsXn, setXnS, eq_setXn, enum_setU, enum_setI, has_set1, has_setU, all_set1, all_setU, big_subset_idem_cond, big_subset_idem, big_setU_cond, big_setU

• in prime.v

  • lemmas primeNsig, all_prime_primes, primes_eq0, totient_gt1

• in tuple.v

  • lemmas tnth_lshift, tnth_rshift

• in path.v

  • lemmas count_sort, sorted_cat_cons, gtn_sorted_uniq_geq

• in poly.v

  • lemmas coef0M, coef0_prod, polyseqXaddC, lead_coefXaddC, lead_coefXnaddC, lead_coefXnsubC, size_XnaddC, size_XnsubC, monicXaddC, lead_coef_prod_XsubC, monicXnaddC, monicXnsubC, prim_root_eq0, polyOverXn, polyOverXaddC, polyOverXnaddC, polyOverXnsubC, prim_root_charF, char_prim_root, prim_root_pi_eq0, prim_root_dvd_eq0, prim_root_natf_neq0, eq_in_map_poly_id0, eq_in_map_poly, map_polyXaddC, map_polyXsubC, map_prod_XsubC, prod_map_poly, mapf_root, lead_coef_prod

• in ssralg.v

  • lemmas prodrM_comm, prodrMl_comm, prodrMr_comm, prodrMl, prodrMr rev_prodr, unitr_prod, unitr_prod_in, rev_prodrV, unitr_prodP, prodrV

• in ssrbool.v

  • lemmas classic_sigW, classic_ex

• in intdiv.v

  • lemmas dvdz_charf, eisenstein_crit

• in mxalgebra.v

  • lemma mulmxP

• in polydiv.v

  • lemmas root_dvdP, eqpW, irredp_XaddC, dvdp_exp_XsubCP, horner_mod,
  • definition mup
  • lemmas mup_geq, mup_leq, mup_ltn, XsubC_dvd, mup_XsubCX, mupNroot, mupMr, mupMl, mupM, mu_prod_XsubC, prod_XsubC_eq

• in vector.v

  • lemmas subset_limgP, lker0_img_cap, SubvsE, span_lfunP, fullv_lfunP
  • definition rVof
  • lemmas rVof_linear, coord_rVof
  • definition vecof
  • lemmas vecof_delta, vecof_linear, rVofK, vecofK, rVofE, coord_vecof, rVof_eq0, vecof_eq0,
  • definition mxof
  • lemma mxof_linear
  • definition funmx
  • lemma funmx_linear
  • definition hommx
  • lemmas hommx_linear, mxofK, hommxK, mul_mxof, hommxE, rVof_mul, hom_vecof, rVof_app, vecof_mul, mxof_eq0, hommx_eq0, mxof_comp, hommx_mul
  • definitions msof, vsof
  • lemmas mxof1, hommx1, msofK, mem_vecof, rVof_sub, vsof_sub, msof_sub, vsofK, sub_msof, sub_vsof, msof0, vsof0, msof_eq0, vsof_eq0
  • definitions leigenspace, leigenvalue
  • lemmas lker_ker, limgE, leigenspaceE

• in action.v

  • lemmas perm_prime_atrans, perm_prime_orbit, perm_prime_astab

• in fingroup.v

  • lemma prod_subG

• in gproduct.v

  • lemma comm_prodG
  • definitions extnprod_mulg, extnprod_invg
  • lemmas extnprod_mul1g, extnprod_mulVg, extnprod_mulgA, oneg_ffun, mulg_ffun, invg_ffun, prodg_ffun, group_setXn
  • definition dfung1
  • lemmas dfung1_id, dfung1_dflt, dfung1_morphM, dffunM, injm_dfung1, group_set_dfwith, group_dfwithE
  • definition set1gXn
  • lemmas set1gXnE, set1gXnP, morphim_dfung1, morphim_dffunXn, set1gXn_group_set, setXn_prod, set1gXn_commute, setXn_dprod, isog_setXn, setXn_gen, groupX0

• in perm.v

  • lemmas tpermJ_tperm, gen_tperm

• in order.v

  • structures meetSemilatticeType, bMeetSemilatticeType, tMeetSemilatticeType, tbMeetSemilatticeType, joinSemilatticeType, bJoinSemilatticeType, tJoinSemilatticeType, tbJoinSemilatticeType, tDistrLatticeType, bOrderType, tOrderType, tbOrderType, cDistrLatticeType (relatively complemented distributive lattices), ctDistrLatticeType (dually sectionally complemented distributive lattices), finBPOrderType, finTPOrderType, finTBPOrderType, finMeetSemilatticeType, finBMeetSemilatticeType, finJoinSemilatticeType, and finTJoinSemilatticeType.
  • factories isDuallyPOrder, Lattice_isDistributive, POrder_isMeetSemilattice, POrder_isJoinSemilattice, POrder_Meet_isSemilattice, POrder_Join_isSemilattice, DistrLattice_hasRelativeComplement, CDistrLattice_hasSectionalComplement, CDistrLattice_hasDualSectionalComplement, CDistrLattice_hasComplement, BDistrLattice_hasSectionalComplement, TDistrLattice_hasDualSectionalComplement, CBDistrLattice_hasComplement, CTDistrLattice_hasComplement, TBDistrLattice_hasComplement
  • rcompl x y z is the relative complement of z in [x, y] defined for any cDistrLatticeType instance.
  • codiff x y is the dual sectional complement of y in [x, \top] defined for any ctDistrLatticeType instance.
  • lemmas lt1x, ltx1, rcomplPmeet, rcomplPjoin, rcomplKI, rcomplKU, diffErcompl, codiffErcompl, complEdiff, complEcodiff, complErcompl

• in archimedean.v

  • lemmas floor_itv, ge_floor, lt_succ_floor x, floor_ge_int, ceil_itv, gt_pred_ceil, le_ceil, ceil_le_int, ceil_floor
  • lemmas real_floorDrz, real_ceilDrz, floorDzr, floorDrz, ceilDzr, ceilDrz
  • archiRealDomainType instance for int (moved from ssrint.v)

• in intdiv.v

  • lemma irreducible_rat_int

• new file mxred.v

  • definition conjmx
  • lemmas stablemx_comp, stablemx_restrict, conjmxM, conjMmx, conjuMmx, conjMumx, conjuMumx, conjmx_scalar, conj0mx, conjmx0, conjumx, conj1mx, conjVmx, conjmxK, conjmxVK, horner_mx_conj, horner_mx_uconj, horner_mx_uconjC, mxminpoly_conj, mxminpoly_uconj, sub_kermxpoly_conjmx, sub_eigenspace_conjmx, eigenpoly_conjmx, eigenvalue_conjmx, conjmx_eigenvalue
  • notation restrictmx
  • definition similar_to
  • notations similar, similar_in, similar_in_to, all_similar_to, similar_diag, diagonalizable_in, diagonalizable, codiagonalizable_in, codiagonalizable, similar_trig, trigonalizable_in, trigonalizable, cotrigonalizable_in, cotrigonalizable
  • lemmas similarPp, similarW, similarP, similarRL, similarLR, similar_mxminpoly, similar_diag_row_base, similar_diagPp, similar_diagP, similar_diagPex, similar_diagLR, similar_diag_mxminpoly, similar_diag_sum, codiagonalizable1, codiagonalizablePfull, codiagonalizable_on, diagonalizable_diag, diagonalizable_scalar, diagonalizable0, diagonalizablePeigen, diagonalizableP, diagonalizable_conj_diag, codiagonalizableP.

• new file sesquilinear.v

  • notations ``_, e_, ^, ^t
  • lemma eq_map_mx_id
  • mixin InvolutiveRMorphism
  • lemma rmorphK
  • definition conjC
  • lemma map_mxCK
  • mixin isBilinear
  • structure Bilinear
  • definition bilinear_for
  • factory bilinear_isBilinear
  • module Bilinear (contents not documented in the changelog)
  • notations {bilinear _ -> _ -> _ | _ & _}, {bilinear _ -> _ -> _ | _}, {bilinear _ -> _ -> _}, {biscalar _}
  • definition applyr_head, notation applyr
  • (coercions and canonicals not documented in the changelog)
  • lemmas linear0r, linearNr, linearDr, linearBr, linearMnr, linearMNnr, linear_sumr, linearZr_LR, linearPr
  • lemma applyrE
  • lemmas linear0l, linearNl, linearDl, linearBl, linearMnl, linearMNnl, linear_sumlz, linearZl_LR, linearPl, linearZl, linearZr, linearZlr, linearZrl
  • lemma mulmx_is_bilinear
  • definition form
  • lemmas form0l, form0r, formDl, formDr, formZr, formZl, formNl, formNr, formee, form0_eq0
  • mixin isHermitianSesquilinear, structure Hermitian, notation {hermitian _ fo _ & _}
  • definitions orthomx, sesqui, fact sesqui_key, canonical sesqui_keyed, notation _.-sesqui
  • lemmas sesquiE, sesquiP, trmx_sesqui, maptrmx_sesqui, formC, form_eq0C
  • definition ortho
  • lemmas normalE, form_eq0P, normalP, normalC, normal_ortho_mx, normal_mx_ortho, rank_normal
  • defintion rad
  • lemmas rad_ker, formDd, formZ, formN, form_sign, formD, formB, formBd
  • notations symmetric_form, skew, hermitian
  • mixin isDotProduct, structure Dot, notation {dot _ for theta _}
  • notations {symmetric _}, {skew_symmetric _}, {hermitian_sym _ for _}
  • definitions is_skew, is_sym, is_hermsym
  • lemmas hermC, hnormN, hnorm_sign, hnormD, hnormB, hnormDd, hnormBd
  • definition ortho_rec, fixpoint pair_ortho_rec, defintions pairwise_orthogonal, orthogonal, orthonormal
  • lemmas orthogonal_cons, orthonormal_not0, orthonormalE, orthonormal_orthogonal
  • definitions isometry, isometry_from_to
  • lemma herm_eq0C
  • definition orthov
  • lemmass mem_orthovPn, mem_orthovP, orthov1E, orthovP, orthov_sym, mem_orthov1, orthov11, mem_orthov1_sym, orthov0, mem_orthov_sym, leq_dim_orthov1, dim_img_form_eq1, eq_dim_orthov1, dim_img_form_eq0, neq_dim_orthov1, leqif_dim_orthov1, leqif_dim_orthov1_full, orthogonal1P, orthogonalP, orthogonal_oppr, orthogonalE, orthovE, orthoDv, orthovD
  • definitons nondegenerate, is_symplectic, is_orthogonal, is_unitary
  • lemmas dnorm_geiff0, dnorm_ge0, dnorm_eq0, dnorm_gt0, sqrt_dnorm_ge0, sqrt_dnorm_eq0, sqrt_dnorm_gt0, dnormZ, dnormD, dnormB, pairwise_orthogonalP, pairwise_orthogonal_cat, orthonormal_cat, orthonormalP, sub_orthonormal, orthonormal2P, orthonormal2P, orthogonal_free, filter_pairwise_orthogonal, orthonormal_free, CauchySchwarzP, CauchySchwarz_sqrt, orthoP, orthoPl, orthogonal_sym, orthoPr, orthogonal_catl, orthogonal_catr, eq_pairwise_orthogonal, eq_orthonormal, orthogonal_oppl, triangle_lerif, span_orthogonal, orthogonal_split,
  • definitions normf1, normf2
  • lemmas isometry_of_dnorm, isometry_of_free, isometry_raddf_inj
  • definitons form_of_matrix, matrix_of_form, form_of_matrixr
  • lemma matrix_of_formE, form_of_matrix_is_bilinear, rV_formee, rV_form0_eq0, matrix_of_formK
  • definition hermitianmx, fact hermitianmx_key, canonical hermitianmx_keyed, structure hermitian_matrix
  • lemmas is_hermitianmxE, is_hermitianmxP, hermitianmxE, trmx_hermitian, maptrmx_hermitian, form_of_matrix_is_hermitian, orthomxE, hermmx_eq0P, orthomxP, orthomx_sym, ortho_ortho_mx, ortho_mx_ortho, rank_orthomx, radmxE, orthoNmx, orthomxN, orthoDmx, orthomxD, orthoZmx, orthomxZ, eqmx_ortho, genmx_ortho
  • notations symmetricmx, skewmx, hermsymmx
  • lemma hermitian1mx_subproof, canonical hermitian1mx

• new file spectral.v

  • lemmas eigenvalue_closed, common_eigenvector, common_eigenvector2
  • notation ^t*, realmx
  • lemmas trmxCK, realmxC, realmxD, Remx_rect, Immx_rect, eqmx_ReiIm, realsym_hermsym, real_similar
  • definition unitarymx, fact unitarymx_key, canonical unitarymx_keyed
  • lemmas unitarymxP, mulmxtVK, unitarymx_unit, invmx_unitary, mulmxKtV, mxrank_unitary, mul_unitarymx, pinvmx_unitary, conjymx, trmx_unitary, conjC_unitary, trmxC_unitary
  • definition normalmx, fact normalmx_key, canonical normalmx_keyed
  • lemmas normalmxP, hermitian_normalmx, symmetric_normalmx
  • definition dotmx
  • lemmas dotmxE, row_unitarymxP, dotmx_is_dotmx, orthomx1E, orthomx1P, orthomx_disj, orthomx_ortho_disj, rank_ortho, add_rank_ortho, addsmx_ortho, ortho_id, submx_ortho
  • definition proj_ortho
  • lemmas sub_adds_genmx_ortho, cap_genmx_ortho, proj_ortho_sub, proj_ortho_compl_sub, proj_ortho_id, proj_ortho_0, add_proj_ortho, proj_ortho_proj, proj_orthoE, orthomx_proj_mx_ortho
  • lemma schmidt_subproof, definition schmidt
  • lemmas schmidt_unitarymx, row_schmidt_sub, form1_row_schmidt, schmidt_sub, eqmx_schmidt_full, eqmx_schmidt_free
  • definiton schmidt_complete
  • lemmas schmidt_complete_unitarymx, cotrigonalization, Schur, cotrigonalization2
  • lemma orthomx_spectral_subproof, definitions spectralmx, `spectral_diag
  • lemmas spectral_unitarymx, spectral_unit, orthomx_spectralP, hermitian_spectral_diag_real

• in ssrfun.v:

  • definitions idempotent_op, idempotent_fun

Changed

• in seq.v

  • fix incorrectly exported notations 'all_view and 'has_view

• in bigop.v

  • weaken hypothesis of lemma telescope_sumn_in

• in path.v

  • generalized count_merge from eqType to Type

• in order.v

  • order_morphism changed to homo from mono and renamed nondecreasing
  • The dual instances are now definitionally involutive, i.e., canonical instances of an order structure on T^d^d and T are convertible (the latter instance may require an eta-expansion on the type record for technical reasons). Similarly, canonical instances of an order structure on (T1 *p T2)^d and T1^d *p T2^d are convertible.
  • In order to achieve the above definitional properties on displays, the type of display is changed from unit to Order.disp_t, which is a primitive record type consisting of two fields of type unit.
  • The default displays for product and lexicographic orders are now defined separately for cartesian products and sequences. They take displays of the parameter types as parameters.
    • prod_display d1 d2 is the default display for the product order of cartesian products of the form T1 * T2, where T1 and T2 have canonical orders of displays d1 and d2, respectively.
    • seqprod_display d is the default display for the product order of sequences and tuples.
    • lexi_display d1 d2 is the default display for the lexicographic order of cartesian products.
    • seqlexi_display d is the default display for the lexicographic order of sequences and tuples.
  • The operator notations for seqprod_display and seqlexi_display now use ^sp and ^sl in place of ^p and ^l, respectively.
  • finLatticeType, finDistrLatticeType, finOrderType, and finCDistrLatticeType now do not require the existence of top and bottom elements, i.e., their instances are not necessarily inhabited. Their counterparts with top and bottom are now finTBLatticeType, finTBDistrLatticeType, finTBOrderType, and finCTBDistrLatticeType, respectively.
  • lemmas meetEdual, leUx, leUr, leUl, lexUl, lexUr, lexU2, leEjoin, eq_joinl, eq_joinr, join_idPl, join_idPr, join_l, join_r, leUidr, leU2, joinC, joinA, joinxx, joinAC, joinCA, joinACA, joinKU, joinUK, joinKUC, joinUKC generalized from latticeType to joinSemilatticeType
  • lemmas joinx0, join0x, join_eq0, joins_sup_seq, joins_min_seq, joins_sup, joins_min, joins_le, joinsP_seq, joinsP, le_joins, joins_setU, joins_seq generalized from bLatticeType to bJoinSemilatticeType
  • lemmas joinx1 and join1x generalized from tLatticeType to tJoinSemilatticeType
  • lemmas joinEdual, lexI, leIr, leIl, leIxl, leIxr, leIx2, leEmeet, eq_meetl, eq_meetr, meet_idPl, meet_idPr, meet_l, meet_r, leIidl, leIidr, leI2, meetC, meetA, meetxx, meetAC, meetCA, meetACA, meetKI, meetIK, meetIKC generalized from latticeType to meetSemilatticeType
  • lemmas meet0x and meetx0 generalized from bLatticeType to bMeetSemilatticeType
  • lemmas meetx1, meet1x, meet_eql, meets_inf_seq, meets_max_seq, meets_inf, meets_max, meets_ge, meetsP_seq, meetsP, le_meets, meets_setU, meets_seq generalized from tLatticeType to tMeetSemilatticeType

• in zmodp.v

  • simpler statement of Fp_Zcast
  • definitions Zp_opp, Zp_add, Zp_mul, Zp_inv generalized from 'I_p.+1 to 'I_p.
  • lemmas Zp_addA, Zp_addC, Zp_mulC, Zp_mulA, Zp_mul_addr, Zp_mul_addl, Zp_inv_out generalized from 'I_p.+1 to 'I_p.

Renamed

• in binomial.v

  • triangular_sum -> bin2_sum

• in order.v (cf. Changed section)

  • finLatticeType -> finTBLatticeType
  • finDistrLatticeType -> finTBDistrLatticeType
  • finOrderType -> finTBOrderType
  • finCDistrLatticeType -> finCTBDistrLatticeType

• in archimedean.v

  • floor_itv -> real_floor_itv
  • ge_floor -> real_ge_floor
  • lt_succ_floor -> real_lt_succ_floor
  • floor_ge_int -> real_floor_ge_int
  • floorD -> real_floorDzr
  • ceil_itv -> real_ceil_itv
  • gt_pred_ceil -> real_gt_pred_ceil
  • le_ceil -> real_le_ceil
  • ceil_le_int -> real_ceil_le_int
  • ceilD -> real_ceilDzr
  • ceil_floor -> real_ceil_floor

• in ssrint.v

  • mulrzDr -> mulrzDl
  • mulrzDl -> mulrzDr

Removed

• in seq.v

  • notation take_take (deprecated since 1.16)

• in ssrnum.v

  • notations ler_opp2, ltr_opp2, lter_opp2, ler_oppr, ltr_oppr, lter_oppr, ler_oppl, ltr_oppl, lter_oppl, lteif_opp2, ler_add2l, ler_add2r, ler_add2, ltr_add2l, ltr_add2r, ltr_add2, lter_add2, ler_add, ler_lt_add, ltr_le_add, ltr_add, ler_sub, ler_lt_sub, ltr_le_sub, ltr_sub, ler_subl_addr, ler_subr_addr, ler_sub_addr, ltr_subl_addr, ltr_subr_addr, ltr_sub_addr, lter_sub_addr, ler_subl_addl, ltr_subl_addl, ler_subr_addl, ltr_subr_addl, ler_sub_addl, ltr_sub_addl, lter_sub_addl, ler_addl, ltr_addl, ler_addr, ltr_addr, ger_addl, gtr_addl, ger_addr, gtr_addr, cpr_add, lteif_add2l, lteif_add2r, lteif_add2, lteif_subl_addr, lteif_subr_addr, lteif_sub_addr, lteif_subl_addl, lteif_subr_addl, lteif_sub_addl, leif_add, gtr_opp, lteif_oppl, lteif_oppr, lteif_0oppr, lteif_oppr0, lter_oppE, ler_dist_add, ler_dist_norm_add, ler_sub_norm_add, ler_sub_dist, ler_sub_real, ger_sub_real, ltr_expn2r, ler_expn2r, lter_expn2r, ler_pmul, ltr_pmul, ler_pinv, ler_ninv, ltr_pinv, ltr_ninv, ler_pmul2l, ltr_pmul2l, lter_pmul2l, ler_pmul2r, ltr_pmul2r, lter_pmul2r, ler_nmul2l, ltr_nmul2l, lter_nmul2l, ler_nmul2r, ltr_nmul2r, lter_nmul2r, minr_pmulr, maxr_pmulr, minr_pmull, maxr_pmull, ltr_wpexpn2r, ler_pexpn2r, ltr_pexpn2r, lter_pexpn2r, ger_pmull, gtr_pmull, ger_pmulr, gtr_pmulr, ler_pmull, ltr_pmull, ler_pmulr, ltr_pmulr, ger_nmull, gtr_nmull, ger_nmulr, gtr_nmulr, ler_nmull, ltr_nmull, ler_nmulr, ltr_nmulr, leif_pmul, leif_nmul, eqr_expn2, real_maxr_nmulr, real_minr_nmulr, real_minr_nmull, real_maxr_nmull, real_ltr_distl_addr, real_ler_distl_addr, real_ltr_distlC_addr, real_ler_distlC_addr, real_ltr_distl_subl, real_ler_distl_subl, real_ltr_distlC_subl, real_ler_distlC_subl, ler_iexpn2l, ltr_iexpn2l, lter_iexpn2l, ler_eexpn2l, ltr_eexpn2l, lter_eexpn2l, ler_wpmul2l, ler_wpmul2r, ler_wnmul2l, ler_wnmul2r, ler_pemull, ler_nemull, ler_pemulr, ler_nemulr, ler_iexp, ltr_iexpr, lter_iexpr, ler_eexpr, ltr_eexpr, lter_eexpr, lter_expr, ler_wiexpn2l, ler_weexpn2l, ler_pimull, ler_nimull, ler_pimulr, ler_nimulr, ler_pmuln2r, ltr_pmuln2r, ler_pmuln2l, ler_wpmuln2l, eqr_pmuln2r, ltr_wmuln2r, ltr_wpmuln2r, ler_wmuln2r, ler_wnmuln2l, ler_muln2r, ltr_muln2r, eqr_muln2r, ltr_pmuln2l, ler_nmuln2l, ltr_nmuln2l, leif_subLR, leif_subRL, lteif_pmul2l, lteif_pmul2r, lteif_nmul2l, lteif_nmul2r, ler_paddl, ltr_paddl, ltr_spaddl, ltr_spsaddl, ler_naddl, ltr_naddl, ltr_snaddl, ltr_snsaddl, ler_paddr, ltr_paddr, ltr_spaddr, ltr_spsaddr, ler_naddr, ltr_naddr, ltr_snaddr, ltr_snsaddr, lef_pinv, lef_ninv, ltf_pinv, ltf_ninv, ltef_pinv, ltef_ninv, lteif_pdivl_mulr, lteif_pdivr_mulr, lteif_pdivl_mull, lteif_pdivr_mull, lteif_ndivl_mulr, lteif_ndivr_mulr, lteif_ndivl_mull, lteif_ndivr_mull, ler_pdivl_mulr, ltr_pdivl_mulr, lter_pdivl_mulr, ler_pdivr_mulr, ltr_pdivr_mulr, lter_pdivr_mulr, ler_pdivl_mull, ltr_pdivl_mull, lter_pdivl_mull, ler_pdivr_mull, ltr_pdivr_mull, lter_pdivr_mull, ler_ndivl_mulr, ltr_ndivl_mulr, lter_ndivl_mulr, ler_ndivr_mulr, ltr_ndivr_mulr, lter_ndivr_mulr, ler_ndivl_mull, ltr_ndivl_mull, lter_ndivl_mull, ler_ndivr_mull, ltr_ndivr_mull, lter_ndivr_mull, normC_add_eq, normC_sub_eq, ler_norm_add, ler_norm_sub, ltr_distl_addr, ler_distl_addr, ltr_distlC_addr, ler_distlC_addr, ltr_distl_subl, ler_distl_subl, ltr_distlC_subl, ler_distlC_subl, maxr_nmulr, minr_nmulr, minr_nmull, maxr_nmull (deprecated since 1.17)
  • structures archiNumDomainType, archiNumFieldType, archiClosedFieldType, archiDomainType, archiFieldType, archiRcfType (deprecated since 2.1 and moved to archimedean.v)
  • factory NumDomain_bounded_isArchimedean (deprecated since 2.1 and moved to archimedean.v)
  • notations Num.Def.trunc, Num.trunc, Num.Def.nat_num, Num.nat, Num.Def.int_num, Num.int, Num.bound (deprecated since 2.1 and moved to archimedean.v)
  • lemmas archi_boundP, upper_nthrootP, truncP, trunc_itv (deprecated since 2.1)

• in ssrint.v

  • notations oppz_add, lez_add1r, lez_addr1, ltz_add1r, ltz_addr1, ler_pmulz2r, ler_pmulz2l, ler_wpmulz2r, ler_wpmulz2l, ler_wnmulz2l, ler_nmulz2r, ler_nmulz2l, ltr_pmulz2r, ltr_pmulz2l, ltr_nmulz2r, ltr_nmulz2l, ler_wnmulz2r, ler_wpexpz2r, ler_wnexpz2r, ler_pexpz2r, ltr_pexpz2r, ler_nexpz2r, ltr_nexpz2r, ler_wpiexpz2l, ler_wniexpz2l, ler_wpeexpz2l, ler_wneexpz2l, ler_weexpz2l, ler_piexpz2l, ltr_piexpz2l, ler_niexpz2l, ltr_niexpz2l, ler_eexpz2l, ltr_eexpz2l, eqr_expz2, exprz_pmulzl, leq_add_dist, leqif_add_distz, leqif_add_dist (deprecated since 1.17)
  • notation polyC_mulrz (deprecated since 2.1.0)
  • definition Znat (deprecated since 2.1)
  • lemmas Znat_def, ZnatP (deprecated since 2.1)
  • archiDomainType instance for int (moved to archimedean.v)

• in fraction.v

  • notation tofracX (deprecated since 1.17)

• in interval.v

  • notations in_segment_addgt0Pr and in_segment_addgt0Pl (deprecated since 1.17)

• in mxrepresentation.v

  • notation mxval_grootX (deprecated since 1.17)

• in div.v

  • definition gcdn_rec, use gcdn directly

• in binomial.v

  • definition binomial_rec, use binomial directly

• in bigop.v

  • definition oAC_subdef, use oAC directly

• in fingroup.v

  • definition expgn_rec, use expgn directly

• in polydiv.v

  • definition gcdp_rec, use gcdp directly
  • notation modp_mod (deprecated since 2.1.0)

• in nilpotent.v

  • definition lower_central_at_rec, use lower_central_at directly
  • definition upper_central_at_rec, use upper_central_at directly

• in commutator.v

  • definition derived_at_rec, use derived_at directly

• in binomial.v

  • lemma textbook_triangular_sum

• in eqtype.v

  • notations [eqType of T], [eqType of T for C], and [eqMixin of T by <:]
  • notations sub, subK, sub_spec, and subP
  • notations InjEqMixin, PcanEqMixin, and CanEqMixin

• in choice.v

  • notations [hasChoice of T], [choiceType of T], [choiceType of T for C], and [choiceMixin of T by <:]
  • notations [isCountable of T], [countType of T], [countType of T for C], [countMixin of T by <:], and [subCountType of T]
  • notations CanChoiceMixin, PcanChoiceMixin, CanCountMixin, and PcanCountMixin

• in fintype.v

  • notations [finType of T], [finType of T for C], [subFinType of T], [finMixin of T by <:]
  • notations EnumMixin, UniqMixin, CountMixin, FinMixin, UniqFinMixin, PcanFinMixin, and CanFinMixin

• in generic_quotient.v

  • notations [quotType of Q] and [eqQuotType e of Q]

• in order.v

  • notations 0%O, 1%O, 0^d%O and 1^d%O (deprecated since 1.17)
  • notations [porderType of T], [porderType of T with disp], [porderType of T for cT], and [porderType of T for cT with disp]
  • notations [latticeType of T], [latticeType of T with disp], [latticeType of T for cT], and [latticeType of T for cT with disp]
  • notations [bLatticeType of T] and [bLatticeType of T for cT]
  • notation [bDistrLatticeType of T]
  • notation [tbDistrLatticeType of T]
  • notation [finPOrderType of T]
  • notation [finLatticeType of T]
  • notation [finDistrLatticeType of T]
  • notation [finCDistrLatticeType of T]
  • notation [finOrderType of T]
  • notations sub, subKI, subIK, subxx, subKU, subUK, subUx, sub_eq0, meet_eq0E_sub, eq_sub, subxU, subx0, sub0x, subIx, subxI, subBx, subxB, disj_subl, disj_subr, sub1x, subE, tnth_sub, and subEtpred
  • notations PcanPartial, CanPartial, PcanTotal, CanTotal, MonoTotalMixin, PcanPOrderMixin, CanPOrderMixin, PcanOrderMixin, CanOrderMixin, IsoLatticeMixin, IsoDistrLatticeMixin
  • notations comparable_le_minr, comparable_le_minl, comparable_lt_minl, comparable_lt_minr, comparable_le_maxr, comparable_le_maxl, comparable_lt_maxr, comparable_lt_maxl, le_maxl, le_maxr, lt_maxl, lt_maxr, lt_minr, lt_minl, le_minr, le_minl (deprecated since 2.1.0)
  • lemmas dual_lt_def, dual_le_anti, dual_total, Order.BoolOrder.subKI, Order.BoolOrder.joinIB
  • definition Order.BoolOrder.sub

• in fingroup.v

  • notations [finGroupType of T] and [baseFinGroupType of T]

• in ssralg.v

  • notation rmorphX (deprecated since 1.17)
  • notations [nmodType of T for cT] and [nmodType of T]
  • notation ZmodMixin
  • notations [zmodType of T for cT] and [zmodType of T]
  • notations [semiRingType of T] and [semiRingType of T for cT]
  • notations [ringType of T] and [ringType of T for cT]
  • notations [lmodType R of T] and [lmodType R of T for cT]
  • notations [lalgType R of T] and [lalgType R of T for cT]
  • notations [comSemiRingType of T] and [comSemiRingType of T for cT]
  • notations [comRingType of T] and [comRingType of T for cT]
  • notations [algType R of T] and [algType R of T for cT]
  • notation [comAlgType R of T]
  • notations [unitRingType of T] and [unitRingType of T for cT]
  • notation [comUnitRingType of T]
  • notation [unitAlgType R of T]
  • notation [comUnitAlgType R of T]
  • notations [idomainType of T] and [idomainType of T for cT]
  • notations [fieldType of T] and [fieldType of T for cT]
  • notations [decFieldType of T] and [decFieldType of T for cT]
  • notations [closedFieldType of T] and [closedFieldType of T for cT]
  • definition Additive.apply_deprecated
  • notation Additive.apply
  • notations [additive of f] and [additive of f as g]
  • notations [rmorphism of f] and [rmorphism of f as g]
  • definition Linear.apply_deprecated
  • notation Linear.apply
  • notations [linear of f] and [linear of f as g]
  • definition LRMorphism.apply_deprecated
  • notation LRMorphism.apply
  • notation [lrmorphism of f]

• in ring_quotient.v

  • notation [zmodQuotType z, o & a of Q]
  • notation [ringQuotType o & m of Q]
  • notation [unitRingQuotType u & i of Q]

• in countalg.v

  • notation [countNmodType of T]
  • notation [countZmodType of T]
  • notation [countSemiRingType of T]
  • notation [countRingType of T]
  • notation [countComSemiRingType of T]
  • notation [countComRingType of T]
  • notation [countUnitRingType of T]
  • notation [countComUnitRingType of T]
  • notation [countIdomainType of T]
  • notation [countFieldType of T]
  • notation [countDecFieldType of T]
  • notation [countClosedFieldType of T]

• in finalg.v

  • notation [finNmodType of T]
  • notation [finZmodType of T]
  • notation [finSemiRingType of T]
  • notation [finRingType of T]
  • notation [finComSemiRingType of T]
  • notation [finComRingType of T]
  • notation [finUnitRingType of T]
  • notation [finComUnitRingType of T]
  • notation [finIntegralDomainType of T]
  • notation [finFieldType of T]
  • notation [finLmodType R of T]
  • notation [finLalgType R of T]
  • notation [finAlgType R of T]
  • notation [finUnitAlgType R of T]
  • notation finIntegralDomainType (deprecated since 2.1.0)

• in ssrnum.v

  • notations [numDomainType of T] and [numDomainType of T for cT]
  • notation [numFieldType of T]
  • notations [numClosedFieldType of T] and [numClosedFieldType of T for cT]
  • notation [realDomainType of T]
  • notation [realFieldType of T]
  • notations [rcfType of T] and [rcfType of T for cT]
  • notations [archiFieldType of T] and [archiFieldType of T for cT]

• in rat.v

  • lemma divq_eq_deprecated
  • definitions Qint and Qnat (deprecated since 2.1)
  • lemmas QintP, Qnat_def, QnatP (deprecated since 2.1)

• in vector.v

  • notations [vectType R of T] and [vectType R of T for cT]

• in falgebra.v

  • notations [FalgType F of L] and [FalgType F of L for L']
  • notation FalgUnitRingType

• in fieldext.v

  • notations [fieldExtType F of L] and [fieldExtType F of L for K]

• in galois.v

  • notations [splittingFieldType F of L] and [splittingFieldType F of L for K]

• in algC.v

  • notations Cint, Cnat, floorC, truncC (deprecated in 2.1)
  • lemmas Creal0, Creal1, floorC_itv, floorC_def, intCK, floorCK, floorC0, floorC1, floorCpK, floorCpP, Cint_int, CintP, floorCD, floorCN, floorCM, floorCX, rpred_Cint, Cint0, Cint1, Creal_Cint, conj_Cint, Cint_normK, CintEsign, truncC_itv, truncC_def, natCK, CnatP, truncCK, truncC_gt0, truncC0Pn, truncC0, truncC1, truncCD, truncCM, truncCX, rpred_Cnat, Cnat_nat, Cnat0, Cnat1, Cnat_ge0, Cnat_gt0, conj_Cnat, norm_Cnat, Creal_Cnat, Cnat_sum_eq1, Cnat_mul_eq1, Cnat_prod_eq1, Cint_Cnat, CintE, Cnat_norm_Cint, CnatEint, CintEge0, Cnat_exp_even, norm_Cint_ge1, sqr_Cint_ge1, Cint_ler_sqr, aut_Cnat, aut_Cint, Cnat_aut, Cint_aut, raddfZ_Cnat, raddfZ_Cint, rpredZ_Cnat, rpredZ_Cint (deprecated in 2.1)

Deprecated

• in ssreflect.v

  • notation nosimpl since Arguments def : simpl never does the job with Coq >= 8.18

• in ssrfun.v

  • notation scope fun_scope, use function_scope instead
  • definition idempotent (is now idempotent_op)

• in vector.v

  • notation vector_axiom, use Vector.axiom instead

• in ssrnat.v

  • definition addn_rec, use addn directly
  • definition subn_rec, use subn directly
  • definition muln_rec, use muln directly
  • definition expn_rec, use expn directly
  • definition fact_rec, use factorial directly
  • definition double_rec, use double directly

• in poly.v

  • lemma size_Xn_sub_1, use size_XnsubC instead
  • lemma monic_Xn_sub_1, use monic_XnsubC instead

• in binomial.v

  • lemma triangular_sum, use bin2_sum instead
  • lemma Pascal, use expnDn instead

• in zmodp.v

  • lemmas big_ord1, big_ord1_cond

• in order.v

  • lemma complE, use complEdiff instead
  • factory hasRelativeComplement, use BDistrLattice_hasSectionalComplement instead
  • factory hasComplement, use CBDistrLattice_hasComplement instead

• in ssrnum.v:

  • lemma mulr_sg_norm (use numEsg instead)
  • lemma eqr_norm_id (use ger0_def instead)
  • lemma eqr_normN (use ler0_def instead)
  • lemma real_mulr_sign_norm (use realEsign instead)

• in archimedean.v

  • structure archiDomainType and its HB class Num.ArchiDomain (use archiRealDomainType and Num.ArchiRealDomain instead, respectively)
  • structure archiFieldType and its HB class Num.ArchiField (use archiRealFieldType and Num.ArchiRealField instead, respectively)

[2.2.0] - 2024-01-17

This release is compatible with Coq versions 8.16, 8.17, 8.18 and 8.19.

The contributors to this version are:

Reynald Affeldt, Cyril Cohen, Pierre Pomeret-Coquot, Pierre Roux, Kazuhiko Sakaguchi, Julin Shaji, Laurent Théry

Added

• in finset.v

  • lemmas big_set1E, big_imset_idem.

• in order.v

  • lemmas bigmin_mkcondl, bigmin_mkcondr, bigmax_mkcondl, bigmax_mkcondr, bigmin_le_id, bigmax_ge_id, bigmin_eq_id, bigmax_eq_id, bigminUl, bigminUr, bigmaxUl, bigmaxUr, bigminIl, bigminIr, bigmaxIl, bigmaxIr, bigminD, bigmaxD, bigminU, bigmaxU, bigmin_set1, bigmax_set1, bigmin_imset, bigmax_imset.

• in vector.v

  • lemma dim_matrix

Changed

• Notations declared in the fun_scope are now declared in the function_scope.

• in ssrfun.v

  • %FUN is changed from the delimiter of fun_scope to that of function_scope
  • fun_scope is closed

• in finset.v

  • generalized lemmas big_set0 and big_set from semigroups to arbitrary binary operators
  • definitions set_of and setTfor (phantom trick now useless with reverse coercions)

• in fingroup.v

  • definitions group_of, group_setT, setT_group (phantom trick now useless with reverse coercions)

• in perm.v

  • definition perm_of (phantom trick now useless with reverse coercions)

• in generic_quotient.v

  • pi_phant -> pi_subdef
  • quot_type_subdef -> quot_type_of

• in ssralg.v

  • definitions char, null_fun_head, in_alg_head (phantom trick now useless with reverse coercions)

• in finalg.v

  • definitions unit_of (phantom trick now useless with reverse coercions)

• in ssrnum.v

  • generalize ler_sqrt
  • generalize ler_psqrt to use nneg instead of pos

• in matrix.v

  • definitions GLtype, GLval, GLgroup and GLgroup_group (phantom trick now useless with reverse coercions)

• in alt.v

  • definitions Sym, Sym_group, Alt, Alt_group (phantom trick now useless with reverse coercions)

• in vector.v

  • definitions vector_axiom_def, space, vs2mx, pred_of_vspace (phantom trick now useless with reverse coercions)

• in fieldext.v

  • definition baseField_type (phantom trick now useless with reverse coercions)

• in qpoly.v

  • definitions polyn (phantom trick now useless with reverse coercions)

Renamed

• in ring_quotient.v

  • Quotient.type -> Quotient.quot

• in qpoly.v

  • npoly_of -> npoly (and removed phantom)
  • NPoly_of -> NPoly (and removed phantom)
  • npoly -> mk_npoly

Removed

• in eqtype.v

  • definition sub_type_of (phantom trick now useless with reverse coercions)

• in order.v

  • definition SetSubsetOrder.type_of (phantom trick now useless with reverse coercions)

• in ring_quotient.v

  • definition Quotient.type_of (phantom trick now useless with reverse coercions)

• in poly.v

  • definition poly_of (phantom trick now useless with reverse coercions)

• in fraction.v

  • definition ratio_of (phantom trick now useless with reverse coercions)
  • definition FracField.type_of (phantom trick now useless with reverse coercions)

• in falgebra.v

  • definition aspace_of (phantom trick now useless with reverse coercions)

Deprecated

• in ssrfun.v

  • notation scope fun_scope, use function_scope instead

• in vector.v

  • notation vector_axiom, use Vector.axiom instead

[2.1.0] - 2023-10-24

This release is compatible with Coq versions 8.16, 8.17, and 8.18.

The contributors to this version are:

Reynald Affeldt, Sophie Bernard, Alessandro Bruni, Fernando Chu, Cyril Cohen, Josh Cohen, Hugo Deleye, Jason Gross, Pierre Jouvelot, Erik Martin-Dorel, Pierre Roux, Kazuhiko Sakaguchi, Julin Shaji, Enrico Tassi, Laurent Théry, Quentin Vermande

Added

• in ssrbool.v

  • lemma relpre_trans

• in ssrnat.v

  • lemma addn_eq1, ltn_min

• in seq.v

  • lemma foldl_foldr
  • lemmas unzip1_map_nth_zip, unzip2_map_nth_zip, perm_zip_sym, perm_zip1, perm_zip2
  • lemmas find_pred0, find_predT
  • lemmas sumn_ncons, sumn_set_nth, sumn_set_nth_ltn, sumn_set_nth0
  • lemma rem_mem
  • lemmas allrel_revl, allrel_revr, allrel_rev2, eq_allrel_meml, eq_allrel_memr, eq_allrel_mem2

• in fintype.v

  • definitions ordS, ord_pred
  • lemmas ordS_subproof, ord_pred_subproof, ordSK, ord_predK, ordS_bij, ordS_inj, ord_pred_bij, ord_pred_inj

• in order.v

  • factory SubPOrder_isSubOrder
  • notations [SubPOrder_isSubOrder of U by <: with disp] and [SubPOrder_isSubOrder of U by <:]

• in bigop.v

  • lemma big_if
  • lemmas sum_nat_seq_eq0, sum_nat_seq_neq0, sum_nat_seq_eq1, sum_nat_eq1, prod_nat_seq_eq0, prod_nat_seq_neq0, prod_nat_seq_eq1, prod_nat_seq_neq1
  • lemma big_condT

• in finset.v

  • lemmas bigA_distr, subset_cons, subset_cons2, subset_catl, subset_catr, subset_cat2, filter_subset, subset_filter, map_subset.

• in ssralg.v

  • semiRingType instance for nat
  • RMorphism instance for GRing.natmul
  • lemmas natr0E, natr1E, natn, natrDE, natrME, natrXE
  • multirule natrE
  • support for negative constant (like -42) in the Number Notation in ring_scope

• in finalg.v

  • lemmas card_finRing_gt1, card_finField_unit

• in zmodp.v

  • lemmas add_1_Zp, add_Zp_1, sub_Zp_1 and add_N1_Zp.

• in poly.v

  • multirule coefE
  • lemmas deg2_poly_canonical, deg2_poly_factor, deg2_poly_root1, deg2_poly_root2, FieldMonic.deg2_poly_canonical, FieldMonic.deg2_poly_factor, FieldMonic.deg2_poly_root1, FieldMonic.deg2_poly_root2
  • lemmas polyC_natr, char_poly

• in polydiv.v

  • lemmas rmodp_id, rmodpN, rmodpB, rmodpZ, rmodp_sum, rmodp_mulml, rmodpX, rmodp_compr

• in ssrnum.v

  • lemmas NumClosed.deg2_poly_factor, NumClosed.deg2_poly_root1, NumClosed.deg2_poly_root2, NumClosedMonic.deg2_poly_factor, NumClosedMonic.deg2_poly_root1, NumClosedMonic.deg2_poly_root2, Real.deg2_poly_min, Real.deg2_poly_minE, Real.deg2_poly_gt0, Real.deg2_poly_ge0, Real.deg2_poly_max, Real.deg2_poly_maxE, Real.deg2_poly_lt0, Real.deg2_poly_le0, Real.deg2_poly_factor, Real.deg2_poly_root1, Real.deg2_poly_root2, Real.deg2_poly_noroot, Real.deg2_poly_gt0l, Real.deg2_poly_gt0r, Real.deg2_poly_lt0m, Real.deg2_poly_ge0l, Real.deg2_poly_ge0r, Real.deg2_poly_le0m, Real.deg2_poly_lt0l, Real.deg2_poly_lt0r, Real.deg2_poly_gt0m, Real.deg2_poly_le0l, Real.deg2_poly_le0r, Real.deg2_poly_ge0m, RealMonic.deg2_poly_min, RealMonic.deg2_poly_minE, RealMonic.deg2_poly_gt0, RealMonic.deg2_poly_ge0, RealMonic.deg2_poly_factor, RealMonic.deg2_poly_root1, RealMonic.deg2_poly_root2, RealMonic.deg2_poly_noroot, RealMonic.deg2_poly_gt0l, RealMonic.deg2_poly_gt0r, RealMonic.deg2_poly_lt0m, RealMonic.deg2_poly_ge0l, RealMonic.deg2_poly_ge0r, RealMonic.deg2_poly_le0m, deg_le2_poly_delta_ge0, deg_le2_poly_delta_le0, deg_le2_poly_ge0, deg_le2_poly_le0
  • structures archiNumDomainType, archiNumFieldType, archiCLosedFieldType, archiDomainType, archiFieldType, archiRcfType
  • factory NumDomain_bounded_isArchimedean (renamed from RealDomain_isArchimedean)
  • lemmas truncP, trunc_itv
  • lemmas gerBl, gtrBl
  • definition Num.npos and lemma nposrE
  • lemmas ger0_le_norm, gtr0_le_norm, ler0_ge_norm and ltr0_ge_norm

• in ssrint.v

  • RMorphism instance for Posz

• in rat.v

  • lemmas floor_rat, ceil_rat

• in cyclic.v

  • added lemma units_Zp_cyclic

• new file archimedean.v

• in archimedean.v

  • new structures archiNumDomainType, archiNumFieldType, archiClosedFieldType, archiDomainType, archiRcfType
  • structure archiFieldType (renamed from archimedeanFieldType from ssrnum.v)
  • notations Num.trunc, Num.floor Num.ceil, Num.nat, Num.int
  • notation Num.bound (moved from ssrnum.v)
  • lemmas trunc_itv, natrE, trunc_def, natrK, truncK, trunc0, trunc1, natr_nat, natrP, truncD, truncM, truncX, rpred_nat_num, nat_num0, nat_num1, nat_num_semiring, Rreal_nat, natr_normK, trunc_gt0, trunc0Pn, natrge0, natrgt0, norm_natr, natrsum_eq1, natr_mul_eq1, natr_prod_eq1, floorP, intrE, floor_itv, ge_floor, lt_succ_floor, floor_def, floor_ge_int, floor_le, intrKfloor, intr_int, intrP, intrEfloor, floorK, floor0, floor1, floorD, floorN, floorM, floorX, ceil_itv, gt_pred_ceil, le_ceil, ceil_def, ceil_le_int, ceil_le, intrKceil, intrEceil, ceilK, ceil0, ceil1, ceilD, ceilN, ceilM, ceilX, ceil_floor, rpred_int_num, int_num0, int_num1, int_num_subring, intr_nat, Rreal_int, intr_normK, intrEsign, natr_norm_int, natrEint, intrEge0, natr_exp_even, norm_intr_ge1, sqr_intr_ge1, intr_ler_sqr, floorpK, floorpP, trunc_floor, raddfZ_nat, rpredZ_nat, raddfZ_int, rpredZ_int, aut_natr, aut_intr, natr_aut_nu, intr_aut_nu, conj_natr, conj_intr
  • lemmas archi_boundP, upper_nthrootP (moved from ssrnum.v)
  • lemmas Znat_def, ZnatP (moved from ssrint.v)
  • instances of SemiringClosed for Num.nat and Num.int
  • lemmas sum_truncK, prod_truncK

• in qpoly.v

  • new file of algebra that defines the algebras R[X]/<p> and their theory.
  • definitions {poly_n R}, 'nX^m, x.-lagrange, x.lagrange_n, {poly %/ p }, 'qX, irreducibleb, mk_monic, in_qpoly
  • lemmas size_npoly, npolyP, coef_npolyp big_coef_npoly, npolypK, coefn_sum npoly_enum_uniq, mem_npoly_enum, card_npoly irreducibleP, dim_polyn , npolyXE, nth_npolyX, npolyX_free, npolyX_full, npolyX_coords, coord npolyX, npolyX_gen, lagrangeE, nth_lagrange, size_lagrange_, size_lagrange, lagrange_sample, lagrange_free, lagrange_full, lagrange_coords, lagrange_gen, monic_mk_monic, size_mk_monic_gt1, size_mk_monic_gt0, mk_monic_neq0, size_mk_monic, poly_of_size_mod, in_qpoly0, in_qpolyD, in_qpolyZ, card_monic_qpoly, in_qpoly1, in_qpolyM, in_qpoly_small, qpolyC_proof, qpolyCE, qpolyC0, qpoly_mul1z, qpoly_mulz1, qpoly_nontrivial, qpolyXE, mk_monic_X, mk_monic_Xn, card_qpoly, qpoly_mulC, qpoly_mulA, qpoly_mul_addr, qpoly_mul_addl, poly_of_qpoly_sum, poly_of_qpolyD, qpolyC_natr, char_qpoly, poly_of_qpolyM, poly_of_qpolyX, qpolyCN, qpolyC, qpolyCD, qpolyCM, qpolyC_is_rmorphism, poly_of_qpolyZ, qpoly_mulVz, qpoly_mulzV, qpoly_intro_unit, qpoly_inv_out, irreducible_poly_coprime

• in qfpoly.v

  • new file of field that extends the algebras R[X]/

    defined in qpoly with the field when p is irreducible

  • definitions monic_irreducible_poly, {poly' %/ p with mi}, primitive_poly, qlogp, plogp
  • lemmas mk_monicE, coprimep_unit, qpoly_mulVp, qpoly_inv0, qpoly_inv, in_qpoly_comp_horner, map_poly_div_inj, map_fpoly_div_inj, card_qfpoly, card_qfpoly_gt1, primitive_polyP, primitive_poly_in_qpoly_eq0, card_primitive_qpoly, primitive_mi, qX_neq0 qX_in_unit, dvdp_order, gX_order, gX_all, qlogp_lt, qlogp_qX, qX_order_card, qX_order_dvd, qlogp0, qlogp1, qlogp_eq0, qlogpD, qX_exp_neq0, qX_exp_inj, powX_eq_mod, qX_expK, plogp_lt, plogp_X, plogp0, plogp1, plogp_div_eq0, plogpD

• in algC.v

  • lemma Implementation.archimedean
  • instance of archiClosedFieldType on Implementation.type

Changed

• in order.v

  • make [Order of T by <:] compatible with the SubOrder hierarchy

• in ssralg.v

  • implicits of natr1 and nat1r
  • implicits of Linear.type, use the {linear _ -> _} notation for compatibility
  • implicits of RMorphism.type, use the {rmorphism _ -> _} notation for compatibility
  • implicits of LRMorphism.type, use the {lrmorphism _ -> _} notation for compatibility
  • fixed (generalized) the comSemiRingType instance for prod

Renamed

• in order.v

  • le_maxl -> ge_max
  • le_maxr -> le_max
  • lt_maxr -> lt_max
  • lt_maxl -> gt_max
  • lt_minr -> lt_min
  • lt_minl -> gt_min
  • le_minr -> le_min
  • le_minl -> ge_min
  • comparable_le_maxr -> comparable_le_max
  • comparable_le_maxl -> comparable_ge_max
  • comparable_lt_maxr -> comparable_lt_max
  • comparable_lt_maxl -> comparable_gt_max
  • comparable_lt_minl -> comparable_gt_min
  • comparable_lt_minr -> comparable_lt_min
  • comparable_le_minr -> comparable_le_min
  • comparable_le_minl -> comparable_ge_min

• in polydiv.v

  • modp_mod -> modp_id

• in algC.v

  • Cint -> Num.int
  • Cnat -> Num.nat
  • floorC -> Num.floor
  • truncC -> Num.trunc
  • Creal0 -> real0
  • Creal1 -> real1
  • floorC_itv -> floor_itv
  • floorC_def -> floor_def
  • intCK -> intrKfloor
  • floorCK -> floorK
  • floorC0 -> floor0
  • floorC1 -> floor1
  • floorCpK -> floorpK
  • floorCpD -> floorpP
  • Cint_int -> intr_int
  • CintP -> intrP
  • floorCD -> floorD
  • floorCN -> floorN
  • floorCM -> floorM
  • floorCX -> floorX
  • rpred_Cint -> rpred_int_num
  • Cint0 -> int_num0
  • Cint1 -> int_num1
  • Creal_Cint -> Rreal_int
  • conj_Cint -> conj_intr
  • Cint_normK -> intr_normK
  • CintEsign -> intrEsign
  • truncC_itv -> trunc_itv
  • truncC_def -> trunc_def
  • natCK -> natrK
  • CnatP -> natrP
  • truncCK -> truncK
  • truncC_gt0 -> trunc_gt0
  • truncC0Pn -> trunc0Pn
  • truncC0 -> trunc0
  • truncC1 -> trunc1
  • truncCD -> truncD
  • truncCM -> truncM
  • truncCX -> truncX
  • rpred_Cnat -> rpred_nat_num
  • Cnat_nat -> natr_nat
  • Cnat0 -> nat_num0
  • Cnat1 -> nat_num1
  • Cnat_ge0 -> natr_ge0
  • Cnat_gt0 -> natr_gt0
  • conj_Cnat -> conj_natr
  • norm_Cnat -> norm_natr
  • Creal_Cnat -> Rreal_nat
  • Cnat_sum_eq1 -> natr_sum_eq1
  • Cnat_mul_eq1 -> natr_mul_eq1
  • Cnat_prod_eq1 -> natr_prod_eq1
  • Cint_Cnat -> intr_nat
  • CintE -> intrE
  • Cnat_norm_Cint -> natr_norm_int
  • CnatEint -> natrEint
  • CintEge0 -> intrEge0
  • Cnat_exp_even -> natr_exp_even
  • norm_Cint_ge1 -> norm_intr_ge1
  • sqr_Cint_ge1 -> sqr_intr_ge1
  • Cint_ler_sqr -> intr_ler_sqr
  • aut_Cnat -> aut_natr
  • aut_Cint -> aut_intr
  • Cnat_aut -> natr_aut
  • Cint_aut -> intr_aut
  • raddfZ_Cnat -> raddfZ_nat
  • raddfZ_Cint -> raddfZ_int
  • rpredZ_Cnat -> rpredZnat
  • rpredZ_Cint -> rpredZint

Removed

• in ssrbool.v

  • rel_of_simpl_rel (use rel_of_simpl)

• in fintype.v

  • enum_ordS (use enum_ordSl instead)

• in ssrint.v

  • definition Znat_pred
  • lemma Znat_semiring_closed

• in rat.v

  • definition Qint_pred, Qnat_pred
  • lemmas rat_archimedean, Qint_subring_closed, Qnat_semiring_closed

• in algC.v

  • lemma floorC_subproof, Cnat_semiring

Deprecated

• in ssrnum.v

  • structures archiNumDomainType, archiNumFieldType, archiCLosedFieldType, archiDomainType, archiFieldType, archiRcfType (moved to archimedean.v)
  • factory RealField_isArchimedean renamed NumDomain_bounded_isArchimedean and moved to archimedean.v
  • factory NumDomain_bounded_isArchimedean (moved to archimedean.v)
  • notations Num.Def.trunc, Num.trunc, Num.Def.nat_num, Num.nat, Num.Def.int_num, Num.int, Num.bound (moved to archimedean.v)
  • lemmas archi_boundP, upper_nthrootP, truncP, trunc_itv (moved to archimedean.v)

• in ssrint.v

  • definition Znat (require archimedean.v and use Num.nat)
  • lemmas Znat_def, ZnatP (moved to archimedean.v)
  • lemma polyC_mulrz (use polyCMz)
  • mulrzDr temporarily deprecated, use mulrzDl_tmp instead, will eventually be renamed mulrzDl
  • mulrzDl temporarily deprecated, use mulrzDr_tmp instead, will eventually be renamed mulrzDr

• in rat.v

  • definitions Qint and Qnat (require archimedean.v and use Num.int and Num.nat)
  • lemma QintP (require archimedean.v and use intrP)
  • lemma Qnat_def (require archimedean.v and use natrEint)
  • lemma QnatP (require archimedean.v and use natrP)

[2.0.0] - 2023-05-10

This release is compatible with Coq versions 8.16 and 8.17.

The contributors to this version are:

Anton Trunov, Cyril Cohen, Enrico Tassi, Kazuhiko Sakaguchi, Laurent Théry, Marie Kerjean, Pierre Roux, Quentin Canu, Reynald Affeldt, Thomas Portet, Xavier Allamigeon, Yves Bertot

Added

• in eqtype.v

  • structure subEqType
  • notation \val

• in choice.v

  • notation subChoiceType, structure SubChoice

• in bigop.v

  • structures SemiGroup.law and SemiGroup.com_law

• in order.v

  • structures OrderMorphism, MeetLatticeMorphism, JoinLatticeMorphism, LatticeMorphism, BLatticeMorphism, TLatticeMorphism, TBLatticeMorphism, MeetLatticeClosed, JoinLatticeClosed, LatticeClosed, BLatticeClosed, BJoinLatticeClosed, TLatticeClosed, TMeetLatticeClosed, TBLatticeClosed, SubPOrder, SubPOrderLattice, SubPOrderBLattice, SubPOrderTLattice, SubPOrderTBLattice, MeetSubLattice, MeetSubBLattice, MeetSubTLattice, MeetSubTBLattice, JoinSubLattice, JoinSubBLattice, JoinSubTLattice, JoinSubTBLattice, SubLattice, SubBLattice, SubTLattice, SubTBLattice, BJoinSubLattice, BJoinSubTLattice, BSubLattice, BSubTLattice, TMeetSubLattice, TMeetSubBLattice, TSubLattice, TSubBLattice, TBSubLattice, SubOrder
  • predicate meet_morphism, join_morphism, meet_closed, join_closed

• in ssralg.v

  • structure nmodType (aka Monoid on a choiceType), semiRingType, comSemiRingType, subNmodType, subZmodType, subSemiRingType, subComSemiRingType, subRingType, subComRingType, subLmodType, subLalgType, subAlgType, subUnitRingType, subComUnitRingType, subIdomainType, subField
  • predicate semi_additive
  • predicate multiplicative
  • morphism semiring2Closed
  • morphism semiringClosed

• in finalg.v

  • structures finComSemiRingType, finSemiRingType and finZsemimodType

• in countalg.v

  • structures countComSemiRingType, countSemiRingType and countZsemimodType

• in ssrnum.v

  • structures porderZmodType

Changed

• in eqtype.v

  • structures eqType and subType ported to HB

• in choice.v

  • [choiceMixin of T by <:] becomes [Choice of T by <:]
  • [countMixin of T by <:] becomes [Countable of T by <:]
  • Choice.mixin_of becomes hasChoice
  • Countable.mixin_of becomes Choice_isCountable
  • ChoiceMixin becomes hasChoice.Build
  • CountMixin becomes Choice_isCountable.Build
  • CountChoiceMixin is subsumed by Equality_isCountable.Build (instead of two successive calls to CountChoiceMixin and CountMixin, only one to Equality_isCountable.Build is necessary)
  • CanChoiceMixin -> use Choice.copy with can_type or CanHasChoice
  • PcanChoiceMixin -> use Choice.copy with pcan_type or PCanHasChoice
  • CanCountMixin -> use Countable.copy with can_type or CanIsCountable
  • PcanCountMixin -> use Countable.copy with pcan_type or PCanIsCountable

• in generic_quotient.v

  • structures quotType and eqQuotType ported to HB

• in bigop.v

  • structures Monoid.law, Monoid.com_law, Monoid.mul_law and Monoid.add_law ported to HB

• in fintype.v

  • notations [seq F | x in A ] and [seq F | x ] now support destructuring patterns in binder positions. In the case of [seq F | x ] and [seq F | x : T ], type inference on x now occurs earlier, meaning that implicit types and typeclass resolution in T will take precedence over unification constraints arising from typechecking x in F. This may result in occasional incompatibilities.
  • structures finType and subFinType ported to HB

• in order.v

  • the structures POrder, Lattice, BLattice, TLattice, TBLattice, DistrLattice, BDistrLattice, TBDistrLattice, CBDistrLattice, CTBDDistrLattice, Total, FinPOrder, FinLattice, FinDistrLattice, FinCDistrLattice, FinTotal
  • PcanPOrderMixin is replaced by Order.PcanPartial
  • CanPOrderMixin is replaced by Order.CanPartial
  • MonoTotalMixin is replaced by MonoTotal
  • IsoLatticeMixin is replaced by Order.IsoLattice

• in ssralg.v

  • structures zmodType, ringType, lmodType, lalgType, comRingType, algType, comAlgType, unitRingType, comUnitRingType, unitAlgType, comUnitAlgType, idomainType, fieldType, decFieldType, closedFieldType ported to HB

  • morphisms additive and rmorphism ported to HB and generalized to nmodType and semiRingType respectively.

  • morphisms linear and lrmorphism ported to HB

  • predicates opprClosed, addrClosed, zmodClosed, mulr2Closed, mulrClosed, smulClosed, subringClosed, divClosed, sdivClosed, submodClosed, subalgClosed, divringClosed, divalgClosed ported to HB

• in finalg.v

  • structures finZmodType, finRingType, finComRingType, finUnitRingType, finComUnitRingType, finIdomType, finFieldType, finLmodType, finLalgType, finAlgType, finUnitAlgType ported to HB

• in countalg.v

  • structures countZmodType, countRingType, countComRingType, countUnitRingType, countComUnitRingType, countIdomainType, countFieldType, countDecFieldType, countClosedFieldType ported to HB

• in ssrnum.v

  • structures normedZmodType, numDomainType, numFieldType, numFieldType, numClosedFieldType, realDomainType, realFieldType, archiFieldType, rcfType ported to HB

• in ring_quotient.v

  • structures zmodQuotType, ringQuotType and unitRingQuotType have been ported to HB.
  • structures proper_ideal, idealr and primeIdealr have been ported to HB.

• in fingroup.v

  • structures baseFinGroupType and finGroupType ported to HB

• in finfield.v

  • structure fieldExtType ported to HB
  • module FinVector removed in favor of alias (feather factory) finvect_type

• in fieldext.v

  • structure fieldExtType ported to HB

• in falgebra.v

  • structure falgType ported to HB

• in closed_field.v

  • notation closed_field_QEMixin, use Field_isAlgClosed.Build

• in galois.v

  • structure splittingFieldType ported to HB

Renamed

• in choice.v

  • choiceMixin -> hasChoice
  • sub_choiceMixin -> sub_hasChoice
  • seq_choiceMixin -> seq_hasChoice
  • tagged_choiceMixin -> tagged_hasChoice
  • nat_choiceMixin -> nat_hasChoice

• in order.v

  • [porderMixin of T by <:] -> [POrder of T by <:]
  • [totalOrderMixin of T by <:] -> [Order of T by <:]
  • sub -> diff
  • subKI -> diffKI
  • subIK -> diffIK
  • subxx -> diffxx
  • subKU -> diffKU
  • subUK -> diffUK
  • subUx -> diffUx
  • sub_eq0 -> diff_eq0
  • meet_eq0E_sub -> meet_eq0E_diff
  • eq_sub -> eq_diff
  • subxU -> diffxU
  • subx0 -> diffx0
  • sub0x -> diff0x
  • subIx -> diffIx
  • subxI -> diffxI
  • subBx -> diffBx
  • subxB -> diffxB
  • disj_subl -> disj_diffl
  • disj_subr -> disj_diffr
  • sub1x -> diff1x
  • subE -> diffE
  • tnth_sub -> tnth_diff
  • subEtprod -> diffEtprod
  • PcanPartial -> PCanIsPartial
  • CanPartial -> CanIsPartial
  • PcanTotal -> PCanIsTotal
  • CanTotal -> CanIsTotal

• in ssralg.v

  • *Pred -> *Closed
  • notation [zmodMixin of M by <:], use [SubChoice_isSubZmodule of U by <:]
  • notation [ringMixin of R by <:], use [SubZmodule_isSubRing of U by <:]
  • notation [comRingMixin of R by <:], use [SubZmodule_isSubComRing of U by <:]
  • notation [unitRingMixin of R by <:], use [SubRing_isSubUnitRing of U by <:]
  • notation [comUnitRingMixin of R by <:], use [SubChoice_isSubComUnitRing of U by <:]
  • notation [idomainMixin of R by <:], use [SubComUnitRing_isSubIntegralDomain of U by <:]
  • notation [fieldMixin of R by <:], use [SubIntegralDomain_isSubField of U by <:]
  • notation [lmodMixin of R by <:], use [SubZmodule_isSubLmodule of U by <:]
  • notation [lalgMixin of R by <:], use [SubRing_SubLmodule_isSubLalgebra of U by <:]
  • notation [algMixin of R by <:], use [SubLalgebra_isSubAlgebra of U by <:]

• in ssrnum.v

  • notation NormedZmodType, use Zmodule_isNormed.Build
  • notation NumDomainType, use isNumRing.Build
  • notation NumClosedFieldType, use NumField_isImaginary.Build
  • notation ArchiFieldType, use RealField_isArchimedean.Build
  • notation RcfType, use RealField_isClosed.Build

• in falgebra.v

  • structure FalgType -> falgType
  • notation FalgUnitRingType, use Algebra_isFalgebra.Build

• in galois.v

  • definition SplittingField.axiom -> splitting_field_axiom
  • notation SplittingFieldType, use FieldExt_isSplittingfield.Build

Removed

• in eqtype.v

  • definitions tuple_eqMixin, tuple_choiceMixin, tuple_countMixin, tuple_finMixin, bseq_eqMixin, bseq_choiceMixin, bseq_countMixin, bseq_finMixin
  • notation EqMixin, use hasDecEq.Build
  • notation [eqMixin of T], use Equality.on T
  • unit_eqMixin and unit_eqType, use unit : eqType
  • bool_eqMixin and bool_eqType, use bool : eqType
  • void_eqMixin and void_eqType, use void : eqType
  • sig_eqMixin and sig_eqType, use {x | P x} : eqType
  • prod_eqMixin and prod_eqType, use (T1 * T2)%type : eqType
  • option_eqMixin and option_eqType, use option T : eqType
  • tag_eqMixin and tag_eqType, use {i : I & T_ i} : eqType
  • sum_eqMixin and sum_eqType, use (T1 + T2)%type : eqType
  • definition clone_subType, use SubType.clone
  • notation [subType for v], use [isSub for v]
  • notation [subType for v by rec], use [isSub for v by rec]
  • notation [subType of T for v], use [isSub of T for v]
  • notation [subType of T], use SubType.clone T _
  • definition NewType
  • notation [newType for v], use [isNew for v]
  • notation [newType for v by rec], use [isNew for v by rec]
  • definition sig_subType, use sig P : subType
  • definitions sub_eqMixin, sub_eqType and SubEqMixin, use alias sub_type
  • notation EqType

• in choice.v

  • ChoiceType
  • CountType
  • sub_choiceClass, sub_choiceType
  • seq_choiceType (use seq _ : choiceType instead, the same applies for other *_choiceType's)
  • tagged_choiceType
  • nat_choiceType
  • bool_choiceMixin, bool_choiceType, bitseq_choiceType, unit_choiceMixin, unit_choiceType, void_choiceMixin, void_choiceType, option_choiceMixin, option_choiceType, sig_choiceMixin, sig_choiceType, prod_choiceMixin, prod_choiceType, sum_choiceMixin, sum_choiceType, tree_choiceMixin, tree_choiceType
  • sub_countMixin
  • seq_countMixin, seq_countType, tag_countMixin, tag_countType, nat_countMixin, nat_countType, bool_countMixin, bool_countType, bitseq_countType, unit_countMixin, unit_countType, void_countMixin, void_countType, option_countMixin, option_countType, sig_countMixin, sig_countType, sig_subCountType, prod_countMixin, prod_countType, sum_countMixin, sum_countType, tree_countMixin, tree_countType
  • CountChoiceMixin

• in generic_quotient.v

  • notation QuotClass, use isQuotient.Build
  • notation EqQuotType, use isEqQuotient.Build

• in fintype.v

  • definition adhoc_seq_sub_choiceMixin

• in order.v

  • LtOrderMixin (see factory LtOrder)
  • OrderType
  • POrderType
  • LatticeType
  • BLatticeType
  • TBLatticeType
  • DistrLatticeType
  • CBDistrLatticeType
  • CTBDistrLatticeType
  • factory lePOrderMixin (use factory isLePOrdered instead)
  • factory ltPOrderMixin (use factory isLtPOrdered instead)
  • factory latticeMixin (use mixin POrder_isLattice instead)
  • factory distrLatticeMixin (use mixin Lattice_MeetIsDistributive instead)
  • factory distrLatticePOrderMixin (use factory POrder_isMeetDistrLattice instead)
  • factory meetJoinMixin (use factory isMeetJoinDistrLattice instead)
  • factory meetJoinLeMixin (use factory POrder_isMeetJoinLattice instead)
  • factory leOrderMixin (use factory isOrdered instead)
  • factory ltOrderMixin (use factory LtOrder instead)
  • factory meetJoinLeMixin (use factory Porder_isMeetJoinLattice instead)
  • factory totalPOrderMixin (use factory POrder_isTotal instead)
  • factory totalLatticeMixin (use factory Lattice_isTotal instead)
  • factory totalOrderMixin (use factory DistrLattice_isTotal instead)
  • factory bottomMixin (use mixin hasBottom instead)
  • factory topMixin (use mixin hasTop instead)
  • factory cbDistrLatticeMixin (use mixin hasSub instead)
  • factory ctbDistrLatticeMixin (use mixin hasCompl instead)
  • DistrLatticeOfChoiceType (use isMeetJoinDistrLattice.Build and HB.pack instead), DistrLatticeOfPOrderType (use POrder_isMeetDistrLattice.Build) OrderOfChoiceType (use isOrdered.Build), OrderOfPOrder (use POrder_isTotal.Build), OrderOfLattice (use Lattice_isTotal.Build)

• in bigop.v

  • definition Monoid.clone_law, use Monoid.Law.clone
  • definition Monoid.clone_com_law, use Monoid.ComLaw.clone
  • definition Monoid.clone_mul_law, use Monoid.MulLaw.clone
  • definition Monoid.clone_add_law, use Monoid.AddLaw.clone
  • notation [law of f], use Monoid.Law.clone f _
  • notation [com_law of f], use f : Monoid.ComLaw.clone f _
  • notation [mul_law of f], use f : Monoid.MulLaw.clone f _
  • notation [add_law of f], use f : Monoid.AddLaw.clone f _
  • definitions andb_monoid and andb_comoid, use andb : Monoid.com_law
  • definitions andb_muloid
  • definitions orb_monoid and orb_comoid, use orb : Monoid.com_law
  • definitions orb_muloid
  • definitions addb_monoid and addb_comoid, use addb : Monoid.com_law
  • definitions orb_addoid, andb_addoid and addb_addoid
  • definitions addn_monoid and addn_comoid, use addn : Monoid.com_law
  • definitions muln_monoid and muln_comoid, use muln : Monoid.com_law
  • definitions addn_addoid
  • definitions maxn_monoid and maxn_comoid, use maxn : Monoid.com_law
  • definitions maxn_addoid
  • definitions gcdn_monoid and gcdn_comoid, use gcdn : Monoid.com_law
  • definitions gcdn_addoid
  • definitions lcmn_monoid and lcmn_comoid, use lcmn : Monoid.com_law
  • definitions lcmn_addoid
  • definitions cat_monoid, use cat : Monoid.law
  • lemma big_undup_AC, use big_undup
  • lemma perm_big_AC, use perm_big
  • lemma big_enum_cond_AC, use big_enum_cond
  • lemma big_enum_AC, use big_enum
  • lemma big_uniq_AC, use big_uniq
  • lemma bigD1_AC, use bigD1
  • lemma bigD1_seq_AC, use bigD1_seq
  • lemma big_image_cond_AC, use big_image_cond
  • lemma big_image_AC, use big_image
  • lemma reindex_omap_AC, use reindex_omap
  • lemma reindex_onto_AC, use reindex_onto
  • lemma reindex_AC, use reindex
  • lemma reindex_inj_AC, use reindex_inj
  • lemma bigD1_ord_AC, use bigD1_ord
  • lemma big_enum_val_cond_AC, use big_enum_val_cond
  • lemma big_enum_rank_cond_AC, use big_enum_rank_cond
  • lemma big_nat_rev_AC, use big_nat_rev
  • lemma big_rev_mkord_AC, use big_rev_mkord

• in ssralg.v

  • notation ZmodType, use isZmodule.Build
  • notation RingType, use Zmodule_isRing.Build
  • notation ComRingType, use hasCommutativeMul.Build
  • notation UnitRingType, use Ring_hasMulInverse.Build
  • notation UnitRingType, use Ring_hasMulInverse.Build
  • notation ComUnitRingMixin, use ComRing_hasMulInverse.Build
  • notation IdomainType, use ComUnitRing_isIntegral.Build
  • notation FieldMixin, use UnitRing_isField.Build
  • notation FieldType, use UnitRing_isField.Build
  • notation FieldUnitMixin, use ComRing_isField.Build
  • notation FieldIdomainMixin
  • notation GRing.Field.IdomainType, use ComRing_isField.Build
  • notation DecFieldMixin, use Field_isDecField.Build
  • notation QEdecFieldMixin, use Field_QE_isDecField.Build
  • notation ClosedFieldType, use DecField_isAlgClosed.Build
  • notation LmodMixin, use Zmodule_isLmodule.Build
  • notation LmodType, use Zmodule_isLmodule.Build
  • notation LalgType, use Lmodule_isLalgebra.Build
  • notation AlgType, use Lalgebra_isAlgebra.Build
  • notation ComAlgType, use Lalgebra_isAlgebra.Build
  • module GRing.DefaultPred
  • notation Additive, use isAdditive.Build
  • notation RMorphism, use Additive_isMultiplicative.Build
  • notation AddRMorphism, use Additive_isMultiplicative.Build
  • notation Linear, use isScalable.Build
  • notation AddLinear, use isScalable.Build
  • notation LRMorphism, use isScalable.Build
  • notation AddLRMorphism, use isScalable.Build

• in ring_quotient.v

  • removed MkIdeal and MkPrimeIdeal in favor of generic HB commands.

• in finalg.v

  • notation [baseFinGroupType of R for +%R]

• in vector.v

  • notation VectMixin and VectType, use Lmodule_hasFinDim.Build

Deprecated

• in eqtype.v

  • notation [eqType of T], use Equality.clone T _ or T : eqType
  • notation [eqType of T for C], use Equality.clone T C
  • definition InjEqMixin, use alias inj_type
  • definition CanEqMixin, use alias can_type
  • definition PCanEqMixin, use alias pcan_type
  • notation [eqMixin of T by <:], use [Equality of T by <:]

• in choice.v

  • notation [hasChoice of T], use Choice.on T
  • notation [choiceType of T for C], use Choice.clone T C
  • notation [choiceType of T], use Choice.clone T _ or T : choiceType
  • notation [choiceMixin of T by <:], use [Choice of T by <:]
  • notation [isCountable of T], use Countable.on T
  • notation [countType of T for C], use Countable.clone T C
  • notation [countType of T], use Countable.clone T _ or T : countType
  • notation [countMixin of T by <:], use [Countable of T by <:]
  • notation [subCountType of T], use SubCountable.clone _ _ T _

• in fintype.v

  • notation EnumMixin, use isFInite.Build
  • notation Finite.UniqMixin, use isFinite.Build and Finite.uniq_enumP
  • notation Finite.CountMixin, use isFinite.Build and Finite.count_enumP
  • notation FinMixin, use isFInite.Build
  • notation UniqFinMixin, use isFInite.Build and Finite.uniq_enumP
  • notation [finType of T for C], use Finite.clone T C
  • notation [finType of T], use Finite.clone T _ or T : finType
  • notation [subFinType of T], use SubFinite.clone T _
  • notation [finMixin of T by <:], use [Finite of T by <:]

• in order.v

  • notation [porderType of T for cT], use POrder.clone _ T cT
  • notation [porderType of T for cT with disp], use POrder.clone disp T cT
  • notation [porderType of T], use POrder.clone _ T _ or T : porderType
  • notation [porderType of T with disp], use POrder.clone disp T _
  • notation [latticeType of T for cT], use Lattice.clone _ T cT
  • notation [latticeType of T for cT with disp], use Lattice.clone disp T cT
  • notation [latticeType of T], use Lattice.clone _ T _ or T : latticeType
  • notation [latticeType of T with disp], use Lattice.clone disp T _
  • notation [bLatticeType of T for cT], use BLattice.clone _ T cT
  • notation [bLatticeType of T], use BLattice.clone _ T _ or T : bLatticeType
  • notation [bDistrLatticeType of T], use BDistrLattice.clone _ T _ or T : bDistrLatticeType
  • notation [tbDistrLatticeType of T], use TBDistrLattice.clone _ T _ or T : tbDistrLatticeType
  • notation [finPOrderType of T], use FinPOrder.clone _ T _ or T : finPOrderType
  • notation [finLatticeType of T], use FinLattice.clone _ T _ or T : finLatticeType
  • notation [finDistrLatticeType of T], use FinDistrLattice.clone _ T _ or T : finDistrLatticeType
  • notation [finCDistrLatticeType of T], use FinCDistrLattice.clone _ T _ or T : finCDistrLatticeType
  • notation [finOrderType of T], use FinTotal.clone _ T _ or T : finOrderType
  • notation PcanPartial, use PCanIsPartial
  • notation CanPartial, use CanIsPartial
  • notation PcanTotal, use PCanIsTotal
  • notation CanTotal, use CanIsTotal

• in generic_quotient.v

  • notation [quotType of Q], use Quotient.clone _ Q _ or Q : quotType
  • notation [eqQuotType e of Q], use EqQuotient.clone _ e Q _

• in ssralg.v

  • notation [nmodType of T for cT], use GRing.Nmodule.clone T cT
  • notation [nmodType of T], use GRing.Nmodule.clone T _ or T : nmodType
  • notation [zmodType of T for cT], use GRing.Zmodule.clone T cT
  • notation [zmodType of T], use GRing.Zmodule.clone T _ or T : zmodType
  • notation [semiRingType of T for cT], use GRing.SemiRing.clone T cT
  • notation [semiRingType of T], use GRing.SemiRing.clone T _ or T : semiRingType
  • notation [ringType of T for cT], use GRing.Ring.clone T cT
  • notation [ringType of T], use GRing.Ring.clone T _ or T : ringType
  • notation [lmodType of T for cT], use GRing.Lmodule.clone T cT
  • notation [lmodType of T], use GRing.Lmodule.clone T _ or T : lmodType
  • notation [lalgType of T for cT], use GRing.Lalgebra.clone T cT
  • notation [lalgType of T], use GRing.Lalgebra.clone T _ or T : lalgType
  • notation [semi_additive of f as g], use GRing.SemiAdditive.clone _ _ f g
  • notation [semi_additive of f], use GRing.SemiAdditive.clone _ _ f _ or f : {semi_additive _ -> _}
  • notation [additive of f as g], use GRing.Additive.clone _ _ f g
  • notation [additive of f], use GRing.Additive.clone _ _ f _ or f : {additive _ -> _}
  • notation [srmorphism of f as g], use GRing.SRMorphism.clone _ _ f g
  • notation [srmorphism of f], use GRing.SRMorphism.clone _ _ f _ or f : {srmorphism _ -> _}
  • notation [rmorphism of f as g], use GRing.RMorphism.clone _ _ f g
  • notation [rmorphism of f], use GRing.RMorphism.clone _ _ f _ or f : {rmorphism _ -> _}
  • notation [linear of f as g], use GRing.Linear.clone _ _ _ _ f g
  • notation [linear of f], use GRing.Linear.clone _ _ _ _ f _ or f : {linear _ -> _}
  • notation [lrmorphism of f], use GRing.LRMorphism.clone _ _ _ _ f _ or f : {lrmorphism _ -> _}
  • notation [comSemiRingType of T for cT], use GRing.ComSemiRing.clone T cT
  • notation [comSemiRingType of T], use GRing.ComSemiRing.clone T _ or T : comSemiRingType
  • notation [comRingType of T for cT], use GRing.ComRing.clone T cT
  • notation [comRingType of T], use GRing.ComRing.clone T _ or T : comRingType
  • notation [algType R of T for cT], use GRing.Algebra.clone R T cT
  • notation [algType R of T], use GRing.Algebra.clone R T _ or T : algType R
  • notation [comAlgType R of T], use GRing.ComAlgebra.clone R T _ or T : comAlgType R
  • notation [unitRingType of T for cT], use GRing.UnitRing.clone T cT
  • notation [unitRingType of T], use GRing.UnitRing.clone T _ or T : unitRingType
  • notation [comUnitRingType of T], use GRing.ComUnitRing.clone T _ or T : comUnitRingType
  • notation [unitAlgType R of T], use GRing.UnitAlgebra.clone R T _ or T : unitAlgType R
  • notation [comUnitAlgType R of T], use GRing.ComUnitAlgebra.clone R T _ or T : comUnitAlgType R
  • notation [idomainType of T for cT], use GRing.IntegralDomain.clone T cT
  • notation [idomainType of T], use GRing.IntegralDomain.clone T _ or T : idomainType
  • notation [fieldType of T for cT], use GRing.Field.clone T cT
  • notation [fieldType of T], use GRing.Field.clone T _ or T : fieldType
  • notation [decFieldType of T for cT], use GRing.DecidableField.clone T cT
  • notation [decFieldType of T], use GRing.DecidableField.clone T _ or T : decFieldType
  • notation [closedFieldType of T for cT], use GRing.ClosedField.clone T cT
  • notation [closedFieldType of T], use GRing.ClosedField.clone T _ or T : closedFieldType

• in finalg.v

  • notation [finZsemimodType of T], use FinRing.Zsemimodule.clone T _ or T : finZsemimodType
  • notation [finZmodType of T], use FinRing.Zmodule.clone T _ or T : finZmodType
  • notation [finSemiRingType of T], use FinRing.SemiRing.clone T _ or T : finSemiRingType
  • notation [finRingType of T], use FinRing.Ring.clone T _ or T : finRingType
  • notation [finComSemiRingType of T], use FinRing.ComSemiRing.clone T _ or T : finComSemiRingType
  • notation [finComRingType of T], use FinRing.ComRing.clone T _ or T : finComRingType
  • notation [finUnitRingType of T], use FinRing.UnitRing.clone T _ or T : finUnitRingType
  • notation [finComUnitRingType of T], use FinRing.ComUnitRing.clone T _ or T : finComUnitRingType
  • notation [finIntegralDomainType of T], use FinRing.IntegralDomain.clone T _ or T : finIntegralDomainType
  • notation [finFieldType of T], use FinRing.Field.clone T _ or T : finFieldType
  • notation [finLmodType of T], use FinRing.Lmodule.clone T _ or T : finLmodType
  • notation [finLalgType of T], use FinRing.Lalgebra.clone T _ or T : finLalgType
  • notation [finAlgType of T], use FinRing.Algebra.clone T _ or T : finAlgType
  • notation [finUnitAlgType of T], use FinRing.UnitAlgebra.clone T _ or T : finUnitAlgType

• in countalg.v

  • notation [countZsemimodType of T], use CountRing.Zsemimodule.clone T _ or T : countZsemimodType
  • notation [countZmodType of T], use CountRing.Zmodule.clone T _ or T : countZmodType
  • notation [countSemiRingType of T], use CountRing.SemiRing.clone T _ or T : countSemiRingType
  • notation [countRingType of T], use CountRing.Ring.clone T _ or T : countRingType
  • notation [countComSemiRingType of T], use CountRing.ComSemiRing.clone T _ or T : countComSemiRingType
  • notation [countComRingType of T], use CountRing.ComRing.clone T _ or T : countComRingType
  • notation [countUnitRingType of T], use CountRing.UnitRing.clone T _ or T : countUnitRingType
  • notation [countComUnitRingType of T], use CountRing.ComUnitRing.clone T _ or T : countComUnitRingType
  • notation [countIdomainType of T], use CountRing.IntegralDomain.clone T _ or T : countIdomainType
  • notation [countFieldType of T], use CountRing.Field.clone T _ or T : countFieldType
  • notation [countDecFieldType of T], use CountRing.DecidableField.clone T _ or T : countDecFieldType
  • notation [countClosedFieldType of T], use CountRing.ClosedField.clone T _ or T : countClosedFieldType

• in ssrnum.v

  • notation [numDomainType of T for cT], use Num.NumDomain.clone T cT
  • notation [numDomainType of T], use Num.NumDomain.clone T _ or T : numDomainType
  • notation [numFieldType of T], use Num.NumField.clone T _ or T : numFieldType
  • notation [numClosedFieldType of T for cT], use Num.ClosedField.clone T cT
  • notation [numClosedFieldType of T], use Num.ClosedField.clone T _ or T : numClosedFieldType
  • notation [realDomainType of T], use Num.RealDomain.clone T _ or T : realDomainType
  • notation [realFieldType of T], use Num.RealField.clone T _ or T : realFieldType
  • notation [archiFieldType of T for cT], use Num.ArchimedeanField.clone T cT
  • notation [archiFieldType of T], use Num.ArchimedeanField.clone T _ or T : archiFieldType
  • notation [rcfType of T for cT], use Num.RealClosedField.clone T cT
  • notation [rcfType of T], use Num.RealClosedField.clone T _ or T : rcfType

• in ring_quotient.v

  • notation [zmodQuotType z, o & a of Q], use ZmodQuotient.clone _ _ z o a Q _
  • notation [ringQuotType o & m of Q], use RingQuotient.clone _ _ _ _ _ o m Q _
  • notation [unitRingQuotType u & i of Q], use UnitRingQuotient.clone _ _ _ _ _ _ _ u i Q _

• in vector.v

  • notation [vectType R of T for cT], use Vector.clone T cT
  • notation [vectType R of T], use Vector.clone T _ or T : vectType R

• in galois.v

  • notation [splittingFieldType F of L for K], use SplittingField.clone F L K
  • notation [splittingFieldType F of L], use SplittingField.clone F L _ or L : splittingFieldType F

• in fieldext.v

  • notation [fieldExtType F of L for K], use FieldExt.clone F L K
  • notation [fieldExtType F of L], use FieldExt.clone F L _ or L : fieldExtType F

• in falgebra.v

  • notation [FalgType F of L for L'], use Falgebra.clone F L L'
  • notation [FalgType F of L], use Falgebra.clone F L _ or L : FalgType F

[1.17.0] - 2023-05-09

This release is compatible with Coq versions 8.15, 8.16 and 8.17.

The contributors to this version are:

Alex Gryzlov, Cyril Cohen, Jason Gross, Kazuhiko Sakaguchi, Kimaya Bedarkar, Laurent Théry, Pierre Jouvelot, Pierre Roux, Quentin Vermande, Reynald Affeldt, Takafumi Saikawa, Mitsuharu Yamamoto, Marina López Chamosa

Added

• in ssrfun.v

  • lemmas inj_omap, omap_id, eq_omap, omapK

• in ssrnat.v

  • lemmas addnCBA, addnBr_leq, addnBl_leq, subnDAC, subnCBA, subnBr_leq, subnBl_leq, subnBAC, subDnAC, subDnCA, subDnCAC, addnBC, addnCB, addBnAC, addBnCAC, addBnA, subBnAC, eqn_sub2lE, eqn_sub2rE

• in seq.v

  • lemmas find_pred0, find_predT
  • lemmas sumn_ncons, sumn_set_nth, sumn_set_nth_ltn, sumn_set_nth0

• in order.v

  • notations 0%O, 1%O, 0^d%O and 1^d%O as backward compatible replacements of removed notation 0, 1, 0^d and 1^d for bottom and top of lattices
  • notations \top and \bot for Order.top and Order.bottom
  • notations \top^d and \bot^d for Order.dual_top and Order.dual_bottom

• in perm.v

  • lemmas perm_on_id, perm_onC, tperm_on

• in bigop.v

  • lemma big_if

• in finset.v

  • lemma bigA_distr

• in ssralg.v

  • bool is now canonically a fieldType with additive law addb and multiplicative law andb

• in finalg.v

  • bool is now canonically a finFieldType and a decFieldType.

• in poly.v

  • lemmas coef_prod_XsubC, coefPn_prod_XsubC, coef0_prod_XsubC, polyOver_mulr_2closed

Changed

• in ssrnat.v

  • change the doubling and halving operators to be left-associative

• in seq.v,

  • notations [seq x <- s | C ], [seq x <- s | C1 & C2 ], [seq E | i <- s ], [seq E | i <- s & C ], [seq E : R | i <- s ], [seq E : R | i <- s & C ], [seq E | x <- s, y <- t ], [seq E : R | x <- s, y <- t ] now support destructuring patterns in binder positions.

• in fintype.v,

  • notations [seq F | x in A ] and [seq F | x ] now support destructuring patterns in binder positions. In the case of [seq F | x ] and [seq F | x : T ], type inference on x now occurs earlier, meaning that implicit types and typeclass resolution in T will take precedence over unification constraints arising from typechecking x in F. This may result in occasional incompatibilities.

• in order.v

  • fix lemmas eq_bigmax and eq_bigmin to respect given predicates
  • fix \meet^p_ and \join^p_ notations
  • fix the scope of n.-tuplelexi notations
  • fix the definition of max_fun (notation \max) which was equal to min_fun

• in intdiv.v

  • zcontents is now of type {poly int} -> int
  • divz is now of type int -> int -> int

Renamed

• in ssralg.v:
  • rmorphX -> rmorphXn
• in fraction.v:
  • tofracX -> tofracXn
• in ssrnum.v:
  • ler_opp2 -> lerN2
  • ltr_opp2 -> ltrN2
  • lter_opp2 -> lterN2
  • ler_oppr -> lerNr
  • ltr_oppr -> ltrNr
  • lter_oppr -> lterNr
  • ler_oppl -> lerNl
  • ltr_oppl -> ltrNl
  • lter_oppl -> lterNl
  • lteif_opp2 -> lteifN2
  • ler_add2l -> lerD2l
  • ler_add2r -> lerD2r
  • ltr_add2l -> ltrD2l
  • ltr_add2r -> ltD2r
  • ler_add2 -> lerD2
  • ltr_add2 -> ltrD2
  • lter_add2 -> lterD2r
  • ler_add -> lerD
  • ler_lt_add -> ler_ltD
  • ltr_le_add -> ltr_leD
  • ltr_add -> ltrD
  • ler_sub -> lerB
  • ler_lt_sub -> ler_ltB
  • ltr_le_sub -> ltr_leB
  • ltr_sub -> ltrB
  • ler_subl_addr -> lerBlDr
  • ltr_subl_addr -> ltrBlDr
  • ler_subr_addr -> lerBrDr
  • ltr_subr_addr -> ltrBrDr
  • ler_sub_addr -> lerBDr
  • ltr_sub_addr -> ltrBDr
  • lter_sub_addr -> lterBDr
  • ler_subl_addl -> lerBlDl
  • ltr_subl_addl -> ltrBlDl
  • ler_subr_addl -> lerBrDl
  • ltr_subr_addl -> ltrBrDl
  • ler_sub_addl -> lerBDl
  • ltr_sub_addl -> ltrBDl
  • lter_sub_addl -> lterBDl
  • ler_addl -> lerDl
  • ltr_addl -> ltrDl
  • ler_addr -> lerDr
  • ltr_addr -> ltrDr
  • ger_addl -> gerDl
  • gtr_addl -> gtrDl
  • ger_addr -> gerDr
  • gtr_addr -> gtrDr
  • cpr_add -> cprD
  • lteif_add2l -> lteifD2l
  • lteif_add2r -> lteifD2r
  • lteif_add2 -> lteifD2
  • lteif_subl_addr -> lteifBlDr
  • lteif_subr_addr -> lteifBrDr
  • lteif_sub_addr -> lteifBDr
  • lteif_subl_addl -> lteifBlDl
  • lteif_subr_addl -> lteifBrDl
  • lteif_sub_addl -> lteifBDl
  • ler_norm_add -> ler_normD
  • ler_norm_sub -> ler_normB
  • leif_add -> leifD
  • gtr_opp -> gtrN
  • lteif_oppl -> lteifNl
  • lteif_oppr -> lteifNr
  • lteif_0oppr -> lteif0Nr
  • lteif_oppr0 -> lteifNr0
  • lter_oppE -> lterNE
  • ler_dist_add -> ler_distD
  • ler_dist_norm_add -> ler_dist_normD
  • ler_sub_norm_add -> lerB_normD
  • ler_sub_dist -> lerB_dist
  • ler_sub_real -> lerB_real
  • ger_sub_real -> gerB_real
  • ltr_expn2r -> ltrXn2r
  • ler_expn2r -> lerXn2r
  • lter_expn2r -> lterXn2r
  • ler_pmul -> ler_pM
  • ltr_pmul -> ltr_pM
  • ler_pinv -> ler_pV2
  • ler_ninv -> ler_nV2
  • ltr_pinv -> ltr_pV2
  • ltr_ninv -> ltr_nV2
  • ler_pmul2l -> ler_pM2l
  • ltr_pmul2l -> ltr_pM2l
  • lter_pmul2l -> lter_pM2l
  • ler_pmul2r -> ler_pM2r
  • ltr_pmul2r -> ltr_pM2r
  • lter_pmul2r -> lter_pM2r
  • ler_nmul2l -> ler_nM2l
  • ltr_nmul2l -> ltr_nM2l
  • lter_nmul2l -> lter_nM2l
  • ler_nmul2r -> ler_nM2r
  • ltr_nmul2r -> ltr_nM2r
  • lter_nmul2r -> lter_nM2r
  • lef_pinv -> lef_pV2
  • lef_ninv -> lef_nV2
  • ltf_pinv -> ltf_pV2
  • ltf_ninv -> ltf_nV2
  • ltef_pinv -> ltef_pV2
  • ltef_ninv -> ltef_nV2
  • minr_pmulr -> minr_pMr
  • maxr_pmulr -> maxr_pMr
  • minr_pmull -> minr_pMl
  • maxr_pmull -> maxr_pMl
  • ltr_wpexpn2r -> ltr_wpXn2r
  • ler_pexpn2r -> ler_pXn2r
  • ltr_pexpn2r -> ltr_pXn2r
  • lter_pexpn2r -> lter_pXn2r
  • ger_pmull -> ger_pMl
  • gtr_pmull -> gtr_pMl
  • ger_pmulr -> ger_pMr
  • gtr_pmulr -> gtr_pMr
  • ler_pmull -> ler_pMl
  • ltr_pmull -> ltr_pMl
  • ler_pmulr -> ler_pMr
  • ltr_pmulr -> ltr_pMr
  • ger_nmull -> ger_nMl
  • gtr_nmull -> gtr_nMl
  • ger_nmulr -> ger_nMr
  • gtr_nmulr -> gtr_nMr
  • ler_nmull -> ler_nMl
  • ltr_nmull -> ltr_nMl
  • ler_nmulr -> ler_nMr
  • ltr_nmulr -> ltr_nMr
  • leif_pmul -> leif_pM
  • leif_nmul -> leif_nM
  • eqr_expn2 -> eqrXn2
  • real_maxr_nmulr -> real_maxr_nMr
  • real_minr_nmulr -> real_minr_nMr
  • real_minr_nmull -> real_minrnMl
  • real_maxr_nmull -> real_maxrnMl
  • real_ltr_distl_addr -> real_ltr_distlDr
  • real_ler_distl_addr -> real_ler_distlDr
  • real_ltr_distlC_addr -> real_ltr_distlCDr
  • real_ler_distlC_addr -> real_ler_distlCDr
  • real_ltr_distl_subl -> real_ltr_distlBl
  • real_ler_distl_subl -> real_ler_distlBl
  • real_ltr_distlC_subl -> real_ltr_distlCBl
  • real_ler_distlC_subl -> real_ler_distlCBl
  • ltr_distl_addr -> ltr_distlDr
  • ler_distl_addr -> ler_distlDr
  • ltr_distlC_addr -> ltr_distlCDr
  • ler_distlC_addr -> ler_distlCDr
  • ltr_distl_subl -> ltr_distlBl
  • ler_distl_subl -> ler_distlBl
  • ltr_distlC_subl -> ltr_distlCBl
  • ler_distlC_subl -> ler_distlCBl
  • maxr_nmulr -> maxr_nMr
  • minr_nmulr -> minr_nMr
  • minr_nmull -> minr_nMl
  • maxr_nmull -> maxr_nMl
  • ler_iexpn2l -> ler_iXn2l
  • ltr_iexpn2l -> ltr_iXn2l
  • lter_iexpn2l -> lter_iXn2l
  • ler_eexpn2l -> ler_eXn2l
  • ltr_eexpn2l -> ltr_eXn2l
  • lter_eexpn2l -> lter_eXn2l
  • ler_wpmul2l -> ler_wpM2l
  • ler_wpmul2r -> ler_wpM2r
  • ler_wnmul2l -> ler_wnM2l
  • ler_wnmul2r -> ler_wnM2r
  • ler_pemull -> ler_peMl
  • ler_nemull -> ler_neMl
  • ler_pemulr -> ler_peMr
  • ler_nemulr -> ler_neMr
  • ler_iexpr -> ler_iXnr
  • ltr_iexpr -> ltr_iXnr
  • lter_iexpr -> lter_iXnr
  • ler_eexpr -> ler_eXnr
  • ltr_eexpr -> ltr_eXnr
  • lter_eexpr -> lter_eXnr
  • lter_expr -> lter_Xnr
  • ler_wiexpn2l -> ler_wiXn2l
  • ler_weexpn2l -> ler_weXn2l
  • ler_pimull -> ler_piMl
  • ler_nimull -> ler_niMl
  • ler_pimulr -> ler_piMr
  • ler_nimulr -> ler_niMr
  • lteif_pdivl_mulr -> lteif_pdivlMr
  • lteif_pdivr_mulr -> lteif_pdivrMr
  • lteif_pdivl_mull -> lteif_pdivlMl
  • lteif_pdivr_mull -> lteif_pdivrMl
  • lteif_ndivl_mulr -> lteif_ndivlMr
  • lteif_ndivr_mulr -> lteif_ndivrMr
  • lteif_ndivl_mull -> lteif_ndivlMl
  • lteif_ndivr_mull -> lteif_ndivrMl
  • ler_pdivl_mulr -> ler_pdivlMr
  • ltr_pdivl_mulr -> ltr_pdivlMr
  • lter_pdivl_mulr -> lter_pdivlMr
  • ler_pdivr_mulr -> ler_pdivrMr
  • ltr_pdivr_mulr -> ltr_pdivrMr
  • lter_pdivr_mulr -> lter_pdivrMr
  • ler_pdivl_mull -> ler_pdivlMl
  • ltr_pdivl_mull -> ltr_pdivlMl
  • lter_pdivl_mull -> lter_pdivlMl
  • ler_pdivr_mull -> ler_pdivrMl
  • ltr_pdivr_mull -> ltr_pdivrMl
  • lter_pdivr_mull -> lter_pdivrMl
  • ler_ndivl_mulr -> ler_ndivlMr
  • ltr_ndivl_mulr -> ltr_ndivlMr
  • lter_ndivl_mulr -> lter_ndivlMr
  • ler_ndivr_mulr -> ler_ndivrMr
  • ltr_ndivr_mulr -> ltr_ndivrMr
  • lter_ndivr_mulr -> lter_ndivrMr
  • ler_ndivl_mull -> ler_ndivlMl
  • ltr_ndivl_mull -> ltr_ndivlMl
  • lter_ndivl_mull -> lter_ndivlMl
  • ler_ndivr_mull -> ler_ndivrMl
  • ltr_ndivr_mull -> ltr_ndivrMl
  • lter_ndivr_mull -> lter_ndivrMl
  • eqr_pmuln2r -> eqr_pMn2r
  • ler_muln2r -> lerMn2r
  • ler_pmuln2r -> ler_pMn2r
  • ler_pmuln2l -> ler_pMn2l
  • ltr_pmuln2r -> ltr_pMn2r
  • ltr_wmuln2r -> ltr_wMn2r
  • ler_wmuln2r -> ler_wMn2r
  • ltr_wpmuln2r -> ltr_wpMn2r
  • ler_wpmuln2l -> ler_wpMn2l
  • ler_wnmuln2l -> ler_wnMn2l
  • ltr_muln2r -> ltrMn2r
  • eqr_muln2r -> eqrMn2r
  • ltr_pmuln2l -> ltr_pMn2l
  • ler_nmuln2l -> ler_nMn2l
  • ltr_nmuln2l -> ltr_nMn2l
  • normC_add_eq -> normCDeq
  • normC_sub_eq -> normCBeq
  • leif_subLR -> leifBLR
  • leif_subRL -> leifBRL
• in ssrint.v:
  • leq_add_dist -> leqD_dist
  • lez_add1r -> lez1D
  • lez_addr1 -> lezD1
  • ltz_add1r -> ltz1D
  • ltz_addr1 -> ltzD1
  • oppz_add -> oppzD
  • leqif_add_distz -> leqifD_distz
  • leqif_add_dist -> leqifD_dist
  • ler_pmulz2r -> ler_pMz2r
  • ler_pmulz2l -> ler_pMz2l
  • ler_wpmulz2r -> ler_wpMz2r
  • ler_wpmulz2l -> ler_wpMz2l
  • ler_wnmulz2l -> ler_wnMz2l
  • ler_nmulz2r -> ler_nMz2r
  • ltr_pmulz2r -> ltr_pMz2r
  • ler_nmulz2l -> ler_nMz2l
  • ltr_pmulz2l -> ltr_pMz2l
  • ltr_nmulz2r -> ltr_nMz2r
  • ltr_nmulz2l -> ltr_nMz2l
  • ler_wnmulz2r -> ler_wnMz2r
  • ler_wpexpz2r -> ler_wpXz2r
  • ler_wnexpz2r -> ler_wnXz2r
  • ler_pexpz2r -> ler_pXz2r
  • ltr_pexpz2r -> ltr_pXz2r
  • ler_nexpz2r -> ler_nXz2r
  • ltr_nexpz2r -> ltr_nXz2r
  • ler_wpiexpz2l -> ler_wpiXz2l
  • ler_wniexpz2l -> ler_wniXz2l
  • ler_wpeexpz2l -> ler_wpeXz2l
  • ler_wneexpz2l -> ler_wneXz2l
  • ler_weexpz2l -> ler_weXz2l
  • ler_piexpz2l -> ler_piXz2l
  • ltr_piexpz2l -> ltr_piXz2l
  • ler_niexpz2l -> ler_niXz2l
  • ltr_niexpz2l -> ltr_niXz2l
  • ler_eexpz2l -> ler_eXz2l
  • ltr_eexpz2l -> ltr_eXz2l
  • eqr_expz2 -> eqrXz2
  • exprz_pmulzl -> exprz_pMzl
  • lteif_pmul2l -> lteif_pM2l
  • lteif_pmul2r -> lteif_pM2r
  • lteif_nmul2l -> lteif_nM2l
  • lteif_nmul2r -> lteif_nM2r
  • ler_paddl -> ler_wpDl
  • ltr_paddl -> ltr_wpDl
  • ltr_spaddl -> ltr_pwDl
  • ltr_spsaddl -> ltr_pDl
  • ler_naddl -> ler_wnDl
  • ltr_naddl -> ltr_wnDl
  • ltr_snaddl -> ltr_nwDl
  • ltr_snsaddl -> ltr_nDl
  • ler_paddr -> ler_wpDr
  • ltr_paddr -> ltr_wpDr
  • ltr_spaddr -> ltr_pwDr
  • ltr_spsaddr -> ltr_pDr
  • ler_naddr -> ler_wnDr
  • ltr_naddr -> ltr_wnDr
  • ltr_snaddr -> ltr_nwDr
  • ltr_snsaddr -> ltr_nDr
• in interval.v:
  • in_segment_addgt0Pr -> in_segmentDgt0Pr
  • in_segment_addgt0Pl -> in_segmentDgt0Pl
• in mxrepresentation.v:
  • mxval_grootX -> mxval_grootXn

Removed

• in ssrbool.v

  • notation mono2W_in that was deprecated in 1.14.0

• in order.v

  • notations 0, 1, 0^d and 1^d in order_scope

Deprecated

• in order.v
  • notations 0%O, 1%O, 0^d%O and 1^d%O

[1.16.0] - 2023-02-01

This release is compatible with Coq versions 8.13, 8.14, 8.15, 8.16 and 8.17.

The contributors to this version are:

Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Georges Gonthier, Yoshihiro Ishiguro, Julien Puydt, Kazuhiko Sakaguchi, Laurent Théry, Mireia G. Bedmar, Pierre-Marie Pédrot, Pierre Roux, Pierre Pomeret-Coquot, Quentin Vermande, Reynald Affeldt, Takafumi Saikawa, Yoshihiro Imai

Added

• in ssrbool.v

  • notation [in A]
  • lemmas if_and, if_or, if_implyb, if_impliybC, if_add

• in eqtype.v

  • lemmas existsb and exists_inb

• in ssrnat.v

  • lemma leqVgt
  • lemmas ltn_half_double, leq_half_double, gtn_half_double
  • lemma double_pred
  • lemmas uphalfE, ltn_uphalf_double, geq_uphalf_double, gtn_uphalf_double
  • lemmas halfK, uphalfK, odd_halfK, even_halfK, odd_uphalfK, even_uphalfK
  • lemmas leq_sub2rE, leq_sub2lE, ltn_sub2rE, ltn_sub2lE

• in seq.v

  • lemmas subset_mapP, take_min, take_taker, perm_allpairs_dep, perm_allpairs
  • lemmas allT, all_mapT, inj_in_map, and mapK_in.
  • lemma if_nth

• in path.v

  • lemmas prefix_path, prefix_sorted, infix_sorted, suffix_sorted

• in finset.v

  • lemmas set_nil, set_seq1

• in bigop.v

  • lemmas big_ord1_eq, big_ord1_cond_eq, big_nat1_eq, big_nat1_cond_eq
  • lemmas big_seq1_id, big_nat1_id, big_pred1_eq_id, big_pred1_id, big_const_idem, big1_idem, big_id_idem, big_rem_AC, perm_big_AC, big_enum_cond_AC, bigD1_AC, bigD1_seq_AC, big_image_cond_AC, big_image_AC, big_image_cond_id_AC, Lemma, cardD1x, reindex_omap_AC, reindex_onto_AC, reindex_AC, reindex_inj_AC, bigD1_ord_AC, big_enum_val_cond_AC, big_enum_rank_cond_AC, big_nat_rev_AC, big_rev_mkord_AC, big_mkcond_idem, big_mkcondr_idem, big_mkcondl_idem, big_rmcond_idem, big_rmcond_in_idem, big_cat_idem, big_allpairs_dep_idem, big_allpairs_idem, big_cat_nat_idem, big_split_idem, big_id_idem_AC, bigID_idem, bigU_idem, partition_big_idem, sig_big_dep_idem, pair_big_dep_idem, pair_big_idem, pair_bigA_idem, exchange_big_dep_idem, exchange_big_idem, exchange_big_dep_nat_idem, exchange_big_nat_idem, big_undup_AC
  • definition oAC
  • lemmas oACE, some_big_AC_mk_monoid, big_AC_mk_monoid
  • canonical instances oAC_law and oAC_com_law
  • lemmas sub_le_big, sub_le_big_seq, sub_le_big_seq_cond, uniq_sub_le_big, uniq_sub_le_big_cond, idem_sub_le_big, idem_sub_le_big_cond, sub_in_le_big, le_big_ord, subset_le_big, le_big_nat_cond, le_big_nat, le_big_ord_cond
  • lemma subset_le_big_cond

• in order.v

  • lemmas bigmax_le, bigmax_lt, lt_bigmin, le_bigmin, bigmin_mkcond, bigmax_mkcond, bigmin_split, bigmax_split, bigmin_idl, bigmax_idl, bigmin_idr, bigmax_idr, bigminID, bigmaxID, sub_bigmin, sub_bigmax, sub_bigmin_seq, sub_bigmax_seq, sub_bigmin_cond, sub_bigmax_cond, sub_in_bigmin, sub_in_bigmax, le_bigmin_nat, le_bigmax_nat, le_bigmin_nat_cond, le_bigmax_cond, le_bigmin_ord, le_bigmax_ord, le_bigmin_ord_cond, le_bigmax_ord_cond, subset_bigmin, subset_bigmax, subset_bigmin_cond, subset_bigmax_cond, bigminD1, bigmaxD1, bigmin_le_cond, le_bigmax_cond, bigmin_le, le_bigmax, bigmin_inf, bigmax_sup, bigmin_geP, bigmax_leP, bigmin_gtP, bigmax_ltP, bigmin_eq_arg, bigmax_eq_arg, eq_bigmin, eq_bigmax, le_bigmin2, le_bigmax2

• in ssralg.v

  • lemmas natr1, nat1r, telescope_sumr_eq, telescope_prodr_eq, telescope_prodf_eq
  • lemma eqr_sum_div
  • lemmas divrN, divrNN

• in poly.v

  • definitions even_poly, odd_poly, take_poly, drop_poly
  • lemmas comm_polyD, comm_polyM, comm_poly_exp, root_exp, root_ZXsubC, size_mulXn, coef_sumMXn, comp_Xn_poly, coef_comp_poly_Xn, comp_poly_Xn, size_even_poly, size_even_poly_eq, coef_even_poly, even_polyE, even_polyD, even_polyZ, even_poly_is_linear, even_polyC, size_odd_poly, coef_odd_poly, odd_polyE, odd_polyC, odd_polyD, odd_polyZ, odd_poly_is_linear, odd_polyMX, even_polyMX, sum_even_poly, sum_odd_poly, poly_even_odd, size_take_poly, coef_take_poly, take_poly_id, take_polyD, take_polyZ, take_poly_is_linear, take_poly_sum, take_poly0l, take_poly0r, take_polyMXn, take_polyMXn_0, take_polyDMXn, size_drop_poly, size_drop_poly_eq, coef_drop_poly, drop_poly_eq0, sum_drop_poly, drop_polyD, drop_polyZ, drop_poly_is_linear, drop_poly_sum, drop_poly0l, drop_poly0r, drop_polyMXn, drop_polyMXn_id, drop_polyDMXn, poly_take_drop, eqp_take_drop, scale_polyC
  • canonical instances even_poly_additive, even_poly_linear, odd_poly_additive, odd_poly_linear, take_poly_additive, take_poly_linear, drop_poly_additive, drop_poly_linear

• in polydiv.v

  • lemmas Pdiv.RingMonic.drop_poly_rdivp, Pdiv.RingMonic.take_poly_rmodp, Pdiv.IdomainMonic.drop_poly_divp, Pdiv.IdomainMonic.take_poly_modp

• in ssrnum.v

  • lemmas psumr_neq0, psumr_neq0P

• in ssrint.v

  • printing only notation for x = y :> int, opening int_scope on x and y to better match the already existing parsing only notation with the introduction of number notations in ring_scope

• in matrix.v

  • definitions Vandermonde, map2_mx
  • lemma det_Vandermonde, map2_trmx, map2_const_mx, map2_row, map2_col, map2_row', map2_col', map2_mxsub, map2_row_perm, map2_col_perm, map2_xrow, map2_xcol, map2_castmx, map2_conform_mx, map2_mxvec, map2_vec_mx, map2_row_mx, map2_col_mx, map2_block_mx, map2_lsubmx, map2_rsubmx, map2_usubmx, map2_dsubmx, map2_ulsubmx, map2_ursubmx, map2_dlsubmx, map2_drsubmx, eq_in_map2_mx, eq_map2_mx, map2_mx_left_in, map2_mx_left, map2_mx_right_in, map2_mx_right, map2_mxA, map2_1mx, map2_mx1, map2_mxC, map2_0mx, map2_mx0, map2_mxDl, map2_mxDr, diag_mx_is_additive, mxtrace_is_additive

Changed

• in seq.v:

  • changed names of implicit arguments of map_id, eq_map, map_comp, mapK, eq_in_map

• in ssrbool.v, eqtype.v, seq.v, path.v, fintype.v, fingraph.v, prime.v, binomial.v, fingraph.v, bigop.v, ssralg.v, ssrnum.v, poly.v, mxpoly.v, action.v, perm.v, presentation.v, abelian.v, cyclic.v, frobenius.v, maximal.v, primitive_action.v, alt.v, burnside_app.v, mxrepresentation.v, mxabelian.v, character.v, inertia.v, integral_char.v, separable.v, galois.v, algebraics_fundamental.v, changed mem XXX and [mem XXX] to [in XX].

• Regressions: now redundant instances of inE rewriting mem A x to x \in A must be deleted or made optional, as [in A] x directly beta-reduces to x \in A.

• in poly.v:

  • generalize eq_poly
  • made hornerE preserve powers

• in matrix.v:

  • updated oppmx, addmx, addmxA, addmxC, add0mx
  • moved to an earlier section of the file diag_mx, tr_diag_mx, diag_mx_row, diag_mxP, diag_mx_is_diag, diag_mx_is_trig, scalar_mx, diag_const_mx, tr_scalar_mx, scalar_mx_is_additive, is_scalar_mx, is_scalar_mxP, scalar_mx_is_scalar, mx0_is_scalar, scalar_mx_is_diag, is_scalar_mx_is_diag, scalar_mx_is_trig, is_scalar_mx_is_trig, mx11_scalar, scalar_mx_block, mxtrace, mxtrace_tr, mxtrace0, mxtraceD, mxtrace_diag, mxtrace_scalar, trace_mx11, mxtrace_block

Renamed

• in eqtype.v and gseries.v, renamed rel_of_simpl_rel to rel_of_simpl, the actual name used in the coq ssr.ssrbool.v file.

Removed

• in ssreflect.v:

  • module Deprecation (deprecated in 1.13.0)
  • notation deprecate (deprecated in 1.13.0)

• in ssrbool.v, removed outdated Coq 8.10 compatibility code.

• in bigop.v:

  • notation big_uncond (deprecated in 1.13.0)

• in finset.v:

  • notations mem_imset_eq and mem_imset2_eq (deprecated in 1.13.0)

• in order.v:

  • notations join_sup_seq, join_min_seq, join_sup, join_min, join_seq, meet_inf_seq, meet_max_seq, meet_seq (deprecated in 1.13.0)

• in path.v:

  • notations sup_path_in, sub_cycle_in, sub_sorted_in, eq_path_in, eq_cycle_in (deprecated in 1.13.0)

• in seq.v:

  • notation iota_add (deprecated in 1.13.0)

• in ssrnat.v:

  • notation fact_smonotone (deprecated in 1.13.0)

• in matrix.v:

  • notation card_matrix (deprecated in 1.13.0)

• in rat.v:

  • notation divq_eq (deprecated in 1.13.0)

• in ssralg.v:

  • notation prodr_natmul (deprecated in 1.13.0)

[1.15.0] - 2022-06-30

This release is compatible with Coq versions 8.13, 8.14, 8.15 and 8.16.

The contributors to this version are: Cyril Cohen, ed-hermoreyes, Enrico Tassi, Erik Martin-Dorel, Evgenii Moiseenko, Georges Gonthier, Jonathan Sterling, Kazuhiko Sakaguchi, Laurent Théry, Mireia G. Bedmar, Pierre Jouvelot, Pierre Roux, Reynald Affeldt, Wojciech Karpiel

Added

• in bigop.v

  • lemmas leq_prod,telescope_big, telescope_sumn, telescope_sumn_in leq_bigmax_seq, bigmax_leqP_seq, bigmax_sup_seq, eq_bigl_supp, perm_big_supp_cond, perm_big_supp

• in path.v

  • lemma sortedP

• in seq.v,

  • definitions prefix, suffix, infix, infix_index
  • lemmas nilpE, prefixE, prefix_refl, prefixs0, prefix0s, prefix_cons, prefix_catr, prefix_prefix, prefixP, prefix_trans, prefixs1, catl_prefix, prefix_catl, prefix_rcons, prefix_rev, prefix_revLR, prefix1s, prefix_uniq, prefix_take, prefix_drop_gt0, size_prefix, suffixE, suffix_refl, suffixs0, suffix0s, suffix_rev, suffix_revLR, suffix_suffix, suffixP, suffix_trans, suffix_rcons, suffix_catl, suffix_catr, catl_suffix, suffix_cons, suffixW, suffix1s, suffix_uniq, suffix_drop, size_suffix, infix0s, infixs0, infix_consl, infix_indexss, infix_index_le, infixTindex, infixPn, infix_index0s, infix_indexs0, infixE, infix_refl, prefixW, prefix_infix, infix_infix, suffix_infix, infixP, infix_rev, infix_trans, infix_revLR, infix_rconsl, infix_cons, infixs1, catl_infix, catr_infix, cons2_infix, rcons2_infix, catr2_infix, catl2_infix, infix_catl, infix_catr, prefix_infix_trans, suffix_infix_trans, infix_prefix_trans, infix_suffix_trans, prefix_suffix_trans, suffix_prefix_trans, infixW, mem_infix, infix1s, infix_rcons, infix_uniq, infix_take, infix_drop, consr_infix, consl_infix, prefix_index, size_infix, mkseqS, mkseq_uniqP,nth_seq1, set_nthE, count_set_nth, count_set_nth_ltn, count_set_nthF, subseq_anti, size_take_min, subseq_anti

• in ssralg.v

  • notation \- f for definition opp_fun
  • notation f \* g for definition mul_fun
  • lemmas opp_fun_is_additive and opp_fun_is_scalable
  • canonical instances opp_fun_additive and opp_fun_linear
  • missing export for eqr_div
  • number notation in scope ring_scope, numbers such as 12 or 42 are now read as 12%:R or 42%:R

• in rat.v

  • Number Notation for numbers of the form -? [0-9][0-9_]* ([.][0-9_]+)? in scope rat_scope (for instance 12%Q or 3.14%Q)
  • lemma rat_vm_compute which is a specialization to the rewriting rule vm_compute to trigger vm_compute by a rewrite

• in ssrint.v

  • number notation in scope int_scope, 12 or -42 are now read as Posz 12 or Negz 41
  • number notation in scope ring_scope, numbers such as -12 are now read as (-12)%:~R

• in fintype.v

  • lemmas enum_ord0, enum_ordSl, enum_ordSr

• in ssrbool.v

  • definition pred_oapp
  • lemmas all_sig2_cond, all_sig2_cond, can_in_pcan, pcan_in_inj, in_inj_comp, can_in_comp, pcan_in_comp, ocan_in_comp, eqbLR, eqbRL, homo_mono1

• in choice.v

  • coercion Choice.mixin

• in eqtype.v

  • notations eqbLHS and eqbRHS

• in order.v

  • notations leLHS, leRHS, ltLHS, ltRHS
  • notation f \min g and f \max g for definitions min_fun and max_fun
  • lemma le_le_trans

• in ssrnat.v

  • notations leqLHS, leqRHS, ltnLHS, ltnRHS
  • lemmas geq_half_double, leq_uphalf_double

• in ssrfun.v

  • definition olift
  • lemmas obindEapp, omapEbind, omapEapp, oappEmap, omap_comp, oapp_comp, oapp_comp_f, olift_comp, compA, ocan_comp

• in tuple.v

  • lemma tuple_uniqP

• in ssreflect.v:

  • typeclass vm_compute_eq and lemma vm_compute in order to trigger a call to the tactic vm_compute when rewriting using rewrite [pattern]vm_compute
  • notation [elaborate t] forcing the elaboration of t using Coq's refine tactic. This notation can be used in tandem with have to force type class resolution when an explicit proof term t is provided (otherwise type class instances are quantified implicitly by have)

• in ssrnum.v

  • lemmas mulCii, ReE, ImE, conjCN1, CrealJ, eqCP, eqC, ImM, ImMil, ReMil, ImMir, ReMir, ReM, invC_Crect, ImV, ReV, rectC_mulr, rectC_mull, divC_Crect, divC_rect, Im_div, Re_div
  • adding resolution of 'Re x \in Num.real and 'Im x \in Num.real as in Hint Extern to core database

• in ssrnum.v

  • lemmas gtr_opp, mulr_ge0_gt0, splitr, ler_addgt0Pr, ler_addgt0Pl, lt_le, gt_ge

• in interval.v

  • definition miditv
  • lemmas in_segment_addgt0Pr, in_segment_addgt0Pl, ltBSide, leBSide, lteBSide, ltBRight_leBLeft, leBRight_ltBLeft, bnd_simp, itv_splitU1, itv_split1U, mem_miditv, miditv_le_left, miditv_ge_right, predC_itvl, predC_itvr, predC_itv
  • coercion pair_of_interval

Changed

• The following notations are now declared in type_scope

  • {tuple n of T} and {bseq n of T} in tuple.v
  • {subset T} and {subset [d] T} in order.v
  • {morphism D >-> T} in morphism.v
  • {acts A, on S | to} and {acts A, on group G | to} in action.v
  • {additive U -> V}, {rmorphism R -> S}, {linear U -> V} {linear U -> V | s}, {scalar U}, {lrmorphism A -> B} {lrmorphism A -> B | s} in ssralg.v
  • {poly R} in poly.v
  • {quot I} and {ideal_quot I} in ring_quotient.v
  • {ratio T} and {fraction T} in fraction.v

• in rat.v

  • zeroq and oneq (hence 0%Q and 1%Q) are now the evaluation of terms fracq (0, 1) and fracq (1, 1) (and not the term themselves), the old and new values are convertible and can be easily converted with rewrite -[0%Q]valqK -[1%Q]valqK

• in order.v

  • fix [distrLatticeType of T with disp] notation

• in fintype.v

  • enum_ordS now a notation

• in gproduct.v

  • put notations G ><| H, G \* H and G \x H in group_scope

• in ssrnum.v

  • locked definitions Re and Im

Renamed

• in ssrbool.v
  • mono2W_in to mono1W_in (was misnamed)

Removed

• in ssrbool.v

  • notations {pred T}, [rel _ | _], [rel _ in _], xrelpre (now in ssrbool in Coq)
  • definitions PredType, simpl_rel, SimplRel, relpre (now in ssrbool in Coq)
  • coercion rel_of_simpl_rel deprecated for rel_of_simpl (in ssrbool in Coq)
  • lemmas simpl_pred_sortE, homo_sym, mono_sym, homo_sym_in, mono_sym_in, homo_sym_in11, mono_sym_in11, onW_can, onW_can_in, in_onW_can, onS_can, onS_can_in, in_onS_can, homoRL_in, homoLR_in, homo_mono_in, monoLR_in, monoRL_in, can_mono_in, inj_can_sym_in_on, inj_can_sym_on, inj_can_sym_in, contra_not, contraPnot, contraTnot, contraNnot, contraPT, contra_notT, contra_notN, contraPN, contraFnot, contraPF, contra_notF (now in ssrbool in Coq, beware that simpl_pred_sortE, contra_not, contraPnot, contraTnot, contraNnot, contraPT, contra_notT, contra_notN, contraPN, contraFnot, contraPF, contra_notF have different implicit arguments and the order of arguments changes in homoRL_in, homoLR_in, homo_mono_in, monoLR_in, monoRL_in, can_mono_in)

• in ssreflect.v

  • structure NonPropType.call_of, constructor Call and field callee (now in ssreflect in Coq)
  • definitions maybeProp, call (now in ssreflect in Coq)
  • structure NonPropType.test_of, constructor Test and field condition (now in ssreflect in Coq, beware that implicit arguments of condition differ)
  • definitions test_Prop, test_negative (now in ssreflect in Coq)
  • structure NonPropType.type, constructor Check and fields result, test, frame (now in ssreflect in Coq, beware that implicit arguments of Check differ)
  • definition check (now in ssreflect in Coq, beware that implicit arguments of check differ)
  • notation [apply], [swap], [dup] in scope ssripat_scope (now in ssreflect in Coq)

• in ssrfun.v

  • lemmas Some_inj, of_voidK, inj_compr (now in ssrfun in Coq, beware that implicit arguments of inj_compr differ)
  • notation void (now in ssrfun in Coq)
  • definition of_void (now in ssrfun in Coq)

• in bigop.v

  • notation big_uncond
  • notations mulm_addl, mulm_addr, filter_index_enum

• in ssrnat.v

  • notations odd_add, odd_sub, iter_add, maxn_mulr, maxn_mull, minn_mulr, minn_mull, odd_opp, odd_mul, odd_exp, sqrn_sub

• in seq.v

  • notations take_addn, rot_addn, nseq_addn, allpairs_catr, allpairs_consr, perm_allpairs_rconsr, iota_addl

• in fintype.v

  • notations arg_minP, arg_maxP, bump_addl, unbump_addl, disjoint_trans

• in perm.v

  • notations tuple_perm_eqP, pcycle, pcycles, mem_pcycle, pcycle_id, uniq_traject_pcycle, pcycle_traject, iter_pcycle, eq_pcycle_mem, pcycle_sym, pcycle_perm, ncycles_mul_tperm

• in classfun.v

  • notation cf_triangle_lerif

• in action.v

  • notations pcycleE, pcycle_actperm

• in prime.v

  • notations primes_mul, primes_exp, pnat_mul, pnat_exp

• in path.v

  • notations sorted_lt_nth, sorted_le_nth, ltn_index, leq_index, subseq_order_path

• in div.v

  • notations coprime_mull, coprime_mulr, coprime_expl, coprime_expr

• in vector.v

  • notation limg_add

• in ssrint.v

  • notation polyC_mulrz

• in poly.v

  • notations polyC_add, polyC_opp, polyC_sub, polyC_muln, polyC_mul, polyC_inv, lead_coef_opp, derivn_sub

• in polydiv.v

  • notations rdivp_addl, rdivp_addr, rmodp_add, dvdp_scalel, dvdp_scaler, dvdp_opp, coprimep_scalel, coprimep_scaler, coprimep_mull, coprimep_mulr, modp_scalel, modp_scaler, modp_opp, modp_add, divp_scalel, divp_scaler, divp_opp, divp_add, modp_scalel, modp_scaler, modp_opp, modp_add, divp_scalel, divp_scaler, divp_opp, divp_add

• in mxalgebra.v

  • notations mulsmx_addl, mulsmx_addr

• in matrix.v

  • notations scalar_mx_comm, map_mx_sub

• in interval.v

  • notations @ 'lersif', lersif, x <= y ?< 'if' b, subr_lersifr0, subr_lersif0r, subr_lersif0, lersif_trans, lersif01, lersif_anti, lersifxx, lersifNF, lersifS, lersifT, lersifF, lersif_oppl, lersif_oppr, lersif_0oppr, lersif_oppr0, lersif_opp2, lersif_oppE, lersif_add2l, lersif_add2r, lersif_add2, lersif_subl_addr, lersif_subr_addr, lersif_sub_addr, lersif_subl_addl, lersif_subr_addl, lersif_sub_addl, lersif_andb, lersif_orb, lersif_imply, lersifW, ltrW_lersif, lersif_pmul2l, lersif_pmul2r, lersif_nmul2l, lersif_nmul2r, real_lersifN, real_lersif_norml, real_lersif_normr, lersif_nnormr, lersifN, lersif_norml, lersif_normr, lersif_distl, lersif_minr, lersif_minl, lersif_maxr, lersif_maxl, lersif_pdivl_mulr, lersif_pdivr_mulr, lersif_pdivl_mull, lersif_pdivr_mull, lersif_ndivl_mulr, lersif_ndivr_mulr, lersif_ndivl_mull, lersif_ndivr_mull, lersif_in_itv, itv_gte, ltr_in_itv, ler_in_itv, itv_splitU2, @ 'itv_intersection', itv_intersection, @ 'itv_intersection1i', itv_intersection1i, @ 'itv_intersectioni1', itv_intersectioni1, @ 'itv_intersectionii', itv_intersectionii, @ 'itv_intersectionC', itv_intersectionC, @ 'itv_intersectionA', itv_intersectionA

• in intdiv.v

  • notations coprimez_mull, coprimez_mulr, coprimez_expl, coprimez_expr

Infrastructure

• in builddoc_lib.sh:
  • change the sed command that removes all starred lines

Misc

• fix warning deprecated-hint-without-locality by adding the #[global] attribute to most hints
• turn warning deprecated-hint-without-locality into an error

[1.14.0] - 2022-01-19

This release is compatible with Coq versions 8.11, 8.12, 8.13, 8.14, and 8.15.

The contributors to this version are: Cyril Cohen, Erik Martin-Dorel, Kazuhiko Sakaguchi, Laurent Théry, Pierre Roux

Added

• in seq.v, added theorem pairwise_trans,

• in prime.v

  • theorems trunc_log0, trunc_log1, trunc_log_eq0, trunc_log_gt0, trunc_log0n, trunc_log1n, leq_trunc_log, trunc_log_eq, trunc_lognn, trunc_expnK, trunc_logMp, trunc_log2_double, trunc_log2S
  • definition up_log
  • theorems up_log0, up_log1, up_log_eq0, up_log_gt0, up_log_bounds , up_logP, up_log_gtn, up_log_min, leq_up_log, up_log_eq, up_lognn, up_expnK, up_logMp, up_log2_double, up_log2S, up_log_trunc_log, trunc_log_up_log

Changed

• in prime.v

  • definition trunc_log now it is 0 when p <= 1

• in ssrnum.v

  • generalized lemma rootCV so that the degree is not necessarily positive.

[1.13.0] - 2021-10-28

This release is compatible with Coq versions 8.11, 8.12, 8.13, and 8.14.

The contributors to this version are: Amel Kebbouche, Anders Mörtberg, Anton Trunov, Christian Doczkal, Cyril Cohen, Emilio Jesus Gallego Arias, Enrico Tassi, Erik Martin-Dorel, Evgenii Moiseenko, Florent Hivert, Gaëtan Gilbert, Kazuhiko Sakaguchi, Laurent Théry, Maxime Dénès, Pierre Jouvelot, Pierre Roux, Reynald Affeldt, Yves Bertot

Added

• Added intro pattern ltac views for rewrite: /[1! rules], /[! rules].

• in ssrbool.v, added lemmas negPP, andPP, orPP, and implyPP.

• In ssrnat.v: new lemmas fact_geq, leq_pfact, leq_fact, ltn_pfact, uphalf_leq, uphalf_gt0.

• in seq.v,

  • new higher-order predicate pairwise r xs which asserts that the relation r holds for any i-th and j-th element of xs such that i < j.
  • new lemmas allrel_mask(l|r), allrel_filter(l|r), sub(_in)_allrel, pairwise_cons, pairwise_cat, pairwise_rcons, pairwise2, pairwise_mask, pairwise_filter, pairwiseP, pairwise_all2rel, sub(_in)_pairwise, eq(_in)_pairwise, pairwise_map, subseq_pairwise, uniq_pairwise, pairwise_uniq, and pairwise_eq.
  • new lemmas zip_map, eqseq_all, and eq_map_all.
  • new lemmas count_undup, eq_count_undup, rev_take, rev_drop, takeEmask, dropEmask, filter_iota_ltn, filter_iota_leq, map_nth_iota0 and map_nth_iota
  • new lemmas cat_nilp, rev_nilp, allrelT, allrel_relI, and pairwise_relI.
  • new lemma undup_map_inj.
  • new lemmas: forall_cons, exists_cons, sub_map, eq_mem_map, eq_in_pmap.

• in path.v,

  • new lemmas: sorted_pairwise(_in), path_pairwise(_in), cycle_all2rel(_in), pairwise_sort, and sort_pairwise_stable.
  • new lemmas cat_sorted2, path_le, take_path, take_sorted, drop_sorted, undup_path, undup_sorted, count_merge, eq_count_merge
  • new lemmas: pairwise_sorted, path_relI, cycle_relI, sorted_relI, eq(_in)_sorted, mergeA, all_merge, and homo_sort_map(_in).

• in fintype.v, new lemma bij_eq_card.

• in fingraph.v, new lemmas: connect_rev, sym_connect_sym

• in finset.v,

  • new lemmas: bigcup0P, bigcup_disjointP, imset_cover, cover1, trivIset1, trivIsetD, trivIsetU, coverD1, partition0, partiton_neq0, partition_trivIset, partitionS, partitionD1, partitionU1, partition_set0, partition_pigeonhole, indexed_partition, imset_inj, imset_disjoint, imset_trivIset, imset0mem, imset_partition.
  • generalized eq_preimset, eq_imset, eq_in_imset, eq_in_imset2 to predicates (not only {set T}).

• in tuple.v, added type of bounded sequences n.-bseq T and its theory, i.e.

  • definition bseq with constructor Bseq,
  • notation n.-bseq, {bseq n of T}, [bseq of s], [bseq x1 ; .. ; xn], and [bseq], coercions to n.-tuple and to seq (which commute definitionally), definitions insub_bseq, in_bseq, cast_bseq, widen_bseq, bseq_tagged_tuple and tagged_tuple_bseq (the later two are mutual inverses).
  • canonical instances making n.-bseq canonically an eqType, a predType, a choiceType, a countType, a subCountType, a finType, a subFinType; and making nil, cons, rcons, behead, belast, cat, take, drop, rev, rot, rotr, map, scanl, pairmap, allpairs, and sort canonical _.-bseq.
  • lemmas size_bseq, bseqE, size_insub_bseq, cast_bseq_id, cast_bseqK, cast_bseqKV, cast_bseq_trans, size_cast_bseq, widen_bseq_id, cast_bseqEwiden, widen_bseqK, widen_bseq_trans, size_widen_bseq, in_bseqE, widen_bseq_in_bseq, bseq0, membsE, bseq_tagged_tupleK, tagged_tuple_bseqK,bseq_tagged_tuple_bij, and tagged_tuple_bseq_bij.
  • added Canonical tuple for sort.
  • new lemma val_tcast

• in bigop.v,

  • generalized lemma partition_big.
  • new lemmas big_pmap, sumnB, card_bseq, big_nat_widenl, big_geq_mkord, big_bool, big_rev_mkord, big_nat_mul

• in interval.v, new lemmas: ge_pinfty, le_ninfty, gt_pinfty, lt_ninfty.

• in order.v

  • we provide a canonical total order on ordinals and lemmas leEord, ltEord, botEord, and topEord to translate generic symbols to the concrete ones. Because of a shortcoming of the current interface, which requires finOrderType structures to be nonempty, the finOrderType is only defined for ordinal which are manifestly nonempty (i.e. 'I_n.+1).
  • we provide a canonical finite complemented distributive lattice structure on finite set ({set T}) ordered by inclusion and lemmas leEsubset, meetEsubset, joinEsubset, botEsubset, topEsubset subEsubset, complEsubset to translate generic symbols to the concrete ones.
  • new notation Order.enum A for sort <=%O (enum A), with new lemmas in module Order: cardE, mem_enum, enum_uniq, cardT, enumT, enum0, enum1, eq_enum, eq_cardT, set_enum, enum_set0, enum_setT, enum_set1, enum_ord, val_enum_ord, size_enum_ord, nth_enum_ord, nth_ord_enum, index_enum_ord, mono_sorted_enum, and mono_unique.
  • a new module Order.EnumVal (which can be imported locally), with definitions enum_rank_in, enum_rank, enum_val on a finite partially ordered type T, which are the same as the one from fintype.v, except they are monotonous when Order.le T is total. We provide the following lemmas: enum_valP, enum_val_nth, nth_enum_rank_in, nth_enum_rank, enum_rankK_in, enum_rankK, enum_valK_in, enum_valK, enum_rank_inj, enum_val_inj, enum_val_bij_in, eq_enum_rank_in, enum_rank_in_inj, enum_rank_bij, enum_val_bij, le_enum_val, le_enum_rank_in, and le_enum_rank. They are all accessible via module Order if one chooses not to import Order.EnumVal.
  • a new module tagnat which provides a monotonous bijection between the finite ordered types {i : 'I_n & 'I_(p_ i)} (canonically ordered lexicographically), and 'I_(\sum_i p_ i), via the functions sig and rank. We provide direct access to the components of the former type via the functions sig1, sig2 and Rank. We provide the following lemmas on these definitions: card, sigK, sig_inj, rankK, rank_inj, sigE12, rankE, sig2K, Rank1K, Rank2K, rank_bij, sig_bij , rank_bij_on, sig_bij_on, le_sig, le_sig1, le_rank, le_Rank, lt_sig, lt_rank, lt_Rank, eq_Rank, rankEsum, RankEsum, rect, and eqRank.
  • lemmas joins_le and meets_ge.
  • new lemmas le_sorted_ltn_nth, le_sorted_leq_nth, lt_sorted_leq_nth, lt_sorted_ltn_nth, filter_lt_nth, count_lt_nth, filter_le_nth, count_le_nth, count_lt_le_mem, sorted_filter_lt, sorted_filter_le, nth_count_le, nth_count_lt, count_le_gt, count_lt_ge, sorted_filter_gt, sorted_filter_ge, nth_count_ge, nth_count_lt and nth_count_eq
  • new lemmas (le|lt)_path_min, (le|lt)_path_sortedE, (le|lt)_(path|sorted)_pairwise, (le|lt)_(path|sorted)_(mask|filter), subseq_(le|lt)_(path|sorted), lt_sorted_uniq, sort_lt_id, perm_sort_leP, filter_sort_le, (sorted_)(mask|subseq)_sort_le, mem2_sort_le.
  • a new mixin meetJoinLeMixin constructing a latticeType from meet, join and proofs that those are respectvely the greatest lower bound and the least upper bound.

• in matrix.v,

  • seven new definitions: mxblock, mxcol, mxrow and mxdiag with notations \mxblock_(i < m, j < n) B_ i j, \mxcol_(i < m) B_ i, \mxrow_(j < n) B_ j, and \mxdiag_(i < n) B_ i (and variants without explicit < n), to form big matrices described by blocks.
  • submxblock, submxcol and submxrow to extract blocks from the former constructions. There is no analogous for mxdiag because one can simply apply submxblock A i i.
  • We provide the following lemmas on these definitions: mxblockEh, mxblockEv, submxblockEh, submxblockEv, mxblockK, mxrowK, mxcolK, submxrow_matrix, submxcol_matrix, submxblockK, submxrowK, submxcolK, mxblockP, mxrowP, mxcolP, eq_mxblockP, eq_mxblock, eq_mxrowP, eq_mxrow, eq_mxcolP, eq_mxcol, row_mxrow, col_mxrow, row_mxcol, col_mxcol, row_mxblock, col_mxblock, tr_mxblock, tr_mxrow, tr_mxcol, tr_submxblock, tr_submxrow, tr_submxcol, mxsize_recl, mxrow_recl, mxcol_recu, mxblock_recl, mxblock_recu, mxblock_recul, mxrowEblock, mxcolEblock, mxEmxrow, mxEmxcol, mxEmxblock, mxrowD, mxrowN, mxrowB, mxrow0, mxrow_const, mxrow_sum, submxrowD, submxrowN, submxrowB, submxrow0, submxrow_sum, mul_mxrow, mul_submxrow, mxcolD, mxcolN, mxcolB, mxcol0, mxcol_const, mxcol_sum, submxcolD, submxcolN, submxcolB, submxcol0, submxcol_sum, mxcol_mul, submxcol_mul, mxblockD, mxblockN, mxblockB, mxblock0, mxblock_const, mxblock_sum, submxblockD, submxblockN, submxblockB, submxblock0, submxblock_sum, mul_mxrow_mxcol, mul_mxcol_mxrow, mul_mxrow_mxblock, mul_mxblock_mxrow, mul_mxblock, is_trig_mxblockP, is_trig_mxblock, is_diag_mxblockP, is_diag_mxblock, submxblock_diag, eq_mxdiagP, eq_mxdiag, mxdiagD, mxdiagN, mxdiagB, mxdiag0, mxdiag_sum, tr_mxdiag, row_mxdiag, col_mxdiag, mxdiag_recl, mxtrace_mxblock, mxdiagZ, diag_mxrow, mxtrace_mxdiag, mul_mxdiag_mxcol, mul_mxrow_mxdiag, mul_mxblock_mxdiag, and mul_mxdiag_mxblock.
  • adding missing lemmas trmx_conform and eq_castmx.
  • new lemmas: row_thin_mx, col_flat_mx, col1, colE, mulmx_lsub, mulmx_rsub, mul_usub_mx, mul_dsub_mx, exp_block_diag_mx, block_diag_mx_unit, invmx_block_diag

• in mxalgegra.v,

  • Lemmas about rank of block matrices with 0s inside rank_col_mx0, rank_col_0mx, rank_row_mx0, rank_row_0mx, rank_diag_block_mx, and rank_mxdiag.
  • we provide an equality of spaces eqmx_col between \mxcol_i V_i and the sum of spaces \sum_i <<V_ i>>)%MS.

• In mxpoly.v

  • developed the theory of diagonalization. To that effect, we define conjmx, restrictmx, and notations A ~_P B, A ~_P {in S'}, A ~_{in S} B, A ~_{in S} {in S'}, all_simmx_in, diagonalizable_for, diagonalizable_in, diagonalizable, codiagonalizable_in, and codiagonalizable; and their theory: stablemx_comp, stablemx_restrict, conjmxM, conjMmx, conjuMmx, conjMumx, conjuMumx, conjmx_scalar, conj0mx, conjmx0, conjumx, conj1mx, conjVmx, conjmxK, conjmxVK, horner_mx_conj, horner_mx_uconj, horner_mx_uconjC, mxminpoly_conj, mxminpoly_uconj, sub_kermxpoly_conjmx, sub_eigenspace_conjmx, eigenpoly_conjmx, eigenvalue_conjmx, conjmx_eigenvalue, simmxPp, simmxW, simmxP, simmxRL, simmxLR, simmx_minpoly, diagonalizable_for_row_base, diagonalizable_forPp, diagonalizable_forP, diagonalizable_forPex, diagonalizable_forLR, diagonalizable_for_mxminpoly, diagonalizable_for_sum, codiagonalizable1, codiagonalizable_on, diagonalizable_diag, diagonalizable_scalar, diagonalizable0, diagonalizablePeigen, diagonalizableP, diagonalizable_conj_diag, and codiagonalizableP.
  • new lemmas row'_col'_char_poly_mx and char_block_diag_mx

• In ssralg.v

  • new lemma fmorph_eq
  • Canonical additive, linear and rmorphism for fst and snd
  • multi-rules linearE, rmorphE, and raddfE, for easier automatic reasoning with linear functions, morphisms, and additive functions.
  • new lemma eqr_div
  • new lemmas lregMl and rregMr

• In ssrnum.v:

  • new lemmas ltr_distlC, ler_distlC, new definition lter_distlC
  • new lemmas sqrtrV, eqNr

• in ssrint.v, new lemmas mulr_absz, natr_absz, lez_abs

• In intdiv.v

  • new definition lcmz
  • new lemmas dvdz_lcmr, dvdz_lcml, dvdz_lcm, lcmzC, lcm0z, lcmz0, lcmz_ge0, lcmz_neq0
  • new lemma lez_pdiv2r

• in polydiv.v, new lemma coprimep_XsubC2

• in poly.v, new lemmas monic_lreg and monic_rreg

• In rat.v

  • new lemmas minr_rat, maxr_rat
  • constants fracq, oppq, addq, mulq, invq, normq, le_rat, and lt_rat are "locked" when applied to variables, computation occurs only when applied to constructors. Moreover the new definition of fracq ensures that if x and y of type int * int represent the same rational then fracq x is definitionally equal to fracq y (i.e. the underlying proofs are the same). Additionally, addq and mulq are tuned to minimize the number of integer arithmetic operations when the denominators are equal to one.
  • notation [rat x // y] for displaying the normal form of a rational. We also provide the parsable notation for debugging purposes.

• In binomial.v: new lemma fact_split

• In interval.v: new lemmas subset_itv, subset_itv_oo_cc, subset_itv_oo_oc, subset_itv_oo_co, subset_itv_oc_cc, subset_itv_co_cc, itvxx, itvxxP

• In perm.v: new lemma perm_onV, porbitV, porbitsV

Changed

• In ssrnum.v, lemma normr_nneg, declared a Hint Resolve in the core database

• In ssralg.v and ssrint.v, the nullary ring notations -%R, +%R, *%R, *:%R, and *~%R are now declared in fun_scope.

• across the library, the deprecation mechanism to use has been changed from the deprecate notation to the deprecated attribute (cf. Removed section).

• in finalg.v, finFieldType now inherits from countDecFieldType.

• fact_smonotone moved from binomial.v to ssrnat.v and renamed to ltn_fact.

• in presentation.v fixes the doc wrongly describing the meaning of G \isog Grp( ... )

Renamed

• in path.v,

  • sub_(path|cycle|sorted)_in -> sub_in_(path|cycle|sorted)
  • eq_(path|cycle)_in -> eq_in_(path|cycle)

• in order.v

  • join_(|sup_|min_)seq -> joins_(|sup_|min_)seq
  • meet_(|sup_|min_)seq -> meets_(|sup_|min_)seq
  • join_(sup|min) -> joins_(sup|min)

• in matrix.v, card_matrix -> card_mx

• in ssralg.v, prodr_natmul -> prodrMn

• in bigop.v, big_uncond -> big_rmcond

• in finset

  • mem_imset_eq -> mem_imset
  • mem_imset2_eq -> mem_imset2

Removed

• in ssreflect.v, the deprecate notation has been deprecated. Use the deprecated attribute instead (cf. Changed section).

• in seq.v, iota_add has been deprecated. Use iotaD instead.

• in ssrnat.v and ssrnum.v, deprecation aliases and the mc_1_10 compatibility modules introduced in MathComp 1.11+beta1 have been removed.

• in seq.v, remove the following deprecation aliases introduced in MathComp 1.9.0: perm_eq_rev, perm_eq_flatten, perm_eq_all, perm_eq_small, perm_eq_nilP, perm_eq_consP, leq_size_perm, uniq_perm_eq, perm_eq_iotaP, and perm_undup_count.

• in path.v, remove the deprecation aliases eq(_in)_sorted introduced in MathComp 1.12.0. These names of lemmas are now taken by new lemmas (cf. Added section).

• in order.v, remove the deprecation aliases eq_sorted_(le|lt).

Infrastructure

• The way hierarchy.ml recognizes inheritance has been changed: S1 inherits from S2 when there is a coercion path from S1.sort to S2.sort and there is a canonical structure instance that unifies S1.sort and S2.sort, regardless of where (which module) these constants are declared. As a result, it recognizes non-forgetful inheritance and checks the uniqueness of join and exhaustiveness of canonical declarations involving it.

[1.12.0] - 2020-11-26

This release is compatible with Coq versions 8.10, 8.11, and 8.12.

The contributors to this version are: Anton Trunov, Christian Doczkal, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Jasper Hugunin, Kazuhiko Sakaguchi, Laurent Théry, Reynald Affeldt, and Yves Bertot.

Added

• Contraposition lemmas involving propositions:

  • in ssrbool.v: contra_not, contraPnot, contraTnot, contraNnot, contraPT, contra_notT, contra_notN, contraPN, contraFnot, contraPF and contra_notF.
  • in eqtype.v: contraPeq, contra_not_eq, contraPneq, and contra_neq_not, contra_not_neq, contra_eq_not.

• Contraposition lemmas involving inequalities:

  • in ssrnat.v: contraTleq, contraTltn, contraNleq, contraNltn, contraFleq, contraFltn, contra_leqT, contra_ltnT, contra_leqN, contra_ltnN, contra_leqF, contra_ltnF, contra_leq, contra_ltn, contra_leq_ltn, contra_ltn_leq, contraPleq, contraPltn, contra_not_leq, contra_not_ltn, contra_leq_not, contra_ltn_not
  • in order.v: comparable_contraTle, comparable_contraTlt, comparable_contraNle, comparable_contraNlt, comparable_contraFle, comparable_contraFlt, contra_leT, contra_ltT, contra_leN, contra_ltN, contra_leF, contra_ltF, comparable_contra_leq_le, comparable_contra_leq_lt, comparable_contra_ltn_le, comparable_contra_ltn_lt, contra_le_leq, contra_le_ltn, contra_lt_leq, contra_lt_ltn, comparable_contra_le, comparable_contra_le_lt, comparable_contra_lt_le, comparable_contra_lt, contraTle, contraTlt, contraNle, contraNlt, contraFle, contraFlt, contra_leq_le, contra_leq_lt, contra_ltn_le, contra_ltn_lt, contra_le, contra_le_lt, contra_lt_le, contra_lt, contra_le_not, contra_lt_not, comparable_contraPle, comparable_contraPlt, comparable_contra_not_le, comparable_contra_not_lt, contraPle, contraPlt, contra_not_le, contra_not_lt

• in ssreflect.v, added intro pattern ltac views for dup, swap, apply: /[apply], /[swap] and /[dup].

• in ssrbool.v (waiting to be integrated in Coq)

  • generic lemmas about interaction between {in _, _} and {on _, _}: in_on1P, in_on1lP, in_on2P, on1W_in, on1lW_in, on2W_in, in_on1W, in_on1lW, in_on2W, on1S, on1lS, on2S, on1S_in, on1lS_in, on2S_in, in_on1S, in_on1lS, in_on2S.
  • lemmas about interaction between {in _, _} and sig: in1_sig, in2_sig, and in3_sig.

• in ssrnat.v, new lemmas: subn_minl, subn_maxl, oddS, subnA, addnBn, addnCAC, addnACl, iterM, iterX

• in seq.v,

  • new lemmas take_uniq, drop_uniq
  • new lemma mkseqP to abstract a sequence s with mkseq f n, where f and n are fresh variables.
  • new high-order relation allrel r xs ys which asserts that r x y holds whenever x is in xs and y is in ys, new notation all2rel r xs (:= allrel r xs xs) which asserts that r holds on all pairs of elements of xs, and
    • lemmas allrel0(l|r), allrel_cons(l|r|2), allrel1(l|r), allrel_cat(l|r), allrel_allpairsE, eq_in_allrel, eq_allrel, allrelC, allrel_map(l|r), allrelP,
    • new lemmas all2rel1, all2rel2, and all2rel_cons under assumptions of symmetry of r.
  • new lemmas allss, all_mask, and all_sigP. allss has also been declared as a hint.
  • new lemmas index_pivot, take_pivot, rev_pivot, eqseq_pivot2l, eqseq_pivot2r, eqseq_pivotl, eqseq_pivotr uniq_eqseq_pivotl, uniq_eqseq_pivotr, mask_rcons, rev_mask, subseq_rev, subseq_cat2l, subseq_cat2r, subseq_rot, and uniq_subseq_pivot.
  • new lemmas find_ltn, has_take, has_take_leq, index_ltn, in_take, in_take_leq, split_find_nth, split_find and nth_rcons_cat_find.
  • added drop_index, in_mask, mask0s, cons_subseq, undup_subseq, leq_count_mask, leq_count_subseq, count_maskP, count_subseqP, count_rem, count_mem_rem, rem_cons, remE, subseq_rem, leq_uniq_countP, and leq_uniq_count.
  • new definition rot_add and new lemmas rot_minn, leq_rot_add, rot_addC, rot_rot_add.
  • new lemmas perm_catACA, allpairs0l, allpairs0r, allpairs1l, allpairs1r, allpairs_cons, eq_allpairsr, allpairs_rcons, perm_allpairs_catr, perm_allpairs_consr, mem_allpairs_rconsr, and allpairs_rconsr (with the alias perm_allpairs_rconsr for the sake of uniformity, but which is already deprecated in favor of allpairs_rconsr, cf renamed section).

• in path.v,

  • new lemmas sub_cycle(_in), eq_cycle_in, (path|sorted)_(mask|filter)_in, rev_cycle, cycle_map, (homo|mono)_cycle(_in).
  • new lemma sort_iota_stable.
  • new lemmas order_path_min_in, path_sorted_inE, sorted_(leq|ltn)_nth_in, subseq_path_in, subseq_sorted_in, sorted_(leq|ltn)_index_in, sorted_uniq_in, sorted_eq_in, irr_sorted_eq_in, sort_sorted_in, sorted_sort_in, perm_sort_inP, all_sort, sort_stable_in, filter_sort_in, (sorted_)mask_sort_in, (sorted_)subseq_sort_in, and mem2_sort_in.
  • added size_merge_sort_push, which documents an invariant of merge_sort_push.

• in fintype.v,

  • new lemmas card_geqP, card_gt1P, card_gt2P, card_le1_eqP (generalizes fintype_le1P),
  • adds lemma split_ordP, a variant of splitP which introduces ordinal equalities between the index and lshift/rshift, rather than equalities in nat, which in some proofs makes the reasoning easier (cf matrix.v), especially together with the new lemma eq_shift (which is a multi-rule for new lemmas eq_lshift, eq_rshift, eq_lrshift and eq_rlshift).
  • new lemmas eq_liftF and lift_eqF.
  • new lemmas disjointFr, disjointFl, disjointWr, disjointW
  • new (pigeonhole) lemmas leq_card_in, leq_card,
  • added mask_enum_ord.

• in finset.v

  • new lemmas set_enum, cards_eqP, cards2P
  • new lemmas properC, properCr, properCl
  • new lemmas mem_imset_eq, mem_imset2_eq. These lemmas will lose the _eq suffix in the next release, when the shortende names will become available (cf. Renamed section)
  • new lemma disjoints1

• in order.v

  • new lemmas comparable_bigl and comparable_bigr.
  • added a factory distrLatticePOrderMixin to build a distrLatticeType from a porderType.
  • new notations 0^d and 1^d for bottom and top elements of dual lattices.
  • new definition lteif and notations <?<=%O, <?<=^d%O, _ < _ ?<= if _, and _ <^d _ ?<= if _ (cf Changed section).
  • new lemmas lteifN, comparable_lteifNE, and comparable_lteif_(min|max)(l|r).

• in bigop.v,

  • new lemma sig_big_dep, analogous to pair_big_dep but with an additional dependency in the index types I and J.
  • new lemma reindex_omap generalizes reindex_onto to the case where the inverse function to h is partial (i.e. with codomain option J, to cope with a potentially empty J.
  • new lemma bigD1_ord takes out an element in the middle of a \big_(i < n) and reindexes the remainder using lift.
  • new lemma big_uncond. The ideal name is big_rmcond but it has just been deprecated from its previous meaning (see Changed section) so as to reuse it in next mathcomp release.
  • new lemma big_uncond_in is a new alias of big_rmcond_in for the sake of uniformity, but it is already deprecated and will be removed two releases from now.
  • added big_mask_tuple and big_mask.

• in fingraph.v, new lemmas fcard_gt0P, fcard_gt1P

• in perm.v, new lemma permS01.

• in ssralg.v

  • new lemmas sumr_const_nat and iter_addr_0
  • new lemmas iter_addr, iter_mulr, iter_mulr_1, and prodr_const_nat.
  • new lemma raddf_inj, characterizing injectivity for additive maps.
  • Lemma expr_sum : equivalent for ring of expn_sum
  • Lemma prodr_natmul : generalization of prodrMn_const. Its name will become prodrMn in the next release when this name will become available (cf. Renamed section).

• in poly.v, new lemma commr_horner.

• in polydiv.v, new lemma dvdpNl.

• in matrix.v,

  • new definitions is_diag_mx and is_trig_mx characterizing respectively diagonal and lower triangular matrices. We provide the new lemmas row_diag_mx, is_diag_mxP, diag_mxP, diag_mx_is_diag, mx0_is_diag, is_trig_mxP, is_diag_mx_is_trig, diag_mx_trig, mx0_is_trig, scalar_mx_is_diag, is_scalar_mx_is_diag, scalar_mx_is_trig and is_scalar_mx_is_trig.
  • new lemmas matrix_eq0, matrix0Pn, rV0Pn and cV0Pn to characterize nonzero matrices and find a nonzero coefficient.
  • new predicate mxOver S qualified with \is a, and
    • new lemmas mxOverP, mxOverS, mxOver_const, mxOver_constE, thinmxOver, flatmxOver, mxOver_scalar, mxOver_scalarE, mxOverZ, mxOverM, mxOver_diag, mxOver_diagE.
    • new canonical structures:
      • mxOver S is closed under addition if S is.
      • mxOver S is closed under negation if S is.
      • mxOver S is a sub Z-module if S is.
      • mxOver S is a semiring for square matrices if S is.
      • mxOver S is a subring for square matrices if S is.
  • new lemmas about map_mx: map_mx_id, map_mx_comp, eq_in_map_mx, eq_map_mx and map_mx_id_in.
  • new lemmas row_usubmx, row_dsubmx, col_lsubmx, and col_rsubmx.
  • new lemma mul_rVP.
  • new inductions lemmas: row_ind, col_ind, mx_ind, sqmx_ind, ringmx_ind, trigmx_ind, trigsqmx_ind, diagmx_ind, diagsqmx_ind.
  • added missing lemma trmx_eq0, det_mx11.
  • new lemmas about diagonal and triangular matrices: mx11_is_diag, mx11_is_trig, diag_mx_row, is_diag_mxEtrig, is_diag_trmx, ursubmx_trig, dlsubmx_diag, ulsubmx_trig, drsubmx_trig, ulsubmx_diag, drsubmx_diag, is_trig_block_mx, is_diag_block_mx, and det_trig.
  • new definition mxsub, rowsub and colsub, corresponding to arbitrary submatrices/reindexation of a matrix.
    • we provide the theorems x?(row|col)(_perm|')?Esub, t?permEsub [lrud]submxEsub, (ul|ur|dl|dr)submxEsub for compatibility with ad-hoc submatrices/permutations.
    • we provide a new, configurable, induction lemma mxsub_ind.
    • we provide the basic theory mxsub_id, eq_mxsub, eq_rowsub, eq_colsub, mxsub_eq_id, mxsub_eq_colsub, mxsub_eq_rowsub, mxsub_ffunl, mxsub_ffunr, mxsub_ffun, mxsub_const, mxsub_comp, rowsub_comp, colsub_comp, mxsubrc, mxsubcr, trmx_mxsub, row_mxsub, col_mxsub, row_rowsub, col_colsub, and map_mxsub, pid_mxErow and pid_mxEcol.
    • interaction with castmx through lemmas rowsub_cast, colsub_cast, mxsub_cast, and castmxEsub.
    • (mx|row|col)sub are canonically additive and linear.
    • interaction with mulmx through lemmas mxsub_mul, mul_rowsub_mx, mulmx_colsub, and rowsubE.
  • added comm_mx and comm_mxb the propositional and boolean versions of matrix commutation, comm_mx A B is definitionally equal to GRing.comm A B when A B : 'M_n.+1, this is witnessed by the lemma comm_mxE. New notation all_comm_mx stands for allrel comm_mxb. New lemmas comm_mx_sym, comm_mx_refl, comm_mx0, comm0mx, comm_mx1, comm1mx, comm_mxN, comm_mxN1, comm_mxD, comm_mxB, comm_mx_sum, comm_mxP, all_comm_mxP, all_comm_mx1, all_comm_mx2P, all_comm_mx_cons, comm_mx_scalar, and comm_scalar_mx. The common arguments of these lemmas R and n are maximal implicits.

• in mxalgebra.v,

  • completed the theory of pinvmx in corner cases, using lemmas mulmxVp, mulmxKp, pinvmxE, mulVpmx, pinvmx_free, and pinvmx_full.
  • new lemmas row_base0, sub_kermx, kermx0 and mulmx_free_eq0.
  • new lemma sub_sums_genmxP (generalizes sub_sumsmxP).
  • new lemma rowsub_sub, eq_row_full, row_full_castmx, row_free_castmx, rowsub_comp_sub, submx_rowsub, eqmx_rowsub_comp_perm, eqmx_rowsub_comp, eqmx_rowsub, row_freePn, and negb_row_free.
  • new lemma row_free_injr which duplicates row_free_inj but exposing mulmxr for compositionality purposes (e.g. with raddf_eq0), and lemma inj_row_free characterizing row_free matrices A through v *m A = 0 -> v = 0 for all v.
  • new notation stablemx V f asserting that f stabilizes V, with new theorems: eigenvectorP, eqmx_stable, stablemx_row_base, stablemx_full, stablemxM, stablemxD, stablemxN, stablemxC, stablemx0, stableDmx, stableNmx, stable0mx, stableCmx, stablemx_sums, and stablemx_unit.
  • added comm_mx_stable, comm_mx_stable_ker, and comm_mx_stable_eigenspace.
  • new definitions maxrankfun, fullrankfun which are "subset function" to be plugged in rowsub, with lemmas: maxrowsub_free, eq_maxrowsub, maxrankfun_inj, maxrowsub_full, fullrowsub_full, fullrowsub_unit, fullrowsub_free, mxrank_fullrowsub, eq_fullrowsub, and fullrankfun_inj.

• in mxpoly.v,

  • new lemmas mxminpoly_minP and dvd_mxminpoly.
  • new lemmas horner_mx_diag and char_poly_trig, root_mxminpoly, and mxminpoly_diag
  • new definitions kermxpoly g p (the kernel of polynomial $p(g)$).
    • new elementary theorems: kermxpolyC, kermxpoly1, kermxpolyX, kermxpoly_min
    • kernel lemmas: mxdirect_kermxpoly, kermxpolyM, kermxpoly_prod, and mxdirect_sum_kermx
    • correspondance between eigenspace and kermxpoly: eigenspace_poly
  • generalized eigenspace geigenspace and a generalization of eigenvalues called eigenpoly g (i.e. polynomials such that kermxpoly g p is nonzero, e.g. eigen polynomials of degree 1 are of the form 'X - a%:P where a are eigenvalues), and
    • correspondance with kermx: geigenspaceE,
    • application of kernel lemmas mxdirect_sum_geigenspace,
    • new lemmas: eigenpolyP, eigenvalue_poly, eigenspace_sub_geigen,
  • new map_mx lemmas: map_kermxpoly, map_geigenspace, eigenpoly_map.
  • new lemma horner_mx_stable.
  • added comm_mx_horner, comm_horner_mx, comm_horner_mx2, horner_mx_stable, comm_mx_stable_kermxpoly, and comm_mx_stable_geigenspace.

• in ssrnum.v,

  • new lemma ler_sum_nat
  • new lemmas big_real, sum_real, prod_real, max_real, min_real, bigmax_real, and bigmin_real.
  • new lemma real_lteif_distl.

• in interval.v,

  • intervals and their bounds of T now have canonical ordered type instances whose ordering relations are the subset relation and the left to right ordering respectively. They form partially ordered types if T is a porderType. If T is a latticeType, they also form tbLatticeType where the join and meet are intersection and convex hull respectively. If T is an orderType, they are distributive, and the interval bounds are totally ordered. (cf Changed section)
  • new lemmas bound_ltxx, subitvE, in_itv, itv_ge, in_itvI, itv_total_meet3E, and itv_total_join3E.

Changed

• in ssrbool.v, use Reserved Notation for [rel _ _ : _ | _] to avoid warnings with coq-8.12

• in seq.v, mask will only expand if both arguments are constructors, the case mask [::] s can be dealt with using mask0s or explicit conversion.

• in path.v,

  • generalized lemmas sub_path_in, sub_sorted_in, and eq_path_in for non-eqTypes.
  • generalized lemmas sorted_ltn_nth and sorted_leq_nth (formerly sorted_lt_nth and sorted_le_nth, cf Renamed section) for non-eqTypes.

• in fintype.v,

  • added lemma ord1, it is the same as zmodp.ord1, except fintype.ord1 does not rely on 'I_n zmodType structure.
  • rename disjoint_trans to disjointWl
  • lemmas inj_card_onto and inj_card_bij take a weaker hypothesis (i.e. #|T| >= #|T'| instead of #|T| = #|T'| thanks to leq_card under injectivity assumption).

• in finset.v, fixed printing of notation [set E | x in A , y in B & P ]

• in bigop.v, lemma big_rmcond is deprecated and has been renamed big_rmcomd_in (and aliased big_uncond_in, see Added). The variant which does not require an eqType is currently named big_uncond (cf Added) but it will be renamed big_mkcond in the next release.

• in ssrAC.v, fix non-reversible-notation warnings

• in order.v,

  • in the definition of structures, displays are removed from parameters of mixins and fields of classes internally and now only appear in parameters of structures. Consequently, each mixin is now parameterized by a class rather than a structure, and the corresponding factory parameterized by a structure is provided to replace the use of the mixin. These factories have the same names as in the mixins before this change except that bLatticeMixin and tbLatticeMixin have been renamed to bottomMixin and topMixin respectively.
  • the dual_* notations such as dual_le are now qualified with the Order module.
  • \join^d_ and \meet^d_ notations are now properly specialized for dual_display.
  • rephrased comparable_(min|max)[rl] in terms of {in _, forall x y, _}, hence reordering the arguments. Made them hints for smoother combination with comparable_big[lr].
  • >=< y now stands for [pred x | x >=< y]
  • >< y now stands for [pred x | x >< y]
  • and the same holds for the dual >=<^d, ><^d, the product >=<^p, ><^p, and lexicographic >=<^l, ><^l. The previous meanings can be obtained through >=<%O x and ><%O x.
  • generalized sort_le_id for any porderType.
  • the names of lemmas join_idPl and join_idPr are transposed to follow the naming convention.

• In ssrnum.v,

  • >=< y now stands for [pred x | x >=< y]
  • fixed notations @minr and @maxr to point Order.min and Order.max respectively.

• in ssrint.v, generalized mulpz for any ringType.

• in interval.v:

  • x <= y ?< if c (lersif) has been generalized to porderType, relocated to order.v, and replaced with x < y ?<= if c' (lteif) where c' is negation of c.
  • Many definitions and lemmas on intervals such as the membership test are generalized from numeric domains to ordered types.
  • Interval bounds itv_bound : Type -> Type are redefined with two constructors BSide : bool -> T -> itv_bound T and BInfty : bool -> itv_bound T. New notations BLeft and BRight are aliases for BSide true and BSide false respectively. BInfty false and BInfty true respectively means positive and negative infinity. BLeft x and BRight x respectively mean close and open bounds as left bounds, and they respectively mean open and close bounds as right bounds. This change gives us the canonical "left to right" ordering of interval bounds.
  • Lemmas mid_in_itv(|oo|cc) have been generalized from realFieldType to numFieldType.

• In matrix.v, generalized diag_mx_comm and scalar_mx_comm to all n, instead of n'.+1, thanks to commmmx.

Renamed

• in ssrnat.v

  • iter_add -> iterD
  • maxn_mul(l|r) -> maxnM(l|r)
  • minn_mul(l|r) -> minnM(l|r)
  • odd_(opp|mul|exp) -> odd(N|M|X)
  • sqrn_sub -> sqrnB

• in div.v

  • coprime_mul(l|r) -> coprimeM(l|r)
  • coprime_exp(l|r) -> coprimeX(l|r)

• in prime.v

  • primes_(mul|exp) -> primes(M|X)
  • pnat_(mul|exp) -> pnat(M|X)

• in seq.v,

  • iota_add(|l) -> iotaD(|l)
  • allpairs_(cons|cat)r -> mem_allpairs_(cons|cat)r (allpairs_consr and allpairs_catr are now deprecated alias, and will be attributed to the new perm_allpairs_catr).

• in path.v,

  • eq_sorted(_irr) -> (irr_)sorted_eq
  • sorted_(lt|le)_nth -> sorted_(ltn|leq)_nth
  • (ltn|leq)_index -> sorted_(ltn|leq)_index
  • subseq_order_path -> subseq_path

• in fintype.v

  • bump_addl -> bumpDl
  • unbump_addl -> unbumpDl

• in finset.v,

  • mem_imset -> imset_f (with deprecation alias, cf. Added section)
  • mem_imset2 -> imset2_f (with deprecation alias, cf. Added section)

• in bigop.v

  • big_rmcond -> big_rmcond_in (cf Changed section)
  • mulm_add(l|r) -> mulmD(l|r)

• in order.v, eq_sorted_(le|lt) -> (le|lt)_sorted_eq

• in interval.v, we deprecate, rename, and relocate to order.v the following:

  • lersif_(trans|anti) -> lteif_(trans|anti)
  • lersif(xx|NF|S|T|F|W) -> lteif(xx|NF|S|T|F|W)
  • lersif_(andb|orb|imply) -> lteif_(andb|orb|imply)
  • ltrW_lersif -> ltrW_lteif
  • lersifN -> lteifNE
  • lersif_(min|max)(l|r) -> lteif_(min|max)(l|r)

• in interval.v, we deprecate, rename, and relocate to ssrnum.v the following:

  • subr_lersif(r0|0r|0) -> subr_lteif(r0|0r|0)
  • lersif01 -> lteif01
  • lersif_(oppl|oppr|0oppr|oppr0|opp2|oppE) -> lteif_(oppl|oppr|0oppr|oppr0|opp2|oppE)
  • lersif_add2(|l|r) -> lteif_add2(|l|r)
  • lersif_sub(l|r)_add(l|r) -> lteif_sub(l|r)_add(l|r)
  • lersif_sub_add(l|r) -> lteif_sub_add(l|r)
  • lersif_(p|n)mul2(l|r) -> lteif_(p|n)mul2(l|r)
  • real_lersifN -> real_lteifNE
  • real_lersif_norm(l|r) -> real_lteif_norm(l|r)
  • lersif_nnormr -> lteif_nnormr
  • lersif_norm(l|r) -> lteif_norm(l|r)
  • lersif_distl -> lteif_distl
  • lersif_(p|n)div(l|r)_mul(l|r) -> lteif_(p|n)div(l|r)_mul(l|r)

• in interval.v, we deprecate and replace the following:

  • lersif_in_itv -> lteif_in_itv
  • itv_gte -> itv_ge
  • l(t|e)r_in_itv -> lt_in_itv

• in ssralg.v, prodrMn-> prodrMn_const (with deprecation alias, cf. Added section)

• in ssrint.v, polyC_mulrz -> polyCMz

• in poly.v

  • polyC_(add|opp|sub|muln|mul|inv) -> polyC(D|N|B|Mn|M|V)
  • lead_coef_opp -> lead_coefN
  • derivn_sub -> derivnB

• in polydiv.v

  • rdivp_add(l|r) -> rdivpD(l|r)
  • rmodp_add -> rmodpD
  • dvdp_scale(l|r) -> dvdpZ(l|r)
  • dvdp_opp -> dvdpNl
  • coprimep_scale(l|r) -> coprimepZ(l|r)
  • coprimep_mul(l|r) -> coprimepM(l|r)
  • modp_scale(l|r) -> modpZ(l|r)
  • modp_(opp|add|scalel|scaler) -> modp(N|D|Zl|Zr)
  • divp_(opp|add|scalel|scaler) -> divp(N|D|Zl|Zr)

• in matrix.v, map_mx_sub -> map_mxB

• in mxalgebra.v, mulsmx_add(l|r) -> mulsmxD(l|r)

• in vector.v, limg_add -> limgD

• in intdiv.v

  • coprimez_mul(l|r) -> coprimezM(l|r)
  • coprimez_exp(l|r) -> coprimezX(l|r)

Removed

• in ssrnat.v, we remove the compatibility module mc_1_9.

• in interval.v, we remove the following:

  • le_bound(l|r) (use Order.le instead)
  • le_bound(l|r)_refl (use lexx instead)
  • le_bound(l|r)_anti (use eq_le instead)
  • le_bound(l|r)_trans (use le_trans instead)
  • le_bound(l|r)_bb (use bound_lexx instead)
  • le_bound(l|r)_total (use le_total instead)

• in interval.v, we deprecate the following:

  • itv_intersection (use Order.meet instead)
  • itv_intersection1i (use meet1x instead)
  • itv_intersectioni1 (use meetx1 instead)
  • itv_intersectionii (use meetxx instead)
  • itv_intersectionC (use meetC instead)
  • itv_intersectionA (use meetA instead)

• in mxpoly.v, we deprecate scalar_mx_comm, and advise to use comm_mxC instead (with maximal implicit arguments R and n).

Infrastructure

• in all the hierarchies (in eqtype.v, choice.v, order.v, ssralg.v,...), the class_of records of structures are turned into primitive records to prevent prevent potential issues of ambiguous paths and convertibility of structure instances.

• across the library, the following constants have been tuned to only reduce when they do not expose a match: subn_rec, decode_rec, nth (thus avoiding a notorious problem of p`_0 expanding too eagerly), set_nth, take, drop, eqseq, incr_nth, elogn2, binomial_rec, sumpT.

[1.11.0] - 2020-06-09

This release is compatible with Coq versions 8.7, 8.8, 8.9, 8.10, and 8.11.

The contributors to this version are: Antonio Nikishaev, Anton Trunov, Assia Mahboubi, Christian Doczkal, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Florent Hivert, Kazuhiko Sakaguchi, Pierre-Marie Pédrot, Pierre-Yves Strub, Reynald Affeldt, Simon Boulier, Yves Bertot.

• Added lemmas about monotony of functions nat -> T where T is an ordered type: homo_ltn_lt_in, incn_inP, nondecn_inP, nhomo_ltn_lt_in, decn_inP, nonincn_inP, homo_ltn_lt, incnP, nondecnP, nhomo_ltn_lt, decnP, nonincnP in file order.v.

• Added lemmas for swapping arguments of homomorphisms and monomorphisms: homo_sym, mono_sym, homo_sym_in, mono_sym_in, homo_sym_in11, mono_sym_in11 in ssrbool.v

Added

• in ssrnum.v, new lemmas:

  • (real_)ltr_normlW, (real_)ltrNnormlW, (real_)ler_normlW, (real_)lerNnormlW
  • (real_)ltr_distl_addr, (real_)ler_distl_addr, (real_)ltr_distlC_addr, (real_)ler_distlC_addr, (real_)ltr_distl_subl, (real_)ler_distl_subl, (real_)ltr_distlC_subl, (real_)ler_distlC_subl

• in order.v, defining min and max independently from meet and join, and providing a theory about for min and max, hence generalizing the theory of Num.min and Num.max from versions <= 1.10, instead of specializing to total order as in 1.11+beta1:

  Definition min (T : porderType) (x y : T) := if x < y then x else y.
  Definition max (T : porderType) (x y : T) := if x < y then y else x.
  

  • Lemmas: min_l, min_r, max_l, max_r, minxx, maxxx, eq_minl, eq_maxr, min_idPl, max_idPr, min_minxK, min_minKx, max_maxxK, max_maxKx, comparable_minl, comparable_minr, comparable_maxl, and comparable_maxr
  • Lemmas about interaction with lattice operations: meetEtotal, joinEtotal,
  • Lemmas under condition of pairwise comparability of a (sub)set of their arguments: comparable_minC, comparable_maxC, comparable_eq_minr, comparable_eq_maxl, comparable_le_minr, comparable_le_minl, comparable_min_idPr, comparable_max_idPl, comparableP, comparable_lt_minr, comparable_lt_minl, comparable_le_maxr, comparable_le_maxl, comparable_lt_maxr, comparable_lt_maxl, comparable_minxK, comparable_minKx, comparable_maxxK, comparable_maxKx, comparable_minA, comparable_maxA, comparable_max_minl, comparable_min_maxl, comparable_minAC, comparable_maxAC, comparable_minCA, comparable_maxCA, comparable_minACA, comparable_maxACA, comparable_max_minr, comparable_min_maxr
  • and the same but in a total order: minC, maxC, minA, maxA, minAC, maxAC, minCA, maxCA, minACA, maxACA, eq_minr, eq_maxl, min_idPr, max_idPl, le_minr, le_minl, lt_minr, lt_minl, le_maxr,le_maxl, lt_maxr, lt_maxl, minxK, minKx, maxxK, maxKx, max_minl, min_maxl, max_minr, min_maxr

• in ssrnum.v, theory about min and max extended to numDomainType:

  • Lemmas: real_oppr_max, real_oppr_min, real_addr_minl, real_addr_minr, real_addr_maxl, real_addr_maxr, minr_pmulr, maxr_pmulr, real_maxr_nmulr, real_minr_nmulr, minr_pmull, maxr_pmull, real_minr_nmull, real_maxr_nmull, real_maxrN, real_maxNr, real_minrN, real_minNr

• the compatibility module ssrnum.mc_1_10 was extended to support definitional compatibility with min and max which had been lost in 1.11+beta1 for most instances.

• in fintype.v, new lemmas: seq_sub_default, seq_subE

• in order.v, new "unfolding" lemmas: minEnat and maxEnat

• in ssrbool.v

  • lemmas about the cancel predicate and {in _, _}/{on _, _} notations:
    • onW_can, onW_can_in, in_onW_can, onS_can, onS_can_in, in_onS_can
  • lemmas about the cancel predicate and injective functions:
    • inj_can_sym_in_on, inj_can_sym_on, inj_can_sym_in

Changed

• in order.v, le_xor_gt, lt_xor_ge, compare, incompare, lel_xor_gt, ltl_xor_ge, comparel, incomparel have more parameters, so that the the following now deal with min and max

  • comparable_ltgtP, comparable_leP, comparable_ltP, comparableP
  • lcomparableP, lcomparable_ltgtP, lcomparable_leP, lcomparable_ltP, ltgtP

• in order.v:

  • [arg min_(i < i0 | P) M] now for porderType (was for orderType)
  • [arg max_(i < i0 | P) M] now for porderType (was for orderType)
  • added comparable_arg_minP, comparable_arg_maxP, real_arg_minP, real_arg_maxP, in order to take advantage of the former generalizations.

• in ssrnum.v, maxr is a notation for (@Order.max ring_display _) (was Order.join) (resp. minr is a notation for (@Order.min ring_display _))

• in ssrnum.v, ler_xor_gt, ltr_xor_ge, comparer, ger0_xor_lt0, ler0_xor_gt0, comparer0 have now more parameters, so that the following now deal with min and max:

  • real_leP, real_ltP x y, real_ltgtP, real_ge0P, real_le0P, real_ltgt0P
  • lerP, ltrP, ltrgtP, ger0P, ler0P, ltrgt0P

• in ssrnum.v, the following have been restated (which were formerly derived from order.v and stated with specializations of the meet and join operators):

  • minrC, minrr, minr_l, minr_r, maxrC, maxrr, maxr_l, maxr_r, minrA, minrCA, minrAC, maxrA, maxrCA, maxrAC
  • eqr_minl, eqr_minr, eqr_maxl, eqr_maxr, ler_minr, ler_minl, ler_maxr, ler_maxl, ltr_minr, ltr_minl, ltr_maxr, ltr_maxl
  • minrK, minKr, maxr_minl, maxr_minr, minr_maxl, minr_maxr

• The new definitions of min and max may require the following rewrite rules changes when dealing with max and min instead of meet and join:

  • ltexI -> (le_minr,lt_minr)
  • lteIx -> (le_minl,lt_minl)
  • ltexU -> (le_maxr,lt_maxr)
  • lteUx -> (le_maxl,lt_maxl)
  • lexU -> le_maxr
  • ltxU -> lt_maxr
  • lexU -> le_maxr

• in ssrbool.v

  • lemmas about monotone functions and the {in _, _} notation:
    • homoRL_in, homoLR_in, homo_mono_in, monoLR_in, monoRL_in, can_mono_in

Renamed

• in fintype we deprecate and rename the following:

  • arg_minP -> arg_minnP
  • arg_maxP -> arg_maxnP

• in order.v, in module NatOrder, renamings:

  • meetEnat -> minEnat, joinEnat -> maxEnat, meetEnat -> minEnat, joinEnat -> maxEnat

Removed

• in order.v, removed total_display (was used to provide the notation max for join and min for meet).
• in order.v, removed minnE and maxnE
• in order.v,
  • removed meetEnat (in favor of meetEtotal followed by minEnat)
  • removed joinEnat (in favor of joinEtotal followed by maxEnat)

[1.11+beta1] - 2020-04-15

This release is compatible with Coq versions 8.7, 8.8, 8.9 and 8.10.

The contributors to this version are: Antonio Nikishaev, Anton Trunov, Assia Mahboubi, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Florent Hivert, Kazuhiko Sakaguchi, Pierre-Marie Pédrot, Pierre-Yves Strub, Reynald Affeldt, Simon Boulier, Yves Bertot.

Added

• Arithmetic theorems in ssrnat, div and prime about logn, coprime, gcd, lcm and partn: logn_coprime, logn_gcd, logn_lcm, eq_partn_from_log and eqn_from_log.

• Lemmas ltnNleqif, eq_leqif, eqTleqif in ssrnat

• Lemmas eqEtupe, tnthS and tnth_nseq in tuple

• Ported order.v from the finmap library, which provides structures of ordered sets (porderType, latticeType, distrLatticeType, orderType, etc.) and its theory.

• Lemmas path_map, eq_path_in, sub_path_in, path_sortedE, sub_sorted and sub_sorted_in in path (and refactored related proofs)

• Added lemmas hasNfind, memNindex and findP in seq

• Added lemmas foldr_rcons, foldl_rcons, scanl_rcons and nth_cons_scanl in seq

• ssrAC tactics, see header of ssreflect/ssrAC.v for documentation of (AC patternshape reordering), (ACl reordering) (ACof reordering reordering), op.[AC patternshape reordering], op.[ACl reordering] and op.[ACof reordering reordering].

• Added definition cast_perm with a group morphism canonical structure, and lemmas permX_fix, imset_perm1, permS0, permS1, cast_perm_id, cast_ord_permE, cast_permE, cast_perm_comp, cast_permK, cast_permKV, cast_perm_inj, cast_perm_sym,cast_perm_morphM, and isom_cast_perm in perm and restr_perm_commute in action.

• Added card_porbit_neq0, porbitP, and porbitPmin in perm

• Added definition Sym with a group set canonical structure and lemmas card_Sn and card_Sym in perm and SymE in action

Changed

• Reorganized the algebraic hierarchy and the theory of ssrnum.v.

  • numDomainType and realDomainType get inheritances respectively from porderType and orderType.
  • normedZmodType is a new structure for numDomainType indexed normed additive abelian groups.
  • [arg minr_( i < n | P ) F] and [arg maxr_( i < n | P ) F] notations are removed. Now [arg min_( i < n | P ) F] and [arg max_( i < n | P ) F] notations are defined in nat_scope (specialized for nat), order_scope (general one), and ring_scope (specialized for ring_display). Lemma fintype.arg_minP is aliased to arg_minnP and the same for arg_maxnP.
  • The following lemmas are generalized, renamed, and relocated to order.v:

    • ltr_def -> lt_def

    • (ger|gtr)E -> (ge|gt)E

    • (le|lt|lte)rr -> (le|lt|lte)xx

    • ltrW -> ltW

    • ltr_neqAle -> lt_neqAle

    • ler_eqVlt -> le_eqVlt

    • (gtr|ltr)_eqF -> (gt|lt)_eqF

    • ler_anti, ler_asym -> le_anti

    • eqr_le -> eq_le

    • (ltr|ler_lt|ltr_le|ler)_trans -> (lt|le_lt|lt_le|le)_trans

    • lerifP -> leifP

    • (ltr|ltr_le|ler_lt)_asym -> (lt|lt_le|le_lt)_asym

    • lter_anti -> lte_anti

    • ltr_geF -> lt_geF

    • ler_gtF -> le_gtF

    • ltr_gtF -> lt_gtF

    • lt(r|nr|rn)W_(n)homo(_in) -> ltW_(n)homo(_in)

    • inj_(n)homo_lt(r|nr|rn)(_in) -> inj_(n)homo_lt(_in)

    • (inc|dec)(r|nr|rn)_inj(_in) -> (inc_dec)_inj(_in)

    • le(r|nr|rn)W_(n)mono(_in) -> leW_(n)mono(_in)

    • lenr_(n)mono(_in) -> le_(n)mono(_in)

    • lerif_(refl|trans|le|eq) -> leif_(refl|trans|le|eq)

    • (ger|ltr)_lerif -> (ge|lt)_leif

    • (n)mono(_in)_lerif -> (n)mono(_in)_leif

    • (ler|ltr)_total -> (le|lt)_total

    • wlog_(ler|ltr) -> wlog_(le|lt)

    • ltrNge -> ltNge

    • lerNgt -> leNgt

    • neqr_lt -> neq_lt

    • eqr_(le|lt)(LR|RL) -> eq_(le|lt)(LR|RL)

    • eqr_(min|max)(l|r) -> eq_(meet|join)(l|r)

    • ler_minr -> lexI

    • ler_minl -> leIx

    • ler_maxr -> lexU

    • ler_maxl -> leUx

    • lt(e)r_min(r|l) -> lt(e)(xI|Ix)

    • lt(e)r_max(r|l) -> lt(e)(xU|Ux)

    • minrK -> meetUKC

    • minKr -> joinKIC

    • maxr_min(l|r) -> joinI(l|r)

    • minr_max(l|r) -> meetU(l|r)

    • minrP, maxrP -> leP, ltP

      Replacing minrP and maxrP with leP and ltP may require to provide some arguments explicitly. The former ones respectively try to match with minr and maxr first but the latter ones try that in the order of <, <=, maxr, and minr.

    • (minr|maxr)(r|C|A|CA|AC) -> (meet|join)(xx|C|A|CA|AC)

    • minr_(l|r) -> meet_(l|r)

    • maxr_(l|r) -> join_(l|r)

    • arg_minrP -> arg_minP

    • arg_maxrP -> arg_maxP

  • Generalized the following lemmas as properties of normedDomainType: normr0, normr0P, normr_eq0, distrC, normr_id, normr_ge0, normr_le0, normr_lt0, normr_gt0, normrE, normr_real, ler_norm_sum, ler_norm_sub, ler_dist_add, ler_sub_norm_add, ler_sub_dist, ler_dist_dist, ler_dist_norm_add, ler_nnorml, ltr_nnorml, lter_nnormr.
  • The compatibility layer for the version 1.10 is provided as the ssrnum.mc_1_10 module. One may compile proofs compatible with the version 1.10 in newer versions by using the mc_1_10.Num module instead of the Num module. However, instances of the number structures may require changes.

• Extended comparison predicates leqP, ltnP, and ltngtP in ssrnat to allow case analysis on minn and maxn.

  • The compatibility layer for the version 1.10 is provided as the ssrnat.mc_1_10 module. One may compile proofs compatible with the version 1.10 in newer versions by using this module.

• The definition of all2 was slightly altered for a better interaction with the guard condition (#469)

Renamed

• real_lerP -> real_leP
• real_ltrP -> real_ltP
• real_ltrNge -> real_ltNge
• real_lerNgt -> real_leNgt
• real_ltrgtP -> real_ltgtP
• real_ger0P -> real_ge0P
• real_ltrgt0P -> real_ltgt0P
• lerif_nat -> leif_nat_r
• Replaced lerif with leif in the following names of lemmas:
  • lerif_subLR, lerif_subRL, lerif_add, lerif_sum, lerif_0_sum, real_lerif_norm, lerif_pmul, lerif_nmul, lerif_pprod, real_lerif_mean_square_scaled, real_lerif_AGM2_scaled, lerif_AGM_scaled, real_lerif_mean_square, real_lerif_AGM2, lerif_AGM, relif_mean_square_scaled, lerif_AGM2_scaled, lerif_mean_square, lerif_AGM2, lerif_normC_Re_Creal, lerif_Re_Creal, lerif_rootC_AGM.
• The following naming inconsistencies have been fixed in ssrnat.v:
  • homo_inj_lt(_in) -> inj_homo_ltn(_in)
  • (inc|dec)r_inj(_in) -> (inc|dec)n_inj(_in)
• switching long suffixes to short suffixes
  • odd_add -> oddD
  • odd_sub -> oddB
  • take_addn -> takeD
  • rot_addn -> rotD
  • nseq_addn -> nseqD
• Replaced cycle by orbit in perm/action:
  • pcycle -> porbit
  • pcycles -> porbits
  • pcycleE -> porbitE
  • pcycle_actperm -> porbit_actperm
  • mem_pcycle -> mem_porbit
  • pcycle_id -> porbit_id
  • uniq_traject_pcycle -> uniq_traject_porbit
  • pcycle_traject -> porbit_traject
  • iter_pcycle -> iter_porbit
  • eq_pcycle_mem -> eq_porbit_mem
  • pcycle_sym -> porbit_sym
  • pcycle_perm -> porbit_perm
  • ncycles_mul_tperm -> porbits_mul_tperm

Removed

The following were deprecated since release 1.9.0

• tuple_perm_eqP (use tuple_permP instead, from perm.v)
• eq_big_perm (use perm_big instead, from bigop.v)
• perm_eqP (use permP instead, from seq.v)
• perm_eqlP (use permPl instead)
• perm_eqrP (use permPr instead)
• perm_eqlE (use permEl instead)
• perm_eq_refl (use perm_refl instead)
• perm_eq_sym (use perm_sym instead)
• perm_eq_trans (use perm_trans instead)
• perm_eq_size (use perm_size instead)
• perm_eq_mem (use perm_mem instead)
• perm_eq_uniq (use perm_uniq instead)

[1.10.0] - 2019-11-29

This release is compatible with Coq versions 8.9 and 8.10.

The contributors to this version are: Antonio Nikishaev, Anton Trunov, Arthur Azevedo de Amorim, Christian Doczkal, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Florent Hivert, Gabriel Taumaturgo, Georges Gonthier, Kazuhiko Sakaguchi, Laurent Théry, Maxime Dénès, Reynald Affeldt, and Yves Bertot.

Added

• Added a void notation for the Empty_set type of the standard library, the canonical injection of_void and its cancellation lemma of_voidK, and eq, choice, count and fin instances.

• Added ltn_ind general induction principle for nat variables, helper lemmas ubnP, ltnSE, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for nat measures that does not rely on the {-2} numerical occurrence selector, and purged this idiom from the mathcomp library (see below).

• Added fixpoint and cofixpoint constructions to finset: fixset, cofixset and fix_order, with a few theorems about them

• Added functions tuple_of_finfun, finfun_of_tuple, and their "cancellation" lemmas.

• Added theorems totient_prime and Euclid_dvd_prod in prime.v

• Added theorems ffact_prod, prime_modn_expSn and fermat_little in binomial.v

• Added theorems flatten_map1, allpairs_consr, mask_filter, all_filter, all_pmap, and all_allpairsP in seq.v.

• Added theorems nth_rcons_default, undup_rcons, undup_cat and undup_flatten_nseq in seq.v

• Fintype theorems: fintype0, card_le1P, mem_card1, card1P, fintype_le1P, fintype1, fintype1P, existsPn, exists_inPn, forallPn, forall_inPn, eq_enum_rank_in, enum_rank_in_inj, lshift_inj, and rshift_inj.

• Bigop theorems: index_enum_uniq, big_rmcond, bigD1_seq, big_enum_val_cond, big_enum_rank_cond, big_enum_val, big_enum_rank, big_set, big_enumP, big_enum_cond, big_enum

• Arithmetic theorems in ssrnat and div:

  • some trivial results in ssrnat: ltn_predL, ltn_predRL, ltn_subrR, leq_subrR, ltn_subrL and predn_sub,
  • theorems about n <=/< p +/- m and m +/- n <=/< p: leq_psubRL, ltn_psubLR, leq_subRL, ltn_subLR, leq_subCl, leq_psubCr, leq_subCr, ltn_subCr, ltn_psubCl and ltn_subCl,
  • some commutations between modulo and division: modn_divl and divn_modl,
  • theorems about the euclidean division of additions and subtraction,
    • without preconditions of divisibility: edivnD, edivnB, divnD, divnB, modnD, modnB,
    • with divisibility of one argument: divnDMl, divnMBl, divnBMl, divnBl and divnBr,
    • specialization of the former theorems for .+1 and .-1: edivnS, divnS, modnS, edivn_pred, divn_pred and modn_pred.

• Added sort_rec1 and sortE to help inductive reasoning on sort.

• Added map/parametricity theorems about path, sort, and sorted: homo_path, mono_path, homo_path_in, mono_path_in, homo_sorted, mono_sorted, map_merge, merge_map, map_sort, sort_map, sorted_map, homo_sorted_in, mono_sorted_in.

• Extracting lemma fpathE from fpathP, and shortening the proof of the latter.

• Added the theorem perm_iota_sort to express that the sorting of any sequence s is equal to a mapping of iota 0 (size s) to the nth elements of s, so that one can still reason on nat, even though the elements of s are not in an eqType.

• Added stability theorems about merge and sort: sorted_merge, merge_stable_path, merge_stable_sorted, sorted_sort, sort_stable, filter_sort, mask_sort, sorted_mask_sort, subseq_sort, sorted_subseq_sort, and mem2_sort.

• New algebraic interfaces in ssralg.v: comAlgebra and comUnitAlgebra for commutative and commutative-unitary algebras.

• Initial property for polynomials in algebras: New canonical lrMoprphism horner_alg evaluating a polynomial in an element of an algebra. The theory include the lemmas in_alg_comm, horner_algC, horner_algX, poly_alg_initial.

• Added lemmas on commutation with difference, big sum and prod: commrB, commr_sum, commr_prod.

• Added a few basic seq lemmas about nseq, take and drop: nseq_addn, take_take, take_drop, take_addn, takeC, take_nseq, drop_nseq, rev_nseq, take_iota, drop_iota.

• Added ssrfun theorem inj_compr.

• Added theorems mem2E, nextE, mem_fcycle, inj_cycle, take_traject, trajectD and cycle_catC in path.v

• Added lemmas about cycle, connect, fconnect, order and orbit in fingraph.v:

  • lemma connect_cycle,
  • lemmas in_orbit, order_gt0, findex_eq0, mem_orbit, image_orbit,
  • lemmas fcycle_rconsE, fcycle_consE, fcycle_consEflatten and undup_cycle_cons which operate under the precondition that the sequence x :: p is a cycle for f (i.e. fcycle f (x :: p)).
  • lemmas which operate under the precondition there is a sequence p which is a cycle for f (i.e. fcycle f p): order_le_cycle, finv_cycle, f_finv_cycle, finv_f_cycle, finv_inj_cycle, iter_finv_cycle, cycle_orbit_cycle, fpath_finv_cycle, fpath_finv_f_cycle, fpath_f_finv_cycle, prevE, fcycleEflatten, fcycle_undup, in_orbit_cycle, eq_order_cycle, iter_order_cycle,
  • lemmas injectivePcycle, orbitPcycle, fconnect_eqVf, order_id_cycle, orderPcycle, fconnect_f, fconnect_findex.

• Added lemma rot_index which explicits the index given by rot_to.

• Added tactic tfae to split an equivalence between n+1 propositions into n+1 goals, and referenced orbitPcycle as a reference of use.

Changed

• Replaced the legacy generalised induction idiom with a more robust one that does not rely on the {-2} numerical occurrence selector, using new ssrnat helper lemmas ltn_ind, ubnP, ubnPleq, ...., (see above). The new idiom is documented in ssrnat. This change anticipates an expected evolution of fintype to integrate finmap. It is likely that the new definition of the #|A| notation will hide multiple occurrences of A, which will break the {-2} induction idiom. Client libraries should update before the 1.11 release (see PR #434 for examples).

• Replaced the use of the accidental convertibility between enum A and filter A (index_enum T) with more explicit lemmas big_enumP, big_enum, big_enum_cond, big_image added to the bigop library, and deprecated the filter_index_enum lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future mathcomp releases when sets over finTypes are generalised to finite sets over choiceTypes, so client libraries should stop relying on this identity. File bigop.v has some boilerplate to help with the port; also see PR #441 for examples.

• Restricted big_image, big_image_cond, big_image_id and big_image_cond_id to bigops over abelian monoids, anticipating the change in the definition of enum. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of big_map and big_enumP.

• eqVneq lemma is changed from {x = y} + {x != y} to eq_xor_neq x y (y == x) (x == y), on which a case analysis performs simultaneous replacement of expressions of the form x == y and y == x by true or false, while keeping the ability to use it in the way it was used before.

• Generalized the allpairs_catr lemma to the case where the types of s, t1, and t2 are non-eqTypes in [seq E | i <- s, j <- t1 ++ t2].

• Generalized muln_modr and muln_modl removing hypothesis 0 < p.

• Generalized sort to non-eqTypes (as well as merge, merge_sort_push, merge_sort_pop), together with all the lemmas that did not really rely on an eqType: size_merge, size_sort, merge_path, merge_sorted, sort_sorted, path_min_sorted (which statement was modified to remove the dependency in eqType), and order_path_min.

• compare_nat type family and ltngtP comparison predicate are changed from compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n) to compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n), to make it tries to match subterms with m < n first, m <= n, then m == n.

  • The compatibility layer for the version 1.9 is provided as the ssrnat.mc_1_9 module. One may compile proofs compatible with the version 1.9 in newer versions by using this module.

• Moved iter_in to ssrnat and reordered its arguments.

• Notation [<-> P0 ; .. ; Pn] now forces Pi to be of type Prop.

Removed

• fin_inj_bij lemma is removed as a duplicate of injF_bij lemma from fintype library.

Infrastructure

• Makefile now supports the test-suite and only targets. Currently, make test-suite will verify the implementation of mathematical structures and their inheritances of MathComp automatically, by using the hierarchy.ml utility. One can use the only target to build the sub-libraries of MathComp specified by the TGTS variable, e.g., make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo".

• Makefilenow supports a doc target to build the documentation as made available on https://mathcomp.github.io/htmldoc/index.html

[1.9.0] - 2019-05-22

MathComp 1.9.0 is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1. Minor releases will remain compatible with Coq 8.9 and 8.10; compatibility with earlier versions may be dropped.

The contributors to this version are: Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Georges Gonthier, Kazuhiko Sakaguchi, Sora Chen, Søren Eller Thomsen.

Added

• nonPropType, an interface for non-Prop types, and {pred T} and relpre f r, all of which will be in the Coq 8.10 core SSreflect library.

• deprecate old_id new_id, notation for new_id that prints a deprecation warning for old_id; Import Deprecation.Silent turns off those warnings, Import Deprecation.Reject raises errors instead of only warning.

• filter_nseq, count_nseq, mem_nseq, rcons_inj, rcons_injl, rcons_injr, nthK, sumn_rot.

• some perm_eq lemmas: perm_cat[lr], perm_nilP, perm_consP, perm_has, perm_flatten, perm_sumn.

• computing (efficiently) (item, multiplicity) tallies of sequences over an eqType: tally s, incr_tally bs x, bs \is a wf_tally, tally_seq bs.

Changed

• definition of PredType which now takes only a P -> pred T function; definition of simpl_rel to improve simplification by inE. Both these changes will be in the Coq 8.10 SSReflect core library.

• definition of permutations s now uses an optimal algorithm (in space and time) to generate all permutations of s back-to-front, using tally s.

Renamed

• perm_eqP -> permP (seq.permP if perm.v is also imported)
• perm_eqlP -> permPl
• perm_eqrP -> permPr
• perm_eqlE -> permEl
• perm_eq_refl -> perm_refl
• perm_eq_sym -> perm_sym
• perm_eq_trans -> perm_trans
• perm_eq_size -> perm_size
• perm_eq_mem -> perm_mem
• perm_eq_uniq -> perm_uniq
• perm_eq_rev -> perm_rev
• perm_eq_flatten -> perm_flatten
• perm_eq_all -> perm_all
• perm_eq_small -> perm_small_eq
• perm_eq_nilP -> perm_nilP
• perm_eq_consP -> perm_consP
• leq_size_perm -> uniq_min_size (permuting conclusions)
• perm_uniq -> eq_uniq (permuting assumptions) --> beware perm_uniq now means perm_eq_uniq
• uniq_perm_eq -> uniq_perm
• perm_eq_iotaP -> perm_iotaP
• perm_undup_count -> perm_count_undup
• tuple_perm_eqP -> tuple_permP
• eq_big_perm -> perm_big
• perm_eq_abelian_type -> abelian_type_pgroup

Misc

• removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to improve robustness of by ...; scripts may need to invoke addn0, addnS, muln0 or mulnS explicitly where these hints were used accidentally.

[1.8.0] - 2019-04-08

Drop compatibility with Coq 8.6 (OCaml plugin removed). MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.

The contributors to this version are: Anton Trunov, Assia Mahboubi, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Florent Hivert, Georges Gonthier, Kazuhiko Sakaguchi, Laurence Rideau, Laurent Théry, Pierre-Yves Strub, Søren Eller Thomsen, Yves Bertot.

Added

• Companion matrix of a polynomial companionmx p and the theorems: companionmxK, map_mx_companion and companion_map_poly

• homoW_in, inj_homo_in, mono_inj_in, anti_mono_in, total_homo_mono_in, homoW, inj_homo, monoj, anti_mono, total_homo_mono

• sorted_lt_nth, ltn_index, sorted_le_nth, leq_index.

• [arg minr_( i < n | P ) F] and [arg maxr_( i < n | P ) F] with all their variants, following the same convention as for nat

• contra_neqN, contra_neqF, contra_neqT, contra_neq_eq, contra_eq_neq

• take_subseq, drop_subseq

• big_imset_cond,big_map_id, big_image_cond big_image, big_image_cond_id and big_image_id

• foldrE, foldlE, foldl_idx and sumnE to turn "seq statements" into "bigop statements"

• all_iff with notation [<-> P0; P1; ..; Pn] to talk about circular implication P0 -> P1 -> ... -> Pn -> P0. Related theorems are all_iffLR and all_iffP

• support for casts in map comprehension notations, e.g., [seq E : T | s <- s].

• a predicate all2, a parallel double seq version of all.

• some perm_eq lemmas: perm_cat[lr], perm_eq_nilP, perm_eq_consP, perm_eq_flatten.

• a function permutations that computes a duplicate-free list of all permutations of a given sequence s over an eqType, along with its theory: mem_permutations, size_permutations, permutations_uniq, permutations_all_uniq, perm_permutations.

• eq_mktuple, eq_ffun, eq_finset, eq_poly, ex_mx that can be used with the under tactic from the Coq 8.10 SSReflect plugin (cf. coq/coq#9651)

Changed

• Theory of lersif and intervals:

  • Many lersif related lemmas are ported from ssrnum
  • Changed: prev_of_itv, itv_decompose, and itv_rewrite
  • New theory of intersections of intervals

• Generalized extremum_spec and its theory, added extremum and extremumP, generalizing arg_min for an arbitrary eqType with an order relation on it (rather than nat). Redefined arg_min and arg_max with it.

• Reshuffled theorems inside files and packages:

  • countalg goes from the field to the algebra package
  • finalg inherits from countalg
  • closed_field contains the construction of algebraic closure for countable fields that used to be in the file countalg.

• Maximal implicits applied to reflection, injectivity and cancellation lemmas so that they are easier to pass to combinator lemmas such as sameP, inj_eq or canLR.

• Added reindex_inj s shorthand for reindexing a bigop with a permutation s.

• Added lemma eqmxMunitP: two matrices with the same shape represent the same subspace iff they differ only by a change of basis.

• Corrected implicits and documentation of MatrixGenField.

• Rewritten proof of quantifier elimination for closed field in a monadic style.

• Specialized bool_irrelevance so that the statement reflects the name.

• Changed the shape of the type of FieldMixin to allow one-line in-proof definition of bespoke fieldType structure.

• Refactored and extended Arguments directives to provide more comprehensive signature information.

• Generalized the notation [seq E | i <- s, j <- t] to the case where t may depend on i. The notation is now primitive and expressed using flatten and map (see documentation of seq). allpairs now expands to this notation when fully applied.

  • Added allpairs_dep and made it self-expanding as well.
  • Generalized some lemmas in a backward compatible way.
  • Some strictly more general lemmas now have suffix _dep.
  • Replaced allpairs_comp with its converse map_allpairs.
  • Added allpairs extensionality lemmas for the following cases: non-localised (eq_allpairs), dependent localised (eq_in_allpairs_dep) and non-dependent localised (eq_in_allpairs); as per eq_in_map, the latter two are equivalences.

• Generalized {ffun A -> R} to handle dependent functions, and to be structurally positive so it can be used in recursive inductive type definitions.

  Minor backward incompatibilities: fgraph f is no longer a field accessor, and no longer equal to val f as {ffun A -> R} is no longer a subType; some instances of finfun, ffunE, ffunK may not unify with a generic non-dependent function type A -> ?R due to a bug in Coq version 8.9 or below.

• Renamed double seq induction lemma from seq2_ind to seq_ind2, and weakened its induction hypothesis.

• Replaced the nosimpl in rev with a Arguments simpl never directive.

• Many corrections in implicits declarations.

• fixed missing joins in ssralg, ssrnum, finalg and countalg

Renamed

Renamings also involve the _in suffix counterpart when applicable

• mono_inj -> incr_inj
• nmono_inj -> decr_inj
• leq_mono_inj -> incnr_inj
• leq_nmono_inj -> decnr_inj
• homo_inj_ltn_lt -> incnr_inj
• nhomo_inj_ltn_lt -> decnr_inj
• homo_inj_in_lt -> inj_homo_ltr_in
• nhomo_inj_in_lt -> inj_nhomo_ltr_in
• ltn_ltrW_homo -> ltnrW_homo
• ltn_ltrW_nhomo -> ltnrW_nhomo
• leq_lerW_mono -> lenrW_mono
• leq_lerW_nmono -> lenrW_nmono
• homo_leq_mono -> lenr_mono
• nhomo_leq_mono -> lenr_nmono
• homo_inj_lt -> inj_homo_ltr
• nhomo_inj_lt -> inj_nhomo_ltr
• homo_inj_ltn_lt -> inj_homo_ltnr
• nhomo_inj_ltn_lt -> inj_nhomo_ltnr
• homo_mono -> ler_mono
• nhomo_mono -> ler_nmono
• big_setIDdep -> big_setIDcond
• sum_nat_dep_const -> sum_nat_cond_const

Misc

• Removed trailing _ : Type field from packed classes. This performance optimization is not strictly necessary with modern Coq versions.

• Removed duplicated definitions of tag, tagged and Tagged from eqtype.v. They are already in ssrfun.v.

• Miscellaneous improvements to proof scripts and file organisation.

[1.7.0] - 2018-04-24

Compatibility with Coq 8.8 and lost compatibility with Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.

• Integration in Coq startng from version 8.7 of:

  • OCaml plugin (plugin for 8.6 still in the archive for backward compatibility)
  • ssreflect.v, ssrbool.v, ssrfun.v and ssrtest/

• Cleaning up the github repository: the math-comp repository is now dedicated to the released material (as in the present release). For instance, directories real-closed/ and odd-order/ now have their own repository.

Changed

• Library refactoring: algC and ssrnum. Library ssrnum.v provides an interface numClosedFieldType, which abstracts the theory of algebraic numbers. In particular, Re, Im, 'i, conjC, n.-root and sqrtC, previously defined in library algC.v, are now part of this generic interface. In case of ambiguity, a cast to type algC, of complex algebraic numbers, can be used to disambiguate via typing constraints. Some theory was thus made more generic, and the corresponding lemmas, previously defined in library algC.v (e.g. conjCK) now feature an extra, non maximal implicit, parameter of type numClosedFieldType. This could break some proofs. Every theorem from ssrnum that used to be in algC changed statement.

• ltngtP, contra_eq, contra_neq, odd_opp, nth_iota

Added

• iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in, iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in, fpath_finv_f_in, fpath_f_finv_in
• big_allpairs
• uniqP, uniqPn
• dec_factor_theorem, mul_bin_down, mul_bin_left
• abstract_context (in ssreflect.v, now merged in Coq proper)

Renamed

• Lemma dvdn_fact was moved from library prime.v to library div.v
• `mul_Sm_binm -> mul_bin_diag
• divn1 -> divz1 (in intdiv)
• rootC -> nthroot
• algRe -> Re
• algIm -> Im
• algCi -> imaginaryC
• reshape_index_leq -> reshape_leq

[1.6.0] - 2015-11-24 (ssreflect + mathcomp)

Major reorganization of the archive.

• Files split into sub-directories: ssreflect/, algebra/, fingroup/, solvable/, field/ and character/. In this way the user can decide to compile only the subset of the Mathematical Components library that is relevant to her. Note that this introduces a possible incompatibility for users of the previous version. A replacement scheme is suggested in the installation notes.

• The archive is now open and based on git. Public mirror at: https://github.com/math-comp/math-comp

• Sources of the reference manual of the Ssreflect tactic language are also open and available at: https://github.com/math-comp/ssr-manual Pull requests improving the documentation are welcome.

Renamed

• conjC_closed -> cfConjC_closed
• class_transr -> class_eqP
• cfclass_transl -> cfclass_transr
• nontrivial_ideal -> proper_ideal
• zchar_orthonormalP -> vchar_orthonormalP

Changed

• seq_sub
• orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl, lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, ltr0_neq0, ltr_prod, Zisometry_of_iso

Added

• adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type
• orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char, extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK, lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms, gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1, dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq, divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn, unlessL, unlessR, unless_sym, unlessP (coercion), classicW, ltr_prod_nat
• Notation \unless C, P

[1.5.0] - 2014-03-12 (ssreflect + mathcomp)

Split the archive in SSReflect and MathComp

• With this release "ssreflect" has been split into two packages. The Ssreflect one contains the proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. The Mathematical Components one contains advanced theory files covering a wider spectrum of mathematics.

• With respect to version 1.4 the proof language got a few new features related to forward reasoning and some bug fixes. The Mathematical Components library features 16 new theory files and in particular: some field and Galois theory, advanced character theory and a construction of algebraic numbers.

[1.4.0] - 2012-09-05 (ssreflect)

• With this release the plugin code received many bug fixes and the existing libraries relevant updates. This release also includes some new libraries on the following topics: rational numbers, divisibility of integers, F-algebras, finite dimensional field extensions and Euclidean division for polynomials over a ring.

• The release includes a major code refactoring of the plugin for Coq 8.4. In particular a documented ML API to access the pattern matching facilities of Ssreflect from third party plugins has been introduced.

[1.3.0] - 2011-03-14 (ssreflect)

• The tactic language has been extended with several new features, inspired by the five years of intensive use in our project. However we have kept the core of the language unchanged; the new library compiles with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" line in ssreflect.v to properly compile the 1.3 library. We will continue supporting new releases of Coq in due course.

• The new library adds general linear algebra (matrix rank, subspaces) and all of the advanced finite group that was developed in the course of completing the Local Analysis part of the Odd Order Theorem, starting from the Sylow and Hall theorems and including full structure theorems for abelian, extremal and extraspecial groups, and general (modular) linear representation theory.

[1.2.0] - 2009-08-14 (ssreflect)

No change log

[1.1.0] - 2008-03-18 (ssreflect)

First public release