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

Added

• in NatInt.v

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

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

• in Inverse_Image.v in Wellfounded

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

• in Operators_Properties.v in Relations

  • lemma clos_t_clos_rt (#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 VectorSpec.v

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

• in List.v

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

• 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 List.v

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

• 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 List.v

  • 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).

• 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 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).

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

• in file 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 file 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).

• Deprecated: module ZArith_Base, module Ztac, and Zeq_bool. Use ZArith (or BinInt), Lia, and Z.eqb instead. Reducing use of the deprecated modules in stdlib changed the transitive dependencies of several stdlib files; you may now need to Require or Import ZArith or Lia. The definition of Zeq_bool was also changed to be an alias for Z.eqb; this is expected to simplify simultaneous compatibility with 8.20 and 9.0 (#19801, by Andres Erbsen).

• Added: Stdlib.All which does Require Export of all other files in the stdlib (#19914, by Gaëtan Gilbert).

• in EquivDec.v in Classes (#19949, by Daniil Iaitskov).

  • EqDec instance for option

• in List.v

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

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 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 Fin.v

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

• 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).

Renamed

Deprecated

Changed

• 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.