CHANGELOG.md 21.4 KB
 Ralf Jung committed Dec 18, 2017 1 ``````This file lists "large-ish" changes to the std++ Coq library, but not every `````` Robbert Krebbers committed Dec 18, 2017 2 3 ``````API-breaking change is listed. `````` Robbert Krebbers committed Mar 11, 2021 4 5 6 7 8 ``````## std++ master - 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). `````` Robbert Krebbers committed Mar 19, 2021 9 ``````- Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13. `````` Ralf Jung committed May 20, 2021 10 `````` (by Lennard Gäher) `````` Robbert Krebbers committed Apr 20, 2021 11 12 13 14 15 16 17 18 19 20 ``````- 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. `````` Ralf Jung committed Apr 29, 2021 21 ``````- Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more. `````` Ralf Jung committed Apr 29, 2021 22 ``````- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more. `````` Robbert Krebbers committed May 03, 2021 23 ``````- Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`. `````` Robbert Krebbers committed May 04, 2021 24 ``````- Add `option_guard_True_pi`. `````` Ralf Jung committed May 26, 2021 25 26 27 28 29 30 ``````- 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) `````` Robbert Krebbers committed May 26, 2021 31 ``````- Add tactics `compute_done` and `compute_by` for solving goals by computation. `````` Robbert Krebbers committed May 26, 2021 32 ``````- Add `Inj` instances for `fmap` on option and maps. `````` Robbert Krebbers committed Jun 01, 2021 33 ``````- Various changes to `Permutation` lemmas: `````` Robbert Krebbers committed Jun 02, 2021 34 35 36 37 38 `````` + 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`. `````` Robbert Krebbers committed Jun 01, 2021 39 40 41 `````` + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`. + Add lemma `Permutation_cross_split`. + Make lemma `elem_of_Permutation` a biimplication `````` Robbert Krebbers committed Jun 02, 2021 42 ``````- Add function `kmap` to transform the keys of finite maps. `````` Robbert Krebbers committed Jun 04, 2021 43 44 ``````- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`, `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`. `````` Dan Frumin committed Jun 06, 2021 45 ``````- Make `map_filter_strong_ext` and `map_filter_ext` bidirectional. `````` Robbert Krebbers committed May 03, 2021 46 47 48 49 50 51 52 `````` 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/\bdecide_left\b/decide_True_pi/g s/\bdecide_right\b/decide_False_pi/g `````` Robbert Krebbers committed Jun 01, 2021 53 54 55 ``````# Permutation s/\bPermutation_nil\b/Permutation_nil_r/g s/\bPermutation_singleton\b/Permutation_singleton_r/g `````` Robbert Krebbers committed Jun 02, 2021 56 ``````s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g `````` Robbert Krebbers committed May 03, 2021 57 58 ``````' \$(find theories -name "*.v") ``` `````` Robbert Krebbers committed Mar 11, 2021 59 `````` `````` Ralf Jung committed May 20, 2021 60 ``````## std++ 1.5.0 (2021-02-16) `````` Ralf Jung committed Feb 15, 2021 61 `````` `````` Robbert Krebbers committed Feb 15, 2021 62 63 ``````Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer supported. `````` Ralf Jung committed Oct 06, 2020 64 `````` `````` Ralf Jung committed Feb 15, 2021 65 66 67 68 ``````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! `````` Robbert Krebbers committed Oct 29, 2020 69 ``````- Overhaul of the theory of positive rationals `Qp`: `````` Ralf Jung committed Oct 30, 2020 70 `````` + Add `max` and `min` operations for `Qp`. `````` Robbert Krebbers committed Oct 29, 2020 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 `````` + 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`. `````` Robbert Krebbers committed Feb 15, 2021 93 94 95 96 97 98 99 100 101 102 103 104 105 ``````- Add `rename select into ` 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`. `````` Robbert Krebbers committed Nov 10, 2020 106 107 ``````- Fix a bug where `pretty 0` was defined as `""`, the empty string. It now returns `"0"` for `N`, `Z`, and `nat`. `````` Robbert Krebbers committed Jan 04, 2021 108 109 ``````- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake. `````` Robbert Krebbers committed Jan 11, 2021 110 111 ``````- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib since Coq 8.12.) `````` Robbert Krebbers committed Jan 19, 2021 112 ``````- Remove `omega` import and hint database in `tactics` file. `````` Ralf Jung committed Jan 20, 2021 113 ``````- Remove unused `find_pat` tactic that was made mostly obsolete by `select`. `````` Robbert Krebbers committed Jan 27, 2021 114 115 ``````- 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 Jan 28, 2021 116 117 ``````- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the names for big operators in Iris. `````` Ralf Jung committed Feb 01, 2021 118 119 120 121 122 ``````- 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`. `````` Paulo Emílio de Vilhena committed Feb 15, 2021 123 124 ``````- 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`. `````` Simon Friis Vindum committed Oct 02, 2020 125 126 127 128 `````` The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): ``` `````` Ralf Jung committed Oct 30, 2020 129 ``````sed -i -E ' `````` Robbert Krebbers committed Oct 31, 2020 130 131 132 133 134 135 136 137 138 ``````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 `````` Robbert Krebbers committed Jan 04, 2021 139 140 ``````s/\bmap_fmap_empty\b/fmap_empty/g s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g `````` Robbert Krebbers committed Jan 11, 2021 141 ``````s/\bseq_S_end_app\b/seq_S/g `````` Robbert Krebbers committed Jan 23, 2021 142 143 144 145 ``````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 `````` Robbert Krebbers committed Jan 27, 2021 146 147 148 149 150 151 152 153 ``````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 Jan 28, 2021 154 ``````s/\bForall_Forall2\b/Forall_Forall2_diag/g `````` Ralf Jung committed Feb 01, 2021 155 156 157 158 ``````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 `````` Simon Friis Vindum committed Oct 02, 2020 159 160 ``````' \$(find theories -name "*.v") ``` `````` Robbert Krebbers committed Jul 16, 2020 161 `````` `````` Ralf Jung committed Jul 15, 2020 162 ``````## std++ 1.4.0 (released 2020-07-15) `````` Michael Sammler committed Mar 31, 2020 163 `````` `````` Ralf Jung committed Jul 14, 2020 164 ``````Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported. `````` Ralf Jung committed Jul 02, 2020 165 `````` `````` Ralf Jung committed Jul 15, 2020 166 167 168 169 ``````This release of std++ received contributions by Gregory Malecha, Michael Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers, sarahzrf, and Tej Chajed. `````` Michael Sammler committed May 12, 2020 170 171 ``````- Rename `Z2Nat_inj_div` and `Z2Nat_inj_mod` to `Nat2Z_inj_div` and `Nat2Z_inj_mod` to follow the naming convention of `Nat2Z` and `````` Ralf Jung committed Jul 14, 2020 172 173 174 175 `````` `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 `````` Michael Sammler committed May 12, 2020 176 `````` computing indicies into a rotated list. `````` Ralf Jung committed Jul 14, 2020 177 ``````- Add the `select` and `revert select` tactics for selecting and `````` Michael Sammler committed Apr 16, 2020 178 `````` reverting a hypothesis based on a pattern. `````` Ralf Jung committed Jul 14, 2020 179 ``````- Extract `list_numbers.v` from `list.v` and `numbers.v` for `````` Michael Sammler committed Apr 15, 2020 180 181 182 183 `````` 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. `````` Tej Chajed committed Mar 31, 2020 184 ``````- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`. `````` Ralf Jung committed Jul 14, 2020 185 ``````- Add `Countable` instance for `Ascii.ascii`. `````` Robbert Krebbers committed May 12, 2020 186 ``````- Make lemma `list_find_Some` more apply friendly. `````` Ralf Jung committed Jul 14, 2020 187 ``````- Add `filter_app` lemma. `````` Robbert Krebbers committed Jun 25, 2020 188 ``````- Add tactic `multiset_solver` for solving goals involving multisets. `````` Ralf Jung committed Jul 14, 2020 189 190 191 192 193 194 195 ``````- 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`). `````` Robbert Krebbers committed Jul 15, 2020 196 197 ``````- 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. `````` Michael Sammler committed Mar 31, 2020 198 `````` `````` Ralf Jung committed Jul 15, 2020 199 ``````## std++ 1.3.0 (released 2020-03-18) `````` Robbert Krebbers committed Mar 17, 2020 200 201 202 203 204 205 206 207 208 `````` 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: `````` Robbert Krebbers committed Sep 11, 2019 209 210 211 212 `````` - 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. `````` Robbert Krebbers committed Oct 01, 2019 213 ``````- Generalize `list_find_Some` and `list_find_None` to become bi-implications. `````` Robbert Krebbers committed Sep 19, 2019 214 215 216 217 ``````- 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 `````` Robbert Krebbers committed Feb 17, 2020 218 219 ``````- Add type class `TopSet` for sets with a `⊤` element. Provide instances for `boolset`, `propset`, and `coPset`. `````` Robbert Krebbers committed Feb 24, 2020 220 ``````- Add `set_solver` support for `dom`. `````` Robbert Krebbers committed Feb 24, 2020 221 222 ``````- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma `list_to_vec_to_list` for the converse. `````` Robbert Krebbers committed Mar 05, 2020 223 224 225 ``````- 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. `````` Robbert Krebbers committed Feb 24, 2020 226 ``````- Add `Countable` instance for `vec`. `````` Armaël Guéneau committed Feb 28, 2020 227 228 229 230 231 232 233 ``````- 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. `````` Robbert Krebbers committed Mar 09, 2020 234 ``````- Add tactic `set_unfold in H`. `````` Robbert Krebbers committed Mar 10, 2020 235 236 ``````- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`, `TCEq`, and `TCDiag`. `````` Robbert Krebbers committed Mar 17, 2020 237 238 239 ``````- 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 `````` Robbert Krebbers committed Mar 17, 2020 240 241 242 `````` 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. `````` Robbert Krebbers committed Mar 17, 2020 243 244 245 246 247 248 249 250 ``````- 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` `````` Robbert Krebbers committed Sep 11, 2019 251 `````` `````` Ralf Jung committed Apr 02, 2020 252 253 ``````The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): `````` Ralf Jung committed Mar 19, 2020 254 ````````` `````` Ralf Jung committed Apr 06, 2020 255 ``````sed -i ' `````` Ralf Jung committed Mar 19, 2020 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 ``````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") ``` `````` Ralf Jung committed Aug 29, 2019 271 ``````## std++ 1.2.1 (released 2019-08-29) `````` Ralf Jung committed Aug 07, 2019 272 `````` `````` Robbert Krebbers committed Aug 24, 2019 273 274 ``````This release of std++ received contributions by Dan Frumin, Michael Sammler, Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers, `````` Robbert Krebbers committed Aug 15, 2019 275 ``````Rodolphe Lepigre, and Simon Spies. `````` Ralf Jung committed Aug 07, 2019 276 277 278 `````` Noteworthy additions and changes: `````` Robbert Krebbers committed Aug 15, 2019 279 ``````- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`. `````` Ralf Jung committed Aug 07, 2019 280 ``````- Make `solve_ndisj` tactic more powerful. `````` Robbert Krebbers committed Aug 15, 2019 281 282 283 284 ``````- 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`. `````` Ralf Jung committed Aug 07, 2019 285 `````` `````` Ralf Jung committed Apr 26, 2019 286 ``````## std++ 1.2.0 (released 2019-04-26) `````` Robbert Krebbers committed Apr 26, 2019 287 288 `````` Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use `````` Ralf Jung committed Apr 26, 2019 289 ``````std++ 1.1 if you have to use Coq 8.6. The repository moved to a new location at `````` Robbert Krebbers committed Apr 26, 2019 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 ``````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. `````` Ralf Jung committed Apr 26, 2019 312 ``````- A `size` function for finite maps and prove some properties. `````` Robbert Krebbers committed Apr 26, 2019 313 314 ``````- More results about `Qp` fractions. - More miscellaneous results about sets, maps, lists, multisets. `````` Robbert Krebbers committed Apr 26, 2019 315 316 ``````- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`, and `tc_to_bool`. `````` Robbert Krebbers committed Apr 26, 2019 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 ``````- 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 `````` Robbert Krebbers committed Oct 29, 2020 334 `````` the max of the multiplicities). `````` Robbert Krebbers committed Nov 12, 2020 335 ``````- Set `Hint Mode` for `pretty`. `````` Robbert Krebbers committed Apr 26, 2019 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 `````` 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: `````` Robbert Krebbers committed Feb 20, 2019 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 `````` ``` 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") ``` `````` Ralf Jung committed Dec 19, 2017 410 ``````## std++ 1.1.0 (released 2017-12-19) `````` Robbert Krebbers committed Dec 18, 2017 411 `````` `````` Ralf Jung committed Dec 18, 2017 412 413 414 ``````Coq 8.5 is no longer supported by this release of std++. Use std++ 1.0 if you have to use Coq 8.5. `````` Robbert Krebbers committed Dec 18, 2017 415 416 417 ``````New features: - Many new lemmas about lists, vectors, sets, maps. `````` Ralf Jung committed Dec 18, 2017 418 419 420 ``````- 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: `````` Robbert Krebbers committed Dec 18, 2017 421 `````` `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`. `````` Ralf Jung committed Dec 18, 2017 422 ``````- A function `tc_opaque` to make definitions type class opaque. `````` Robbert Krebbers committed Dec 18, 2017 423 424 425 426 427 428 429 430 431 ``````- 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. `````` Ralf Jung committed Dec 18, 2017 432 433 `````` Also get rid of `Set Asymmetric Patterns`. - Various changes and improvements to `f_equiv` and `solve_proper`. `````` Robbert Krebbers committed Dec 18, 2017 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 ``````- `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. `````` Ralf Jung committed Dec 18, 2017 449 ``````- All notations are now in `stdpp_scope` with scope key `stdpp` `````` Robbert Krebbers committed Dec 18, 2017 450 `````` (formerly `C_scope` and `C`). `````` Ralf Jung committed Dec 18, 2017 451 452 ``````- Higher precedence for `.1` and `.2` that is compatible with ssreflect. - Various changes to monadic notations to improve compatibility with Mtac2: `````` Robbert Krebbers committed Dec 18, 2017 453 454 455 456 457 `````` + 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`. `````` Ralf Jung committed Dec 18, 2017 458 459 460 461 462 463 464 465 `````` ## 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.``````