...
 
Commits (132)
*.v gitlab-language=coq
*.vo
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
......@@ -14,3 +15,4 @@ Makefile.coq.conf
*.crashcoqide
html/
build-dep/
_opam
......@@ -2,24 +2,17 @@ image: ralfjung/opam-ci:latest
stages:
- build
- deploy
- build_more
variables:
CPU_CORES: "9"
CPU_CORES: "10"
GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template
stage: build
tags:
- fp-timing
- fp
script:
# prepare
- . 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'
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
......@@ -27,49 +20,59 @@ variables:
only:
- master
- /^ci/
except:
- triggers
- schedules
opam:
stage: deploy
script:
# Send a trigger to the repository doing the work
- 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
## Build jobs
build-coq.dev:
<<: *template
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:
OPAM_PINS: "coq version 8.8.0"
OPAM_PKG: "coq-stdpp"
only:
- master
except:
- triggers
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_PROJECT: "stdpp"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
build-coq.8.7.dev:
build-coq.8.7.2:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev"
except:
- triggers
OPAM_PINS: "coq version 8.7.2"
TIMING_PROJECT: "stdpp"
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:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.0"
except:
- triggers
build-coq.8.6.1:
<<: *template
variables:
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
stage: build_more
variables:
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
clean: Makefile.coq
+@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
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
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
# Install build-dependencies
build-dep/opam: opam Makefile
# Creating the build-dep package.
@echo "# Creating build-dep package."
@mkdir -p build-dep
@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
......@@ -31,12 +31,15 @@ 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.
@# Upgrading is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
((! opam --version | grep "^1\." > /dev/null) || ( \
echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
uninstall::
@# This makes sure we also delete stale files in the destination directory
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
# run tests with main build
real-all: test
# the test suite
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:
`Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See
[`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
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
theories/hlist.v
theories/sorting.v
theories/infinite.v
theories/nat_cancel.v
theories/namespaces.v
theories/telescopes.v
......@@ -19,17 +19,5 @@
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
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}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
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".
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
(** Enable implicit generalization. *)
(* This option enables implicit generalization in arguments of the form
(** * Enable implicit generalization. *)
(** This option enables implicit generalization in arguments of the form
`{...} (i.e., anonymous arguments). Unfortunately, it also enables
implicit generalization in `Instance`. We think that the fact taht both
behaviors are coupled together is a [bug in
......@@ -46,14 +46,44 @@ End seal.
Arguments unseal {_ _} _ : 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 *)
(* 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]. *)
Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque 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
existing logical operators as type classes. That is, we do not say:
......@@ -91,6 +121,23 @@ Existing Class TCForall.
Existing Instance TCForall_nil.
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
notations that do not belong to a more specific scope. *)
Delimit Scope stdpp_scope with stdpp.
......@@ -99,8 +146,8 @@ Global Open Scope stdpp_scope.
(** Change [True] and [False] into notations in order to enable overloading.
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
Notation "'True'" := True : type_scope.
Notation "'False'" := False : type_scope.
Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope.
(** * Equality *)
......@@ -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, 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 100 (_ _) => discriminate.
Instance: @PreOrder A (=).
Instance: A, PreOrder (=@{A}).
Proof. split; repeat intro; congruence. Qed.
(** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on
(Spitters/van der Weegen, 2011). *)
(** We define an operational type class for setoid equality, i.e., the
"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.
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)
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 "( X ≡)" := (equiv 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.
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.
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
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
......@@ -141,22 +204,22 @@ reverse. *)
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x y x = y.
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.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
Ltac fold_leibniz := repeat
match goal with
| H : context [ @equiv ?A _ _ _ ] |- _ =>
| H : context [ _ @{?A} _ ] |- _ =>
setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
| |- context [ @equiv ?A _ _ _ ] =>
| |- context [ _ @{?A} _ ] =>
setoid_rewrite (leibniz_equiv_iff (A:=A))
end.
Ltac unfold_leibniz := repeat
match goal with
| H : context [ @eq ?A _ _ ] |- _ =>
| H : context [ _ =@{?A} _ ] |- _ =>
setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
| |- context [ @eq ?A _ _ ] =>
| |- context [ _ =@{?A} _ ] =>
setoid_rewrite <-(leibniz_equiv_iff (A:=A))
end.
......@@ -201,7 +264,7 @@ Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :> Decision (R x y).
Hint Mode RelDecision ! ! ! : typeclass_instances.
Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
Notation EqDecision A := (RelDecision (@eq A)).
Notation EqDecision A := (RelDecision (=@{A})).
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
......@@ -363,9 +426,9 @@ Lemma exist_proper {A} (P Q : A → Prop) :
( x, P x Q x) ( x, P x) ( x, Q x).
Proof. firstorder. Qed.
Instance: Comm () (@eq A).
Instance: Comm () (=@{A}).
Proof. red; intuition. Qed.
Instance: Comm () (λ x y, @eq A y x).
Instance: Comm () (λ x y, y =@{A} x).
Proof. red; intuition. Qed.
Instance: Comm () ().
Proof. red; intuition. Qed.
......@@ -503,7 +566,7 @@ Proof. now intros -> ?. Qed.
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Instance unit_equivalence : Equivalence (@{unit}).
Proof. repeat split. Qed.
Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
......@@ -684,14 +747,10 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A.
Hint Mode Empty ! : typeclass_instances.
Notation "∅" := empty : stdpp_scope.
Notation "∅" := empty (format "∅") : stdpp_scope.
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.
Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2.
......@@ -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, 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.
Notation "(⊆*)" := (Forall2 ()) (only parsing) : stdpp_scope.
Infix "⊆**" := (Forall2 (*)) (at level 70) : 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, 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.
......@@ -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.
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.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2.
......@@ -806,6 +875,10 @@ Infix "##" := disjoint (at level 70) : stdpp_scope.
Notation "(##)" := disjoint (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint 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.
Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
......@@ -837,17 +910,19 @@ Class DisjointList A := disjoint_list : list A → Prop.
Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2.
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.
Context `{Disjoint A, Union A, Empty A}.
Implicit Types X : 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).
Global Existing Instance disjoint_list_default.
Lemma disjoint_list_nil : ## @nil A True.
Lemma disjoint_list_nil : ##@{A} [] True.
Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
......@@ -1118,5 +1193,47 @@ Class FreshSpec A C `{ElemOf A C,
(** * Miscellaneous *)
Class Half A := half: A A.
Hint Mode Half ! : typeclass_instances.
Notation "½" := half : stdpp_scope.
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.
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.
- intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto.
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.
Typeclasses Opaque bset_elem_of.
......
......@@ -190,16 +190,16 @@ Proof.
intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _).
Instance coPset_elem_of_dec : RelDecision (@{coPset}).
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.
Instance mapset_disjoint_dec : RelDecision (@disjoint coPset _).
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Instance mapset_subseteq_dec : RelDecision (@subseteq coPset _).
Instance mapset_subseteq_dec : RelDecision (@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.
......@@ -251,7 +251,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
| Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
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.
Proof.
......
......@@ -7,11 +7,13 @@ From stdpp Require Export orders list.
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
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.
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.
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.
Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
......@@ -19,27 +21,26 @@ Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
Section setoids_simple.
Context `{SimpleCollection A C}.
Global Instance collection_equivalence: @Equivalence C ().
Global Instance collection_equivalence : Equivalence (@{C}).
Proof.
split.
- done.
- intros X Y ? x. by symmetry.
- intros X Y Z ?? x; by trans (x Y).
Qed.
Global Instance singleton_proper : Proper ((=) ==> ()) (singleton (B:=C)).
Global Instance singleton_proper : Proper ((=) ==> (@{C})) singleton.
Proof. apply _. Qed.
Global Instance elem_of_proper :
Proper ((=) ==> () ==> iff) (@elem_of A C _) | 5.
Global Instance elem_of_proper : Proper ((=) ==> () ==> iff) (@{C}) | 5.
Proof. by intros x ? <- X Y. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _).
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (##@{C}).
Proof.
intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
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.
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.
Global Instance subseteq_proper : Proper (() ==> () ==> iff) (() : relation C).
Global Instance subseteq_proper : Proper ((@{C}) ==> (@{C}) ==> iff) ().
Proof.
intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
Qed.
......@@ -50,12 +51,12 @@ Section setoids.
(** * Setoids *)
Global Instance intersection_proper :
Proper (() ==> () ==> ()) (@intersection C _).
Proper (() ==> () ==> (@{C})) intersection.
Proof.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
Qed.
Global Instance difference_proper :
Proper (() ==> () ==> ()) (@difference C _).
Proper (() ==> () ==> (@{C})) difference.
Proof.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
Qed.
......@@ -316,10 +317,10 @@ Section simple_collection.
Proof. set_solver. Qed.
(** Subset relation *)
Global Instance collection_subseteq_antisymm: AntiSymm () (() : relation C).
Global Instance collection_subseteq_antisymm: AntiSymm () (@{C}).
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.
Lemma subseteq_union X Y : X Y X Y Y.
......@@ -357,15 +358,15 @@ Section simple_collection.
Lemma union_mono X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. set_solver. Qed.
Global Instance union_idemp : IdemP (() : relation C) ().
Global Instance union_idemp : IdemP (@{C}) ().
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.
Global Instance union_empty_r : RightId (() : relation C) ().
Global Instance union_empty_r : RightId (@{C}) ().
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.
Global Instance union_assoc : Assoc (() : relation C) ().
Global Instance union_assoc : Assoc (@{C}) ().
Proof. intros X Y Z. set_solver. Qed.
Lemma empty_union X Y : X Y X Y .
......@@ -408,7 +409,7 @@ Section simple_collection.
Lemma elem_of_disjoint X Y : X ## Y x, x X x Y False.
Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _).
Global Instance disjoint_sym : Symmetric (##@{C}).
Proof. intros X Y. set_solver. Qed.
Lemma disjoint_empty_l Y : ## Y.
Proof. set_solver. Qed.
......@@ -468,8 +469,7 @@ Section simple_collection.
Proof. unfold_leibniz. apply collection_equiv_spec. Qed.
(** Subset relation *)
Global Instance collection_subseteq_partialorder :
PartialOrder (() : relation C).
Global Instance collection_subseteq_partialorder : PartialOrder (@{C}).
Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
Lemma subseteq_union_L X Y : X Y X Y = Y.
......@@ -480,15 +480,15 @@ Section simple_collection.
Proof. unfold_leibniz. apply subseteq_union_2. Qed.
(** Union *)
Global Instance union_idemp_L : IdemP (@eq C) ().
Global Instance union_idemp_L : IdemP (=@{C}) ().
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.
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.
Global Instance union_comm_L : Comm (@eq C) ().
Global Instance union_comm_L : Comm (=@{C}) ().
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.
Lemma empty_union_L X Y : X Y = X = Y = .
......@@ -527,7 +527,7 @@ Section simple_collection.
End leibniz.
Section dec.
Context `{!RelDecision (@equiv C _)}.
Context `{!RelDecision (@{C})}.
Lemma collection_subseteq_inv X Y : X Y X Y X Y.
Proof. destruct (decide (X Y)); [by right|left;set_solver]. Qed.
Lemma collection_not_subset_inv X Y : X Y X Y X Y.
......@@ -580,15 +580,15 @@ Section collection.
X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. set_solver. Qed.
Global Instance intersection_idemp : IdemP (() : relation C) ().
Global Instance intersection_idemp : IdemP (@{C}) ().
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.
Global Instance intersection_assoc : Assoc (() : relation C) ().
Global Instance intersection_assoc : Assoc (@{C}) ().
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.
Global Instance intersection_empty_r: RightAbsorb (() : relation C) ().
Global Instance intersection_empty_r: RightAbsorb (@{C}) ().
Proof. intros X; set_solver. Qed.
Lemma intersection_singletons x : ({[x]} : C) {[x]} {[x]}.
......@@ -622,7 +622,8 @@ Section collection.
Proof. set_solver. Qed.
Lemma subset_difference_elem_of {x: A} {s: C} (inx: x s): s {[ x ]} s.
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 :
X1 X2 Y2 Y1 X1 Y1 X2 Y2.
......@@ -647,15 +648,15 @@ Section collection.
Lemma subseteq_intersection_2_L X Y : X Y = X X Y.
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.
Global Instance intersection_comm_L : Comm ((=) : relation C) ().
Global Instance intersection_comm_L : Comm (=@{C}) ().
Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
Global Instance intersection_assoc_L : Assoc ((=) : relation C) ().
Global Instance intersection_assoc_L : Assoc (=@{C}) ().
Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
Global Instance intersection_empty_l_L: LeftAbsorb ((=) : relation C) ().
Global Instance intersection_empty_l_L: LeftAbsorb (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
Global Instance intersection_empty_r_L: RightAbsorb ((=) : relation C) ().
Global Instance intersection_empty_r_L: RightAbsorb (=@{C}) ().
Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
Lemma intersection_singletons_L x : {[x]} {[x]} = ({[x]} : C).
......@@ -688,6 +689,8 @@ Section collection.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
Lemma difference_disjoint_L X Y : X ## Y X Y = X.
Proof. unfold_leibniz. apply difference_disjoint. Qed.
Lemma difference_difference_L X Y Z : (X Y) Z = X (Y Z).
Proof. unfold_leibniz. apply difference_difference. Qed.
(** Disjointness *)
Lemma disjoint_intersection_L X Y : X ## Y X Y = .
......@@ -695,7 +698,7 @@ Section collection.
End leibniz.
Section dec.
Context `{!RelDecision (@elem_of A C _)}.
Context `{!RelDecision (@{C})}.
Lemma not_elem_of_intersection x X Y : x X Y x X x Y.
Proof. rewrite elem_of_intersection. destruct (decide (x X)); tauto. Qed.
Lemma not_elem_of_difference x X Y : x X Y x X x Y.
......@@ -776,17 +779,17 @@ Section of_option_list.
SetUnfold (x l) P SetUnfold (x of_list (C:=C) l) P.
Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x l) P). Qed.
Lemma of_list_nil : of_list (C:=C) [] = .
Lemma of_list_nil : of_list [] =@{C} .
Proof. done. Qed.
Lemma of_list_cons x l : of_list (C:=C) (x :: l) = {[ x ]} of_list l.
Lemma of_list_cons x l : of_list (x :: l) =@{C} {[ x ]} of_list l.
Proof. done. Qed.
Lemma of_list_app l1 l2 : of_list (C:=C) (l1 ++ l2) of_list l1 of_list l2.
Lemma of_list_app l1 l2 : of_list (l1 ++ l2) @{C} of_list l1 of_list l2.
Proof. set_solver. Qed.
Global Instance of_list_perm : Proper ((≡ₚ) ==> ()) (of_list (C:=C)).
Proof. induction 1; set_solver. Qed.
Context `{!LeibnizEquiv C}.
Lemma of_list_app_L l1 l2 : of_list (C:=C) (l1 ++ l2) = of_list l1 of_list l2.
Lemma of_list_app_L l1 l2 : of_list (l1 ++ l2) =@{C} of_list l1 of_list l2.
Proof. set_solver. Qed.
Global Instance of_list_perm_L : Proper ((≡ₚ) ==> (=)) (of_list (C:=C)).
Proof. induction 1; set_solver. Qed.
......@@ -887,10 +890,9 @@ Section fresh.
Context `{FreshSpec A C}.
Implicit Types X Y : C.
Global Instance fresh_proper: Proper (() ==> (=)) (fresh (C:=C)).
Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
Global Instance fresh_list_proper n:
Proper (() ==> (=)) (fresh_list (C:=C) n).
Global Instance fresh_list_proper n : Proper ((@{C}) ==> (=)) (fresh_list n).
Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
Lemma exist_fresh X : x, x X.
......@@ -1049,22 +1051,26 @@ Section seq_set.
x seq_set (C:=C) start len start x < start + len.
Proof.
revert start. induction len as [|len IH]; intros start; simpl.
- rewrite elem_of_empty. omega.
- rewrite elem_of_union, elem_of_singleton, IH. omega.
- rewrite elem_of_empty. lia.
- rewrite elem_of_union, elem_of_singleton, IH. lia.
Qed.
Lemma seq_set_start_disjoint start len :
{[ start ]} ## seq_set (C:=C) (S start) len.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. lia. Qed.
Lemma seq_set_S_disjoint start len :
{[ start + len ]} ## seq_set (C:=C) start len.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. lia. Qed.
Lemma seq_set_S_union start len :
seq_set start (C:=C) (S len) {[ start + len ]} seq_set start len.
seq_set start (S len) @{C} {[ start + len ]} seq_set start len.
Proof.
intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega.
intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. lia.
Qed.
Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
seq_set start (C:=C) (S len) = {[ start + len ]} seq_set start len.
seq_set start (S len) =@{C} {[ start + len ]} seq_set start len.
Proof. unfold_leibniz. apply seq_set_S_union. Qed.
End seq_set.
......@@ -1078,7 +1084,7 @@ Section minimal.
Context `{SimpleCollection A C} {R : relation A}.
Implicit Types X Y : C.
Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x).
Global Instance minimal_proper x : Proper ((@{C}) ==> iff) (minimal R x).
Proof. intros X X' y; unfold minimal; set_solver. Qed.
Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
......
......@@ -37,9 +37,9 @@ Section choice.
Context `{Countable A} (P : A Prop).
Inductive choose_step: relation positive :=
| choose_step_None {p} : decode (A:=A) p = None choose_step (Psucc p) p
| choose_step_None {p} : decode (A:=A) p = None choose_step (Pos.succ p) p
| choose_step_Some {p} {x : A} :
decode p = Some x ¬P x choose_step (Psucc p) p.
decode p = Some x ¬P x choose_step (Pos.succ p) p.
Lemma choose_step_acc : ( x, P x) Acc choose_step 1%positive.
Proof.
intros [x Hx]. cut ( i p,
......@@ -348,11 +348,11 @@ Fixpoint gen_tree_of_list {T}
Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) :
gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
Proof.
revert t k l; fix 1; intros [|n ts] k l; simpl; auto.
revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto.
trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
- rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
rewrite reverse_cons, <-!(assoc_L _), gen_tree_of_to_list; simpl; auto.
rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
- simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
by (by rewrite reverse_length).
Qed.
......
......@@ -23,7 +23,7 @@ Implicit Types X Y : C.
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100.
Instance elem_of_dec_slow : RelDecision (