\[\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

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.