\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Recent changes

Unreleased changes

Changed

• in HLevels.v

  • Split into HLevels into HLevelsBase, which does not depend on axioms, and HLevels, which exports the former and provides the previous functionality (#133, by Andres Erbsen).

• in ZArith,v and dependencies

  • Reducing reliance on Znumtheory within stdlib changed the internal dependencies between files, code relying on files being transitively required in stdlib may need to now explicitly Require Znumtheory, BinInt, BinList, BinNat, BinNums, BinPos, Setoid, Tauto, Zhints, Zpow_def, Zpow_facts, or Zbool (#136, by Andres Erbsen).

• in Permutation

  • Moved Fin-specific definitons into FinFun (#154, by Andres Erbsen).

• in FinFun

  • Split out non-Fin-specific definitons into Lists.Finite (#154, by Andres Erbsen).

• in NsatzTactic.v

  • Split NsatzTactic into a smaller NsatzTactic that only depends on setoid_ring, and per-domain files ZNsatz, QNsatz, and RNsatz (#155, by Andres Erbsen).

Added

• in HLevelsBase.v

  • transparent lemmas false_hprop, true_hprop, Is_true_hprop, eq_true_hprop, and a wrappers transparent_Is_true and transparent_eq_true to produce transparent proofs for Is_true and eq_true given not necessarily transparent proofs of the same (#133, by Andres Erbsen).

• in BinNatDef.v and BinNat.v

  • Added definition Niter_op for repeating associative operations, a proof relating it to the generic N.iter (iter_op_correct), and properties iter_op_0_r, iter_op_1_r, iter_op_succ_r, and iter_op_add_r (#134, by Andres Erbsen).

• in Zcong.v

  • theory of integer congruences and multiplicative inverses up to Chinese Remainder Theorem (#135, by Andres Erbsen).

• in ZModOffset.v

  • Added theory of Z.modulo with output range shifted by a constant. The main definition is Z.omodulo, with Z.smodulo capturing the special case where the offset is equal to half of the modulus, such as in two's-complement arithmetic (#135, by Andres Erbsen).

• Zdivisibility.v

  • Refactored theory of integer divisibility including primality and coprimality. This file is intended to replace Znumtheory (#136, by Andres Erbsen).

• in Zmod.v

  • Added theory of modular integer arithmetic, including machine words / bitvectors and the multiplicative group of integers modulo another integer. About 450 lemmas are provided (#144, by Andres Erbsen).

• in ZmodNsatz and Zmod

  • Added support for the nsatz tactic on Zmod (#156, by Andres Erbsen).

• in Ncring_tac

  • Added extension-point typeclass extra_reify that is only resolved on non-variables for which built-in syntax-directed reification did not find a match (#156, by Andres Erbsen).

• in NsatzTactic

  • Added support for nsatz using ring hypotheses above non-ring hypotheses. If a proof relies on nsatz not using earlier ring hypotheses, clear these hypotheses before calling nsatz. (#157, by Andres Erbsen).

Renamed

Removed

• in Zdiv.v

  • alias Zmod for Z.modulo, deprecated since 8.17 (#149, by Andres Erbsen).

Deprecated

• in Znumtheory.v

  • Deprecated most definitions in favor of Zdivisibility.v or appropriate established files (#136, by Andres Erbsen).

• in Rtauto and rtauto.Bintree

  • If you use this plugin and would like to continue using it, please open an issue to discuss its maintainership (#161, by Andres Erbsen).

Version 9.0

Changes in 9.0.0

Changed

• Changed the requirement prefix of the standard library from Coq to Stdlib and made it mandatory. As a temporary measure, for backward compatibility with older versions, Coq, or a missing From Stdlib, is immediatly translated to Stdlib with a warning. It is thus not recommended to name anything Coq or Coq.*. The recommended transition path is to first potentially silence the warnings, adding the lines -arg -w -arg -deprecated-from-Coq, -arg -w -arg -deprecated-dirpath-Coq and -arg -w -arg -deprecated-missing-stdlib or simply the more generic -arg -compat -arg 8.20 to your _CoqProject. Then, when droping support for Coq <= 8.20, replacing requirement of Stdlib modules by From Stdlib Require {Import,Export,} <LibraryModules>.. Beware that the Stdlib still has a handful redundant names, that is for modules Byte, you still have to use From Stdlib.Strings or From Stdlib.Init, for Tactics use From Stdlib.Program or From Stdlib.Init, for Tauto use From Stdlib.micromega or From Stdlib.Init and for Wf, use From Stdlib.Program or From Stdlib.Init (#19310 and #19530, the latter starting to implement CEP#83 by Pierre Roux).

• in Fin.v

  • case_L_R' and case_L_R made transparent definitions (#19655, by Andrej Dudenhefner).

• in List.v

  • lemmas that were using the letter O in their name to refer to zero now use instead the digit 0 (#19479, by Hugo Herbelin).

• in several files

  • remove transitive requirements or export of theories about Z, you may need to add explicit Require or Import of ZArith or Lia (#19801, by Andres Erbsen).

• in Zbool.v

  • definition of Zeq_bool is now an alias for Z.eqb, this is expected to simplify simultaneous compatibility with 8.20 and 9.0 (#19801, by Andres Erbsen).

Added

• file All.v which does Require Export of all other files in Stdlib (#19914, by Gaëtan Gilbert).

• in BinPos.v

  • lemma BinPos.iter_op_correct, relating Pos.iter_op for associative operations to the more general Pos.iter (#19749, by Andres Erbsen).

• in Eqdep_dec.v in Logic

  • lemmas UIP_None_l, UIP_None_r, UIP_None_None, UIP_nil_l, UIP_nil_r, UIP_nil_nil (#19483, by Andres Erbsen).

• in EquivDec.v in Classes

  • EqDec instance for option (#19949, by Daniil Iaitskov).

• in Fin.v

  • lemmas case_L_R'_L, case_L_R'_R, case_L_R_L, case_L_R_R (#19655, by Andrej Dudenhefner).

• in Inverse_Image.v in Wellfounded

  • lemmas Acc_simulation and wf_simulation (#18183, by Andrej Dudenhefner).

• in List.v

  • lemmas length_cons and length_nil (#19479, by Hugo Herbelin).

  • Proper instance to enable setoid_rewrite to rewrite inside the function argument of List.map (#19515, by Andres Erbsen).

  • lemmas length_tl, tl_map, filter_rev, filter_map_swap, filter_true, filter_false, list_prod_as_flat_map, skipn_seq, map_const, fst_list_prod, snd_list_prod, Injective_map_NoDup_in, and Permutation_map_same_l (#19748, by Andres Erbsen).

  • lemma length_app_comm (#75, by Nicholas Hubbard).

• file List_Extension.v in Wellfounded (#18183, by Andrej Dudenhefner).

• in List_Extension.v

  • well-founded list extension list_ext of a well-founded relation, including infrastructure lemmas. It can be used for well-foundedness proofs such as wf_lex_exp in Lexicographic_Exponentiation.v (#18183, by Andrej Dudenhefner).

• in NatInt.v

  • lemmas mul_reg_l and mul_reg_r (#17560, by Remzi Yang).

• in Operators_Properties.v in Relations

  • lemma clos_t_clos_rt (#18183, by Andrej Dudenhefner).

• in Reals

  • new file Zfloor.v with definitions of Zfloor and Zceil and corresponding lemmas up_Zfloor, IZR_up_Zfloor, Zfloor_bound, Zfloor_lub, Zfloor_eq, Zfloor_le, Zfloor_addz, ZfloorZ, ZfloorNZ, ZfloorD_cond, Zceil_eq, Zceil_le, Zceil_addz, ZceilD_cond, ZfloorB_cond, ZceilB_cond (#89, by Laurent Théry).

• in VectorSpec.v

  • lemma Forall2_cons_iff (#19269, by Lucas Donati and Andrej Dudenhefner and Pierre Rousselin).

• in Zdiv.v

  • lemma Z.mod_id_iff generalizes Z.mod_small. (#19752, by Andres Erbsen).

  • lemmas Z.mod_opp_mod_opp, Z.mod_mod_opp_r, Z.mod_opp_r_mod, Z.mod_mod_abs_r, Z.mod_abs_r_mod combining Z.modulo with Z.opp or Z.abs (#19752, by Andres Erbsen).

  • Lemmas cong_iff_0 and cong_iff_ex can be used to reduce congruence equalities to equations where only one side is headed by Z.modulo. (#19752, by Andres Erbsen).

  • Lemmas Z.gcd_mod_l and Z.gcd_mod_r generalize Z.gcd_mod. (#19752, by Andres Erbsen).

  • Lemma Z.mod_mod_divide generalizes Zmod_mod. (#19752, by Andres Erbsen).

  • Lemma Z.mod_pow_l allows pushing modulo inside exponentiation (#19752, by Andres Erbsen).

• file Zdiv_facts.v (#19752, by Andres Erbsen).

• in Zdiv_facts.v

  • lemmas Z.diveq_iff and Z.mod_diveq_iff that further genralize the same concept as Z.mod_small to known quotients other than 0. (#19752, by Andres Erbsen).

  • lemmas Z.eq_mod_opp and Z.eq_mod_abs (#19752, by Andres Erbsen).

• in Znat.v

  • lemmas N2Z.inj_lxor, N2Z.inj_land, N2Z.inj_lor, N2Z.inj_ldiff, N2Z.inj_shiftl, and N2Z.inj_shiftr relating bitwise operations on N to those on Z (#19750, by Andres Erbsen).

Deprecated

• modules ZArith_Base and Ztac, use ZArith (or BinInt) or Lia instead (#19801, by Andres Erbsen).

• in Zbool.v

  • definition Zeq_bool, use Z.eqb instead. (#19801, by Andres Erbsen).

Previous versions

The standard library historically used to be distributed with Coq, please look in Coq own changelog for details about older changes.