CHANGELOG.md 30.7 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
This file lists "large-ish" changes to the std++ Coq library, but not every
2
3
API-breaking change is listed.

Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
## std++ master

Tej Chajed's avatar
Tej Chajed committed
6
7
8
9
10
11
12
13
14
15
16
## 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!

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
- 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).
20
- Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13.
Ralf Jung's avatar
Ralf Jung committed
21
  (by Lennard Gäher)
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
29
30
31
- 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's avatar
Ralf Jung committed
32
- Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
33
- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
- Rename `decide_left``decide_True_pi` and `decide_right``decide_False_pi`.
35
- Add `option_guard_True_pi`.
Ralf Jung's avatar
Ralf Jung committed
36
37
38
39
40
41
- 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's avatar
Robbert Krebbers committed
42
- Add tactics `compute_done` and `compute_by` for solving goals by computation.
43
- Add `Inj` instances for `fmap` on option and maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
- Various changes to `Permutation` lemmas:
45
46
47
48
49
  + 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's avatar
Robbert Krebbers committed
50
51
52
  + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
  + Add lemma `Permutation_cross_split`.
  + Make lemma `elem_of_Permutation` a biimplication
Robbert Krebbers's avatar
Robbert Krebbers committed
53
- Add function `kmap` to transform the keys of finite maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
  `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
56
57
58
59
60
61
- 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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
66
67
68
69
70
- 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
Robbert Krebbers's avatar
Robbert Krebbers committed
71
- Setoid results for options:
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  + Add instance `option_fmap_equiv_inj`.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
  + 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
  + Add lemma `map_equiv_lookup_r`.
  + Add lemma `map_equiv_iff`.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
  + Rename `map_equiv_empty``map_empty_equiv_eq`.
  + Add `≡`-inversion lemmas `insert_equiv_eq`, `delete_equiv_eq`,
    `map_union_equiv_eq`, etc.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
98
99
100
101
- 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
105
106
- 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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
109
110
111
112
113
- 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
- Remove explicit equality from cross split lemmas so that they become easier
  to use in forward-style proofs.
116
117
118
- 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`.
Ralf Jung's avatar
Ralf Jung committed
119
120
- Rename `insert_delete``insert_delete_insert`; add new `insert_delete` that
  is consistent with `delete_insert`.
Ralf Jung's avatar
Ralf Jung committed
121
- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
Robbert Krebbers's avatar
Robbert Krebbers committed
122
- Make `done` work on goals of the form `is_Some`.
Ralf Jung's avatar
Ralf Jung committed
123
124
- Add `mk_evar` tactic to generate evars (intended as a more useful replacement
  for Coq's `evar` tactic).
Ralf Jung's avatar
Ralf Jung committed
125
- Make `solve_ndisj` able to solve more goals of the form `_ ⊆ ⊤ ∖ _`,
126
127
  `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`,
  and goals containing `_ ∖ _ ∖ _`.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
131
132
133
- 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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
  + Add lemmas that say that `curry`/`curry3`/`curry4` and
    `uncurry`/`uncurry3`/`uncurry4` are inverses.
136
137
138
- 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}'`.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
- Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
Ralf Jung's avatar
Ralf Jung committed
140
  `union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
- Rename `gmultiset_elem_of_singleton_subseteq``gmultiset_singleton_subseteq_l`
Ralf Jung's avatar
Ralf Jung committed
142
  and swap the equivalence to be consistent with Iris's `singleton_included_l`. Add
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
  `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
  Iris.
- Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
- Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
Ralf Jung's avatar
Ralf Jung committed
147
148
- Add lemmas `singleton_submseteq_l` and `singleton_submseteq` for unordered
  list inclusion, as well as `lookup_submseteq` and `submseteq_insert`.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
- Make `map_empty` a biimplication.
- Clean up `empty{',_inv,_iff}` lemmas:
  + Write them all using `↔` and consistently use the `_iff` suffix.
152
    (But keep the `_inv` version when it is useful for rewriting.)
Ralf Jung's avatar
Ralf Jung committed
153
  + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    `map_to_list_empty_iff` instead.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  + Add lemma `map_filter_empty_iff`.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
- 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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
- Weaken premise of `map_filter_delete_not` to make it consistent with
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  `map_filter_insert_not'`.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164
165
- 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)
Ralf Jung's avatar
Ralf Jung committed
166
- Add `map_size_disj_union`, `size_dom`, `size_list_to_set`.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
167
168
- Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
  does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
Ralf Jung's avatar
Ralf Jung committed
169
170
- Add `get_head` tactic to determine the syntactic head of a function
  application term.
