...
 
Commits (198)
# Enable syntax highlighting.
*.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......
......@@ -18,61 +18,46 @@ variables:
paths:
- opamroot/
only:
- master
- /^ci/
- master@iris/stdpp
- /^ci/@iris/stdpp
except:
- triggers
- schedules
- api
## Build jobs
build-coq.dev:
build-coq.8.11.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
OPAM_PINS: "coq version 8.11.dev"
CI_COQCHK: "1"
build-coq.8.9.0:
build-coq.8.11.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PINS: "coq version 8.11.0"
OPAM_PKG: "coq-stdpp"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
build-coq.8.10.2:
<<: *template
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
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
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
OPAM_PINS: "coq version 8.8.2"
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,107 @@ API-breaking change is listed.
## std++ master
Numerous functions and theorems have been renamed.
- Consistently use `set` instead of `collection`.
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection`
is called `SemiSet`, and `FinCollection` is called `FinSet`, and
`CollectionMonad` is called `MonadSet`.
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`,
respectively.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise
`bset` into `boolset`.
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map`
instead of the former `map_of_list`.
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.
- Add `Countable` instance for `vec`.
## 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 '
......
......@@ -9,7 +9,7 @@ all: Makefile.coq
clean: Makefile.coq
+@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
rm -f Makefile.coq
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
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
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
......@@ -45,11 +45,11 @@ Notably:
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.0
## 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:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -79,3 +79,9 @@ your account. Then you can fork the
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
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
# "Declare Scope" does not exist yet in 8.9
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
theories/base.v
theories/tactics.v
theories/option.v
......@@ -33,6 +34,7 @@ theories/numbers.v
theories/nmap.v
theories/zmap.v
theories/coPset.v
theories/coGset.v
theories/lexico.v
theories/propset.v
theories/decidable.v
......@@ -44,3 +46,4 @@ theories/infinite.v
theories/nat_cancel.v
theories/namespaces.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"
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"]
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: "This project contains an extended \"Standard Library\" for Coq called coq-std++"
description: """
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.
"""
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.
Context `{FinMap K M}.
......@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed.
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 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.
......@@ -48,7 +48,7 @@ Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
(** * 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
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
......@@ -60,12 +60,12 @@ issue #6714.
See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
of this type class. *)
Class NoBackTrack (P : Prop) := { no_backtrack : P }.
Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
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
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
would not be able to prove the negation of [P]. *)
Inductive TCIf (P Q R : Prop) : Prop :=
......@@ -167,11 +167,11 @@ Notation "'False'" := False (format "False") : type_scope.
(** * Equality *)
(** Introduce some Haskell style like notations. *)
Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "( x =)" := (eq x) (only parsing) : stdpp_scope.
Notation "(= x )" := (λ y, eq y 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, 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, x y) (only parsing) : stdpp_scope.
Notation "(.≠ x )" := (λ y, y x) (only parsing) : stdpp_scope.
Infix "=@{ A }" := (@eq A)
(at level 70, only parsing, no associativity) : stdpp_scope.
......@@ -199,12 +199,12 @@ Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(≡ X )" := (λ Y, Y 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, ¬X Y) (only parsing) : 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, Y X) (only parsing) : stdpp_scope.
Notation "( X ≢.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(.≢ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
......@@ -295,8 +295,8 @@ Hint Mode ProofIrrel ! : typeclass_instances.
(** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it
allows us to write [inj (k ++)] instead of [app_inv_head k]. *)
properties in a generic way. For example, for injectivity of [(k ++.)] it
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 :=
inj x y : S (f x) (f y) R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
......@@ -328,6 +328,11 @@ Class Trichotomy {A} (R : relation A) :=
Class TrichotomyT {A} (R : relation A) :=
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 inj {_ _ _ _} _ {_} _ _ _ : assert.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
......@@ -408,17 +413,19 @@ Class TotalOrder {A} (R : relation A) : Prop := {
}.
(** * Logic *)
Instance prop_inhabited : Inhabited Prop := populate True.
Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
Notation "(.∧ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope.
Notation "(.∨ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
Notation "(.↔ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core.
......@@ -483,18 +490,18 @@ Proof. unfold impl. red; intuition. Qed.
(** * Common data types *)
(** ** Functions *)
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 "( A →.)" := (λ B, A B) (only parsing) : stdpp_scope.
Notation "(.→ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "t $ r" := (t r)
(at level 65, right associativity, 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.
Notation "(∘)" := compose (only parsing) : stdpp_scope.
Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A B) :=
populate (λ _, inhabitant).
......@@ -586,9 +593,16 @@ Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
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 *)
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation "( x ,.)" := (pair x) (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 .2" := (snd p) (at level 2, left associativity, format "p .2").
......@@ -753,6 +767,10 @@ Section sig_map.
End sig_map.
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 *)
(** We define operational type classes for the traditional operations and
......@@ -770,8 +788,8 @@ Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2 := {}.
Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
Notation "( x ∪.)" := (union 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.
Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∪**" := (zip_with (zip_with ()))
......@@ -788,24 +806,24 @@ Hint Mode DisjUnion ! : typeclass_instances.
Instance: Params (@disj_union) 2 := {}.
Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
Notation "(⊎)" := disj_union (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 ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
Class Intersection A := intersection: A A A.
Hint Mode Intersection ! : typeclass_instances.
Instance: Params (@intersection) 2 := {}.
Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class Difference A := difference: A A A.
Hint Mode Difference ! : typeclass_instances.
Instance: Params (@difference) 2 := {}.
Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
Notation "(∖)" := difference (only parsing) : stdpp_scope.
Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
Notation "( x ∖.)" := (difference 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.
Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∖**" := (zip_with (zip_with ()))
......@@ -830,12 +848,12 @@ Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2 := {}.
Infix "⊆" := subseteq (at level 70) : stdpp_scope.
Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope.
Notation "(⊆ X )" := (λ Y, Y 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" := (¬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, Y X) (only parsing) : stdpp_scope.
Notation "( X ⊈.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(.⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
......@@ -854,12 +872,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core.
Infix "⊂" := (strict ()) (at level 70) : stdpp_scope.
Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope.
Notation "( X ⊂)" := (strict () X) (only parsing) : stdpp_scope.
Notation "(⊂ X )" := (λ Y, Y 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" := (¬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, Y X) (only parsing) : stdpp_scope.
Notation "( X ⊄.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(.⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.
......@@ -887,16 +905,19 @@ Hint Mode ElemOf - ! : typeclass_instances.
Instance: Params (@elem_of) 3 := {}.
Infix "∈" := elem_of (at level 70) : stdpp_scope.
Notation "(∈)" := elem_of (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 ∈.)" := (elem_of 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) (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.
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.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2 := {}.
......@@ -986,8 +1007,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4 := {}.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
......@@ -1024,10 +1045,21 @@ Hint Mode Lookup - - ! : typeclass_instances.
Instance: Params (@lookup) 4 := {}.
Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope.
Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
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 *)
Class SingletonM K A M := singletonM: K A M.
Hint Mode SingletonM - - ! : typeclass_instances.
......@@ -1126,25 +1158,76 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
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 *)
(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
elements of type [A]. The first class, [SemiSet] does not include intersection
and difference. It is useful for the case of lists, where decidable equality
is needed to implement intersection and difference, but not union.
(** The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets of
type [C] with elements of type [A]. The first class, [SemiSet] does not include
intersection and difference. It is useful for the case of lists, where decidable
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
we use [Set_]. *)
Class SemiSet A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ;
elem_of_singleton (x y : A) : x {[ y ]} x = y;
elem_of_union X Y (x : A) : x X Y x X x Y
not_elem_of_empty (x : A) : x @{C} ; (* We prove
[elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
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,
Union C, Intersection C, Difference C} : Prop := {
set_semi_set :>> SemiSet A C;
elem_of_intersection X Y (x : A) : x X Y x X x Y;
elem_of_difference X Y (x : A) : x X Y x X x Y
set_semi_set :> SemiSet A C;
elem_of_intersection (X Y : C) (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
......@@ -1182,9 +1265,9 @@ Qed.
anyway so as to avoid cycles in type class search. *)
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_set_set :>> Set_ A C;
elem_of_elements X x : x elements X x X;
NoDup_elements X : NoDup (elements X)
fin_set_set :> Set_ A C;
elem_of_elements (X : C) x : x elements X x X;
NoDup_elements (X : C) : NoDup (elements X)
}.
Class Size C := size: C nat.
Hint Mode Size ! : typeclass_instances.
......@@ -1205,10 +1288,11 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
monad_set_semi_set A :> SemiSet A (M A);
elem_of_bind {A B} (f : A M B) (X : M A) (x : B) :
x X = f y, x f y y X;
elem_of_ret {A} (x y : A) : x mret y x = y;
elem_of_ret {A} (x y : A) : x @{M A} mret y x = y;
elem_of_fmap {A B} (f : A B) (X : M A) (x : B) :
x f <$> X y, x = f y y X;
elem_of_join {A} (X : M (M A)) (x : A) : x mjoin X Y, x Y Y X
elem_of_join {A} (X : M (M A)) (x : A) :
x mjoin X Y : M A, x Y Y X
}.
(** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
......@@ -1222,7 +1306,10 @@ to pick fresh elements from other data structure like sets. See the file
[FinSet C A].
Note: we require [fresh] to respect permutations, which is needed to define the
aforementioned [fresh] function on finite sets that respects set equality. *)
aforementioned [fresh] function on finite sets that respects set equality.
Instead of instantiating [Infinite] directly, consider using [max_infinite] or
[inj_infinite] from the [infinite] module. *)
Class Fresh A C := fresh: C A.
Hint Mode Fresh - ! : typeclass_instances.
Instance: Params (@fresh) 3 := {}.
......@@ -1240,45 +1327,3 @@ Class Half A := half: A → A.
Hint Mode Half ! : typeclass_instances.
Notation "½" := half (format "½") : stdpp_scope.
Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
(** * 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 () := {}.
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.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements a type [binder] with elements [BAnon] for the
anonymous binder, and [BNamed] for named binders. This type is isomorphic to
[option string], but we use a special type so that we can define [BNamed] as
a coercion.
This library is used in various Iris developments, like heap-lang, LambdaRust,
Iron, Fairis. *)
From stdpp Require Export strings.
From stdpp Require Import sets countable finite fin_maps.
Inductive binder := BAnon | BNamed :> string binder.
Bind Scope binder_scope with binder.
Delimit Scope binder_scope with binder.
Notation "<>" := BAnon : binder_scope.
Instance binder_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Instance binder_inhabited : Inhabited binder := populate BAnon.
Instance binder_countable : Countable binder.
Proof.
refine (inj_countable'
(λ b, match b with BAnon => None | BNamed s => Some s end)
(λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
Qed.
(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [b], respectively [bs], are the binders that are being
added. *)
Definition cons_binder (b : binder) (ss : list string) : list string :=
match b with BAnon => ss | BNamed s => s :: ss end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
Infix "+b+" := app_binder (at level 60, right associativity).
Instance set_unfold_cons_binder s b ss P :
SetUnfoldElemOf s ss P SetUnfoldElemOf s (b :b: ss) (BNamed s = b P).
Proof.
constructor. rewrite <-(set_unfold (s ss) P).
destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed.
Instance set_unfold_app_binder s bs ss P Q :
SetUnfoldElemOf (BNamed s) bs P SetUnfoldElemOf s ss Q
SetUnfoldElemOf s (bs +b+ ss) (P Q).
Proof.
intros HinP HinQ.
constructor. rewrite <-(set_unfold (s ss) Q), <-(set_unfold (BNamed s bs) P).
clear HinP HinQ.
induction bs; set_solver.
Qed.
Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
Instance cons_binder_Permutation b : Proper (() ==> ()) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
Instance app_binder_Permutation : Proper (() ==> () ==> ()) app_binder.
Proof.
assert ( bs, Proper (() ==> ()) (app_binder bs)).
{ induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
Qed.
Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
match b with BAnon => m | BNamed s => delete s m end.
Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
match b with BAnon => m | BNamed s => <[s:=x]> m end.
Instance: Params (@binder_insert) 4 := {}.
Section binder_delete_insert.
Context `{FinMap string M}.
Global Instance binder_insert_proper `{Equiv A} b :
Proper (() ==> () ==> (@{M A})) (binder_insert b).
Proof. destruct b; solve_proper. Qed.
Lemma binder_delete_empty {A} b : binder_delete b =@{M A} .
Proof. destruct b; simpl; auto using delete_empty. Qed.
Lemma lookup_binder_delete_None {A} (m : M A) b s :
binder_delete b m !! s = None b = BNamed s m !! s = None.
Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
Lemma binder_insert_fmap {A B} (f : A B) (x : A) b (m : M A) :
f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
Lemma binder_delete_insert {A} b s x (m : M A) :
b BNamed s binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
Lemma binder_delete_delete {A} b s (m : M A) :
binder_delete b (delete s m) = delete s (binder_delete b m).
Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
End binder_delete_insert.
......@@ -19,15 +19,16 @@ Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Instance boolset_set `{EqDecision A} : Set_ A (boolset A).
Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof.
split; [split| |].
split; [split; [split| |]|].
- by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro.
- split. apply andb_prop_elim. apply andb_prop_intro.
- intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
Qed.
Instance boolset_elem_of_dec {A} : RelDecision (@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
......
(* Copyright (c) 2020, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements the type [coGset A] of finite/cofinite sets
of elements of any countable type [A].
Note that [coGset positive] cannot represent all elements of [coPset]
(e.g., [coPset_suffixes], [coPset_l], and [coPset_r] construct
infinite sets that cannot be represented). *)
From stdpp Require Export sets countable.
From stdpp Require Import decidable finite gmap coPset.
(* Set Default Proof Using "Type". *)
Inductive coGset `{Countable A} :=
| FinGSet (X : gset A)
| CoFinGset (X : gset A).
Arguments coGset _ {_ _} : assert.
Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Proof. solve_decision. Defined.
Instance coGset_countable `{Countable A} : Countable (coGset A).
Proof.
apply (inj_countable'
(λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
(λ s, match s with inl X => FinGSet X | inr X => CoFinGset X end)).
by intros [].
Qed.
Section coGset.
Context `{Countable A}.
Global Instance coGset_elem_of : ElemOf A (coGset A) := λ x X,
match X with FinGSet X => x X | CoFinGset X => x X end.
Global Instance coGset_empty : Empty (coGset A) := FinGSet .
Global Instance coGset_top : Top (coGset A) := CoFinGset .
Global Instance coGset_singleton : Singleton A (coGset A) := λ x,
FinGSet {[x]}.
Global Instance coGset_union : Union (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => CoFinGset (X Y)
| FinGSet X, CoFinGset Y => CoFinGset (Y X)
| CoFinGset X, FinGSet Y => CoFinGset (X Y)
end.
Global Instance coGset_intersection : Intersection (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => CoFinGset (X Y)
| FinGSet X, CoFinGset Y => FinGSet (X Y)
| CoFinGset X, FinGSet Y => FinGSet (Y X)
end.
Global Instance coGset_difference : Difference (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => FinGSet (Y X)
| FinGSet X, CoFinGset Y => FinGSet (X Y)
| CoFinGset X, FinGSet Y => CoFinGset (X Y)
end.
Global Instance coGset_set : TopSet A (coGset A).
Proof.
split; [split; [split| |]|].
- by intros ??.
- intros x y. unfold elem_of, coGset_elem_of; simpl.
by rewrite elem_of_singleton.
- intros [X|X] [Y|Y] x; unfold elem_of, coGset_elem_of, coGset_union; simpl.
+ set_solver.
+ by rewrite not_elem_of_difference, (comm ()).
+ by rewrite not_elem_of_difference.
+ by rewrite not_elem_of_intersection.
- intros [] [];
unfold elem_of, coGset_elem_of, coGset_intersection; set_solver.
- intros [X|X] [Y|Y] x;
unfold elem_of, coGset_elem_of, coGset_difference; simpl.
+ set_solver.
+ rewrite elem_of_intersection. destruct (decide (x Y)); tauto.
+ set_solver.
+ rewrite elem_of_difference. destruct (decide (x Y)); tauto.
- done.
Qed.
End coGset.
Instance coGset_elem_of_dec `{Countable A} : RelDecision (@{coGset A}) :=
λ x X,
match X with
| FinGSet X => decide_rel elem_of x X
| CoFinGset X => not_dec (decide_rel elem_of x X)
end.
Section infinite.
Context `{Countable A, Infinite A}.
Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
Proof.
intros [X|X] [Y|Y]; rewrite elem_of_equiv;
unfold elem_of, coGset_elem_of; simpl; intros HXY.
- f_equal. by apply leibniz_equiv.
- by destruct (exist_fresh (X Y)) as [? [? ?%HXY]%not_elem_of_union].
- by destruct (exist_fresh (X Y)) as [? [?%HXY ?]%not_elem_of_union].
- f_equal. apply leibniz_equiv; intros x. by apply not_elem_of_iff.
Qed.
Global Instance coGset_equiv_dec : RelDecision (@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
Defined.
Global Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Global Instance coGset_subseteq_dec : RelDecision (@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X Y = Y)));
abstract (by rewrite subseteq_union_L).
Defined.
Definition coGset_finite (X : coGset A) : bool :=
match X with FinGSet _ => true | CoFinGset _ => false end.
Lemma coGset_finite_spec X : set_finite X coGset_finite X.
Proof.
destruct X as [X|X];
unfold set_finite, elem_of at 1, coGset_elem_of; simpl.
- split; [done|intros _]. exists (elements X). set_solver.
- split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
by destruct (exist_fresh (X Y)) as [? [?%HXY ?]%not_elem_of_union].
Qed.
Global Instance coGset_finite_dec (X : coGset A) : Decision (set_finite X).
Proof.
refine (cast_if (decide (coGset_finite X)));
abstract (by rewrite coGset_finite_spec).
Defined.
End infinite.
(** * Pick elements from infinite sets *)
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
fresh (match X with FinGSet _ => | CoFinGset X => X end).
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X coGpick X X.
Proof.
unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
done. by intros _; apply is_fresh.
Qed.
(** * Conversion to and from gset *)
Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
match X with FinGSet X => X | CoFinGset _ => end.
Definition gset_to_coGset `{Countable A} : gset A coGset A := FinGSet.
Section to_gset.
Context `{Countable A, Infinite A}.
Lemma elem_of_coGset_to_gset (X : coGset A) x :
set_finite X x coGset_to_gset X x X.