CHANGELOG.md 32.8 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. `````` Tej Chajed committed Jan 20, 2022 4 ``````## std++ 1.7.0 `````` Robbert Krebbers committed Mar 11, 2021 5 `````` `````` Tej Chajed committed Jan 20, 2022 6 7 8 9 10 11 12 ``````Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain supported. Coq 8.10 is no longer supported. This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a lot to everyone involved! `````` Ralf Jung committed Dec 03, 2021 13 `````` `````` Michael Sammler committed Dec 07, 2021 14 15 ``````- Add `is_closed_term` tactic for determining whether a term depends on variables bound in the context. (by Michael Sammler) `````` Glen Mével committed Dec 01, 2021 16 17 ``````- Add `list.zip_with_take_both` and `list.zip_with_take_both'` - Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'` `````` Michael Sammler committed Dec 01, 2021 18 19 ``````- Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler) - Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler) `````` Michael Sammler committed Nov 24, 2021 20 ``````- Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`. `````` Robbert Krebbers committed Dec 07, 2021 21 ``````- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`. `````` Ralf Jung committed Dec 13, 2021 22 ``````- Remove a spurious `Global Arguments Pos.of_nat : simpl never`. `````` Robbert Krebbers committed Dec 16, 2021 23 ``````- Add tactics `destruct select ` and `destruct select as `. `````` Glen Mével committed Dec 21, 2021 24 ``````- Add some more lemmas about `Finite` and `pred_finite`. `````` Jonas Kastberg committed Jan 12, 2022 25 26 ``````- Add lemmas about `last`: `last_app_cons`, `last_app`, `last_Some`, and `last_Some_elem_of`. `````` Michael Sammler committed Nov 24, 2021 27 28 29 30 31 32 33 34 `````` 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") <` and `-n>`. `````` Ralf Jung committed Sep 27, 2021 213 214 215 216 217 ``````- 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. `````` Paolo G. Giarrusso committed Nov 04, 2021 218 219 ``````- Add lemma `choose_proper` showing that `choose P` respects predicate equivalence. (by Paolo G. Giarrusso, BedRock Systems) `````` Paolo G. Giarrusso committed Nov 05, 2021 220 ``````- Extract module `well_founded` from `relations`, and re-export it for `````` Robbert Krebbers committed Nov 05, 2021 221 `````` compatibility. This contains `wf`, `Acc_impl`, `wf_guard`, `````` Paolo G. Giarrusso committed Nov 05, 2021 222 `````` `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`. `````` Robbert Krebbers committed Nov 05, 2021 223 ``````- Add induction principle `well_founded.Acc_dep_ind`, a dependent `````` Paolo G. Giarrusso committed Nov 05, 2021 224 `````` version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems) `````` Ralf Jung committed Jun 25, 2021 225 `````` `````` Robbert Krebbers committed May 03, 2021 226 ``````The following `sed` script should perform most of the renaming `````` Ralf Jung committed Jun 25, 2021 227 228 ``````(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 committed May 03, 2021 229 ````````` `````` Robbert Krebbers committed Jul 27, 2021 230 ``````sed -i -E -f- \$(find theories -name "*.v") < 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 328 329 ``````- 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 330 331 ``````- 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 332 333 ``````- 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 334 ``````- Remove `omega` import and hint database in `tactics` file. `````` Ralf Jung committed Jan 20, 2021 335 ``````- Remove unused `find_pat` tactic that was made mostly obsolete by `select`. `````` Robbert Krebbers committed Jan 27, 2021 336 337 ``````- 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 338 339 ``````- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the names for big operators in Iris. `````` Ralf Jung committed Feb 01, 2021 340 341 342 343 344 ``````- 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 345 346 ``````- 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 347 348 349 350 `````` 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 351 ``````sed -i -E ' `````` Robbert Krebbers committed Oct 31, 2020 352 353 354 355 356 357 358 359 360 ``````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 361 362 ``````s/\bmap_fmap_empty\b/fmap_empty/g s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g `````` Robbert Krebbers committed Jan 11, 2021 363 ``````s/\bseq_S_end_app\b/seq_S/g `````` Robbert Krebbers committed Jan 23, 2021 364 365 366 367 ``````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 368 369 370 371 372 373 374 375 ``````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 376 ``````s/\bForall_Forall2\b/Forall_Forall2_diag/g `````` Ralf Jung committed Feb 01, 2021 377 378 379 380 ``````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 381 382 ``````' \$(find theories -name "*.v") ``` `````` Robbert Krebbers committed Jul 16, 2020 383 `````` `````` Ralf Jung committed Jul 15, 2020 384 ``````## std++ 1.4.0 (released 2020-07-15) `````` Michael Sammler committed Mar 31, 2020 385 `````` `````` Ralf Jung committed Jul 14, 2020 386 ``````Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported. `````` Ralf Jung committed Jul 02, 2020 387 `````` `````` Ralf Jung committed Jul 15, 2020 388 389 390 391 ``````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 392 393 ``````- 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 394 395 396 397 `````` `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 398 `````` computing indicies into a rotated list. `````` Ralf Jung committed Jul 14, 2020 399 ``````- Add the `select` and `revert select` tactics for selecting and `````` Michael Sammler committed Apr 16, 2020 400 `````` reverting a hypothesis based on a pattern. `````` Ralf Jung committed Jul 14, 2020 401 ``````- Extract `list_numbers.v` from `list.v` and `numbers.v` for `````` Michael Sammler committed Apr 15, 2020 402 403 404 405 `````` 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 406 ``````- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`. `````` Ralf Jung committed Jul 14, 2020 407 ``````- Add `Countable` instance for `Ascii.ascii`. `````` Robbert Krebbers committed May 12, 2020 408 ``````- Make lemma `list_find_Some` more apply friendly. `````` Ralf Jung committed Jul 14, 2020 409 ``````- Add `filter_app` lemma. `````` Robbert Krebbers committed Jun 25, 2020 410 ``````- Add tactic `multiset_solver` for solving goals involving multisets. `````` Ralf Jung committed Jul 14, 2020 411 412 413 414 415 416 417 ``````- 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 418 419 ``````- 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 420 `````` `````` Ralf Jung committed Jul 15, 2020 421 ``````## std++ 1.3.0 (released 2020-03-18) `````` Robbert Krebbers committed Mar 17, 2020 422 423 424 425 426 427 428 429 430 `````` 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 431 432 433 434 `````` - 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 435 ``````- Generalize `list_find_Some` and `list_find_None` to become bi-implications. `````` Robbert Krebbers committed Sep 19, 2019 436 437 438 439 ``````- 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 440 441 ``````- Add type class `TopSet` for sets with a `⊤` element. Provide instances for `boolset`, `propset`, and `coPset`. `````` Robbert Krebbers committed Feb 24, 2020 442 ``````- Add `set_solver` support for `dom`. `````` Robbert Krebbers committed Feb 24, 2020 443 444 ``````- 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 445 446 447 ``````- 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 448 ``````- Add `Countable` instance for `vec`. `````` Armaël Guéneau committed Feb 28, 2020 449 450 451 452 453 454 455 ``````- 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 456 ``````- Add tactic `set_unfold in H`. `````` Robbert Krebbers committed Mar 10, 2020 457 458 ``````- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`, `TCEq`, and `TCDiag`. `````` Robbert Krebbers committed Mar 17, 2020 459 460 461 ``````- 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 462 463 464 `````` 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 465 466 467 468 469 470 471 472 ``````- 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 473 `````` `````` Ralf Jung committed Apr 02, 2020 474 475 ``````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 476 ````````` `````` Ralf Jung committed Apr 06, 2020 477 ``````sed -i ' `````` Ralf Jung committed Mar 19, 2020 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 ``````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 493 ``````## std++ 1.2.1 (released 2019-08-29) `````` Ralf Jung committed Aug 07, 2019 494 `````` `````` Robbert Krebbers committed Aug 24, 2019 495 496 ``````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 497 ``````Rodolphe Lepigre, and Simon Spies. `````` Ralf Jung committed Aug 07, 2019 498 499 500 `````` Noteworthy additions and changes: `````` Robbert Krebbers committed Aug 15, 2019 501 ``````- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`. `````` Ralf Jung committed Aug 07, 2019 502 ``````- Make `solve_ndisj` tactic more powerful. `````` Robbert Krebbers committed Aug 15, 2019 503 504 505 506 ``````- 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 507 `````` `````` Ralf Jung committed Apr 26, 2019 508 ``````## std++ 1.2.0 (released 2019-04-26) `````` Robbert Krebbers committed Apr 26, 2019 509 510 `````` Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use `````` Ralf Jung committed Apr 26, 2019 511 ``````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 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 ``````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 534 ``````- A `size` function for finite maps and prove some properties. `````` Robbert Krebbers committed Apr 26, 2019 535 536 ``````- More results about `Qp` fractions. - More miscellaneous results about sets, maps, lists, multisets. `````` Robbert Krebbers committed Apr 26, 2019 537 538 ``````- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`, and `tc_to_bool`. `````` Robbert Krebbers committed Apr 26, 2019 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 ``````- 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 556 `````` the max of the multiplicities). `````` Robbert Krebbers committed Nov 12, 2020 557 ``````- Set `Hint Mode` for `pretty`. `````` Robbert Krebbers committed Apr 26, 2019 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 `````` 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 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 `````` ``` 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 632 ``````## std++ 1.1.0 (released 2017-12-19) `````` Robbert Krebbers committed Dec 18, 2017 633 `````` `````` Ralf Jung committed Dec 18, 2017 634 635 636 ``````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 637 638 639 ``````New features: - Many new lemmas about lists, vectors, sets, maps. `````` Ralf Jung committed Dec 18, 2017 640 641 642 ``````- 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 643 `````` `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`. `````` Ralf Jung committed Dec 18, 2017 644 ``````- A function `tc_opaque` to make definitions type class opaque. `````` Robbert Krebbers committed Dec 18, 2017 645 646 647 648 649 650 651 652 653 ``````- 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 654 655 `````` Also get rid of `Set Asymmetric Patterns`. - Various changes and improvements to `f_equiv` and `solve_proper`. `````` Robbert Krebbers committed Dec 18, 2017 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 ``````- `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 671 ``````- All notations are now in `stdpp_scope` with scope key `stdpp` `````` Robbert Krebbers committed Dec 18, 2017 672 `````` (formerly `C_scope` and `C`). `````` Ralf Jung committed Dec 18, 2017 673 674 ``````- 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 675 676 677 678 679 `````` + 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 680 681 682 683 684 685 686 687 `````` ## 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.``````