Ralf Jung's avatar
Ralf Jung committed
171
172
- Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
  `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
Ralf Jung's avatar
Ralf Jung committed
173
174
175
- 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`.
Ralf Jung's avatar
Ralf Jung committed
176
177
178
- 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>`.
Ralf Jung's avatar
Ralf Jung committed
179
180
181
182
183
- 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.
Ralf Jung's avatar
Ralf Jung committed
184

Robbert Krebbers's avatar
Robbert Krebbers committed
185
The following `sed` script should perform most of the renaming
Ralf Jung's avatar
Ralf Jung committed
186
187
(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.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
```
189
sed -i -E -f- $(find theories -name "*.v") <<EOF
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
s/\bdecide_left\b/decide_True_pi/g
s/\bdecide_right\b/decide_False_pi/g
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
# Permutation
s/\bPermutation_nil\b/Permutation_nil_r/g
s/\bPermutation_singleton\b/Permutation_singleton_r/g
195
s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
# Filter
s/\bmap_disjoint_filter\b/map_disjoint_filter_complement/g
s/\bmap_union_filter\b/map_filter_union_complement/g
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
# mbind
s/\boption_mbind_proper\b/option_bind_proper/g
s/\boption_mjoin_proper\b/option_join_proper/g
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
205
206
# 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
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
# setoid
s/\bequiv_None\b/None_equiv_eq/g
s/\bmap_equiv_empty\b/map_empty_equiv_eq/g
Ralf Jung's avatar
Ralf Jung committed
210
211
# insert_delete
s/\binsert_delete\b/insert_delete_insert/g
212
213
214
# 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
Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
217
218
219
220
221
222
# 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
223
s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
224
225
# map_union_subseteq
s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
# singleton
s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
# empty_iff
s/\bmap_to_list_empty('|_inv)\b/map_to_list_empty_iff/g
s/\bkmap_empty_inv\b/kmap_empty_iff/g
Ralf Jung's avatar
Ralf Jung committed
231
232
s/\belements_empty'\b/elements_empty_iff/g
s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
235
# 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
Ralf Jung's avatar
Ralf Jung committed
236
237
# Forall2
s/\bForall2_cons_inv\b/Forall2_cons_1/g
238
EOF
Robbert Krebbers's avatar
Robbert Krebbers committed
239
```
Robbert Krebbers's avatar
Robbert Krebbers committed
240

Ralf Jung's avatar
Ralf Jung committed
241
## std++ 1.5.0 (2021-02-16)
Ralf Jung's avatar
Ralf Jung committed
242

243
244
Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer
supported.
Ralf Jung's avatar
Ralf Jung committed
245

Ralf Jung's avatar
Ralf Jung committed
246
247
248
249
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's avatar
Robbert Krebbers committed
250
- Overhaul of the theory of positive rationals `Qp`:
251
  + Add `max` and `min` operations for `Qp`.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
  + 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`.
274
275
276
277
278
279
280
281
282
283
284
285
286
- 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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
- Fix a bug where `pretty 0` was defined as `""`, the empty string. It now
  returns `"0"` for `N`, `Z`, and `nat`.
289
290
- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
  `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
291
292
- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
  since Coq 8.12.)
Robbert Krebbers's avatar
Robbert Krebbers committed
293
- Remove `omega` import and hint database in `tactics` file.
Ralf Jung's avatar
Ralf Jung committed
294
- Remove unused `find_pat` tactic that was made mostly obsolete by `select`.
295
296
- 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.
297
298
- Rename `Forall_Forall2``Forall_Forall2_diag` to be consistent with the
  names for big operators in Iris.
299
300
301
302
303
- 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`.
304
305
- 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's avatar
Simon Friis Vindum committed
306
307
308
309

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's avatar
Ralf Jung committed
310
sed -i -E '
311
312
313
314
315
316
317
318
319
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
320
321
s/\bmap_fmap_empty\b/fmap_empty/g
s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
322
s/\bseq_S_end_app\b/seq_S/g
323
324
325
326
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
327
328
329
330
331
332
333
334
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
335
s/\bForall_Forall2\b/Forall_Forall2_diag/g
336
337
338
339
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's avatar
Simon Friis Vindum committed
340
341
' $(find theories -name "*.v")
```
342

343
## std++ 1.4.0 (released 2020-07-15)
Michael Sammler's avatar
Michael Sammler committed
344

Ralf Jung's avatar
Ralf Jung committed
345
Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
Ralf Jung's avatar
Ralf Jung committed
346

Ralf Jung's avatar
Ralf Jung committed
347
348
349
350
This release of std++ received contributions by Gregory Malecha, Michael
Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers,
sarahzrf, and Tej Chajed.

351
352
- 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's avatar
Ralf Jung committed
353
354
355
356
  `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
357
  computing indicies into a rotated list.
Ralf Jung's avatar
Ralf Jung committed
358
- Add the `select` and `revert select` tactics for selecting and
359
  reverting a hypothesis based on a pattern.
Ralf Jung's avatar
Ralf Jung committed
360
- Extract `list_numbers.v` from `list.v` and `numbers.v` for
361
362
363
364
  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's avatar
Tej Chajed committed
365
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
Ralf Jung's avatar
Ralf Jung committed
366
- Add `Countable` instance for `Ascii.ascii`.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
- Make lemma `list_find_Some` more apply friendly.
Ralf Jung's avatar
Ralf Jung committed
368
- Add `filter_app` lemma.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
- Add tactic `multiset_solver` for solving goals involving multisets.
Ralf Jung's avatar
Ralf Jung committed
370
371
372
373
374
375
376
- 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's avatar
Robbert Krebbers committed
377
378
- 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's avatar
Michael Sammler committed
379

380
## std++ 1.3.0 (released 2020-03-18)
381
382
383
384
385
386
387
388
389

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:
390
391
392
393

- 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.
394
- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
396
397
398
- 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's avatar
Robbert Krebbers committed
399
400
- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
  `boolset`, `propset`, and `coPset`.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
- Add `set_solver` support for `dom`.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
  `list_to_vec_to_list` for the converse.
404
405
406
- 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's avatar
Robbert Krebbers committed
407
- Add `Countable` instance for `vec`.
Armaël Guéneau's avatar
Armaël Guéneau committed
408
409
410
411
412
413
414
- 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.
415
- Add tactic `set_unfold in H`.
416
417
- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
  `TCEq`, and `TCDiag`.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419
420
- 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's avatar
Robbert Krebbers committed
421
422
423
  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's avatar
Robbert Krebbers committed
424
425
426
427
428
429
430
431
- 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`
432

Ralf Jung's avatar
Ralf Jung committed
433
434
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's avatar
Ralf Jung committed
435
```
Ralf Jung's avatar
Ralf Jung committed
436
sed -i '
Ralf Jung's avatar
Ralf Jung committed
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
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's avatar
Ralf Jung committed
452
## std++ 1.2.1 (released 2019-08-29)
Ralf Jung's avatar
Ralf Jung committed
453

454
455
This release of std++ received contributions by Dan Frumin, Michael Sammler,
Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
456
Rodolphe Lepigre, and Simon Spies.
Ralf Jung's avatar
Ralf Jung committed
457
458
459

Noteworthy additions and changes:

460
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
Ralf Jung's avatar
Ralf Jung committed
461
- Make `solve_ndisj` tactic more powerful.
462
463
464
465
- 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's avatar
Ralf Jung committed
466

Ralf Jung's avatar
Ralf Jung committed
467
## std++ 1.2.0 (released 2019-04-26)
Robbert Krebbers's avatar
Robbert Krebbers committed
468
469

Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
Ralf Jung's avatar
Ralf Jung committed
470
std++ 1.1 if you have to use Coq 8.6. The repository moved to a new location at
Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
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's avatar
Ralf Jung committed
493
- A `size` function for finite maps and prove some properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
494
495
- More results about `Qp` fractions.
- More miscellaneous results about sets, maps, lists, multisets.
496
497
- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
  and `tc_to_bool`.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
- 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's avatar
Robbert Krebbers committed
515
  the max of the multiplicities).
