Newer
Older
This file lists "large-ish" changes to the std++ Coq library, but not every
- 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
- Add function `map_preimage` to compute the preimage of a finite map.
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
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.
- 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 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.
+ 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
+ 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)
- 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 `apply`ed.
- 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
- 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
- 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)
- 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
# 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
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!
+ 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.
Robbert Krebbers
committed
- 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`):
```
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
Robbert Krebbers
committed
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
Robbert Krebbers
committed
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
Robbert Krebbers
committed
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 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.
Coq 8.11 is supported by this release.
This release of std++ received contributions by Amin Timany, Armaël Guéneau,
Dan Frumin, David Swasey, Jacques-Henri Jourdan, Michael Sammler, Paolo G.
Giarrusso, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Simon Friis Vindum,
Tej Chajed, and William Mansky
Noteworthy additions and changes:
- Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
`dom_map_filter` for the version with the equality. This follows the naming
convention for similar lemmas.
- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
- Disambiguate Haskell-style notations for partially applied operators. For
example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
prefix, as done in VST. A sed script to perform the renaming can be found at:
https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
`boolset`, `propset`, and `coPset`.
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
`list_to_vec_to_list` for the converse.
- Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into
`fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow
the conventions.
- Introduce `destruct_or{?,!}` to repeatedly destruct disjunctions in
assumptions. The tactic can also be provided an explicit assumption name;
`destruct_and{?,!}` has been generalized accordingly and now can also be
provided an explicit assumption name.
Slight breaking change: `destruct_and` no longer handle `False`;
`destruct_or` now handles `False` while `destruct_and` handles `True`,
as the respective units of disjunction and conjunction.
- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
`TCEq`, and `TCDiag`.
- Add type class `LookupTotal` with total lookup operation `(!!!) : M → K → A`.
Provide instances for `list`, `fin_map`, and `vec`, as well as corresponding
lemmas for the operations on these types. The instance for `vec` replaces the
ad-hoc `!!!` definition. As a consequence, arguments of `!!!` are no longer
parsed in `vec_scope` and `fin_scope`, respectively. Moreover, since `!!!`
is overloaded, coercions around `!!!` no longer work.
- Make lemmas for `seq` and `seqZ` consistent:
+ Rename `fmap_seq` → `fmap_S_seq`
+ Add `fmap_add_seq`, and rename `seqZ_fmap` → `fmap_add_seqZ`
+ Rename `lookup_seq` → `lookup_seq_lt`
+ Rename `seqZ_lookup_lt` → `lookup_seqZ_lt`,
`seqZ_lookup_ge` → `lookup_seqZ_ge`, and `seqZ_lookup` → `lookup_seqZ`
+ Rename `lookup_seq_inv` → `lookup_seq` and generalize it to a bi-implication
+ Add `NoDup_seqZ` and `Forall_seqZ`
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
s/\bdom_map_filter\b/dom_map_filter_subseteq/g
s/\bfmap_seq\b/fmap_S_seq/g
s/\bseqZ_fmap\b/fmap_add_seqZ/g
s/\blookup_seq\b/lookup_seq_lt/g
s/\blookup_seq_inv\b/lookup_seq/g
s/\bseqZ_lookup_lt\b/lookup_seqZ_lt/g
s/\bseqZ_lookup_ge\b/lookup_seqZ_ge/g
s/\bseqZ_lookup\b/lookup_seqZ/g
s/\bvec_to_list_of_list\b/vec_to_list_to_vec/g
s/\bfin_of_nat\b/nat_to_fin/g
s/\bfin_to_of_nat\b/fin_to_nat_to_fin/g
s/\bfin_of_to_nat\b/nat_to_fin_to_nat/g
' $(find theories -name "*.v")
```
This release of std++ received contributions by Dan Frumin, Michael Sammler,
Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
Rodolphe Lepigre, and Simon Spies.
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
- Add type class `Involutive`.
- Improve `naive_solver` performance in case the goal is trivially solvable.
- Add a bunch of new lemmas for list, set, and map operations.
- Rename `lookup_imap` into `map_lookup_imap`.
Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
std++ 1.1 if you have to use Coq 8.6. The repository moved to a new location at
https://gitlab.mpi-sws.org/iris/stdpp and automatically generated Coq-doc of
master is available at https://plv.mpi-sws.org/coqdoc/stdpp/.
This release of std++ received contributions by Dan Frumin, Hai Dang, Jan-Oliver
Kaiser, Mackie Loeffel, Maxime Dénès, Ralf Jung, Robbert Krebbers, and Tej
Chajed.
New features:
- New notations `=@{A}`, `≡@{A}`, `∈@{A}`, `∉@{A}`, `##@{A}`, `⊆@{A}`, `⊂@{A}`,
`⊑@{A}`, `≡ₚ@{A}` for being explicit about the type.
- A definition of basic telescopes `tele` and some theory about them.
- A simple type class based canceler `NatCancel` for natural numbers.
- A type `binder` for anonymous and named binders to be used in program language
definitions with string-based binders.
- More results about `set_fold` on sets and multisets.
- Notions of infinite and finite predicates/sets and basic theory about them.
- New operation `map_seq`.
- The symmetric and reflexive/transitive/symmetric closure of a relation (`sc`
and `rtsc`, respectively).
- Different notions of confluence (diamond property, confluence, local
confluence) and the relations between these.
- A `size` function for finite maps and prove some properties.
- More results about `Qp` fractions.
- More miscellaneous results about sets, maps, lists, multisets.
- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
and `tc_to_bool`.
- Generalize `gset_to_propset` to `set_to_propset` for any `SemiSet`.
Changes:
- Consistently use `lia` instead of `omega` everywhere.
- Consistently block `simpl` on all `Z` operations.
- The `Infinite` class is now defined using a function `fresh : list A → A`
that given a list `xs`, gives an element `fresh xs ∉ xs`.
- Make `default` an abbreviation for `from_option id` (instead of just swapping
the argument order of `from_option`).
- More efficient `Countable` instance for `list` that is linear instead of
exponential.
- Improve performance of `set_solver` significantly by introducing specialized
type class `SetUnfoldElemOf` for propositions involving `∈`.
- Make `gset` a `Definition` instead of a `Notation` to improve performance.
- Use `disj_union` (notation `⊎`) for disjoint union on multisets (that adds the
multiplicities). Repurpose `∪` on multisets for the actual union (that takes
Naming:
- Consistently use the `set` prefix instead of the `collection` prefix for
definitions and lemmas.
- Renaming of classes:
+ `Collection` into `Set_` (`_` since `Set` is a reserved keyword)
+ `SimpleCollection` into `SemiSet`
+ `FinCollection` into `FinSet`
+ `CollectionMonad` into `MonadSet`
- Types:
+ `set A := A → Prop` into `propset`
+ `bset := A → bool` into `boolset`.
- Files:
+ `collections.v` into `sets.v`
+ `fin_collections.v` into `fin_sets.v`
+ `bset` into `boolset`
+ `set` into `propset`
- Consistently use the naming scheme `X_to_Y` for conversion functions, e.g.
`list_to_map` instead of the former `map_of_list`.
The following `sed` script should perform most of the renaming:
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
s/to\_gmap/gset\_to\_gmap/g;
s/of\_bools/bools\_to\_natset/g;
s/to_bools/natset\_to\_bools/g;
s/coPset\.of_gset/gset\_to\_coPset/g;
s/coPset\.elem\_of\_of\_gset/elem\_of\_gset\_to\_coPset/g;
s/of\_gset\_finite/gset\_to\_coPset\_finite/g;
s/set\_seq\_S\_disjoint/set\_seq\_S\_end\_disjoint/g;
s/set\_seq\_S\_union/set\_seq\_S\_end\_union/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/of\_bools/bools\_to\_natset/g;
s/to\_bools/natset\_to\_bools/g;
' -i $(find -name "*.v")
```
Coq 8.5 is no longer supported by this release of std++. Use std++ 1.0 if you
have to use Coq 8.5.
New features:
- Many new lemmas about lists, vectors, sets, maps.
- Equivalence proofs between std++ functions and their alternative in the the
Coq standard library, e.g. `List.nth`, `List.NoDop`.
- Typeclass versions of the logical connectives and list predicates:
`TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
- A function `tc_opaque` to make definitions type class opaque.
- A type class `Infinite` for infinite types.
- A generic implementation to obtain fresh elements of infinite types.
- More theory about curry and uncurry functions on `gmap`.
- A generic `filter` and `zip_with` operation on finite maps.
- A type of generic trees for showing that arbitrary types are countable.
Changes:
- Get rid of `Automatic Coercions Import`, it is deprecated.
Also get rid of `Set Asymmetric Patterns`.
- Various changes and improvements to `f_equiv` and `solve_proper`.
- `Hint Mode` is now set for all operational type classes to make instance
search less likely to diverge.
- New type class `RelDecision` for decidable relations, and `EqDecision` is
defined in terms of it. This class allows to set `Hint Mode` properly.
- Use the flag `assert` of `Arguments` to make it more robust.
- The functions `imap` and `imap2` on lists are defined so that they enjoy more
definitional equalities.
- Theory about `fin` is moved to its own file `fin.v`.
- Rename `preserving` → `mono`.
Changes to notations:
- Operational type classes for lattice notations: `⊑`,`⊓`, `⊔`, `⊤` `⊥`.
- Replace `⊥` for disjointness with `##`, so that `⊥` can be used for the
bottom lattice element.
- All notations are now in `stdpp_scope` with scope key `stdpp`
- Higher precedence for `.1` and `.2` that is compatible with ssreflect.
- Various changes to monadic notations to improve compatibility with Mtac2:
+ Pattern matching notation for monadic bind `'pat ← x; y` where `pat` can
be any Coq pattern.
+ Change the level of the do-notation.
+ `<$>` is left associative.
+ Notation `x ;; y` for `_ ← x; y`.
## History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
part of the [Iris project](http://iris-project.org), and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.