Verified Commit b5b97894 authored by Tej Chajed's avatar Tej Chajed
Browse files

std++ 1.6.0 release notes

parent 0499e9bc
Pipeline #56113 passed with stage
in 7 minutes and 42 seconds
......@@ -3,20 +3,31 @@ API-breaking change is listed.
## std++ master
## std++ 1.6.0
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 Tej Chajed and Ralf Jung, with
contributions from Alix Trieu, Andrej Dudenhefner, Dan Frumin, Fengmin Zhu,
Hoang-Hai Dang, Jan, 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
- Add a new type class `SingletonMS` (with projection `{[+ x +]}` for
multiset singletons.
+ Define `{[+ x1; .. ; xn +]}` as notation for `{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}`.
- 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
- 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
- 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.
......@@ -31,68 +42,68 @@ API-breaking change is listed.
- 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`,
- 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
- 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 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
- 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`.
- 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
- Sets: Add lemmas `disjoint_filter`, `disjoint_filter_complement`, and
`filter_union_complement`.
+ Maps: Rename `map_disjoint_filter``map_disjoint_filter_complement` and
- 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
- 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
- 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
- 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
- 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`.
- 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`,
- 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
- 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.
- 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`)
- 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`.
- 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`,
......@@ -115,12 +126,12 @@ API-breaking change is listed.
`_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`,
and goals containing `_ ∖ _ ∖ _`.
- Improvements to curry:
+ Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
- 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`,
- Add `Params` and `Proper` instances for `curry`/`uncurry`,
`curry3`/`uncurry3`, and `curry4`/`uncurry4`.
+ Add lemmas that say that `curry`/`curry3`/`curry4` and
- 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
......@@ -137,11 +148,11 @@ API-breaking change is listed.
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.
- 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
- 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 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`.
......@@ -174,6 +185,7 @@ API-breaking change is listed.
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
......@@ -234,31 +246,31 @@ 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!
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
- 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
- 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
- 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,
- 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
- 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
- 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`,
- 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
- 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
- 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.
......@@ -295,6 +307,7 @@ Simon Friis Vindum, and Tej Chajed. Thanks a lot to everyone involved!
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
......@@ -411,16 +424,17 @@ Noteworthy additions and changes:
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`,
- 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`
- 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`):
```
sed -i '
s/\bdom_map_filter\b/dom_map_filter_subseteq/g
......@@ -509,18 +523,18 @@ 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`
- `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`.
- `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`
- `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`.
......@@ -579,7 +593,7 @@ s/to\_bools/natset\_to\_bools/g;
## std++ 1.1.0 (released 2017-12-19)
Coq 8.5 is no longer supported by this release of std++. Use std++ 1.0 if you
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:
......@@ -620,11 +634,11 @@ Changes to notations:
(formerly `C_scope` and `C`).
- 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
- 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`.
- Change the level of the do-notation.
- `<$>` is left associative.
- Notation `x ;; y` for `_ ← x; y`.
## History
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment