...
 
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.
This diff is collapsed.
......@@ -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.
......
This diff is collapsed.
......@@ -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 (@{C}) | 100.
Proof.
refine (λ x X, cast_if (decide_rel () x (elements X)));
by rewrite <-(elem_of_elements _).
......@@ -149,7 +149,7 @@ Proof.
Qed.
(** * 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.
Lemma collection_ind (P : C Prop) :
Proper (() ==> iff) P
......@@ -284,4 +284,3 @@ Proof.
by rewrite set_Exists_elements.
Defined.
End fin_collection.
This diff is collapsed.
......@@ -17,7 +17,7 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {|
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)
|}.
Arguments Pos.of_nat : simpl never.
......@@ -134,7 +134,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} :
0 < card A card B g : B A, Surj (=) g.
Proof.
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).
{ pose proof (encode_lt_card x); lia. }
exists y. by rewrite Hy2, decode_encode_nat.
......
......@@ -131,7 +131,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
gmap (K1 * K2) A gmap K1 (gmap K2 A) :=
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.
Context `{Countable K1, Countable K2} {A : Type}.
......
......@@ -25,6 +25,8 @@ Section definitions.
0 < multiplicity x X.
Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, x,
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,
let (X) := X in ''(x,n) map_to_list X; replicate (S n) x.
......@@ -62,6 +64,10 @@ Proof.
specialize (HXY x); unfold multiplicity in *; simpl in *.
repeat case_match; naive_solver.
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 *)
Lemma multiplicity_empty x : multiplicity x = 0.
......@@ -74,14 +80,14 @@ Lemma multiplicity_union X Y x :
multiplicity x (X Y) = multiplicity x X + multiplicity x Y.
Proof.
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.
Lemma multiplicity_difference X Y x :
multiplicity x (X Y) = multiplicity x X - multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_difference_with.
destruct (X !! _), (Y !! _); simplify_option_eq; omega.
destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Qed.
(* Collection *)
......@@ -91,42 +97,42 @@ Proof. done. Qed.
Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
Proof.
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 [->|].
+ rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia.
+ rewrite elem_of_multiplicity, multiplicity_singleton_ne by done.
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.
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.
(* Algebraic laws *)
Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) ().
Global Instance gmultiset_comm : Comm (=@{gmultiset A}) ().
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.
Global Instance gmultiset_assoc : Assoc (@eq (gmultiset A)) ().
Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) ().
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.
Global Instance gmultiset_left_id : LeftId (@eq (gmultiset A)) ().
Global Instance gmultiset_left_id : LeftId (=@{gmultiset A}) ().
Proof.
intros X. apply gmultiset_eq; intros x.
by rewrite multiplicity_union, multiplicity_empty.
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.
Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ).
Proof.
intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
rewrite !multiplicity_union. omega.
rewrite !multiplicity_union. lia.
Qed.
Global Instance gmultiset_union_inj_2 X : Inj (=) (=) ( X).
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.
rewrite gmultiset_eq. intros Hx; generalize (Hx x).
by rewrite multiplicity_singleton, multiplicity_empty.
......@@ -179,15 +185,15 @@ Proof.
unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
rewrite elem_of_list_bind. split.
- 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].
apply elem_of_replicate; auto with omega.
apply elem_of_replicate; auto with lia.
Qed.
Lemma gmultiset_elem_of_dom x X : x dom (gset A) X x X.
Proof.
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 !! x); naive_solver omega.
destruct (X !! x); naive_solver lia.
Qed.
(* Properties of the size operation *)
......@@ -231,7 +237,7 @@ Proof.
Qed.
(* Order stuff *)
Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _).
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Proof.
split; [split|].
- by intros X x.
......@@ -244,9 +250,9 @@ Lemma gmultiset_subseteq_alt X Y :
map_relation () (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
Proof.
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.
Global Instance gmultiset_subseteq_dec : RelDecision (@subseteq (gmultiset A) _).
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation ()
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
......@@ -258,12 +264,12 @@ Proof. apply strict_include. Qed.
Hint Resolve gmultiset_subset_subseteq.
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.
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.
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.
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.
......@@ -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.
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.
Proof.
intros HY%gmultiset_size_non_empty_iff.
apply gmultiset_subset; auto using gmultiset_union_subseteq_l.
rewrite gmultiset_size_union; omega.
rewrite gmultiset_size_union; lia.
Qed.
Lemma gmultiset_union_subset_r X Y : X Y X Y.
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.
Proof.
rewrite elem_of_multiplicity. split.
- intros Hx y; destruct (decide (x = y)) as [->|].
+ rewrite multiplicity_singleton; omega.
+ rewrite multiplicity_singleton_ne by done; omega.
- intros Hx. generalize (Hx x). rewrite multiplicity_singleton. omega.
+ rewrite multiplicity_singleton; lia.
+ rewrite multiplicity_singleton_ne by done; lia.
- intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
Qed.
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.
Lemma gmultiset_union_difference X Y : X Y Y = X Y X.
Proof.
intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
rewrite multiplicity_union, multiplicity_difference; omega.
rewrite multiplicity_union, multiplicity_difference; lia.
Qed.
Lemma gmultiset_union_difference' x Y : x Y Y = {[ x ]} Y {[ x ]}.
Proof.
......@@ -308,14 +314,14 @@ Qed.
Lemma gmultiset_size_difference X Y : Y X size (X Y) = size X - size Y.
Proof.
intros HX%gmultiset_union_difference.
rewrite HX at 2; rewrite gmultiset_size_union. omega.
rewrite HX at 2; rewrite gmultiset_size_union. lia.
Qed.
Lemma gmultiset_non_empty_difference X Y : X Y Y X .
Proof.
intros [_ HXY2] Hdiff; destruct HXY2; intros x.
generalize (f_equal (multiplicity x) Hdiff).
rewrite multiplicity_difference, multiplicity_empty; omega.
rewrite multiplicity_difference, multiplicity_empty; lia.
Qed.
Lemma gmultiset_difference_subset X Y : X X Y Y X Y.
......@@ -342,7 +348,7 @@ Proof.
Qed.
(* Well-foundedness *)
Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)).
Lemma gmultiset_wf : wf (@{gmultiset A}).
Proof.
apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
......
......@@ -26,7 +26,7 @@ Qed.
(** * Fresh elements *)
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 :=
let cand := inject n in
......@@ -52,15 +52,15 @@ Section Fresh.
revert n.
induction s as [s IH] using (well_founded_ind collection_wf); intros n.
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))
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.
destruct Hnotin as [?|?%inject_injective]; auto with omega.
destruct Hnotin as [?|?%inject_injective]; auto with lia.
- intros i Hibound.
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.
Qed.
......@@ -76,8 +76,8 @@ Section Fresh.
destruct (fresh_generic_fixpoint_spec Y 0)
as (mY & _ & -> & HnotinY & HbelowinY).
destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
+ contradict HnotinX. rewrite HeqXY. apply HbelowinY; omega.
+ contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; omega.
+ contradict HnotinX. rewrite HeqXY. apply HbelowinY; lia.
+ contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; lia.
- intros X. unfold fresh, fresh_generic.
destruct (fresh_generic_fixpoint_spec X 0)
as (m & _ & -> & HnotinX & HbelowinX); auto.
......
This diff is collapsed.
......@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
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. *)
Record mapset (M : Type Type) : Type :=
......@@ -76,16 +76,19 @@ Section deciders.
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
abstract congruence.
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.
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.
Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _).
Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Global Instance mapset_subseteq_dec : RelDecision (@subseteq (mapset M) _).
Global Instance mapset_subseteq_dec : RelDecision (@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = X2)));
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.
Existing Instance nat_cancel_r | 100.
(** The implementation of the canceler is highly non-deterministic, but since
it will always succeed, no backtracking will ever be performed. In order to
avoid issues like:
https://gitlab.mpi-sws.org/FP/iris-coq/issues/153
we wrap the entire canceler in the [NoBackTrack] class. *)
Instance nat_cancel_start m n m' n' :
NoBackTrack (NatCancelL m n m' n') NatCancel m n m' n'.
Proof. by intros [?]. Qed.
Class MakeNatS (n1 n2 m : nat) := make_nat_S : m = n1 + n2.
Instance make_nat_S_0_l n : MakeNatS 0 n n.
Proof. done. Qed.
Instance make_nat_S_1 n : MakeNatS 1 n (S n).
Proof. done. Qed.
Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
Proof. done. Qed.
Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
Proof. done. Qed.
Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
Proof. by unfold NatCancelR, NatCancelL. Qed.
Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
Proof. by unfold NatCancelR. Qed.
Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
NatCancelR m n1 m' n1' NatCancelR m' n2 m'' n2'
MakeNatPlus n1' n2' n1'n2' NatCancelR m (n1 + n2) m'' n1'n2' | 2.
Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. lia. Qed.
Instance nat_cancel_leaf_S_here m n m' n' :
NatCancelR m n m' n' NatCancelR (S m) (S n) m' n' | 3.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
Instance nat_cancel_leaf_S_else m n m' n' :
NatCancelR m n m' n' NatCancelR m (S n) m' (S n') | 4.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
quite a bit, e.g. when canceling constants in constants. *)
Instance nat_cancel_S_both m n m' n' :
NatCancelL m n m' n' NatCancelL (S m) (S n) m' n' | 1.
Proof. unfold NatCancelL. lia. Qed.
Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
NatCancelL m1 n m1' n' NatCancelL m2 n' m2' n''
MakeNatPlus m1' m2' m1'm2' NatCancelL (m1 + m2) n m1'm2' n'' | 2.
Proof. unfold NatCancelL, MakeNatPlus. lia. Qed.
Instance nat_cancel_S m m' m'' Sm' n n' n'' :
NatCancelL m n m' n' NatCancelR 1 n' m'' n''
MakeNatS m'' m' Sm' NatCancelL (S m) n Sm' n'' | 3.
Proof. unfold NatCancelR, NatCancelL, MakeNatS. lia. Qed.
End nat_cancel.
......@@ -35,7 +35,7 @@ Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
match t with
| NMap o t =>
default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
from_option (λ x, [(0,x)]) [] o ++ (prod_map Npos id <$> map_to_list t)
end.
Instance Nomap: OMap Nmap := λ A B f t,
match t with NMap o t => NMap (o = f) (omap f t) end.
......
......@@ -48,11 +48,11 @@ Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
Proof.
assert ( x y (p : x y) y' (q : x y'),
y = y' eq_dep nat (le x) y p y' q) as aux.
{ fix 3. intros x ? [|y p] ? [|y' q].
{ fix FIX 3. intros x ? [|y p] ? [|y' q].
- done.
- clear nat_le_pi. intros; exfalso; auto with lia.
- clear nat_le_pi. intros; exfalso; auto with lia.
- injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
- clear FIX. intros; exfalso; auto with lia.
- clear FIX. intros; exfalso; auto with lia.
- injection 1. intros Hy. by case (FIX x y p y' q Hy). }
intros x y p q.
by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed.
......@@ -223,10 +223,10 @@ Proof. by injection 1. Qed.
Instance N_eq_dec: EqDecision N := N.eq_dec.
Program Instance N_le_dec : RelDecision N.le := λ x y,
match Ncompare x y with Gt => right _ | _ => left _ end.
match N.compare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
match Ncompare x y with Lt => left _ | _ => right _ end.
match N.compare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
Instance N_inhabited: Inhabited N := populate 1%N.
Instance N_le_po: PartialOrder ()%N.
......@@ -418,19 +418,17 @@ Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y x + z < y + z.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
Instance: Inj (=) (=) Qcopp.
Instance Qcopp_inj : Inj (=) (=) Qcopp.
Proof.
intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
Instance: z, Inj (=) (=) (Qcplus z).
Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
Proof.
intros z x y H. by apply (anti_symm ());
rewrite (Qcplus_le_mono_l _ _ z), H.
intros x y H. by apply (anti_symm ());rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
Instance: z, Inj (=) (=) (λ x, x + z).
Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
Proof.
intros z x y H. by apply (anti_symm ());
rewrite (Qcplus_le_mono_r _ _ z), H.
intros x y H. by apply (anti_symm ()); rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x 0 y 0 < x + y.
Proof.
......@@ -543,11 +541,14 @@ Next Obligation.
<-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.
Notation "1" := Qp_one : Qp_scope.
Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
Infix "*" := Qp_mult : Qp_scope.
Infix "/" := Qp_div : Qp_scope.
Notation "1" := Qp_one : Qp_scope.
Notation "2" := (1 + 1)%Qp : Qp_scope.
Notation "3" := (1 + 2)%Qp : Qp_scope.
Notation "4" := (1 + 3)%Qp : Qp_scope.
Lemma Qp_eq x y : x = y Qp_car x = Qp_car y.
Proof.
......@@ -565,6 +566,10 @@ Instance Qp_plus_assoc : Assoc (=) Qp_plus.
Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
Instance Qp_plus_comm : Comm (=) Qp_plus.
Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
Instance Qp_plus_inj_l p : Inj (=)