CHANGELOG.md

This file lists "large-ish" changes to the std++ Coq library, but not every API-breaking change is listed.

std++ master

Coq 8.11 is no longer supported.

• Make sure that gset and mapset do not bump the universe.
• Rewrite tele_arg to make it not bump universes. (by Gregory Malecha, BedRock Systems)
• Change dom D M (where D is the domain type) to dom M; the domain type is now inferred automatically. To make this possible, getting the domain of a gmap as a coGset and of a Pmap as a coPset is no longer supported. Use gset_to_coGset/Pset_to_coPset instead. When combining dom with ≡, this can run into an old issue (due to a Coq issue, Equiv does not the desired Hint Mode !), which can make it necessary to annotate the set type at the ≡ via ≡@{D}.
• Rename "unsealing" lemmas from _eq to _unseal. This affects ndot_eq and nclose_eq. These unsealing lemmas are internal, so in principle you should not rely on them.
• Declare Hint Mode for FinSet A C so that C is input, and A is output (i.e., inferred from C).
• Add function map_preimage to compute the preimage of a finite map.
• Rename map_disjoint_subseteq → kmap_subseteq and map_disjoint_subset → kmap_subset.
• Add map_Exists as an analogue to map_Forall. (by Michael Sammler)
• Add case_match eqn:H that behaves like case_match but allows naming the generated equality. (by Michael Sammler)
• Flip direction of map_disjoint_fmap.
• Add map_agree as a weaker version of ##ₘ which requires the maps to agree on keys contained in both maps. (by Michael Sammler)
• Rename lookup_union_l → lookup_union_l' and add lookup_union_l as the dual to lookup_union_r.
• Add map_seqZ as the Z analogue of map_seq. (by Michael Sammler)
• Add the coq-stdpp-unstable package for libraries that are not deemed stable enough to be included in the main std++ library, following the coq-iris-unstable package. This library is contained in the stdpp_unstable folder. The theories folder was renamed to stdpp.
• Add an unstable bitblast tactic for solving equalities between integers involving bitwise operations. (by Michael Sammler)

The following sed script should perform most of the renaming (on macOS, replace sed by gsed, installed via e.g. brew install gnu-sed). Note that the script is not idempotent, do not run it twice.

sed -i -E -f- $(find theories -name "*.v") <<EOF
s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
s/\bmap_disjoint_subset\b/kmap_subset/g
s/\blookup_union_l\b/lookup_union_l'/g
EOF

• Add the bind operation set_bind for finite sets. (by Dan Frumin and Paolo G. Giarrusso)

std++ 1.7.0 (2022-01-22)

Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain supported. Coq 8.10 is no longer supported.

This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a lot to everyone involved!

• Add is_closed_term tactic for determining whether a term depends on variables bound in the context. (by Michael Sammler)
• Add list.zip_with_take_both and list.zip_with_take_both'
• Specialize list.zip_with_take_{l,r}, add generalized lemmas list.zip_with_take_{l,r}'
• Add bool_to_Z that converts true to 1 and false to 0. (by Michael Sammler)
• Add lemmas for lookup on mjoin for lists. (by Michael Sammler)
• Rename Is_true_false → Is_true_false_2 and eq_None_ne_Some → eq_None_ne_Some_1.
• Rename decide_iff → decide_ext and bool_decide_iff → bool_decide_ext.
• Remove a spurious Global Arguments Pos.of_nat : simpl never.
• Add tactics destruct select <pat> and destruct select <pat> as <intro_pat>.
• Add some more lemmas about Finite and pred_finite.
• Add lemmas about last: last_app_cons, last_app, last_Some, and last_Some_elem_of.
• Add versions of Pigeonhole principle for Finite types, natural numbers, and lists.

The following sed script should perform most of the renaming (on macOS, replace sed by gsed, installed via e.g. brew install gnu-sed). Note that the script is not idempotent, do not run it twice.

sed -i -E -f- $(find theories -name "*.v") <<EOF
s/\bIs_true_false\b/Is_true_false_2/g
s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
# bool decide
s/\b(bool_|)decide_iff\b/\1decide_ext/g
EOF

