Commits (659)
# Enable syntax highlighting.
*.v gitlab-language=coq *.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
*.vo *.vo
*.vos
*.vok
*.vio *.vio
*.v.d *.v.d
.coqdeps.d .coqdeps.d
.Makefile.coq.d
*.glob *.glob
*.cache *.cache
*.aux *.aux
...@@ -14,5 +17,5 @@ Makefile.coq ...@@ -14,5 +17,5 @@ Makefile.coq
Makefile.coq.conf Makefile.coq.conf
*.crashcoqide *.crashcoqide
html/ html/
build-dep/ builddep/
_opam _opam
...@@ -16,63 +16,46 @@ variables: ...@@ -16,63 +16,46 @@ variables:
cache: cache:
key: "$CI_JOB_NAME" key: "$CI_JOB_NAME"
paths: paths:
- opamroot/ - _opam/
only: only:
- master - master@iris/stdpp
- /^ci/ - /^ci/@iris/stdpp
except: except:
- triggers - triggers
- schedules - schedules
- api
## Build jobs ## Build jobs
build-coq.dev: build-coq.dev:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev" OPAM_PINS: "coq version dev"
MANGLE_NAMES: "1"
CI_COQCHK: "1" CI_COQCHK: "1"
build-coq.8.9.0: build-coq.8.13.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.9.0" OPAM_PINS: "coq version 8.13.2"
OPAM_PKG: "coq-stdpp" DENY_WARNINGS: "1"
OPAM_PKG: "1"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp" DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
tags: tags:
- fp-timing - fp-timing
build-coq.8.8.2: build-coq.8.12.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.2" OPAM_PINS: "coq version 8.12.2"
DENY_WARNINGS: "1"
build-coq.8.8.1: build-coq.8.11.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.1" OPAM_PINS: "coq version 8.11.2"
build-coq.8.8.0: build-coq.8.10.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.0" OPAM_PINS: "coq version 8.10.2"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
build-coq.8.7.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.0"
...@@ -3,20 +3,332 @@ API-breaking change is listed. ...@@ -3,20 +3,332 @@ API-breaking change is listed.
## std++ master ## std++ master
Numerous functions and theorems have been renamed. - 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
- Consistently use `set` instead of `collection`. with a product for maps (there's now the `singletonM` class).
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection` - Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13.
is called `SemiSet`, and `FinCollection` is called `FinSet`, and - Add multiset literal notation `{[+ x1; .. ; xn +]}`.
`CollectionMonad` is called `MonadSet`. + Add a new type class `SingletonMS` (with projection `{[+ x +]}` for
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`, multiset singletons.
respectively. + Define `{[+ x1; .. ; xn +]}` as notation for `{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}`.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise - Remove the `Singleton` and `Semiset` instances for multisets to avoid
`bset` into `boolset`. accidental use.
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map` + This means the notation `{[ x1; .. ; xn ]}` no longer works for multisets
instead of the former `map_of_list`. (previously, its definition was wrong, since it used `∪` instead of `⊎`).
+ Add lemmas for `∈` and `∉` specific for multisets, since the set lemmas no
The following `sed` script should get you a long way: longer work for multisets.
- Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
- Rename `decide_left``decide_True_pi` and `decide_right``decide_False_pi`.
- Add `option_guard_True_pi`.
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
' $(find theories -name "*.v")
```
## std++ 1.5.0
Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer
supported.
This release of std++ was managed by Ralf Jung and Robbert Krebbers, with
contributions by Alix Trieu, Dan Frumin, Hugo Herbelin, Paulo Emílio de Vilhena,
Simon Friis Vindum, and Tej Chajed. Thanks a lot to everyone involved!
- Overhaul of the theory of positive rationals `Qp`:
+ Add `max` and `min` operations for `Qp`.
+ Add the orders `Qp_le` and `Qp_lt`.
+ Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent
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`.
- 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`.
- Fix a bug where `pretty 0` was defined as `""`, the empty string. It now
returns `"0"` for `N`, `Z`, and `nat`.
- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
`map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
since Coq 8.12.)
- Remove `omega` import and hint database in `tactics` file.
- Remove unused `find_pat` tactic that was made mostly obsolete by `select`.
- 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.
- Rename `Forall_Forall2``Forall_Forall2_diag` to be consistent with the
names for big operators in Iris.
- 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`.
- 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`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
```
sed -i -E '
s/\bQp_plus\b/Qp_add/g
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
s/\bmap_fmap_empty\b/fmap_empty/g
s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
s/\bseq_S_end_app\b/seq_S/g
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
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
s/\bForall_Forall2\b/Forall_Forall2_diag/g
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
' $(find theories -name "*.v")
```
## std++ 1.4.0 (released 2020-07-15)
Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
This release of std++ received contributions by Gregory Malecha, Michael
Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers,
sarahzrf, and Tej Chajed.
- 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`. 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
computing indicies into a rotated list.
- Add the `select` and `revert select` tactics for selecting and
reverting a hypothesis based on a pattern.
- Extract `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.
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
- Add `Countable` instance for `Ascii.ascii`.
- Make lemma `list_find_Some` more apply friendly.
- Add `filter_app` lemma.
- Add tactic `multiset_solver` for solving goals involving multisets.
- 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`).
- 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.
## std++ 1.3.0 (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:
- 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.
- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
- 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
- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
`boolset`, `propset`, and `coPset`.
- Add `set_solver` support for `dom`.
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
`list_to_vec_to_list` for the converse.
- 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.
- Add `Countable` instance for `vec`.
- 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.
- Add tactic `set_unfold in H`.
- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
`TCEq`, and `TCDiag`.
- 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
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.
- 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`
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
```
sed -i '
s/\bdom_map_filter\b/dom_map_filter_subseteq/g
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")
```
## std++ 1.2.1 (released 2019-08-29)
This release of std++ received contributions by Dan Frumin, Michael Sammler,
Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
Rodolphe Lepigre, and Simon Spies.
Noteworthy additions and changes:
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
- Make `solve_ndisj` tactic more powerful.
- 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`.
## std++ 1.2.0 (released 2019-04-26)
Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
std++ 1.1 if you have to use Coq 8.6. The repository moved to a new location at
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.
- A `size` function for finite maps and prove some properties.
- More results about `Qp` fractions.
- More miscellaneous results about sets, maps, lists, multisets.
- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
and `tc_to_bool`.
- 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).
- Set `Hint Mode` for `pretty`.
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:
``` ```
sed ' sed '
......
All files in this development are distributed under the terms of the BSD All files in this development are distributed under the terms of the 3-clause
license, included below. BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
------------------------------------------------------------------------------ Copyright: std++ developers and contributors
BSD LICENCE ------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met: modification, are permitted provided that the following conditions are met:
...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met: ...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright * Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution. documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the * Neither the name of the copyright holder nor the names of its contributors
names of its contributors may be used to endorse or promote products may be used to endorse or promote products derived from this software
derived from this software without specific prior written permission. without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Forward most targets to Coq makefile (with some trick to make this phony) # Default target
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq all: Makefile.coq
+@make -f Makefile.coq all +@$(MAKE) -f Makefile.coq all
.PHONY: all .PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq clean: Makefile.coq
+@make -f Makefile.coq clean +@$(MAKE) -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true @# Make sure not to enter the `_opam` folder.
rm -f Makefile.coq find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean .PHONY: clean
# Create Coq Makefile. # Create Coq Makefile.
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile OPAMFILES=$(wildcard *.opam)
@echo "# Creating build-dep package." BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam builddep/%-builddep.opam: %.opam Makefile
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @echo "# Creating builddep package for $<."
@mkdir -p builddep
build-dep: build-dep/opam phony @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself. @# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \ @echo "# Installing builddep packages."
if opam --version | grep "^1\." -q; then \ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \ .PHONY: builddep
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \ # Backwards compatibility target
else \ build-dep: builddep
opam install $(OPAMFLAGS) build-dep/; \ .PHONY: build-dep
fi
# Some files that do *not* need to be forwarded to Makefile.coq.
# Some files that do *not* need to be forwarded to Makefile.coq # ("::" lets Makefile.local overwrite this.)
Makefile: ; Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
# use NO_TEST=1 to skip the tests
NO_TEST:=
# use MAKE_REF=1 to generate new reference files
MAKE_REF:=
# Run tests interleaved with main build. They have to be in the same target for this. # Run tests interleaved with main build. They have to be in the same target for this.
real-all: $(if $(NO_TEST),,test) real-all: $(if $(NO_TEST),,test)
# the test suite # the test suite
TESTFILES=$(wildcard tests/*.v) TESTFILES:=$(shell find tests -name "*.v")
NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo) test: $(TESTFILES:.v=.vo)
# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
if egrep '^\s*(Instance|Arguments|Remove|Hint (Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold))\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
done
.PHONY: test .PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1) COQ_MINOR_VERSION:=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES) tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES' $(SHOW)'COQDEP TESTFILES'
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok) $(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
-include tests/.coqdeps.d -include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) # Main test script (comments out-of-line because macOS otherwise barfs?!?)
$(HIDE)TEST="$$(basename -s .v $<)" && \ # - Determine reference file (`REF`).
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \ # - Print user-visible status line.
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \ # - Dump Coq output into a temporary file.
# - Run `sed -i` on that file in a way that works on macOS.
# - Either compare the result with the reference file, or move it over the reference file.
# - Cleanup, and mark as done for make.
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
$(HIDE)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
REF=$*".$(COQ_MINOR_VERSION).ref"; \
else \ else \
REF="tests/$$TEST.ref"; \ REF=$*".ref"; \
fi && \ fi && \
echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \ echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
TMPFILE="$$(mktemp)" && \ TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \ $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
$(if $(COQ_OLD),true, \ sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \ mv "$$TMPFILE".new "$$TMPFILE" && \
) && \ $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") && \
rm -f "$$TMPFILE" && \ rm -f "$$TMPFILE" && \
touch $@ touch $@
...@@ -45,11 +45,11 @@ Notably: ...@@ -45,11 +45,11 @@ Notably:
This version is known to compile with: This version is known to compile with:
- Coq version 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2 / 8.9.0 - Coq version 8.10.2 / 8.11.2 / 8.12.2 / 8.13.2
## Installing via opam ## Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add To obtain the latest stable release via opam (2.0.0 or newer), you have to add
the Coq opam repository: the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
...@@ -79,3 +79,9 @@ your account. Then you can fork the ...@@ -79,3 +79,9 @@ your account. Then you can fork the
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your [Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
changes in your fork, and create a merge request. changes in your fork, and create a merge request.
## Common problems
On Windows, differences in line endings may cause tests to fail. This can be
fixed by setting Git's autocrlf option to true:
git config --global core.autocrlf true
-Q theories stdpp -Q theories stdpp
# "Declare Scope" does not exist yet in 8.9
-arg -w -arg -undeclared-scope theories/options.v
theories/base.v theories/base.v
theories/tactics.v theories/tactics.v
theories/option.v theories/option.v
...@@ -33,10 +33,12 @@ theories/numbers.v ...@@ -33,10 +33,12 @@ theories/numbers.v
theories/nmap.v theories/nmap.v
theories/zmap.v theories/zmap.v
theories/coPset.v theories/coPset.v
theories/coGset.v
theories/lexico.v theories/lexico.v
theories/propset.v theories/propset.v
theories/decidable.v theories/decidable.v
theories/list.v theories/list.v
theories/list_numbers.v
theories/functions.v theories/functions.v
theories/hlist.v theories/hlist.v
theories/sorting.v theories/sorting.v
...@@ -44,3 +46,4 @@ theories/infinite.v ...@@ -44,3 +46,4 @@ theories/infinite.v
theories/nat_cancel.v theories/nat_cancel.v
theories/namespaces.v theories/namespaces.v
theories/telescopes.v theories/telescopes.v
theories/binders.v
This project contains an extended "Standard Library" for Coq called coq-std++. opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The std++ team"
license: "BSD-3-Clause"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
synopsis: "std++ is an extended \"Standard Library\" for Coq"
description: """
The key features of this library are as follows: The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data - It provides a great number of definitions and lemmas for common data
...@@ -17,3 +26,11 @@ The key features of this library are as follows: ...@@ -17,3 +26,11 @@ The key features of this library are as follows:
for proving compatibility of functions with respect to relations, and a solver for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations. `set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free. - It is entirely dependency- and axiom-free.
"""
depends: [
"coq" { (>= "8.10.2" & < "8.14~") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
opam-version: "1.2"
name: "coq-stdpp"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/iris/stdpp.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") }
]
# adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g
"eunify_test"
: string
The command has indeed failed with message:
No matching clauses for match.
((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) x y)
"eunify_test_evars"
: string
The command has indeed failed with message:
No matching clauses for match.
From stdpp Require Import tactics strings.
Unset Mangle Names.
Check "eunify_test".
Lemma eunify_test : x y, 0 < S x + y.
Proof.
intros x y.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
match goal with
| |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
end.
lia.
Qed.
Check "eunify_test_evars".
Lemma eunify_test_evars : x y, 0 < S x + y.
Proof.
eexists _, _.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds even if the goal contains evars *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
(* Let's try to use [eunify] to instantiate the first evar *)
match goal with
| |- 0 < ?x => eunify x (1 + _)
end.
(* And the other evar *)
match goal with
| |- 0 < ?x => eunify x 2
end.
lia.
Qed.
\ No newline at end of file
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps fin_map_dom.
Section map_disjoint. Section map_disjoint.
Context `{FinMap K M}. Context `{FinMap K M}.
...@@ -11,3 +11,14 @@ Section map_disjoint. ...@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None. m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed. Proof. intros. solve_map_disjoint. Qed.
End map_disjoint. End map_disjoint.
Section map_dom.
Context `{FinMapDom K M D}.
Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
{[i; j]} dom D (<[i:=x]> (<[j:=y]> ( : M A))).
Proof. set_solver. Qed.
Lemma set_solver_dom_disjoint {A} (X : D) : dom D ( : M A) ## X.
Proof. set_solver. Qed.
End map_dom.
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
From stdpp Require prelude strings list.
(** Check that we always get the [length] function on lists, not on strings. *)
Module test1.
Import stdpp.base.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.base.
Check length.
End test1.
Module test2.
Import stdpp.prelude.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test2.
Module test3.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test3.
Module test4.
Import stdpp.list.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.list.
Check length.
End test4.
From stdpp Require Import gmultiset.
Section test.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Lemma test_eq_1 x y X : {[+ x; y +]} X = {[+ y; x +]} X.
Proof. multiset_solver. Qed.
Lemma test_eq_2 x y z X Y :
{[+ z +]} X = {[+ y +]} Y
{[+ x; z +]} X = {[+ y; x +]} Y.
Proof. multiset_solver. Qed.
Lemma test_neq_1 x y X : {[+ x; y +]} X .
Proof. multiset_solver. Qed.
Lemma test_neq_2 x : {[+ x +]} @{gmultiset A} .
Proof. multiset_solver. Qed.
Lemma test_neq_3 X x : X = {[+ x +]} X @{gmultiset A} .
Proof. multiset_solver. Qed.
Lemma test_neq_4 x y : {[+ x +]} {[+ y +]} @{gmultiset A} x y.
Proof. multiset_solver. Qed.
Lemma test_neq_5 x y Y : y Y {[+ x +]} Y x y.
Proof. multiset_solver. Qed.
Lemma test_multiplicity_1 x X Y :
2 < multiplicity x X X Y 1 < multiplicity x Y.
Proof. multiset_solver. Qed.
Lemma test_multiplicity_2 x X :
2 < multiplicity x X {[+ x; x; x +]} X.
Proof. multiset_solver. Qed.
Lemma test_multiplicity_3 x X :
multiplicity x X < 3 {[+ x; x; x +]} X.
Proof. multiset_solver. Qed.
Lemma test_elem_of_1 x X : x X {[+ x +]} X.
Proof. multiset_solver. Qed.
Lemma test_elem_of_2 x X : x X {[+ x +]} X.
Proof. multiset_solver. Qed.
Lemma test_elem_of_3 x y X : x y x X y X {[+ x; y +]} X.
Proof. multiset_solver. Qed.
Lemma test_elem_of_4 x y X Y : x y x X y Y {[+ x; y +]} X Y.
Proof. multiset_solver. Qed.
Lemma test_elem_of_5 x y X Y : x y x X y Y {[+ x +]} (X Y) {[+ y +]}.
Proof. multiset_solver. Qed.
Lemma test_elem_of_6 x y X : {[+ x; y +]} X x X y X.
Proof. multiset_solver. Qed.
Lemma test_big_1 x1 x2 x3 x4 :
{[+ x1; x2; x3; x4; x4 +]} @{gmultiset A} {[+ x1; x1; x2; x3; x4; x4 +]}.
Proof. multiset_solver. Qed.
Lemma test_big_2 x1 x2 x3 x4 X :
2 multiplicity x4 X
{[+ x1; x2; x3; x4; x4 +]} @{gmultiset A} {[+ x1; x1; x2; x3 +]} X.
Proof. multiset_solver. Qed.
Lemma test_big_3 x1 x2 x3 x4 X :
4 multiplicity x4 X
{[+ x1; x2; x3; x4; x4 +]} {[+ x1; x2; x3; x4; x4 +]}
@{gmultiset A} {[+ x1; x1; x2; x3 +]} {[+ x1; x1; x2; x3 +]} X.
Proof. multiset_solver. Qed.
Lemma test_big_4 x1 x2 x3 x4 x5 x6 x7 x8 x9 :
{[+ x1; x2; x3; x4; x4 +]} {[+ x5; x6; x7; x8; x8; x9 +]}
@{gmultiset A}
{[+ x1; x1; x2; x3; x4; x4 +]} {[+ x5; x5; x6; x7; x9; x8; x8 +]}.
Proof. multiset_solver. Qed.
Lemma test_firstorder_1 (P : A Prop) x X :
P x ( y, y X P y) ( y, y {[+ x +]} X P y).
Proof. multiset_solver. Qed.
End test.
test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
: M (M nat)
test_3 =
{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
: M (M nat)
test_4 =
{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
: M (M nat)
test_op_2 =
{[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
: M (M nat)
test_op_3 =
{[10 := {[20 - 2 := [11]; 1 := [22]]};
20 := {[99 + length [1] := [1; 2; 3]]};
4 := {[4 := [4]]};
5 := {[5 := [5]]}]}
: M (M (list nat))
test_op_4 =
{[10 := {[20 - 2 := [11];
1 := [22];
3 := [23];
4 := [1; 2; 3; 4; 5; 6; 7; 8; 9]]};
20 := {[99 + length [1] := [1; 2; 3]]};
4 := {[4 := [4]]};
5 := {[5 := [5]]}]}
: M (M (list nat))
test_gmultiset_1 = {[+ 10 +]}
: gmultiset nat
test_gmultiset_2 = {[+ 10; 11 +]}
: gmultiset nat
test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
: gmultiset nat
test_gmultiset_4 =
{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
: gmultiset (gmultiset nat)
From stdpp Require Import base tactics fin_maps gmultiset.
(** Test parsing of variants of [(≡)] notation. *)
Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (@{A})} (x : A) :
x @{A} x (@{A}) x x (x .) x (. x) x
((x @{A} x)) ((@{A})) x x ((x .)) x ((. x)) x
( x @{A} x) ( x .) x
(x @{A} x ) (@{A} ) x x (. x ) x.
Proof. naive_solver. Qed.
(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
Section map_notations.
Context `{FinMap nat M}.
Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
Definition test_3 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
30 := {[ 30 := 3]} ]}.
Definition test_4 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
30 := {[ 30 := 3]}; 40 := {[ 40 := 4 ]} ]}.
Definition test_op_2 : M (M nat) := {[ 10 := {[pow 10 2 := 99]};
10 + 1 := {[ 10 - 100 := 42 * 1337 ]} ]}.
Definition test_op_3 : M (M (list nat)) := {[ 10 := {[ 20 - 2 := [11]; 1 := [22] ]};
20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}.
Definition test_op_4 : M (M (list nat)) :=
({[ 10 := {[ 20 - 2 := [11]; 1 := [22]; 3 := [23]; 4:=[1;2;3;4;5;6;7;8;9]]};
20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}).
Print test_2.
Print test_3.
Print test_4.
Print test_op_2.
Print test_op_3.
Print test_op_4.
End map_notations.
(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
Section multiset_notations.
Definition test_gmultiset_1 : gmultiset nat := {[+ 10 +]}.
Definition test_gmultiset_2 : gmultiset nat := {[+ 10; 11 +]}.
Definition test_gmultiset_3 : gmultiset nat := {[+ 10; 11; 2 - 2 +]}.
Definition test_gmultiset_4 : gmultiset (gmultiset nat) :=
{[+ {[+ 10 +]}; ; {[+ 2 - 2; 10 +]} +]}.
Print test_gmultiset_1.
Print test_gmultiset_2.
Print test_gmultiset_3.
Print test_gmultiset_4.
End multiset_notations.
\ No newline at end of file
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
From stdpp Require base numbers prelude.
(** Check that we always get the [le] and [lt] functions on [nat]. *)
Module test1.
Import stdpp.base.
Check le.
Check lt.
End test1.
Module test2.
Import stdpp.prelude.
Check le.
Check lt.
End test2.
Module test3.
Import stdpp.numbers.
Check le.
Check lt.
End test3.
Module test4.
Import stdpp.list.
Check le.
Check lt.
End test4.
From stdpp Require Import pretty.
Section N.
Local Open Scope N_scope.
Lemma pretty_N_0 : pretty 0 = "0".
Proof. reflexivity. Qed.
Lemma pretty_N_1 : pretty 1 = "1".
Proof. reflexivity. Qed.
Lemma pretty_N_9 : pretty 9 = "9".
Proof. reflexivity. Qed.
Lemma pretty_N_10 : pretty 10 = "10".
Proof. reflexivity. Qed.
Lemma pretty_N_100 : pretty 100 = "100".
Proof. reflexivity. Qed.
Lemma pretty_N_123456789 : pretty 123456789 = "123456789".
Proof. reflexivity. Qed.
End N.
Section nat.
Local Open Scope nat_scope.
Lemma pretty_nat_0 : pretty 0 = "0".
Proof. reflexivity. Qed.
Lemma pretty_nat_1 : pretty 1 = "1".
Proof. reflexivity. Qed.
Lemma pretty_nat_9 : pretty 9 = "9".
Proof. reflexivity. Qed.
Lemma pretty_nat_10 : pretty 10 = "10".
Proof. reflexivity. Qed.
Lemma pretty_nat_100 : pretty 100 = "100".
Proof. reflexivity. Qed.
Lemma pretty_nat_1234 : pretty 1234 = "1234".
Proof. reflexivity. Qed.
End nat.
Section Z.
Local Open Scope Z_scope.
Lemma pretty_Z_0 : pretty 0 = "0".
Proof. reflexivity. Qed.
Lemma pretty_Z_1 : pretty 1 = "1".
Proof. reflexivity. Qed.
Lemma pretty_Z_9 : pretty 9 = "9".
Proof. reflexivity. Qed.
Lemma pretty_Z_10 : pretty 10 = "10".
Proof. reflexivity. Qed.
Lemma pretty_Z_100 : pretty 100 = "100".
Proof. reflexivity. Qed.
Lemma pretty_Z_123456789 : pretty 123456789 = "123456789".
Proof. reflexivity. Qed.
Lemma pretty_Z_opp_1 : pretty (-1) = "-1".
Proof. reflexivity. Qed.
Lemma pretty_Z_opp_9 : pretty (-9) = "-9".
Proof. reflexivity. Qed.
Lemma pretty_Z_opp_10 : pretty (-10) = "-10".
Proof. reflexivity. Qed.
Lemma pretty_Z_opp_100 : pretty (-100) = "-100".
Proof. reflexivity. Qed.
Lemma pretty_Z_opp_123456789 : pretty (-123456789) = "-123456789".
Proof. reflexivity. Qed.
End Z.
\ No newline at end of file
From stdpp Require Import sets.
Lemma foo `{Set_ A C} (x : A) (X Y : C) : x X Y x X.
Proof. intros Hx. set_unfold in Hx. tauto. Qed.
From stdpp Require Import namespaces strings.
Lemma test1 (N1 N2 : namespace) :
N1 ## N2 N1 @{coPset} N2.
Proof. solve_ndisj. Qed.
Lemma test2 (N1 N2 : namespace) :
N1 ## N2 N1.@"x" @{coPset} N1.@"y" N2.
Proof. solve_ndisj. Qed.
Lemma test3 (N : namespace) :
N @{coPset} N.@"x".
Proof. solve_ndisj. Qed.
Lemma test4 (N : namespace) :
N @{coPset} N.@"x" N.@"y".
Proof. solve_ndisj. Qed.
Lemma test5 (N1 N2 : namespace) :
N1 N2 @{coPset} N1.@"x" N2 N1.@"y".
Proof. solve_ndisj. Qed.
...@@ -9,16 +9,16 @@ Section tests. ...@@ -9,16 +9,16 @@ Section tests.
!Proper (() ==> () ==> ()) baz}. !Proper (() ==> () ==> ()) baz}.
Definition test1 (x : A) := baz (bar (foo x)) x. Definition test1 (x : A) := baz (bar (foo x)) x.
Global Instance : Proper (() ==> ()) test1. Goal Proper (() ==> ()) test1.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Definition test2 (b : bool) (x : A) := Definition test2 (b : bool) (x : A) :=
if b then bar (foo x) else bar x. if b then bar (foo x) else bar x.
Global Instance : b, Proper (() ==> ()) (test2 b). Goal b, Proper (() ==> ()) (test2 b).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Definition test3 (f : nat A) := Definition test3 (f : nat A) :=
baz (bar (f 0)) (f 2). baz (bar (f 0)) (f 2).
Global Instance : Proper (pointwise_relation nat () ==> ()) test3. Goal Proper (pointwise_relation nat () ==> ()) test3.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
End tests. End tests.
The command has indeed failed with message:
Failed to progress.
The command has indeed failed with message:
Failed to progress.
The command has indeed failed with message:
Failed to progress.
From stdpp Require Import tactics.
Goal P1 P2 P3 P4 (P: Prop),
P1 (Is_true (P2 || P3)) P4
(P1 P)
(P2 P)
(P3 P)
(P4 P)
P.
Proof.
intros * HH X1 X2 X3 X4.
destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
Qed.
Goal P1 P2 P3 P4 (P: Prop),
P1 P2
P3 P4
(P1 P3 P)
(P1 P4 P)