Robbert Krebbers's avatar
Robbert Krebbers committed
516
- Set `Hint Mode` for `pretty`.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538

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:
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590

```
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's avatar
Ralf Jung committed
591
## std++ 1.1.0 (released 2017-12-19)
592

Ralf Jung's avatar
Ralf Jung committed
593
594
595
Coq 8.5 is no longer supported by this release of std++.  Use std++ 1.0 if you
have to use Coq 8.5.

596
597
598
New features:

- Many new lemmas about lists, vectors, sets, maps.
Ralf Jung's avatar
Ralf Jung committed
599
600
601
- 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:
602
  `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
Ralf Jung's avatar
Ralf Jung committed
603
- A function `tc_opaque` to make definitions type class opaque.
604
605
606
607
608
609
610
611
612
- 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's avatar
Ralf Jung committed
613
614
  Also get rid of `Set Asymmetric Patterns`.
- Various changes and improvements to `f_equiv` and `solve_proper`.
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
- `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's avatar
Ralf Jung committed
630
- All notations are now in `stdpp_scope` with scope key `stdpp`
631
  (formerly `C_scope` and `C`).
Ralf Jung's avatar
Ralf Jung committed
632
633
- Higher precedence for `.1` and `.2` that is compatible with ssreflect.
- Various changes to monadic notations to improve compatibility with Mtac2:
634
635
636
637
638
  + 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's avatar
Ralf Jung committed
639
640
641
642
643
644
645
646

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