std++ 1.6.0 (2021-11-05)

Coq 8.14 is newly supported by this release, and Coq 8.10 to 8.13 remain supported.

This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Alix Trieu, Andrej Dudenhefner, Dan Frumin, Fengmin Zhu, Hoang-Hai Dang, Jan Menz, Lennard Gäher, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Gregersen, and Tej Chajed. Thanks a lot to everyone involved!

• Remove singleton notations {[ x,y ]} and {[ x,y,z ]} for {[ (x,y) ]} and {[ (x,y,z) ]}. They date back to the time we used the singleton class with a product for maps (there's now the singletonM class).
• Add map notations {[ k1 := x1 ; .. ; kn := xn ]} up to arity 13. (by Lennard Gäher)
• Add multiset literal notation {[+ x1; .. ; xn +]}.
  • Add a new type class SingletonMS (with projection {[+ x +]} for multiset singletons.
  • Define {[+ x1; .. ; xn +]} as notation for {[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}.
• Remove the Singleton and Semiset instances for multisets to avoid accidental use.
  • This means the notation {[ x1; .. ; xn ]} no longer works for multisets (previously, its definition was wrong, since it used ∪ instead of ⊎).
  • Add lemmas for ∈ and ∉ specific for multisets, since the set lemmas no longer work for multisets.
• Make Qc_of_Z' not an implicit coercion (from Z to Qc) any more.
• Make Z.of_nat' not an implicit coercion (from nat to Z) any more.
• Rename decide_left → decide_True_pi and decide_right → decide_False_pi.
• Add option_guard_True_pi.
• Add lemma surjective_finite. (by Alix Trieu)
• Add type classes TCFalse, TCUnless, TCExists, and TCFastDone. (by Michael Sammler)
• Add various results about bit representations of Z. (by Michael Sammler)
• Add tactic learn_hyp. (by Michael Sammler)
• Add Countable instance for decidable Sigma types. (by Simon Gregersen)
• Add tactics compute_done and compute_by for solving goals by computation.
• Add Inj instances for fmap on option and maps.
• Various changes to Permutation lemmas:
  • Rename Permutation_nil → Permutation_nil_r, Permutation_singleton → Permutation_singleton_r, and Permutation_cons_inv → Permutation_cons_inv_r.
  • Add lemmas Permutation_nil_l, Permutation_singleton_l, and Permutation_cons_inv_l.
  • Add new instance cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k)..
  • Add lemma Permutation_cross_split.
  • Make lemma elem_of_Permutation a biimplication
• Add function kmap to transform the keys of finite maps.
• Set Hint Mode for the classes PartialOrder, TotalOrder, MRet, MBind, MJoin, FMap, OMap, MGuard, SemiSet, Set_, TopSet, and Infinite.
• Strengthen the extensionality lemmas map_filter_ext and map_filter_strong_ext:
  • Rename map_filter_strong_ext → map_filter_strong_ext_1 and map_filter_ext → map_filter_ext_1.
  • Add new bidirectional lemmas map_filter_strong_ext and map_filter_ext.
  • Add map_filter_strong_ext_2 and map_filter_ext_2.
• Make collection of lemmas for filter + union/disjoint consistent for sets and maps:
  • Sets: Add lemmas disjoint_filter, disjoint_filter_complement, and filter_union_complement.
  • Maps: Rename map_disjoint_filter → map_disjoint_filter_complement and map_union_filter → map_filter_union_complement to be consistent with sets.
  • Maps: Add lemmas map_disjoint_filter and map_filter_union analogous to sets.
• Add cross split lemma map_cross_split for maps
• Setoid results for options:
  • Add instance option_fmap_equiv_inj.
  • Add Proper instances for union, union_with, intersection_with, and difference_with.
  • Rename instances option_mbind_proper → option_bind_proper and option_mjoin_proper → option_join_proper to be consistent with similar instances for sets and lists.
  • Rename equiv_None → None_equiv_eq.
  • Replace equiv_Some_inv_l, equiv_Some_inv_r, equiv_Some_inv_l', and equiv_Some_inv_r' by new lemma Some_equiv_eq that follows the pattern of other ≡-inversion lemmas: it uses a ↔ and puts the arguments of ≡ and = in consistent order.
• Setoid results for lists:
  • Add ≡-inversion lemmas nil_equiv_eq, cons_equiv_eq, list_singleton_equiv_eq, and app_equiv_eq.
  • Add lemmas Permutation_equiv and equiv_Permutation.
• Setoid results for maps:
  • Add instances map_singleton_equiv_inj and map_fmap_equiv_inj.
  • Add and generalize many Proper instances.
  • Add lemma map_equiv_lookup_r.
  • Add lemma map_equiv_iff.
  • Rename map_equiv_empty → map_empty_equiv_eq.
  • Add ≡-inversion lemmas insert_equiv_eq, delete_equiv_eq, map_union_equiv_eq, etc.
• Drop DiagNone precondition of lookup_merge rule of FinMap interface.
  • Drop DiagNone class.
  • Add merge_proper instance.
  • Simplify lemmas about merge by dropping the DiagNone precondition.
  • Generalize lemmas partial_alter_merge, partial_alter_merge_l, and partial_alter_merge_r.
  • Drop unused merge_assoc' instance.
• Improvements to head and tail functions for lists:
  • Define head as notation that prints (Coq defines it as parsing only) similar to tail.
  • Declare tail as simpl nomatch.
  • Add lemmas about head and tail.
• Add and extend equivalences between closure operators:
  • Add ↔ lemmas that relate rtc, tc, nsteps, and bsteps.
  • Rename → lemmas rtc_nsteps → rtc_nsteps_1, nsteps_rtc → rtc_nsteps_2, rtc_bsteps → rtc_bsteps_1, and bsteps_rtc → rtc_bsteps_2.
  • Add lemmas that relate rtc, tc, nsteps, and bsteps to path representations as lists.
• Remove explicit equality from cross split lemmas so that they become easier to use in forward-style proofs.
• Add lemmas for finite maps: dom_map_zip_with, dom_map_zip_with_L, map_filter_id, map_filter_subseteq, and map_lookup_zip_Some.
• Add lemmas for sets: elem_of_weaken and not_elem_of_weaken.
• Rename insert_delete → insert_delete_insert; add new insert_delete that is consistent with delete_insert.
• Fix statement of sum_inhabited_r. (by Paolo G. Giarrusso)
• Make done work on goals of the form is_Some.
• Add mk_evar tactic to generate evars (intended as a more useful replacement for Coq's evar tactic).
• Make solve_ndisj able to solve more goals of the form _ ⊆ ⊤ ∖ _, _ ∖ _ ## _, _ ## _ ∖ _, as well as _ ## ∅ and ∅ ## _, and goals containing _ ∖ _ ∖ _.
• Improvements to curry:
  • Swap names of curry/uncurry, curry3/uncurry3, curry4/uncurry4, gmap_curry/gmap_uncurry, and hcurry/huncurry to be consistent with Haskell and friends.
  • Add Params and Proper instances for curry/uncurry, curry3/uncurry3, and curry4/uncurry4.
  • Add lemmas that say that curry/curry3/curry4 and uncurry/uncurry3/uncurry4 are inverses.
• Rename map_union_subseteq_l_alt → map_union_subseteq_l' and map_union_subseteq_r_alt → map_union_subseteq_r' to be consistent with or_intro_{l,r}'.
• Add union_subseteq_l', union_subseteq_r' as transitive versions of union_subseteq_l, union_subseteq_r that can be more easily applyed.
• Rename gmultiset_elem_of_singleton_subseteq → gmultiset_singleton_subseteq_l and swap the equivalence to be consistent with Iris's singleton_included_l. Add gmultiset_singleton_subseteq, which is similar to singleton_included in Iris.
• Add lemmas singleton_subseteq_l and singleton_subseteq for sets.
• Add lemmas map_singleton_subseteq_l and map_singleton_subseteq for maps.
• Add lemmas singleton_submseteq_l and singleton_submseteq for unordered list inclusion, as well as lookup_submseteq and submseteq_insert.
• Make map_empty a biimplication.
• Clean up empty{',_inv,_iff} lemmas:
  • Write them all using ↔ and consistently use the _iff suffix. (But keep the _inv version when it is useful for rewriting.)
  • Remove map_to_list_empty_inv_alt; chain Permutation_nil_r and map_to_list_empty_iff instead.
  • Add lemma map_filter_empty_iff.
• Add generalized lemma map_filter_insert that covers both the True and False case. Rename old map_filter_insert → map_filter_insert_True and map_filter_insert_not_delete → map_filter_insert_False.
• Weaken premise of map_filter_delete_not to make it consistent with map_filter_insert_not'.
• Add lemmas for maps: map_filter_strong_subseteq_ext, map_filter_subseteq_ext, map_filter_subseteq_mono, map_filter_singleton, map_filter_singleton_True, map_filter_singleton_False, map_filter_comm, map_union_least, map_subseteq_difference_l, insert_difference, insert_difference', difference_insert, difference_insert_subseteq. (by Hai Dang)
• Add map_size_disj_union, size_dom, size_list_to_set.
• Tweak reduction on gset, so that cbn matches the behavior by simpl and does not unfold gset operations. (by Paolo G. Giarrusso, BedRock Systems)
• Add get_head tactic to determine the syntactic head of a function application term.
• Add map lookup lemmas: lookup_union_is_Some, lookup_difference_is_Some, lookup_union_Some_l_inv, lookup_union_Some_r_inv.
• Make Forall2_nil, Forall2_cons bidirectional lemmas with Forall2_nil_2, Forall2_cons_2 being the original one-directional versions (matching Forall_nil and Forall_cons). Rename Forall2_cons_inv to Forall2_cons_1.
• Enable f_equiv (and by extension solve_proper) to handle goals of the form f x ≡ g x when f ≡ g is in scope, where f has a type like Iris's -d> and -n>.
• Optimize f_equiv by doing more syntactic checking before handing off to unification. This can make some uses 50x faster, but also makes the tactic slightly weaker in case the left-hand side and right-hand side of the relation call a function with arguments that are convertible but not syntactically equal.
• Add lemma choose_proper showing that choose P respects predicate equivalence. (by Paolo G. Giarrusso, BedRock Systems)
• Extract module well_founded from relations, and re-export it for compatibility. This contains wf, Acc_impl, wf_guard, wf_projected, Fix_F_proper, Fix_unfold_rel.
• Add induction principle well_founded.Acc_dep_ind, a dependent version of Acc_ind. (by Paolo G. Giarrusso, BedRock Systems)

The following sed script should perform most of the renaming (on macOS, replace sed by gsed, installed via e.g. brew install gnu-sed). Note that the script is not idempotent, do not run it twice.

sed -i -E -f- $(find theories -name "*.v") <<EOF
s/\bdecide_left\b/decide_True_pi/g
s/\bdecide_right\b/decide_False_pi/g
# Permutation
s/\bPermutation_nil\b/Permutation_nil_r/g
s/\bPermutation_singleton\b/Permutation_singleton_r/g
s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
# Filter
s/\bmap_disjoint_filter\b/map_disjoint_filter_complement/g
s/\bmap_union_filter\b/map_filter_union_complement/g
# mbind
s/\boption_mbind_proper\b/option_bind_proper/g
s/\boption_mjoin_proper\b/option_join_proper/g
# relations
s/\brtc_nsteps\b/rtc_nsteps_1/g
s/\bnsteps_rtc\b/rtc_nsteps_2/g
s/\brtc_bsteps\b/rtc_bsteps_1/g
s/\bbsteps_rtc\b/rtc_bsteps_2/g
# setoid
s/\bequiv_None\b/None_equiv_eq/g
s/\bmap_equiv_empty\b/map_empty_equiv_eq/g
# insert_delete
s/\binsert_delete\b/insert_delete_insert/g
# filter extensionality lemmas
s/\bmap_filter_ext\b/map_filter_ext_1/g
s/\bmap_filter_strong_ext\b/map_filter_strong_ext_1/g
# swap curry/uncurry
s/\b(lookup_gmap_|gmap_|h|)curry(|3|4)\b/OLD\1curry\2/g
s/\b(lookup_gmap_|gmap_|h|)uncurry(|3|4)\b/\1curry\2/g
s/\bOLD(lookup_gmap_|gmap_|h|)curry(|3|4)\b/\1uncurry\2/g
s/\bgmap_curry_uncurry\b/gmap_uncurry_curry/g
s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
s/\bhcurry_uncurry\b/huncurry_curry/g
s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
# map_union_subseteq
s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
# singleton
s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
# empty_iff
s/\bmap_to_list_empty('|_inv)\b/map_to_list_empty_iff/g
s/\bkmap_empty_inv\b/kmap_empty_iff/g
s/\belements_empty'\b/elements_empty_iff/g
s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
# map_filter_insert
s/\bmap_filter_insert\b/map_filter_insert_True/g
s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
# Forall2
s/\bForall2_cons_inv\b/Forall2_cons_1/g
EOF

std++ 1.5.0 (2021-02-16)

Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer supported.

This release of std++ was managed by Ralf Jung and Robbert Krebbers, with contributions by Alix Trieu, Dan Frumin, Hugo Herbelin, Paulo Emílio de Vilhena, Simon Friis Vindum, and Tej Chajed. Thanks a lot to everyone involved!

• Overhaul of the theory of positive rationals Qp:
  • Add max and min operations for Qp.
  • Add the orders Qp_le and Qp_lt.
  • Rename Qp_plus into Qp_add and Qp_mult into Qp_mul to be consistent with the corresponding names for nat, N, and Z.
  • Add a function Qp_inv for the multiplicative inverse.
  • Define the division function Qp_div in terms of Qp_inv, and generalize the second argument from positive to Qp.
  • Add a function pos_to_Qp that converts a positive into a positive rational Qp.
  • Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.
  • Remove the coercion from Qp to Qc. This follows our recent tradition of getting rid of coercions since they are more often confusing than useful.
  • Rename the conversion from Qp_car : Qp → Qc into Qp_to_Qc to be consistent with other conversion functions in std++. Also rename the lemma Qp_eq into Qp_to_Qc_inj_iff.
  • Use let '(..) = ... in the definitions of Qp_plus, Qp_mult, Qp_inv, Qp_le and Qp_lt to avoid Coq tactics (like injection) to unfold these definitions eagerly.
  • Define the Qp literals 1, 2, 3, 4 in terms of pos_to_Qp instead of iterated addition.
  • Rename and restate many lemmas so as to be consistent with the conventions for Coq's number types nat, N, and Z.
• Add rename select <pat> into <name> tactic to find a hypothesis by pattern and give it a fixed name.
• Add eunify tactic that lifts Coq's unify tactic to open_constr.
• Generalize omap_insert, omap_singleton, map_size_insert, and map_size_delete to cover the Some and None case. Add _Some and _None versions of the lemmas for the specific cases.
• Rename dom_map filter → dom_filter, dom_map_filter_L → dom_filter_L, and dom_map_filter_subseteq → dom_filter_subseteq for consistency's sake.
• Remove unused notations ∪**, ∪*∪**, ∖**, ∖*∖**, ⊆**, ⊆1*, ⊆2*, ⊆1**, ⊆2**", ##**, ##1*, ##2*, ##1**, ##2** for nested zip_with and Forall2 versions of ∪, ∖, and ##.
• Remove unused type classes DisjointE, DisjointList, LookupE, and InsertE.
• Fix a bug where pretty 0 was defined as "", the empty string. It now returns "0" for N, Z, and nat.
• Remove duplicate map_fmap_empty of fmap_empty, and rename map_fmap_empty_inv into fmap_empty_inv for consistency's sake.
• Rename seq_S_end_app to seq_S. (The lemma seq_S is also in Coq's stdlib since Coq 8.12.)
• Remove omega import and hint database in tactics file.
• Remove unused find_pat tactic that was made mostly obsolete by select.
• Rename _11 and _12 into _1_1 and _1_2, respectively. These suffixes are used for A → B1 and A → B2 variants of A ↔ B1 ∧ B2 lemmas.
• Rename Forall_Forall2 → Forall_Forall2_diag to be consistent with the names for big operators in Iris.
• Rename set equality and equivalence lemmas: elem_of_equiv_L → set_eq, set_equiv_spec_L → set_eq_subseteq, elem_of_equiv → set_equiv, set_equiv_spec → set_equiv_subseteq.
• Remove lemmas map_filter_iff and map_filter_lookup_eq in favor of the stronger extensionality lemmas map_filter_ext and map_filter_strong_ext.

The following sed script should perform most of the renaming (on macOS, replace sed by gsed, installed via e.g. brew install gnu-sed):

sed -i -E '
s/\bQp_plus\b/Qp_add/g
s/\bQp_mult\b/Qp_mul/g
s/\bQp_mult_1_l\b/Qp_mul_1_l/g
s/\bQp_mult_1_r\b/Qp_mul_1_r/g
s/\bQp_plus_id_free\b/Qp_add_id_free/g
s/\bQp_not_plus_ge\b/Qp_not_add_le_l/g
s/\bQp_le_plus_l\b/Qp_le_add_l/g
s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
s/\bmap_fmap_empty\b/fmap_empty/g
s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
s/\bseq_S_end_app\b/seq_S/g
s/\bomap_insert\b/omap_insert_Some/g
s/\bomap_singleton\b/omap_singleton_Some/g
s/\bomap_size_insert\b/map_size_insert_None/g
s/\bomap_size_delete\b/map_size_delete_Some/g
s/\bNoDup_cons_11\b/NoDup_cons_1_1/g
s/\bNoDup_cons_12\b/NoDup_cons_1_2/g
s/\bmap_filter_lookup_Some_11\b/map_filter_lookup_Some_1_1/g
s/\bmap_filter_lookup_Some_12\b/map_filter_lookup_Some_1_2/g
s/\bmap_Forall_insert_11\b/map_Forall_insert_1_1/g
s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
s/\bForall_Forall2\b/Forall_Forall2_diag/g
s/\belem_of_equiv_L\b/set_eq/g
s/\bset_equiv_spec_L\b/set_eq_subseteq/g
s/\belem_of_equiv\b/set_equiv/g
s/\bset_equiv_spec\b/set_equiv_subseteq/g
' $(find theories -name "*.v")

std++ 1.4.0 (released 2020-07-15)

Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.

This release of std++ received contributions by Gregory Malecha, Michael Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, sarahzrf, and Tej Chajed.

• Rename Z2Nat_inj_div and Z2Nat_inj_mod to Nat2Z_inj_div and Nat2Z_inj_mod to follow the naming convention of Nat2Z and Z2Nat. Re-purpose the names Z2Nat_inj_div and Z2Nat_inj_mod for be the lemmas they should actually be.
• Add rotate and rotate_take functions for accessing a list with wrap-around. Also add rotate_nat_add and rotate_nat_sub for computing indicies into a rotated list.
• Add the select and revert select tactics for selecting and reverting a hypothesis based on a pattern.
• Extract list_numbers.v from list.v and numbers.v for functions, which operate on lists of numbers (seq, seqZ, sum_list(_with) and max_list(_with)). list_numbers.v is exported by the prelude. This is a breaking change if one only imports list.v, but not the prelude.
• Rename drop_insert into drop_insert_gt and add drop_insert_le.
• Add Countable instance for Ascii.ascii.
• Make lemma list_find_Some more apply friendly.
• Add filter_app lemma.
• Add tactic multiset_solver for solving goals involving multisets.
• Rename fin_maps.singleton_proper into singletonM_proper since it concerns singletonM and to avoid overlap with sets.singleton_proper.
• Add wn R for weakly normalizing elements w.r.t. a relation R.
• Add encode_Z/decode_Z functions to encode elements of a countable type as integers Z, in analogy with encode_nat/decode_nat.
• Fix list Datatypes.length and string strings.length shadowing (length should now always be Datatypes.length).
• Change the notation for pattern matching monadic bind into 'pat ← x; y. It was ''pat ← x; y (with double ') due to a shortcoming of Coq ≤8.7.

std++ 1.3.0 (released 2020-03-18)