...
 
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.
This diff is collapsed.
...@@ -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.
......
This diff is collapsed.
...@@ -37,9 +37,9 @@ Section choice. ...@@ -37,9 +37,9 @@ Section choice.
Context `{Countable A} (P : A Prop). Context `{Countable A} (P : A Prop).
Inductive choose_step: relation positive := 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} : | 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. Lemma choose_step_acc : ( x, P x) Acc choose_step 1%positive.
Proof. Proof.
intros [x Hx]. cut ( i p, intros [x Hx]. cut ( i p,
...@@ -348,11 +348,11 @@ Fixpoint gen_tree_of_list {T} ...@@ -348,11 +348,11 @@ Fixpoint gen_tree_of_list {T}
Lemma gen_tree_of_to_list {T} k l (t : gen_tree 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. gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
Proof. 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)). trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
- rewrite <-(assoc_L _). revert k. generalize ([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. 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 - simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
by (by rewrite reverse_length). by (by rewrite reverse_length).
Qed. Qed.
......
...@@ -23,7 +23,7 @@ Implicit Types X Y : C. ...@@ -23,7 +23,7 @@ Implicit Types X Y : C.
Lemma fin_collection_finite X : set_finite X. Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. 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 (@{C}) | 100.
Proof. Proof.
refine (λ x X, cast_if (decide_rel () x (elements X))); refine (λ x X, cast_if (decide_rel () x (elements X)));
by rewrite <-(elem_of_elements _). by rewrite <-(elem_of_elements _).
...@@ -149,7 +149,7 @@ Proof. ...@@ -149,7 +149,7 @@ Proof.
Qed. Qed.
(** * Induction principles *) (** * Induction principles *)
Lemma collection_wf : wf (strict (@subseteq C _)). Lemma collection_wf : wf (@{C}).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C Prop) : Lemma collection_ind (P : C Prop) :
Proper (() ==> iff) P Proper (() ==> iff) P
...@@ -284,4 +284,3 @@ Proof. ...@@ -284,4 +284,3 @@ Proof.
by rewrite set_Exists_elements. by rewrite set_Exists_elements.
Defined. Defined.
End fin_collection. End fin_collection.
This diff is collapsed.
...@@ -17,7 +17,7 @@ Definition card A `{Finite A} := length (enum A). ...@@ -17,7 +17,7 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {| Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x, encode := λ x,
Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A); Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p) decode := λ p, enum A !! pred (Pos.to_nat p)
|}. |}.
Arguments Pos.of_nat : simpl never. Arguments Pos.of_nat : simpl never.
...@@ -134,7 +134,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} : ...@@ -134,7 +134,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} :
0 < card A card B g : B A, Surj (=) g. 0 < card A card B g : B A, Surj (=) g.
Proof. Proof.
intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
exists (λ y : B, from_option id x' (decode_nat (encode_nat y))). exists (λ y : B, default x' (decode_nat (encode_nat y))).
intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2). intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
{ pose proof (encode_lt_card x); lia. } { pose proof (encode_lt_card x); lia. }
exists y. by rewrite Hy2, decode_encode_nat. exists y. by rewrite Hy2, decode_encode_nat.
......
...@@ -131,7 +131,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} : ...@@ -131,7 +131,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
Definition gmap_uncurry `{Countable K1, Countable K2} {A} : Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
gmap (K1 * K2) A gmap K1 (gmap K2 A) := gmap (K1 * K2) A gmap K1 (gmap K2 A) :=
map_fold (λ ii x, let '(i1,i2) := ii in map_fold (λ ii x, let '(i1,i2) := ii in
partial_alter (Some <[i2:=x]> from_option id ) i1) . partial_alter (Some <[i2:=x]> default ) i1) .
Section curry_uncurry. Section curry_uncurry.
Context `{Countable K1, Countable K2} {A : Type}. Context `{Countable K1, Countable K2} {A : Type}.
......
...@@ -25,6 +25,8 @@ Section definitions. ...@@ -25,6 +25,8 @@ Section definitions.
0 < multiplicity x X. 0 < multiplicity x X.
Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, x, Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, x,
multiplicity x X multiplicity x Y. multiplicity x X multiplicity x Y.
Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, x,
multiplicity x X = multiplicity x Y.
Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X, Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
let (X) := X in ''(x,n) map_to_list X; replicate (S n) x. let (X) := X in ''(x,n) map_to_list X; replicate (S n) x.
...@@ -43,7 +45,7 @@ Section definitions. ...@@ -43,7 +45,7 @@ Section definitions.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom _ X. let (X) := X in dom _ X.
End definitions. End definitions.
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq. Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty. Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
...@@ -62,6 +64,10 @@ Proof. ...@@ -62,6 +64,10 @@ Proof.
specialize (HXY x); unfold multiplicity in *; simpl in *. specialize (HXY x); unfold multiplicity in *; simpl in *.
repeat case_match; naive_solver. repeat case_match; naive_solver.
Qed. Qed.
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
Global Instance gmultiset_equivalence : Equivalence (@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
(* Multiplicity *) (* Multiplicity *)
Lemma multiplicity_empty x : multiplicity x = 0. Lemma multiplicity_empty x : multiplicity x = 0.
...@@ -74,14 +80,14 @@ Lemma multiplicity_union X Y x : ...@@ -74,14 +80,14 @@ Lemma multiplicity_union X Y x :
multiplicity x (X Y) = multiplicity x X + multiplicity x Y. multiplicity x (X Y) = multiplicity x X + multiplicity x Y.
Proof. Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl. destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; omega. rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed. Qed.
Lemma multiplicity_difference X Y x : Lemma multiplicity_difference X Y x :
multiplicity x (X Y) = multiplicity x X - multiplicity x Y. multiplicity x (X Y) = multiplicity x X - multiplicity x Y.
Proof. Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl. destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_difference_with. rewrite lookup_difference_with.
destruct (X !! _), (Y !! _); simplify_option_eq; omega. destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Qed. Qed.
(* Collection *) (* Collection *)
...@@ -91,42 +97,42 @@ Proof. done. Qed. ...@@ -91,42 +97,42 @@ Proof. done. Qed.
Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A). Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
Proof. Proof.
split. split.
- intros x. rewrite elem_of_multiplicity, multiplicity_empty. omega. - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
- intros x y. destruct (decide (x = y)) as [->|]. - intros x y. destruct (decide (x = y)) as [->|].
+ rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia. + rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia.
+ rewrite elem_of_multiplicity, multiplicity_singleton_ne by done. + rewrite elem_of_multiplicity, multiplicity_singleton_ne by done.
by split; auto with lia. by split; auto with lia.
- intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega. - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
Qed. Qed.
Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _). Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined. Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
(* Algebraic laws *) (* Algebraic laws *)
Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) (). Global Instance gmultiset_comm : Comm (=@{gmultiset A}) ().
Proof. Proof.
intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Qed. Qed.
Global Instance gmultiset_assoc : Assoc (@eq (gmultiset A)) (). Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) ().
Proof. Proof.
intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Qed. Qed.
Global Instance gmultiset_left_id : LeftId (@eq (gmultiset A)) (). Global Instance gmultiset_left_id : LeftId (=@{gmultiset A}) ().
Proof. Proof.
intros X. apply gmultiset_eq; intros x. intros X. apply gmultiset_eq; intros x.
by rewrite multiplicity_union, multiplicity_empty. by rewrite multiplicity_union, multiplicity_empty.
Qed. Qed.
Global Instance gmultiset_right_id : RightId (@eq (gmultiset A)) (). Global Instance gmultiset_right_id : RightId (=@{gmultiset A}) ().
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed. Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ). Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ).
Proof. Proof.
intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x). intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
rewrite !multiplicity_union. omega. rewrite !multiplicity_union. lia.
Qed. Qed.
Global Instance gmultiset_union_inj_2 X : Inj (=) (=) ( X). Global Instance gmultiset_union_inj_2 X : Inj (=) (=) ( X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed. Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
Lemma gmultiset_non_empty_singleton x : {[ x ]} ( : gmultiset A). Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Proof. Proof.
rewrite gmultiset_eq. intros Hx; generalize (Hx x). rewrite gmultiset_eq. intros Hx; generalize (Hx x).
by rewrite multiplicity_singleton, multiplicity_empty. by rewrite multiplicity_singleton, multiplicity_empty.
...@@ -179,15 +185,15 @@ Proof. ...@@ -179,15 +185,15 @@ Proof.
unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl. unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
rewrite elem_of_list_bind. split. rewrite elem_of_list_bind. split.
- intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia. - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
- intros. destruct (X !! x) as [n|] eqn:Hx; [|omega]. - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
exists (x,n); split; [|by apply elem_of_map_to_list]. exists (x,n); split; [|by apply elem_of_map_to_list].
apply elem_of_replicate; auto with omega. apply elem_of_replicate; auto with lia.
Qed. Qed.
Lemma gmultiset_elem_of_dom x X : x dom (gset A) X x X. Lemma gmultiset_elem_of_dom x X : x dom (gset A) X x X.
Proof. Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity. unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some. destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver omega. destruct (X !! x); naive_solver lia.
Qed. Qed.
(* Properties of the size operation *) (* Properties of the size operation *)
...@@ -231,7 +237,7 @@ Proof. ...@@ -231,7 +237,7 @@ Proof.
Qed. Qed.
(* Order stuff *) (* Order stuff *)
Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _). Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Proof. Proof.
split; [split|]. split; [split|].
- by intros X x. - by intros X x.
...@@ -244,9 +250,9 @@ Lemma gmultiset_subseteq_alt X Y : ...@@ -244,9 +250,9 @@ Lemma gmultiset_subseteq_alt X Y :
map_relation () (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y). map_relation () (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
Proof. Proof.
apply forall_proper; intros x. unfold multiplicity. apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver omega. destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
Qed. Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (@subseteq (gmultiset A) _). Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
Proof. Proof.
refine (λ X Y, cast_if (decide (map_relation () refine (λ X Y, cast_if (decide (map_relation ()
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y)))); (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
...@@ -258,12 +264,12 @@ Proof. apply strict_include. Qed. ...@@ -258,12 +264,12 @@ Proof. apply strict_include. Qed.
Hint Resolve gmultiset_subset_subseteq. Hint Resolve gmultiset_subset_subseteq.
Lemma gmultiset_empty_subseteq X : X. Lemma gmultiset_empty_subseteq X : X.
Proof. intros x. rewrite multiplicity_empty. omega. Qed. Proof. intros x. rewrite multiplicity_empty. lia. Qed.
Lemma gmultiset_union_subseteq_l X Y : X X Y. Lemma gmultiset_union_subseteq_l X Y : X X Y.
Proof. intros x. rewrite multiplicity_union. omega. Qed. Proof. intros x. rewrite multiplicity_union. lia. Qed.
Lemma gmultiset_union_subseteq_r X Y : Y X Y. Lemma gmultiset_union_subseteq_r X Y : Y X Y.
Proof. intros x. rewrite multiplicity_union. omega. Qed. Proof. intros x. rewrite multiplicity_union. lia. Qed.
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2. Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed. Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed.
Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 Y2 X Y1 X Y2. Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 Y2 X Y1 X Y2.
...@@ -272,12 +278,12 @@ Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. ...@@ -272,12 +278,12 @@ Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
Proof. intros. by apply gmultiset_union_mono. Qed. Proof. intros. by apply gmultiset_union_mono. Qed.
Lemma gmultiset_subset X Y : X Y size X < size Y X Y. Lemma gmultiset_subset X Y : X Y size X < size Y X Y.
Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed. Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
Lemma gmultiset_union_subset_l X Y : Y X X Y. Lemma gmultiset_union_subset_l X Y : Y X X Y.
Proof. Proof.
intros HY%gmultiset_size_non_empty_iff. intros HY%gmultiset_size_non_empty_iff.
apply gmultiset_subset; auto using gmultiset_union_subseteq_l. apply gmultiset_subset; auto using gmultiset_union_subseteq_l.
rewrite gmultiset_size_union; omega. rewrite gmultiset_size_union; lia.
Qed. Qed.
Lemma gmultiset_union_subset_r X Y : X Y X Y. Lemma gmultiset_union_subset_r X Y : X Y X Y.
Proof. rewrite (comm_L ()). apply gmultiset_union_subset_l. Qed. Proof. rewrite (comm_L ()). apply gmultiset_union_subset_l. Qed.
...@@ -286,9 +292,9 @@ Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X. ...@@ -286,9 +292,9 @@ Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X.
Proof. Proof.
rewrite elem_of_multiplicity. split. rewrite elem_of_multiplicity. split.
- intros Hx y; destruct (decide (x = y)) as [->|]. - intros Hx y; destruct (decide (x = y)) as [->|].
+ rewrite multiplicity_singleton; omega. + rewrite multiplicity_singleton; lia.
+ rewrite multiplicity_singleton_ne by done; omega. + rewrite multiplicity_singleton_ne by done; lia.
- intros Hx. generalize (Hx x). rewrite multiplicity_singleton. omega. - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
Qed. Qed.
Lemma gmultiset_elem_of_subseteq X1 X2 x : x X1 X1 X2 x X2. Lemma gmultiset_elem_of_subseteq X1 X2 x : x X1 X1 X2 x X2.
...@@ -297,7 +303,7 @@ Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed. ...@@ -297,7 +303,7 @@ Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.
Lemma gmultiset_union_difference X Y : X Y Y = X Y X. Lemma gmultiset_union_difference X Y : X Y Y = X Y X.
Proof. Proof.
intros HXY. apply gmultiset_eq; intros x; specialize (HXY x). intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
rewrite multiplicity_union, multiplicity_difference; omega. rewrite multiplicity_union, multiplicity_difference; lia.
Qed. Qed.
Lemma gmultiset_union_difference' x Y : x Y Y = {[ x ]} Y {[ x ]}. Lemma gmultiset_union_difference' x Y : x Y Y = {[ x ]} Y {[ x ]}.
Proof. Proof.
...@@ -308,14 +314,14 @@ Qed. ...@@ -308,14 +314,14 @@ Qed.
Lemma gmultiset_size_difference X Y : Y X size (X Y) = size X - size Y. Lemma gmultiset_size_difference X Y : Y X size (X Y) = size X - size Y.
Proof. Proof.
intros HX%gmultiset_union_difference. intros HX%gmultiset_union_difference.
rewrite HX at 2; rewrite gmultiset_size_union. omega. rewrite HX at 2; rewrite gmultiset_size_union. lia.
Qed. Qed.
Lemma gmultiset_non_empty_difference X Y : X Y Y X . Lemma gmultiset_non_empty_difference X Y : X Y Y X .
Proof. Proof.
intros [_ HXY2] Hdiff; destruct HXY2; intros x. intros [_ HXY2] Hdiff; destruct HXY2; intros x.
generalize (f_equal (multiplicity x) Hdiff). generalize (f_equal (multiplicity x) Hdiff).
rewrite multiplicity_difference, multiplicity_empty; omega. rewrite multiplicity_difference, multiplicity_empty; lia.
Qed. Qed.
Lemma gmultiset_difference_subset X Y : X X Y Y X Y. Lemma gmultiset_difference_subset X Y : X X Y Y X Y.
...@@ -342,7 +348,7 @@ Proof. ...@@ -342,7 +348,7 @@ Proof.
Qed. Qed.
(* Well-foundedness *) (* Well-foundedness *)
Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)). Lemma gmultiset_wf : wf (@{gmultiset A}).
Proof. Proof.
apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf. apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed. Qed.
......
...@@ -26,7 +26,7 @@ Qed. ...@@ -26,7 +26,7 @@ Qed.
(** * Fresh elements *) (** * Fresh elements *)
Section Fresh. Section Fresh.
Context `{FinCollection A C, Infinite A, !RelDecision (@elem_of A C _)}. Context `{FinCollection A C, Infinite A, !RelDecision (@{C})}.
Definition fresh_generic_body (s : C) (rec : s', s' s nat A) (n : nat) : A := Definition fresh_generic_body (s : C) (rec : s', s' s nat A) (n : nat) : A :=
let cand := inject n in let cand := inject n in
...@@ -52,15 +52,15 @@ Section Fresh. ...@@ -52,15 +52,15 @@ Section Fresh.
revert n. revert n.
induction s as [s IH] using (well_founded_ind collection_wf); intros n. induction s as [s IH] using (well_founded_ind collection_wf); intros n.
setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body. setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
destruct decide as [Hcase|Hcase]; [|by eauto with omega]. destruct decide as [Hcase|Hcase]; [|by eauto with lia].
destruct (IH _ (subset_difference_elem_of Hcase) (S n)) destruct (IH _ (subset_difference_elem_of Hcase) (S n))
as (m & Hmbound & Heqfix & Hnotin & Hinbelow). as (m & Hmbound & Heqfix & Hnotin & Hinbelow).
exists m; repeat split; auto with omega. exists m; repeat split; auto with lia.
- rewrite not_elem_of_difference, elem_of_singleton in Hnotin. - rewrite not_elem_of_difference, elem_of_singleton in Hnotin.
destruct Hnotin as [?|?%inject_injective]; auto with omega. destruct Hnotin as [?|?%inject_injective]; auto with lia.
- intros i Hibound. - intros i Hibound.
destruct (decide (i = n)) as [<-|Hneq]; [by auto|]. destruct (decide (i = n)) as [<-|Hneq]; [by auto|].
assert (inject i s {[inject n]}) by auto with omega. assert (inject i s {[inject n]}) by auto with lia.
set_solver. set_solver.
Qed. Qed.
...@@ -76,8 +76,8 @@ Section Fresh. ...@@ -76,8 +76,8 @@ Section Fresh.
destruct (fresh_generic_fixpoint_spec Y 0) destruct (fresh_generic_fixpoint_spec Y 0)
as (mY & _ & -> & HnotinY & HbelowinY). as (mY & _ & -> & HnotinY & HbelowinY).
destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto. destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
+ contradict HnotinX. rewrite HeqXY. apply HbelowinY; omega. + contradict HnotinX. rewrite HeqXY. apply HbelowinY; lia.
+ contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; omega. + contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; lia.
- intros X. unfold fresh, fresh_generic. - intros X. unfold fresh, fresh_generic.
destruct (fresh_generic_fixpoint_spec X 0) destruct (fresh_generic_fixpoint_spec X 0)
as (m & _ & -> & HnotinX & HbelowinX); auto. as (m & _ & -> & HnotinX & HbelowinX); auto.
......
This diff is collapsed.
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with (** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *) constructed finite sets do so as well. *)
From stdpp Require Export fin_map_dom. From stdpp Require Export countable fin_map_dom.
(* FIXME: This file needs a 'Proof Using' hint. *) (* FIXME: This file needs a 'Proof Using' hint. *)
Record mapset (M : Type Type) : Type := Record mapset (M : Type Type) : Type :=
...@@ -76,16 +76,19 @@ Section deciders. ...@@ -76,16 +76,19 @@ Section deciders.
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
abstract congruence. abstract congruence.
Defined. Defined.
Global Instance mapset_equiv_dec : RelDecision (@equiv (mapset M)_) | 1. Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
inj_countable mapset_car (Some Mapset) _.
Next Obligation. by intros ? ? []. Qed.
Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1.
Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined. Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
Global Instance mapset_elem_of_dec : RelDecision (@elem_of _ (mapset M) _) | 1. Global Instance mapset_elem_of_dec : RelDecision (@{mapset M}) | 1.
Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined. Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _). Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Proof. Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = ))); refine (λ X1 X2, cast_if (decide (X1 X2 = )));
abstract (by rewrite disjoint_intersection_L). abstract (by rewrite disjoint_intersection_L).
Defined. Defined.
Global Instance mapset_subseteq_dec : RelDecision (@subseteq (mapset M) _). Global Instance mapset_subseteq_dec : RelDecision (@{mapset M}).
Proof. Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = X2))); refine (λ X1 X2, cast_if (decide (X1 X2 = X2)));
abstract (by rewrite subseteq_union_L). abstract (by rewrite subseteq_union_L).
......
From stdpp Require Export countable coPset.
Set Default Proof Using "Type".
Definition namespace := list positive.
Instance namespace_eq_dec : EqDecision namespace := _.
Instance namespace_countable : Countable namespace := _.
Typeclasses Opaque namespace.
Definition nroot : namespace := nil.
Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count.
Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
Notation "N .@ x" := (ndot N x)
(at level 19, left associativity, format "N .@ x") : stdpp_scope.
Notation "(.@)" := ndot (only parsing) : stdpp_scope.
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ## nclose N2.
Section namespace.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types N : namespace.
Implicit Types E : coPset.
Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
Lemma nclose_nroot : nroot = (:coPset).
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N (N:coPset).
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Lemma nclose_subseteq N x : N.@x (N : coPset).
Proof.
intros p. unfold up_close. rewrite !nclose_eq, !ndot_eq.
unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
{ by exists [encode x]. }
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Lemma nclose_subseteq' E N x : N E N.@x E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N.@x) (N:coPset).
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite ( N : coPset).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
Lemma ndot_ne_disjoint N x y : x y N.@x ## N.@y.
Proof.
intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
Qed.
Lemma ndot_preserve_disjoint_l N E x : N ## E N.@x ## E.
Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
Lemma ndot_preserve_disjoint_r N E x : E ## N E ## N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma namespace_subseteq_difference E1 E2 E3 :
E1 ## E3 E1 E2 E1 E2 E3.
Proof. set_solver. Qed.
Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 E3 E1 E2 E3.
Proof. set_solver. Qed.
Lemma ndisj_difference_l E N1 N2 : N2 (N1 : coPset) E N1 ## N2.
Proof. set_solver. Qed.
End namespace.
(* The hope is that registering these will suffice to solve most goals
of the forms:
- [N1 ## N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj.
Hint Resolve namespace_subseteq_difference : ndisj.
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
Ltac solve_ndisj :=
repeat match goal with
| H : _ _ _ |- _ => apply union_subseteq in H as [??]
end;
solve [eauto 10 with ndisj].
Hint Extern 1000 => solve_ndisj : solve_ndisj.
From stdpp Require Import numbers.
(** The class [NatCancel m n m' n'] is a simple canceler for natural numbers
implemented using type classes.
Input: [m], [n]; output: [m'], [n'].
It turns an equality [n = m] into an equality [n' = m'] by canceling out terms
that appear on both sides of the equality. We provide instances to handle the
following connectives over natural numbers:
n := 0 | t | n + m | S m
Here, [t] represents arbitrary terms that do not fit the grammar. The instances
the class perform a depth-first traversal (from left to right) through [n] and
try to cancel each leaf in [m]. This implies that the shape of the original
expressions [n] and [m] are preserved as much as possible. For example,
canceling:
S (S m2) + (k1 + (S k2 + k3)) + n1 = 2 + S ((n1 + S n2) + S (S m1 + m2))
Results in:
k1 + (k2 + k3) = S (n2 + S (S m1))
The instances are setup up so that canceling is performed in two stages.
- In the first stage, using the class [NatCancelL], it traverses [m] w.r.t. [S]
and [+].
- In the second stage, for each leaf (i.e. a constant or arbitrary term)
obtained by the traversal in stage 1, it uses the class [NatCancelR] to
cancel the leaf in [n].
Be warned: Since the canceler is implemented using type classes it should only
be used it either of the inputs is relatively small. For bigger inputs, an
approach based on reflection would be better, but for small inputs, the overhead
of reification will probably not be worth it. *)
Class NatCancel (m n m' n' : nat) := nat_cancel : m' + n = m + n'.
Hint Mode NatCancel ! ! - - : typeclass_instances.
Module nat_cancel.
Class NatCancelL (m n m' n' : nat) := nat_cancel_l : m' + n = m + n'.
Hint Mode NatCancelL ! ! - - : typeclass_instances.
Class NatCancelR (m n m' n' : nat) := nat_cancel_r : NatCancelL m n m' n'.
Hint Mode NatCancelR ! ! - - : typeclass_instances