...
 
Commits (132)
*.v gitlab-language=coq
*.vo *.vo
*.vio *.vio
*.v.d *.v.d
.coqdeps.d
*.glob *.glob
*.cache *.cache
*.aux *.aux
...@@ -14,3 +15,4 @@ Makefile.coq.conf ...@@ -14,3 +15,4 @@ Makefile.coq.conf
*.crashcoqide *.crashcoqide
html/ html/
build-dep/ build-dep/
_opam
...@@ -2,24 +2,17 @@ image: ralfjung/opam-ci:latest ...@@ -2,24 +2,17 @@ image: ralfjung/opam-ci:latest
stages: stages:
- build - build
- deploy
- build_more
variables: variables:
CPU_CORES: "9" CPU_CORES: "10"
GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template .template: &template
stage: build stage: build
tags: tags:
- fp-timing - fp
script: script:
# prepare - ci/buildjob
- . build/opam-ci.sh $OPAM_PINS
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
cache: cache:
key: "$CI_JOB_NAME" key: "$CI_JOB_NAME"
paths: paths:
...@@ -27,49 +20,59 @@ variables: ...@@ -27,49 +20,59 @@ variables:
only: only:
- master - master
- /^ci/ - /^ci/
except:
- triggers
- schedules
opam: ## Build jobs
stage: deploy
script: build-coq.dev:
# Send a trigger to the repository doing the work <<: *template
- curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline variables:
OPAM_PINS: "coq version dev"
VALIDATE: "1"
build-coq.8.8.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.1"
build-coq.8.8.0:
<<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.0"
OPAM_PKG: "coq-stdpp" OPAM_PKG: "coq-stdpp"
only: DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
- master TIMING_PROJECT: "stdpp"
except: TIMING_CONF: "coq-8.8.0"
- triggers tags:
- fp-timing
build-coq.8.7.dev: build-coq.8.7.2:
<<: *template <<: *template
stage: build_more
variables: variables:
OPAM_PINS: "coq version 8.7.dev" OPAM_PINS: "coq version 8.7.2"
except: TIMING_PROJECT: "stdpp"
- triggers TIMING_CONF: "coq-8.7.2"
tags:
- fp-timing
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
build-coq.8.7.0: build-coq.8.7.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.7.0" OPAM_PINS: "coq version 8.7.0"
except:
- triggers
build-coq.8.6.1: build-coq.8.6.1:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.6.1" OPAM_PINS: "coq version 8.6.1"
artifacts:
paths:
- build-time.txt
- build-env.txt
except:
- triggers
build-coq.8.6: build-coq.8.6.0:
<<: *template <<: *template
stage: build_more
variables: variables:
OPAM_PINS: "coq version 8.6" OPAM_PINS: "coq version 8.6"
except:
- triggers
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
This file lists "large-ish" changes to the std++ Coq library, but not every
API-breaking change is listed.
## std++ 1.1.0 (released 2017-12-19)
Coq 8.5 is no longer supported by this release of std++. Use std++ 1.0 if you
have to use Coq 8.5.
New features:
- Many new lemmas about lists, vectors, sets, maps.
- Equivalence proofs between std++ functions and their alternative in the the
Coq standard library, e.g. `List.nth`, `List.NoDop`.
- Typeclass versions of the logical connectives and list predicates:
`TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
- A function `tc_opaque` to make definitions type class opaque.
- A type class `Infinite` for infinite types.
- A generic implementation to obtain fresh elements of infinite types.
- More theory about curry and uncurry functions on `gmap`.
- A generic `filter` and `zip_with` operation on finite maps.
- A type of generic trees for showing that arbitrary types are countable.
Changes:
- Get rid of `Automatic Coercions Import`, it is deprecated.
Also get rid of `Set Asymmetric Patterns`.
- Various changes and improvements to `f_equiv` and `solve_proper`.
- `Hint Mode` is now set for all operational type classes to make instance
search less likely to diverge.
- New type class `RelDecision` for decidable relations, and `EqDecision` is
defined in terms of it. This class allows to set `Hint Mode` properly.
- Use the flag `assert` of `Arguments` to make it more robust.
- The functions `imap` and `imap2` on lists are defined so that they enjoy more
definitional equalities.
- Theory about `fin` is moved to its own file `fin.v`.
- Rename `preserving``mono`.
Changes to notations:
- Operational type classes for lattice notations: `⊑`,`⊓`, `⊔`, `⊤` `⊥`.
- Replace `⊥` for disjointness with `##`, so that `⊥` can be used for the
bottom lattice element.
- All notations are now in `stdpp_scope` with scope key `stdpp`
(formerly `C_scope` and `C`).
- Higher precedence for `.1` and `.2` that is compatible with ssreflect.
- Various changes to monadic notations to improve compatibility with Mtac2:
+ Pattern matching notation for monadic bind `'pat ← x; y` where `pat` can
be any Coq pattern.
+ Change the level of the do-notation.
+ `<$>` is left associative.
+ Notation `x ;; y` for `_ ← x; y`.
## History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
part of the [Iris project](http://iris-project.org), and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
...@@ -8,19 +8,19 @@ all: Makefile.coq ...@@ -8,19 +8,19 @@ all: Makefile.coq
clean: Makefile.coq clean: Makefile.coq
+@make -f Makefile.coq clean +@make -f Makefile.coq clean
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq rm -f Makefile.coq
.PHONY: clean .PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics. # filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile build-dep/opam: opam Makefile
# Creating the build-dep package. @echo "# Creating build-dep package."
@mkdir -p build-dep @mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam @sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
...@@ -31,12 +31,15 @@ build-dep: build-dep/opam phony ...@@ -31,12 +31,15 @@ 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. @# dependencies, but does not actually install anything.
@# Upgrading is needed in case the pin already exists, but the builddep package changed. @# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \ @# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \ echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \ opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \ ((! opam --version | grep "^1\." > /dev/null) || ( \
opam upgrade "$$BUILD_DEP_PACKAGE" echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
# 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: ;
......
uninstall:: # run tests with main build
@# This makes sure we also delete stale files in the destination directory real-all: test
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\ # the test suite
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi TESTFILES=$(wildcard tests/*.v)
test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.9\b" > /dev/null && echo 1)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
# Oh Unix...
REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
-include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
$(if $(COQ_BROKEN), \
true, \
diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
) \
) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
touch $@
...@@ -34,20 +34,26 @@ Notably: ...@@ -34,20 +34,26 @@ Notably:
`Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See
[`base.v`](theories/base.v) for further details. [`base.v`](theories/base.v) for further details.
## History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
part of the [Iris project](http://iris-project.org), and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
## Prerequisites ## Prerequisites
This version is known to compile with: This version is known to compile with:
- Coq version 8.6 / 8.6.1 / 8.7.0 - Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1
## Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add
the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released
Then you can do `opam install coq-stdpp`.
To obtain a development version, add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
## Building Instructions ## Building from source
Run `make` to build the full development. Run `make install` to install the library. Run `make -jN` in this directory to build the library, where `N` is the number
of your CPU cores. Then run `make install` to install the library.
...@@ -40,4 +40,6 @@ theories/functions.v ...@@ -40,4 +40,6 @@ theories/functions.v
theories/hlist.v theories/hlist.v
theories/sorting.v theories/sorting.v
theories/infinite.v theories/infinite.v
theories/nat_cancel.v
theories/namespaces.v
theories/telescopes.v
...@@ -19,17 +19,5 @@ ...@@ -19,17 +19,5 @@
next next
} }
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines # This forwards all unchanged lines
1 1
#!/bin/bash
set -e
set -x
## This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM.
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
eval `opam conf env`
# Make sure the pin for the builddep package is not stale.
make build-dep/opam
# Update repositories
opam update
# Make sure we got the right set of repositories registered
if echo "$@" | fgrep "dev" > /dev/null; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
else
# No dev version, make sure we do not have the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
test -d "$OPAMROOT/repo/coq-core-dev" && opam repo remove coq-core-dev
fi
test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
echo
# We really want to run all of the following in one opam transaction, but due to opam limitations,
# that is not currently possible.
# Install fixed versions of some dependencies.
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
else
echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
fi
done
# Upgrade cached things.
echo
echo "[opam-ci] Upgrading opam"
opam upgrade -y --fixup && opam upgrade -y
# Install build-dependencies.
echo
echo "[opam-ci] Installing build-dependencies"
make build-dep OPAMFLAGS=-y
# done
echo
coqc -v
Subproject commit fb4a01dacbd489e6a4c50c2659486f589ba470d3
...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"] ...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [ depends: [
"coq" { (>= "8.6" & < "8.8~") | (= "dev") } "coq" { (>= "8.6" & < "8.9~") | (= "dev") }
] ]
From stdpp Require Import prelude.
(** Some tests for solve_proper. *)
Section tests.
Context {A B : Type} `{!Equiv A, !Equiv B}.
Context (foo : A A) (bar : A B) (baz : B A A).
Context `{!Proper (() ==> ()) foo,
!Proper (() ==> ()) bar,
!Proper (() ==> () ==> ()) baz}.
Definition test1 (x : A) := baz (bar (foo x)) x.
Global Instance : Proper (() ==> ()) test1.
Proof. solve_proper. Qed.
Definition test2 (b : bool) (x : A) :=
if b then bar (foo x) else bar x.
Global Instance : b, Proper (() ==> ()) (test2 b).
Proof. solve_proper. Qed.
Definition test3 (f : nat A) :=
baz (bar (f 0)) (f 2).
Global Instance : Proper (pointwise_relation nat () ==> ()) test3.
Proof. solve_proper. Qed.
End tests.
From stdpp Require Import prelude.
(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
we cannot [1]. So at least we try to make sure the first solution found
is the right one, to not pay performance in the success case [2].
[1] https://github.com/coq/coq/issues/7916
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
exists R, @Reflexive Prop R /\ R = iff.
Proof.
eexists. split.
- apply _.
- reflexivity.
Qed.
...@@ -10,8 +10,8 @@ Set Default Proof Using "Type". ...@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
(** Enable implicit generalization. *) (** * Enable implicit generalization. *)
(* This option enables implicit generalization in arguments of the form (** This option enables implicit generalization in arguments of the form
`{...} (i.e., anonymous arguments). Unfortunately, it also enables `{...} (i.e., anonymous arguments). Unfortunately, it also enables
implicit generalization in `Instance`. We think that the fact taht both implicit generalization in `Instance`. We think that the fact taht both
behaviors are coupled together is a [bug in behaviors are coupled together is a [bug in
...@@ -46,14 +46,44 @@ End seal. ...@@ -46,14 +46,44 @@ End seal.
Arguments unseal {_ _} _ : assert. Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert. Arguments seal_eq {_ _} _ : assert.
(** * Non-backtracking type classes *)
(** The type class [NoBackTrack 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
depends on this evar.
The proper way of handling this would be by setting Coq's option
`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq
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.
(* 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,
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 :=
| TCIf_true : P Q TCIf P Q R
| TCIf_false : R TCIf P Q R.
Existing Class TCIf.
Hint Extern 0 (TCIf _ _ _) =>
first [apply TCIf_true; [apply _|]
|apply TCIf_false] : typeclass_instances.
(** * Typeclass opaque definitions *) (** * Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type (** The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *) class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x. Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque. Typeclasses Opaque tc_opaque.
Arguments tc_opaque {_} _ /. Arguments tc_opaque {_} _ /.
(* Below we define type class versions of the common logical operators. It is (** Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say: existing logical operators as type classes. That is, we do not say:
...@@ -91,6 +121,23 @@ Existing Class TCForall. ...@@ -91,6 +121,23 @@ Existing Class TCForall.
Existing Instance TCForall_nil. Existing Instance TCForall_nil.
Existing Instance TCForall_cons. Existing Instance TCForall_cons.
Inductive TCForall2 {A B} (P : A B Prop) : list A list B Prop :=
| TCForall2_nil : TCForall2 P [] []
| TCForall2_cons x y xs ys :
P x y TCForall2 P xs ys TCForall2 P (x :: xs) (y :: ys).
Existing Class TCForall2.
Existing Instance TCForall2_nil.
Existing Instance TCForall2_cons.
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Instance TCEq_refl.
Inductive TCDiag {A} (C : A Prop) : A A Prop :=
| TCDiag_diag x : C x TCDiag C x x.
Existing Class TCDiag.
Existing Instance TCDiag_diag.
(** Throughout this development we use [stdpp_scope] for all general purpose (** Throughout this development we use [stdpp_scope] for all general purpose
notations that do not belong to a more specific scope. *) notations that do not belong to a more specific scope. *)
Delimit Scope stdpp_scope with stdpp. Delimit Scope stdpp_scope with stdpp.
...@@ -99,8 +146,8 @@ Global Open Scope stdpp_scope. ...@@ -99,8 +146,8 @@ Global Open Scope stdpp_scope.
(** Change [True] and [False] into notations in order to enable overloading. (** Change [True] and [False] into notations in order to enable overloading.
We will use this to give [True] and [False] a different interpretation for We will use this to give [True] and [False] a different interpretation for
embedded logics. *) embedded logics. *)
Notation "'True'" := True : type_scope. Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False : type_scope. Notation "'False'" := False (format "False") : type_scope.
(** * Equality *) (** * Equality *)
...@@ -112,20 +159,31 @@ Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope. ...@@ -112,20 +159,31 @@ 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)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
(at level 70, only parsing, no associativity) : stdpp_scope.
Hint Extern 0 (_ = _) => reflexivity. Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ _) => discriminate. Hint Extern 100 (_ _) => discriminate.
Instance: @PreOrder A (=). Instance: A, PreOrder (=@{A}).
Proof. split; repeat intro; congruence. Qed. Proof. split; repeat intro; congruence. Qed.
(** ** Setoid equality *) (** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on (** We define an operational type class for setoid equality, i.e., the
(Spitters/van der Weegen, 2011). *) "canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
Class Equiv A := equiv: relation A. Class Equiv A := equiv: relation A.
(* No Hint Mode set because of Coq bug #5735 (* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *) Hint Mode Equiv ! : typeclass_instances. *)
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope. Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡@{ A }" := (@equiv A _)
(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.
...@@ -134,6 +192,11 @@ Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope. ...@@ -134,6 +192,11 @@ 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 } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
Notation "X ≢@{ A } Y":= (¬X @{ A } Y)
(at level 70, only parsing, no associativity) : stdpp_scope.
(** The type class [LeibnizEquiv] collects setoid equalities that coincide (** The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
...@@ -141,22 +204,22 @@ reverse. *) ...@@ -141,22 +204,22 @@ reverse. *)
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x y x = y. Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x y x = y.
Hint Mode LeibnizEquiv ! - : typeclass_instances. Hint Mode LeibnizEquiv ! - : typeclass_instances.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) : Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) :
x y x = y. x y x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed. Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
Ltac fold_leibniz := repeat Ltac fold_leibniz := repeat
match goal with match goal with
| H : context [ @equiv ?A _ _ _ ] |- _ => | H : context [ _ @{?A} _ ] |- _ =>
setoid_rewrite (leibniz_equiv_iff (A:=A)) in H setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
| |- context [ @equiv ?A _ _ _ ] => | |- context [ _ @{?A} _ ] =>
setoid_rewrite (leibniz_equiv_iff (A:=A)) setoid_rewrite (leibniz_equiv_iff (A:=A))
end. end.
Ltac unfold_leibniz := repeat Ltac unfold_leibniz := repeat
match goal with match goal with
| H : context [ @eq ?A _ _ ] |- _ => | H : context [ _ =@{?A} _ ] |- _ =>
setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
| |- context [ @eq ?A _ _ ] => | |- context [ _ =@{?A} _ ] =>
setoid_rewrite <-(leibniz_equiv_iff (A:=A)) setoid_rewrite <-(leibniz_equiv_iff (A:=A))
end. end.
...@@ -201,7 +264,7 @@ Class RelDecision {A B} (R : A → B → Prop) := ...@@ -201,7 +264,7 @@ Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :> Decision (R x y). decide_rel x y :> Decision (R x y).
Hint Mode RelDecision ! ! ! : typeclass_instances. Hint Mode RelDecision ! ! ! : typeclass_instances.
Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert. Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
Notation EqDecision A := (RelDecision (@eq A)). Notation EqDecision A := (RelDecision (=@{A})).
(** ** Inhabited types *) (** ** Inhabited types *)
(** This type class collects types that are inhabited. *) (** This type class collects types that are inhabited. *)
...@@ -363,9 +426,9 @@ Lemma exist_proper {A} (P Q : A → Prop) : ...@@ -363,9 +426,9 @@ Lemma exist_proper {A} (P Q : A → Prop) :
( x, P x Q x) ( x, P x) ( x, Q x). ( x, P x Q x) ( x, P x) ( x, Q x).
Proof. firstorder. Qed. Proof. firstorder. Qed.
Instance: Comm () (@eq A). Instance: Comm () (=@{A}).
Proof. red; intuition. Qed. Proof. red; intuition. Qed.
Instance: Comm () (λ x y, @eq A y x). Instance: Comm () (λ x y, y =@{A} x).
Proof. red; intuition. Qed. Proof. red; intuition. Qed.
Instance: Comm () (). Instance: Comm () ().
Proof. red; intuition. Qed. Proof. red; intuition. Qed.
...@@ -503,7 +566,7 @@ Proof. now intros -> ?. Qed. ...@@ -503,7 +566,7 @@ Proof. now intros -> ?. Qed.
(** ** Unit *) (** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True. Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _). Instance unit_equivalence : Equivalence (@{unit}).
Proof. repeat split. Qed. Proof. repeat split. Qed.
Instance unit_leibniz : LeibnizEquiv unit. Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed. Proof. intros [] []; reflexivity. Qed.
...@@ -684,14 +747,10 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset ...@@ -684,14 +747,10 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *) [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A. Class Empty A := empty: A.
Hint Mode Empty ! : typeclass_instances. Hint Mode Empty ! : typeclass_instances.
Notation "∅" := empty : stdpp_scope. Notation "∅" := empty (format "∅") : stdpp_scope.
Instance empty_inhabited `(Empty A) : Inhabited A := populate . Instance empty_inhabited `(Empty A) : Inhabited A := populate .
Class Top A := top : A.
Hint Mode Top ! : typeclass_instances.
Notation "⊤" := top : stdpp_scope.
Class Union A := union: A A A. Class Union A := union: A A A.
Hint Mode Union ! : typeclass_instances. Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2. Instance: Params (@union) 2.
...@@ -755,6 +814,10 @@ Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : stdpp_scope. ...@@ -755,6 +814,10 @@ 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.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
Infix "⊆*" := (Forall2 ()) (at level 70) : stdpp_scope. Infix "⊆*" := (Forall2 ()) (at level 70) : stdpp_scope.
Notation "(⊆*)" := (Forall2 ()) (only parsing) : stdpp_scope. Notation "(⊆*)" := (Forall2 ()) (only parsing) : stdpp_scope.
Infix "⊆**" := (Forall2 (*)) (at level 70) : stdpp_scope. Infix "⊆**" := (Forall2 (*)) (at level 70) : stdpp_scope.
...@@ -776,6 +839,9 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope. ...@@ -776,6 +839,9 @@ 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.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.
Notation "X ⊆ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope. Notation "X ⊆ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊆ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope. Notation "X ⊆ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊂ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope. Notation "X ⊂ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
...@@ -799,6 +865,9 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope. ...@@ -799,6 +865,9 @@ 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.
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.
...@@ -806,6 +875,10 @@ Infix "##" := disjoint (at level 70) : stdpp_scope. ...@@ -806,6 +875,10 @@ Infix "##" := disjoint (at level 70) : stdpp_scope.
Notation "(##)" := disjoint (only parsing) : stdpp_scope. Notation "(##)" := disjoint (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope. Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope. Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
Infix "##@{ A }" := (@disjoint A _) (at level 70, only parsing) : stdpp_scope.
Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope.
Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope. Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope. Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope. Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
...@@ -837,17 +910,19 @@ Class DisjointList A := disjoint_list : list A → Prop. ...@@ -837,17 +910,19 @@ Class DisjointList A := disjoint_list : list A → Prop.
Hint Mode DisjointList ! : typeclass_instances. Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2. Instance: Params (@disjoint_list) 2.
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope. Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope.
Notation "##@{ A } Xs" :=
(@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
Section disjoint_list. Section disjoint_list.
Context `{Disjoint A, Union A, Empty A}. Context `{Disjoint A, Union A, Empty A}.
Implicit Types X : A. Implicit Types X : A.
Inductive disjoint_list_default : DisjointList A := Inductive disjoint_list_default : DisjointList A :=
| disjoint_nil_2 : ## (@nil A) | disjoint_nil_2 : ##@{A} []
| disjoint_cons_2 (X : A) (Xs : list A) : X ## Xs ## Xs ## (X :: Xs). | disjoint_cons_2 (X : A) (Xs : list A) : X ## Xs ## Xs ## (X :: Xs).
Global Existing Instance disjoint_list_default. Global Existing Instance disjoint_list_default.
Lemma disjoint_list_nil : ## @nil A True. Lemma disjoint_list_nil : ##@{A} [] True.
Proof. split; constructor. Qed. Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs. Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed. Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
...@@ -1118,5 +1193,47 @@ Class FreshSpec A C `{ElemOf A C, ...@@ -1118,5 +1193,47 @@ Class FreshSpec A C `{ElemOf A C,
(** * Miscellaneous *) (** * Miscellaneous *)
Class Half A := half: A A. Class Half A := half: A A.
Hint Mode Half ! : typeclass_instances. Hint Mode Half ! : typeclass_instances.
Notation "½" := half : stdpp_scope. Notation "½" := half (format "½") : stdpp_scope.
Notation "½*" := (fmap (M:=list) half) : 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.
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.
...@@ -29,7 +29,7 @@ Proof. ...@@ -29,7 +29,7 @@ Proof.
- intros X Y x; unfold elem_of, bset_elem_of; simpl. - intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto. destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed. Qed.
Instance bset_elem_of_dec {A} : RelDecision (@elem_of _ (bset A) _). Instance bset_elem_of_dec {A} : RelDecision (@{bset A}).
Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined. Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
Typeclasses Opaque bset_elem_of. Typeclasses Opaque bset_elem_of.
......
...@@ -190,16 +190,16 @@ Proof. ...@@ -190,16 +190,16 @@ Proof.
intros p; apply eq_bool_prop_intro, (HXY p). intros p; apply eq_bool_prop_intro, (HXY p).
Qed. Qed.
Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _). Instance coPset_elem_of_dec : RelDecision (@{coPset}).
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
Instance coPset_equiv_dec : RelDecision (@equiv coPset _). Instance coPset_equiv_dec : RelDecision (@{coPset}).
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined. Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Instance mapset_disjoint_dec : RelDecision (@disjoint coPset _). Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Proof. Proof.
refine (λ X Y, cast_if (decide (X Y = ))); refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L). abstract (by rewrite disjoint_intersection_L).
Defined. Defined.
Instance mapset_subseteq_dec : RelDecision (@subseteq coPset _). Instance mapset_subseteq_dec : RelDecision (@{coPset}).
Proof. Proof.
refine (λ X Y, cast_if (decide (X Y = Y))); abstract (by rewrite subseteq_union_L). refine (λ X Y, cast_if (decide (X Y = Y))); abstract (by rewrite subseteq_union_L).
Defined. Defined.
...@@ -251,7 +251,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive := ...@@ -251,7 +251,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
| Some i => Some (i~0) | None => (~1) <$> coPpick_raw r | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
end end
end. end.
Definition coPpick (X : coPset) : positive := from_option id 1 (coPpick_raw (`X)). Definition coPpick (X : coPset) : positive := default 1 (coPpick_raw (`X)).
Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i e_of i t. Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i e_of i t.
Proof. Proof.
......
...@@ -7,11 +7,13 @@ From stdpp Require Export orders list. ...@@ -7,11 +7,13 @@ From stdpp Require Export orders list.
(* FIXME: This file needs a 'Proof Using' hint, but the default we use (* FIXME: This file needs a 'Proof Using' hint, but the default we use
everywhere makes for lots of extra ssumptions. *) everywhere makes for lots of extra ssumptions. *)
Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y, (* Higher precedence to make sure these instances are not used for other types
with an [ElemOf] instance, such as lists. *)
Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
x, x X x Y. x, x X x Y.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y, Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
x, x X x Y. x, x X x Y.
Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y, Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
x, x X x Y False. x, x X x Y False.
Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint. Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
...@@ -19,27 +21,26 @@ Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint. ...@@ -19,27 +21,26 @@ Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
Section setoids_simple. Section setoids_simple.
Context `{SimpleCollection A C}. Context `{SimpleCollection A C}.
Global Instance collection_equivalence: @Equivalence C (). Global Instance collection_equivalence : Equivalence (@{C}).
Proof. Proof.
split. split.
- done. - done.
- intros X Y ? x. by symmetry. - intros X Y ? x. by symmetry.
- intros X Y Z ?? x; by trans (x Y). - intros X Y Z ?? x; by trans (x Y).
Qed. Qed.
Global Instance singleton_proper : Proper ((=) ==> ()) (singleton (B:=C)). Global Instance singleton_proper : Proper ((=) ==> (@{C})) singleton.
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance elem_of_proper : Global Instance elem_of_proper : Proper ((=) ==> () ==> iff) (@{C}) | 5.
Proper ((=) ==> () ==> iff) (@elem_of A C _) | 5.
Proof. by intros x ? <- X Y. Qed. Proof. by intros x ? <- X Y. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _). Global Instance disjoint_proper: Proper (() ==> () ==> iff) (##@{C}).
Proof. Proof.
intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY. intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
Qed. Qed.
Global Instance union_proper : Proper (() ==> () ==> ()) (@union C _). Global Instance union_proper : Proper (() ==> () ==> (@{C})) union.
Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed. Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed.
Global Instance union_list_proper: Proper (() ==> ()) (union_list (A:=C)). Global Instance union_list_proper: Proper (() ==> (@{C})) union_list.
Proof. by induction 1; simpl; try apply union_proper. Qed. Proof. by induction 1; simpl; try apply union_proper. Qed.
Global Instance subseteq_proper : Proper (() ==> () ==> iff) (() : relation C). Global Instance subseteq_proper : Proper ((@{C}) ==> (@{C}) ==> iff) ().
Proof. Proof.
intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY. intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
Qed. Qed.
...@@ -50,12 +51,12 @@ Section setoids. ...@@ -50,12 +51,12 @@ Section setoids.
(** * Setoids *) (** * Setoids *)
Global Instance intersection_proper : Global Instance intersection_proper :
Proper (() ==> () ==> ()) (@intersection C _). Proper (() ==> () ==> (@{C})) intersection.
Proof. Proof.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY. intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
Qed. Qed.
Global Instance difference_proper : Global Instance difference_proper :
Proper (() ==> () ==> ()) (@difference C _). Proper (() ==> () ==> (@{C})) difference.
Proof. Proof.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY. intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
Qed. Qed.
...@@ -316,10 +317,10 @@ Section simple_collection. ...@@ -316,10 +317,10 @@ Section simple_collection.
Proof. set_solver. Qed. Proof. set_solver. Qed.
(** Subset relation *) (** Subset relation *)
Global Instance collection_subseteq_antisymm: AntiSymm () (() : relation C). Global Instance collection_subseteq_antisymm: AntiSymm () (@{C}).
Proof. intros ??. set_solver. Qed. Proof. intros ??. set_solver. Qed.
Global Instance collection_subseteq_preorder: PreOrder (() : relation C). Global Instance collection_subseteq_preorder: PreOrder (@{C}).
Proof. split. by intros ??. intros ???; set_solver. Qed. Proof. split. by intros ??. intros ???; set_solver. Qed.
Lemma subseteq_union X Y : X Y X Y Y. Lemma subseteq_union X Y : X Y X Y Y.
...@@ -357,15 +358,15 @@ Section simple_collection. ...@@ -357,15 +358,15 @@ Section simple_collection.
Lemma union_mono X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2. Lemma union_mono X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Global Instance union_idemp : IdemP (() : relation C) (). Global Instance union_idemp : IdemP (@{C}) ().
Proof. intros X. set_solver. Qed. Proof. intros X. set_solver. Qed.
Global Instance union_empty_l : LeftId (() : relation C) (). Global Instance union_empty_l : LeftId (@{C}) ().
Proof. intros X. set_solver. Qed. Proof. intros X. set_solver. Qed.
Global Instance union_empty_r : RightId (() : relation C) (). Global Instance union_empty_r : RightId (@{C}) ().
Proof. intros X. set_solver. Qed. Proof. intros X. set_solver. Qed.
Global Instance union_comm : Comm (() : relation C) (). Global Instance union_comm : Comm (@{C}) ().
Proof. intros X Y. set_solver. Qed. Proof. intros X Y. set_solver. Qed.
Global Instance union_assoc : Assoc (() : relation C) (). Global Instance union_assoc : Assoc (@{C}) ().
Proof. intros X Y Z. set_solver. Qed. Proof. intros X Y Z. set_solver. Qed.
Lemma empty_union X Y : X Y X Y . Lemma empty_union X Y : X Y X Y .
...@@ -408,7 +409,7 @@ Section simple_collection. ...@@ -408,7 +409,7 @@ Section simple_collection.
Lemma elem_of_disjoint X Y : X ## Y x, x X x Y False. Lemma elem_of_disjoint X Y : X ## Y x, x X x Y False.
Proof. done. Qed. Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _). Global Instance disjoint_sym : Symmetric (##@{C}).
Proof. intros X Y. set_solver. Qed. Proof. intros X Y. set_solver. Qed.
Lemma disjoint_empty_l Y : ## Y. Lemma disjoint_empty_l Y : ## Y.
Proof. set_solver. Qed. Proof. set_solver. Qed.
...@@ -468,8 +469,7 @@ Section simple_collection. ...@@ -468,8 +469,7 @@ Section simple_collection.
Proof. unfold_leibniz. apply collection_equiv_spec. Qed. Proof. unfold_leibniz. apply collection_equiv_spec. Qed.
(** Subset relation *) (** Subset relation *)
Global Instance collection_subseteq_partialorder : Global Instance collection_subseteq_partialorder : PartialOrder (@{C}).
PartialOrder (() : relation C).
Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed. Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
Lemma subseteq_union_L X Y : X Y X Y = Y. Lemma subseteq_union_L X Y : X Y X Y = Y.
...@@ -480,15 +480,15 @@ Section simple_collection. ...@@ -480,15 +480,15 @@ Section simple_collection.
Proof. unfold_leibniz. apply subseteq_union_2. Qed. Proof. unfold_leibniz. apply subseteq_union_2. Qed.
(** Union *) (** Union *)
Global Instance union_idemp_L : IdemP (@eq C) (). Global Instance union_idemp_L : IdemP (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (idemp _). Qed. Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
Global Instance union_empty_l_L : LeftId (@eq C) (). Global Instance union_empty_l_L : LeftId (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed. Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
Global Instance union_empty_r_L : RightId (@eq C) (). Global Instance union_empty_r_L : RightId (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed. Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
Global Instance union_comm_L : Comm (@eq C) (). Global Instance union_comm_L : Comm (=@{C}) ().
Proof. intros ??. unfold_leibniz. apply (comm _). Qed. Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
Global Instance union_assoc_L : Assoc (@eq C) (). Global Instance union_assoc_L : Assoc (=@{C}) ().
Proof. intros ???. unfold_leibniz. apply (assoc _). Qed. Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
Lemma empty_union_L X Y : X Y = X = Y = . Lemma empty_union_L X Y : X Y = X = Y = .
...@@ -527,7 +527,7 @@ Section simple_collection. ...@@ -527,7 +527,7 @@ Section simple_collection.
End leibniz. End leibniz.
Section dec. Section dec.
Context `{!RelDecision (@equiv C _)}. Context `{!RelDecision (@{C})}.
Lemma collection_subseteq_inv X Y : X Y X Y X Y. Lemma collection_subseteq_inv X Y : X Y X Y X Y.
Proof. destruct (decide (X Y)); [by right|left;set_solver]. Qed. Proof. destruct (decide (X Y)); [by right|left;set_solver]. Qed.
Lemma collection_not_subset_inv X Y : X Y X Y X Y. Lemma collection_not_subset_inv X Y : X Y X Y X Y.
...@@ -580,15 +580,15 @@ Section collection. ...@@ -580,15 +580,15 @@ Section collection.
X1 X2 Y1 Y2 X1 Y1 X2 Y2. X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Global Instance intersection_idemp : IdemP (() : relation C) (). Global Instance intersection_idemp : IdemP (@{C}) ().
Proof. intros X; set_solver. Qed. Proof. intros X; set_solver. Qed.
Global Instance intersection_comm : Comm (() : relation C) (). Global Instance intersection_comm : Comm (@{C}) ().
Proof. intros X Y; set_solver. Qed. Proof. intros X Y; set_solver. Qed.
Global Instance intersection_assoc : Assoc (() : relation C) (). Global Instance intersection_assoc : Assoc (@{C}) ().
Proof. intros X Y Z; set_solver. Qed. Proof. intros X Y Z; set_solver. Qed.
Global Instance intersection_empty_l : LeftAbsorb (() : relation C) (). Global Instance intersection_empty_l : LeftAbsorb (@{C}) ().
Proof. intros X; set_solver. Qed. Proof. intros X; set_solver. Qed.
Global Instance intersection_empty_r: RightAbsorb (() : relation C) (). Global Instance intersection_empty_r: RightAbsorb (@{C}) ().
Proof. intros X; set_solver. Qed. Proof. intros X; set_solver. Qed.
Lemma intersection_singletons x : ({[x]} : C) {[x]} {[x]}. Lemma intersection_singletons x : ({[x]} : C) {[x]} {[x]}.
...@@ -622,7 +622,8 @@ Section collection. ...@@ -622,7 +622,8 @@ Section collection.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma subset_difference_elem_of {x: A} {s: C} (inx: x s): s {[ x ]} s. Lemma subset_difference_elem_of {x: A} {s: C} (inx: x s): s {[ x ]} s.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma difference_difference X Y Z : (X Y) Z X (Y Z).
Proof. set_solver. Qed.
Lemma difference_mono X1 X2 Y1 Y2 : Lemma difference_mono X1 X2 Y1 Y2 :
X1 X2 Y2 Y1 X1 Y1 X2 Y2. X1 X2 Y2 Y1 X1 Y1 X2 Y2.
...@@ -647,15 +648,15 @@ Section collection. ...@@ -647,15 +648,15 @@ Section collection.
Lemma subseteq_intersection_2_L X Y : X Y = X X Y. Lemma subseteq_intersection_2_L X Y : X Y = X X Y.
Proof. unfold_leibniz. apply subseteq_intersection_2. Qed. Proof. unfold_leibniz. apply subseteq_intersection_2. Qed.
Global Instance intersection_idemp_L : IdemP ((=) : relation C) (). Global Instance intersection_idemp_L : IdemP (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (idemp _). Qed. Proof. intros ?. unfold_leibniz