...
 
Commits (257)
# 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
......
...@@ -18,61 +18,46 @@ variables: ...@@ -18,61 +18,46 @@ variables:
paths: paths:
- opamroot/ - opamroot/
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.8.11.dev:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-base-compiler.4.07.0" OPAM_PINS: "coq version 8.11.dev"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1" CI_COQCHK: "1"
build-coq.8.9.0: build-coq.8.11.1:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.9.0" OPAM_PINS: "coq version 8.11.1"
OPAM_PKG: "coq-stdpp" OPAM_PKG: "coq-stdpp"
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.10.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.2" OPAM_PINS: "coq version 8.10.2"
build-coq.8.8.1: build-coq.8.9.1:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.1" OPAM_PINS: "coq version 8.9.1"
build-coq.8.8.0: build-coq.8.8.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.0" OPAM_PINS: "coq version 8.8.2"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
build-coq.8.7.2: build-coq.8.7.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.7.2" 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,168 @@ API-breaking change is listed. ...@@ -3,20 +3,168 @@ API-breaking change is listed.
## std++ master ## std++ master
Numerous functions and theorems have been renamed. - Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
- Consistently use `set` instead of `collection`. ## std++ 1.3 (released 2020-03-18)
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection`
is called `SemiSet`, and `FinCollection` is called `FinSet`, and Coq 8.11 is supported by this release.
`CollectionMonad` is called `MonadSet`.
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`, This release of std++ received contributions by Amin Timany, Armaël Guéneau,
respectively. Dan Frumin, David Swasey, Jacques-Henri Jourdan, Michael Sammler, Paolo G.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise Giarrusso, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Simon Friis Vindum,
`bset` into `boolset`. Tej Chajed, and William Mansky
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map`
instead of the former `map_of_list`. Noteworthy additions and changes:
The following `sed` script should get you a long way: - 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`
- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
`singletonM` and to avoid overlap with `sets.singleton_proper`.
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).
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 BSD
license, included below. license, 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.
...@@ -9,7 +9,7 @@ all: Makefile.coq ...@@ -9,7 +9,7 @@ all: Makefile.coq
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 find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq rm -f Makefile.coq .lia.cache
.PHONY: clean .PHONY: clean
# Create Coq Makefile. # Create Coq Makefile.
...@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony ...@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony
@# 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 build-dep package."
if opam --version | grep "^1\." -q; then \ @opam install $(OPAMFLAGS) build-dep/
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) 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
Makefile: ; Makefile: ;
......
...@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo) ...@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo)
.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_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\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)
......
...@@ -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.7.2 / 8.8.2 / 8.9.1 / 8.10.2 / 8.11.1
## 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 # "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope -arg -w -arg -undeclared-scope
theories/base.v theories/base.v
theories/tactics.v theories/tactics.v
theories/option.v theories/option.v
...@@ -33,6 +34,7 @@ theories/numbers.v ...@@ -33,6 +34,7 @@ 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
...@@ -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++.
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
opam-version: "1.2" opam-version: "2.0"
name: "coq-stdpp" name: "coq-stdpp"
maintainer: "Ralf Jung <jung@mpi-sws.org>" maintainer: "Ralf Jung <jung@mpi-sws.org>"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung" authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
license: "BSD" license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/iris/stdpp.git" homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
build: [make "-j%{jobs}%"] bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
install: [make "install"] dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
synopsis: "std++ is an extended \"Standard Library\" for Coq"
description: """
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
"""
depends: [ depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") } "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9.1" & < "8.12~") | (= "dev") }
] ]
build: [make "-j%{jobs}%"]
install: [make "install"]
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.
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.
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 forall 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 forall P1 P2 P3 P4 (P: Prop),
P1 P2
P3 P4
(P1 P3 P)
(P1 P4 P)
(P2 P3 P)
(P2 P4 P)
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
id (P1 P2)
id (P3 P4)
(P1 P3 P)
(P1 P4 P)
(P2 P3 P)
(P2 P4 P)
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
Fail progress destruct_or?.
Fail progress destruct_or!.
destruct_or! HH1; destruct_or! HH2;
[ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4,
P1 (Is_true (P2 && P3)) P4
P1 P2 P3.
Proof.
intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
destruct_and?. Fail destruct_and!. assumption.
Qed.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems (** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, sets, and various other data abstract interfaces for ordered structures, sets, and various other data
...@@ -48,7 +46,7 @@ Arguments unseal {_ _} _ : assert. ...@@ -48,7 +46,7 @@ Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert. Arguments seal_eq {_ _} _ : assert.
(** * Non-backtracking type classes *) (** * Non-backtracking type classes *)
(** The type class [NoBackTrack P] can be used to establish [P] without ever (** The type class [TCNoBackTrack P] can be used to establish [P] without ever
backtracking on the instance of [P] that has been found. Backtracking may backtracking on the instance of [P] that has been found. Backtracking may
normally happen when [P] contains evars that could be instanciated in different normally happen when [P] contains evars that could be instanciated in different
ways depending on which instance is picked, and type class search somewhere else ways depending on which instance is picked, and type class search somewhere else
...@@ -60,12 +58,12 @@ issue #6714. ...@@ -60,12 +58,12 @@ issue #6714.
See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
of this type class. *) of this type class. *)
Class NoBackTrack (P : Prop) := { no_backtrack : P }. Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances. Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
(* A conditional at the type class level. Note that [TCIf P Q R] is not the same (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
establish [R], i.e. does not have the behavior of a conditional. Furthermore, establish [Q], i.e. does not have the behavior of a conditional. Furthermore,
note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
would not be able to prove the negation of [P]. *) would not be able to prove the negation of [P]. *)
Inductive TCIf (P Q R : Prop) : Prop := Inductive TCIf (P Q R : Prop) : Prop :=
...@@ -106,10 +104,12 @@ Inductive TCOr (P1 P2 : Prop) : Prop := ...@@ -106,10 +104,12 @@ Inductive TCOr (P1 P2 : Prop) : Prop :=
Existing Class TCOr. Existing Class TCOr.
Existing Instance TCOr_l | 9. Existing Instance TCOr_l | 9.
Existing Instance TCOr_r | 10. Existing Instance TCOr_r | 10.
Hint Mode TCOr ! ! : typeclass_instances.
Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 P2 TCAnd P1 P2. Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 P2 TCAnd P1 P2.
Existing Class TCAnd. Existing Class TCAnd.
Existing Instance TCAnd_intro. Existing Instance TCAnd_intro.
Hint Mode TCAnd ! ! : typeclass_instances.
Inductive TCTrue : Prop := TCTrue_intro : TCTrue. Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
Existing Class TCTrue. Existing Class TCTrue.
...@@ -121,7 +121,11 @@ Inductive TCForall {A} (P : A → Prop) : list A → Prop := ...@@ -121,7 +121,11 @@ Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
Existing Class TCForall. Existing Class TCForall.
Existing Instance TCForall_nil. Existing Instance TCForall_nil.
Existing Instance TCForall_cons. Existing Instance TCForall_cons.
Hint Mode TCForall ! ! ! : typeclass_instances.
(** The class [TCForall2 P l k] is commonly used to transform an input list [l]
into an output list [k], or the converse. Therefore there are two modes, either
[l] input and [k] output, or [k] input and [l] input. *)
Inductive TCForall2 {A B} (P : A B Prop) : list A list B Prop := Inductive TCForall2 {A B} (P : A B Prop) : list A list B Prop :=
| TCForall2_nil : TCForall2 P [] [] | TCForall2_nil : TCForall2 P [] []
| TCForall2_cons x y xs ys : | TCForall2_cons x y xs ys :
...@@ -129,6 +133,8 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop := ...@@ -129,6 +133,8 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
Existing Class TCForall2. Existing Class TCForall2.
Existing Instance TCForall2_nil. Existing Instance TCForall2_nil.
Existing Instance TCForall2_cons. Existing Instance TCForall2_cons.
Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
Inductive TCElemOf {A} (x : A) : list A Prop := Inductive TCElemOf {A} (x : A) : list A Prop :=
| TCElemOf_here xs : TCElemOf x (x :: xs) | TCElemOf_here xs : TCElemOf x (x :: xs)
...@@ -136,15 +142,26 @@ Inductive TCElemOf {A} (x : A) : list A → Prop := ...@@ -136,15 +142,26 @@ Inductive TCElemOf {A} (x : A) : list A → Prop :=
Existing Class TCElemOf. Existing Class TCElemOf.
Existing Instance TCElemOf_here. Existing Instance TCElemOf_here.
Existing Instance TCElemOf_further. Existing Instance TCElemOf_further.
Hint Mode TCElemOf ! ! ! : typeclass_instances.
(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
[TCEq] can also be used to unify evars. This is harmless: since the only
instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x. Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Existing Class TCEq. Existing Class TCEq.
Existing Instance TCEq_refl. Existing Instance TCEq_refl.
Hint Mode TCEq ! - - : typeclass_instances.
Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 x1 = x2.
Proof. split; destruct 1; reflexivity. Qed.
Inductive TCDiag {A} (C : A Prop) : A A Prop := Inductive TCDiag {A} (C : A Prop) : A A Prop :=
| TCDiag_diag x : C x TCDiag C x x. | TCDiag_diag x : C x TCDiag C x x.
Existing Class TCDiag. Existing Class TCDiag.
Existing Instance TCDiag_diag. Existing Instance TCDiag_diag.
Hint Mode TCDiag ! ! ! - : typeclass_instances.
Hint Mode TCDiag ! ! - ! : typeclass_instances.
(** Given a proposition [P] that is a type class, [tc_to_bool P] will return (** Given a proposition [P] that is a type class, [tc_to_bool P] will return
[true] iff there is an instance of [P]. It is often useful in Ltac programming, [true] iff there is an instance of [P]. It is often useful in Ltac programming,
...@@ -167,11 +184,11 @@ Notation "'False'" := False (format "False") : type_scope. ...@@ -167,11 +184,11 @@ Notation "'False'" := False (format "False") : type_scope.
(** * Equality *) (** * Equality *)
(** Introduce some Haskell style like notations. *) (** Introduce some Haskell style like notations. *)
Notation "(=)" := eq (only parsing) : stdpp_scope. Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "( x =)" := (eq x) (only parsing) : stdpp_scope. Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : stdpp_scope. Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
Notation "(≠)" := (λ x y, x y) (only parsing) : stdpp_scope. Notation "(≠)" := (λ x y, x y) (only parsing) : stdpp_scope.
Notation "( x ≠)" := (λ y, x y) (only parsing) : stdpp_scope. Notation "( x ≠.)" := (λ y, x y) (only parsing) : stdpp_scope.
Notation "(≠ x )" := (λ y, y x) (only parsing) : stdpp_scope. Notation "(.≠ x )" := (λ y, y x) (only parsing) : stdpp_scope.
Infix "=@{ A }" := (@eq A) Infix "=@{ A }" := (@eq A)
(at level 70, only parsing, no associativity) : stdpp_scope. (at level 70, only parsing, no associativity) : stdpp_scope.
...@@ -199,12 +216,12 @@ Infix "≡@{ A }" := (@equiv A _) ...@@ -199,12 +216,12 @@ Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope. (at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope. Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope. Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(≡ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.≡ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "(≢)" := (λ X Y, ¬X Y) (only parsing) : stdpp_scope. Notation "(≢)" := (λ X Y, ¬X Y) (only parsing) : stdpp_scope.
Notation "X ≢ Y":= (¬X Y) (at level 70, no associativity) : stdpp_scope. Notation "X ≢ Y":= (¬X Y) (at level 70, no associativity) : stdpp_scope.
Notation "( X ≢)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ≢.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(≢ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.≢ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope. Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope. Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
...@@ -295,8 +312,8 @@ Hint Mode ProofIrrel ! : typeclass_instances. ...@@ -295,8 +312,8 @@ Hint Mode ProofIrrel ! : typeclass_instances.
(** ** Common properties *) (** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical (** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it properties in a generic way. For example, for injectivity of [(k ++.)] it
allows us to write [inj (k ++)] instead of [app_inv_head k]. *) allows us to write [inj (k ++.)] instead of [app_inv_head k]. *)
Class Inj {A B} (R : relation A) (S : relation B) (f : A B) : Prop := Class Inj {A B} (R : relation A) (S : relation B) (f : A B) : Prop :=
inj x y : S (f x) (f y) R x y. inj x y : S (f x) (f y) R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
...@@ -328,6 +345,11 @@ Class Trichotomy {A} (R : relation A) := ...@@ -328,6 +345,11 @@ Class Trichotomy {A} (R : relation A) :=
Class TrichotomyT {A} (R : relation A) := Class TrichotomyT {A} (R : relation A) :=
trichotomyT x y : {R x y} + {x = y} + {R y x}. trichotomyT x y : {R x y} + {x = y} + {R y x}.
Notation Involutive R f := (Cancel R f f).
Lemma involutive {A} {R : relation A} (f : A A) `{Involutive R f} x :
R (f (f x)) x.
Proof. auto. Qed.
Arguments irreflexivity {_} _ {_} _ _ : assert. Arguments irreflexivity {_} _ {_} _ _ : assert.
Arguments inj {_ _ _ _} _ {_} _ _ _ : assert. Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert. Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
...@@ -408,17 +430,19 @@ Class TotalOrder {A} (R : relation A) : Prop := { ...@@ -408,17 +430,19 @@ Class TotalOrder {A} (R : relation A) : Prop := {
}. }.
(** * Logic *) (** * Logic *)
Instance prop_inhabited : Inhabited Prop := populate True.
Notation "(∧)" := and (only parsing) : stdpp_scope. Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope. Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.∧ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(∨)" := or (only parsing) : stdpp_scope. Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope. Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.∨ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(↔)" := iff (only parsing) : stdpp_scope. Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope. Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.↔ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity : core. Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core. Hint Extern 0 (_ _) => symmetry; assumption : core.
...@@ -483,18 +507,18 @@ Proof. unfold impl. red; intuition. Qed. ...@@ -483,18 +507,18 @@ Proof. unfold impl. red; intuition. Qed.
(** * Common data types *) (** * Common data types *)
(** ** Functions *) (** ** Functions *)
Notation "(→)" := (λ A B, A B) (only parsing) : stdpp_scope. Notation "(→)" := (λ A B, A B) (only parsing) : stdpp_scope.
Notation "( A →)" := (λ B, A B) (only parsing) : stdpp_scope. Notation "( A →.)" := (λ B, A B) (only parsing) : stdpp_scope.
Notation "(→ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.→ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "t $ r" := (t r) Notation "t $ r" := (t r)
(at level 65, right associativity, only parsing) : stdpp_scope. (at level 65, right associativity, only parsing) : stdpp_scope.
Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope. Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
Notation "($ x )" := (λ f, f x) (only parsing) : stdpp_scope. Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope.
Infix "∘" := compose : stdpp_scope. Infix "∘" := compose : stdpp_scope.
Notation "(∘)" := compose (only parsing) : stdpp_scope. Notation "(∘)" := compose (only parsing) : stdpp_scope.
Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope. Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope. Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A B) := Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A B) :=
populate (λ _, inhabitant). populate (λ _, inhabitant).
...@@ -586,9 +610,16 @@ Instance unit_leibniz : LeibnizEquiv unit. ...@@ -586,9 +610,16 @@ Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed. Proof. intros [] []; reflexivity. Qed.
Instance unit_inhabited: Inhabited unit := populate (). Instance unit_inhabited: Inhabited unit := populate ().
(** ** Empty *)
Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
Instance Empty_set_equivalence : Equivalence (@{Empty_set}).
Proof. repeat split. Qed.
Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Proof. intros [] []; reflexivity. Qed.
(** ** Products *) (** ** Products *)
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope. Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope. Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1"). Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2"). Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
...@@ -753,6 +784,10 @@ Section sig_map. ...@@ -753,6 +784,10 @@ Section sig_map.
End sig_map. End sig_map.
Arguments sig_map _ _ _ _ _ _ !_ / : assert. Arguments sig_map _ _ _ _ _ _ !_ / : assert.
Definition proj1_ex {P : Prop} {Q : P Prop} (p : x, Q x) : P :=
let '(ex_intro _ x _) := p in x.
Definition proj2_ex {P : Prop} {Q : P Prop} (p : x, Q x) : Q (proj1_ex p) :=
let '(ex_intro _ x H) := p in H.
(** * Operations on sets *) (** * Operations on sets *)
(** We define operational type classes for the traditional operations and (** We define operational type classes for the traditional operations and
...@@ -770,8 +805,8 @@ Hint Mode Union ! : typeclass_instances. ...@@ -770,8 +805,8 @@ Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2 := {}. Instance: Params (@union) 2 := {}.
Infix "∪" := union (at level 50, left associativity) : stdpp_scope. Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope. Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope. Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope. Notation "(.∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
Infix "∪*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope. Infix "∪*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope.
Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope. Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∪**" := (zip_with (zip_with ())) Infix "∪**" := (zip_with (zip_with ()))
...@@ -788,24 +823,24 @@ Hint Mode DisjUnion ! : typeclass_instances. ...@@ -788,24 +823,24 @@ Hint Mode DisjUnion ! : typeclass_instances.
Instance: Params (@disj_union) 2 := {}. Instance: Params (@disj_union) 2 := {}.
Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope. Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
Notation "(⊎)" := disj_union (only parsing) : stdpp_scope. Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
Notation "( x ⊎)" := (disj_union x) (only parsing) : stdpp_scope. Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope. Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
Class Intersection A := intersection: A A A. Class Intersection A := intersection: A A A.
Hint Mode Intersection ! : typeclass_instances. Hint Mode Intersection ! : typeclass_instances.
Instance: Params (@intersection) 2 := {}. Instance: Params (@intersection) 2 := {}.
Infix "∩" := intersection (at level 40) : stdpp_scope. Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope. Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope. Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope. Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class Difference A := difference: A A A. Class Difference A := difference: A A A.
Hint Mode Difference ! : typeclass_instances. Hint Mode Difference ! : typeclass_instances.
Instance: Params (@difference) 2 := {}. Instance: Params (@difference) 2 := {}.
Infix "∖" := difference (at level 40, left associativity) : stdpp_scope. Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
Notation "(∖)" := difference (only parsing) : stdpp_scope. Notation "(∖)" := difference (only parsing) : stdpp_scope.
Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope. Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope. Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope. Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope.
Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope. Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∖**" := (zip_with (zip_with ())) Infix "∖**" := (zip_with (zip_with ()))
...@@ -830,12 +865,12 @@ Hint Mode SubsetEq ! : typeclass_instances. ...@@ -830,12 +865,12 @@ Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2 := {}. Instance: Params (@subseteq) 2 := {}.
Infix "⊆" := subseteq (at level 70) : stdpp_scope. Infix "⊆" := subseteq (at level 70) : stdpp_scope.
Notation "(⊆)" := subseteq (only parsing) : stdpp_scope. Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope. Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
Notation "(⊆ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊆ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "X ⊈ Y" := (¬X Y) (at level 70) : stdpp_scope. Notation "X ⊈ Y" := (¬X Y) (at level 70) : stdpp_scope.
Notation "(⊈)" := (λ X Y, X Y) (only parsing) : stdpp_scope. Notation "(⊈)" := (λ X Y, X Y) (only parsing) : stdpp_scope.
Notation "( X ⊈)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ⊈.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope. Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope. Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
...@@ -854,12 +889,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core. ...@@ -854,12 +889,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core.
Infix "⊂" := (strict ()) (at level 70) : stdpp_scope. Infix "⊂" := (strict ()) (at level 70) : stdpp_scope.
Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope. Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope.
Notation "( X ⊂)" := (strict () X) (only parsing) : stdpp_scope. Notation "( X ⊂.)" := (strict () X) (only parsing) : stdpp_scope.
Notation "(⊂ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊂ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "X ⊄ Y" := (¬X Y) (at level 70) : stdpp_scope. Notation "X ⊄ Y" := (¬X Y) (at level 70) : stdpp_scope.
Notation "(⊄)" := (λ X Y, X Y) (only parsing) : stdpp_scope. Notation "(⊄)" := (λ X Y, X Y) (only parsing) : stdpp_scope.
Notation "( X ⊄)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ⊄.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope. Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope. Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.
...@@ -887,16 +922,19 @@ Hint Mode ElemOf - ! : typeclass_instances. ...@@ -887,16 +922,19 @@ Hint Mode ElemOf - ! : typeclass_instances.
Instance: Params (@elem_of) 3 := {}. Instance: Params (@elem_of) 3 := {}.
Infix "∈" := elem_of (at level 70) : stdpp_scope. Infix "∈" := elem_of (at level 70) : stdpp_scope.
Notation "(∈)" := elem_of (only parsing) : stdpp_scope. Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope. Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope. Notation "(.∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
Notation "x ∉ X" := (¬x X) (at level 80) : stdpp_scope. Notation "x ∉ X" := (¬x X) (at level 80) : stdpp_scope.
Notation "(∉)" := (λ x X, x X) (only parsing) : stdpp_scope. Notation "(∉)" := (λ x X, x X) (only parsing) : stdpp_scope.
Notation "( x ∉)" := (λ X, x X) (only parsing) : stdpp_scope. Notation "( x ∉.)" := (λ X, x X) (only parsing) : stdpp_scope.
Notation "(∉ X )" := (λ x, x X) (only parsing) : stdpp_scope. Notation "(.∉ X )" := (λ x, x X) (only parsing) : stdpp_scope.
Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope. Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope. Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
Notation "x ∉@{ B } X" := (¬x @{B} X) (at level 80, only parsing) : stdpp_scope.
Notation "(∉@{ B } )" := (λ x X, x @{B} X) (only parsing) : stdpp_scope.
Class Disjoint A := disjoint : A A Prop. Class Disjoint A := disjoint : A A Prop.
Hint Mode Disjoint ! : typeclass_instances. Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2 := {}. Instance: Params (@disjoint) 2 := {}.
...@@ -965,7 +1003,7 @@ Hint Mode UpClose - ! : typeclass_instances. ...@@ -965,7 +1003,7 @@ Hint Mode UpClose - ! : typeclass_instances.
Notation "↑ x" := (up_close x) (at level 20, format "↑ x"). Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
(** * Monadic operations *) (** * Monadic operations *)
(** We define operational type classes for the monadic operations bind, join (** We define operational type classes for the monadic operations bind, join
and fmap. We use these type classes merely for convenient overloading of and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *) class with the monad laws). *)
...@@ -986,8 +1024,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert. ...@@ -986,8 +1024,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4 := {}. Instance: Params (@omap) 4 := {}.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope. Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope. Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope. Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope. Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) Notation "x ← y ; z" := (y = (λ x : _, z))
...@@ -1024,10 +1062,21 @@ Hint Mode Lookup - - ! : typeclass_instances. ...@@ -1024,10 +1062,21 @@ Hint Mode Lookup - - ! : typeclass_instances.
Instance: Params (@lookup) 4 := {}. Instance: Params (@lookup) 4 := {}.
Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope. Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope. Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope. Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope. Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert. Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [lookup_total] should be the total over-approximation
of the partial [lookup] function. *)
Class LookupTotal (K A M : Type) := lookup_total : K M A.
Hint Mode LookupTotal - - ! : typeclass_instances.
Instance: Params (@lookup_total) 4 := {}.
Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope.
Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *) (** The singleton map *)
Class SingletonM K A M := singletonM: K A M. Class SingletonM K A M := singletonM: K A M.
Hint Mode SingletonM - - ! : typeclass_instances. Hint Mode SingletonM - - ! : typeclass_instances.
...@@ -1060,7 +1109,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert. ...@@ -1060,7 +1109,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
(** The function [partial_alter f k m] should update the value at key [k] using the (** The function [partial_alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None] function [f], which is called with the original value at key [k] or [None]
if [k] is not a member of [m]. The value at [k] should be deleted if [f] if [k] is not a member of [m]. The value at [k] should be deleted if [f]
yields [None]. *) yields [None]. *)
Class PartialAlter (K A M : Type) := Class PartialAlter (K A M : Type) :=
partial_alter: (option A option A) K M M. partial_alter: (option A option A) K M M.
...@@ -1126,25 +1175,76 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a) ...@@ -1126,25 +1175,76 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert. Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
(** * Notations for lattices. *)
(** SqSubsetEq registers the "canonical" partial order for a type, and is used
for the \sqsubseteq symbol. *)
Class SqSubsetEq A := sqsubseteq: relation A.
Hint Mode SqSubsetEq ! : typeclass_instances.
Instance: Params (@sqsubseteq) 2 := {}.
Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (@{A}) := {}.
Hint Extern 0 (_ _) => reflexivity : core.
Class Meet A := meet: A A A.
Hint Mode Meet ! : typeclass_instances.
Instance: Params (@meet) 2 := {}.
Infix "⊓" := meet (at level 40) : stdpp_scope.
Notation "(⊓)" := meet (only parsing) : stdpp_scope.
Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
Class Join A := join: A A A.
Hint Mode Join ! : typeclass_instances.
Instance: Params (@join) 2 := {}.
Infix "⊔" := join (at level 50) : stdpp_scope.
Notation "(⊔)" := join (only parsing) : stdpp_scope.
Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
Class Top A := top : A.
Hint Mode Top ! : typeclass_instances.
Notation "⊤" := top (format "⊤") : stdpp_scope.
Class Bottom A := bottom : A.
Hint Mode Bottom ! : typeclass_instances.
Notation "⊥" := bottom (format "⊥") : stdpp_scope.
(** * Axiomatization of sets *) (** * Axiomatization of sets *)
(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with (** The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets of
elements of type [A]. The first class, [SemiSet] does not include intersection type [C] with elements of type [A]. The first class, [SemiSet] does not include
and difference. It is useful for the case of lists, where decidable equality intersection and difference. It is useful for the case of lists, where decidable
is needed to implement intersection and difference, but not union. equality is needed to implement intersection and difference, but not union.
Note that we cannot use the name [Set] since that is a reserved keyword. Hence Note that we cannot use the name [Set] since that is a reserved keyword. Hence
we use [Set_]. *) we use [Set_]. *)
Class SemiSet A C `{ElemOf A C, Class SemiSet A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := { Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ; not_elem_of_empty (x : A) : x @{C} ; (* We prove
elem_of_singleton (x y : A) : x {[ y ]} x = y; [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
elem_of_union X Y (x : A) : x X Y x X x Y rewriting. *)
elem_of_singleton (x y : A) : x @{C} {[ y ]} x = y;
elem_of_union (X Y : C) (x : A) : x X Y x X x Y
}. }.
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C, Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := { Union C, Intersection C, Difference C} : Prop := {
set_semi_set :>> SemiSet A C; set_semi_set :> SemiSet A C;
elem_of_intersection X Y (x : A) : x X Y x X x Y; elem_of_intersection (X Y : C) (x : A) : x X Y x X x Y;
elem_of_difference X Y (x : A) : x X Y x X x Y elem_of_difference (X Y : C) (x : A) : x X Y x X x Y
}.
Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
top_set_set :> Set_ A C;
elem_of_top' (x : A) : x @{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
in [sets.v], which is more convenient for rewriting. *)
}. }.
(** We axiomative a finite set as a set whose elements can be (** We axiomative a finite set as a set whose elements can be
...@@ -1182,9 +1282,9 @@ Qed. ...@@ -1182,9 +1282,9 @@ Qed.
anyway so as to avoid cycles in type class search. *) anyway so as to avoid cycles in type class search. *)
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C, Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := { Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_set_set :>> Set_ A C; fin_set_set :> Set_ A C;
elem_of_elements X x : x elements X x X; elem_of_elements (X : C) x : x elements X x X;
NoDup_elements X : NoDup (elements X) NoDup_elements (X : C) : NoDup (elements X)
}. }.
Class Size C := size: C nat. Class Size C := size: C nat.