CHANGELOG.md 12.9 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.

Michael Sammler's avatar
Michael Sammler committed
4
5
## std++ master

6
7
8
9
- 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`. The names `Z2Nat_inj_div` and `Z2Nat_inj_mod` have been
  repurposed for be the lemmas they should actually be.
10
11
12
- Added `rotate` and `rotate_take` functions for accessing a list with
  wrap-around. Also added `rotate_nat_add` and `rotate_nat_sub` for
  computing indicies into a rotated list.
13
14
- Added the `select` and `revert select` tactics for selecting and
  reverting a hypothesis based on a pattern.
15
16
17
18
19
- Extracted `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.
Tej Chajed's avatar
Tej Chajed committed
20
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
21
- Added `Countable` instance for `Ascii.ascii`.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
- Make lemma `list_find_Some` more apply friendly.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
- Add tactic `multiset_solver` for solving goals involving multisets.
Michael Sammler's avatar
Michael Sammler committed
24

25
26
27
28
29
30
31
32
33
34
## std++ 1.3 (released 2020-03-18)

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:
35
36
37
38

- 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.
39
- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
- 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
44
45
- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
  `boolset`, `propset`, and `coPset`.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
- Add `set_solver` support for `dom`.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
  `list_to_vec_to_list` for the converse.
49
50
51
- 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
52
- Add `Countable` instance for `vec`.
Armaël Guéneau's avatar
Armaël Guéneau committed
53
54
55
56
57
58
59
- 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.
60
- Add tactic `set_unfold in H`.
61
62
- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
  `TCEq`, and `TCDiag`.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
- 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
66
67
68
  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
69
70
71
72
73
74
75
76
- 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`
77
78
- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
  `singletonM` and to avoid overlap with `sets.singleton_proper`.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
80
81
- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
  as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
82

Ralf Jung's avatar
Ralf Jung committed
83
84
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
85
```
Ralf Jung's avatar
Ralf Jung committed
86
sed -i '
Ralf Jung's avatar
Ralf Jung committed
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
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
102
## std++ 1.2.1 (released 2019-08-29)
Ralf Jung's avatar
Ralf Jung committed
103

104
105
This release of std++ received contributions by Dan Frumin, Michael Sammler,
Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
106
Rodolphe Lepigre, and Simon Spies.
Ralf Jung's avatar
Ralf Jung committed
107
108
109

Noteworthy additions and changes:

110
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
Ralf Jung's avatar
Ralf Jung committed
111
- Make `solve_ndisj` tactic more powerful.
112
113
114
115
- 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
116

Ralf Jung's avatar
Ralf Jung committed
117
## std++ 1.2.0 (released 2019-04-26)
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119

Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
Ralf Jung's avatar
Ralf Jung committed
120
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
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
143
- A `size` function for finite maps and prove some properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
- More results about `Qp` fractions.
- More miscellaneous results about sets, maps, lists, multisets.
146
147
- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
  and `tc_to_bool`.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
- 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
  the max of the multiplicities). 

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:
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239

```
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
240
## std++ 1.1.0 (released 2017-12-19)
241

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

245
246
247
New features:

- Many new lemmas about lists, vectors, sets, maps.
Ralf Jung's avatar
Ralf Jung committed
248
249
250
- 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:
251
  `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
Ralf Jung's avatar
Ralf Jung committed
252
- A function `tc_opaque` to make definitions type class opaque.
253
254
255
256
257
258
259
260
261
- 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
262
263
  Also get rid of `Set Asymmetric Patterns`.
- Various changes and improvements to `f_equiv` and `solve_proper`.
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
- `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
279
- All notations are now in `stdpp_scope` with scope key `stdpp`
280
  (formerly `C_scope` and `C`).
Ralf Jung's avatar
Ralf Jung committed
281
282
- Higher precedence for `.1` and `.2` that is compatible with ssreflect.
- Various changes to monadic notations to improve compatibility with Mtac2:
283
284
285
286
287
  + 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
288
289
290
291
292
293
294
295

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