...
 
Commits (408)
# Enable syntax highlighting.
*.v gitlab-language=coq *.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
*.vo *.vo
*.vos
*.vok
*.vio *.vio
*.v.d *.v.d
.coqdeps.d .coqdeps.d
.Makefile.coq.d
*.glob *.glob
*.cache *.cache
*.aux *.aux
...@@ -14,5 +17,5 @@ Makefile.coq ...@@ -14,5 +17,5 @@ Makefile.coq
Makefile.coq.conf Makefile.coq.conf
*.crashcoqide *.crashcoqide
html/ html/
build-dep/ builddep/
_opam _opam
...@@ -16,63 +16,40 @@ variables: ...@@ -16,63 +16,40 @@ variables:
cache: cache:
key: "$CI_JOB_NAME" key: "$CI_JOB_NAME"
paths: paths:
- opamroot/ - _opam/
only: only:
- master - master@iris/stdpp
- /^ci/ - /^ci/@iris/stdpp
except: except:
- triggers - triggers
- schedules - schedules
- api
## Build jobs ## Build jobs
build-coq.dev: build-coq.dev:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev" OPAM_PINS: "coq version dev"
MANGLE_NAMES: "1"
CI_COQCHK: "1" CI_COQCHK: "1"
build-coq.8.9.0: build-coq.8.12.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.9.0" OPAM_PINS: "coq version 8.12.0"
DENY_WARNINGS: "1"
OPAM_PKG: "coq-stdpp" OPAM_PKG: "coq-stdpp"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp" DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
tags: tags:
- fp-timing - fp-timing
build-coq.8.8.2: build-coq.8.11.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.2" OPAM_PINS: "coq version 8.11.2"
build-coq.8.8.1: build-coq.8.10.2:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.1" OPAM_PINS: "coq version 8.10.2"
build-coq.8.8.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
build-coq.8.7.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.0"
This diff is collapsed.
All files in this development are distributed under the terms of the BSD All files in this development are distributed under the terms of the 3-clause
license, included below. BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
------------------------------------------------------------------------------ Copyright: std++ developers and contributors
BSD LICENCE ------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met: modification, are permitted provided that the following conditions are met:
...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met: ...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright * Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution. documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the * Neither the name of the copyright holder nor the names of its contributors
names of its contributors may be used to endorse or promote products may be used to endorse or promote products derived from this software
derived from this software without specific prior written permission. without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Forward most targets to Coq makefile (with some trick to make this phony) # Default target
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq all: Makefile.coq
+@make -f Makefile.coq all +@make -f Makefile.coq all
.PHONY: all .PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@make -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq clean: Makefile.coq
+@make -f Makefile.coq clean +@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean .PHONY: clean
# Create Coq Makefile. # Create Coq Makefile.
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile OPAMFILES=$(wildcard *.opam)
@echo "# Creating build-dep package." BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam builddep/%-builddep.opam: %.opam Makefile
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @echo "# Creating builddep package for $<."
@mkdir -p builddep
build-dep: build-dep/opam phony @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# 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 itself. @# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \ @echo "# Installing builddep packages."
if opam --version | grep "^1\." -q; then \ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \ .PHONY: builddep
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \ # Backwards compatibility target
else \ build-dep: builddep
opam install $(OPAMFLAGS) build-dep/; \ .PHONY: build-dep
fi
# Some files that do *not* need to be forwarded to Makefile.coq.
# Some files that do *not* need to be forwarded to Makefile.coq # ("::" lets Makefile.local overwrite this.)
Makefile: ; Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
...@@ -5,10 +5,14 @@ real-all: $(if $(NO_TEST),,test) ...@@ -5,10 +5,14 @@ real-all: $(if $(NO_TEST),,test)
TESTFILES=$(wildcard tests/*.v) TESTFILES=$(wildcard tests/*.v)
test: $(TESTFILES:.v=.vo) test: $(TESTFILES:.v=.vo)
# Make sure everything imports the options.
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
done
.PHONY: test .PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1) COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o) COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES) tests/.coqdeps.d: $(TESTFILES)
......
...@@ -45,11 +45,11 @@ Notably: ...@@ -45,11 +45,11 @@ Notably:
This version is known to compile with: This version is known to compile with:
- Coq version 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2 / 8.9.0 - Coq version 8.10.2 / 8.11.2 / 8.12.0
## Installing via opam ## Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add To obtain the latest stable release via opam (2.0.0 or newer), you have to add
the Coq opam repository: the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
...@@ -79,3 +79,9 @@ your account. Then you can fork the ...@@ -79,3 +79,9 @@ your account. Then you can fork the
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your [Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
changes in your fork, and create a merge request. changes in your fork, and create a merge request.
## Common problems
On Windows, differences in line endings may cause tests to fail. This can be
fixed by setting Git's autocrlf option to true:
git config --global core.autocrlf true
-Q theories stdpp -Q theories stdpp
# "Declare Scope" does not exist yet in 8.9
-arg -w -arg -undeclared-scope theories/options.v
theories/base.v theories/base.v
theories/tactics.v theories/tactics.v
theories/option.v theories/option.v
...@@ -33,10 +33,12 @@ theories/numbers.v ...@@ -33,10 +33,12 @@ theories/numbers.v
theories/nmap.v theories/nmap.v
theories/zmap.v theories/zmap.v
theories/coPset.v theories/coPset.v
theories/coGset.v
theories/lexico.v theories/lexico.v
theories/propset.v theories/propset.v
theories/decidable.v theories/decidable.v
theories/list.v theories/list.v
theories/list_numbers.v
theories/functions.v theories/functions.v
theories/hlist.v theories/hlist.v
theories/sorting.v theories/sorting.v
...@@ -44,3 +46,4 @@ theories/infinite.v ...@@ -44,3 +46,4 @@ theories/infinite.v
theories/nat_cancel.v theories/nat_cancel.v
theories/namespaces.v theories/namespaces.v
theories/telescopes.v theories/telescopes.v
theories/binders.v
This project contains an extended "Standard Library" for Coq called coq-std++. opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The std++ team"
license: "BSD-3-Clause"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
synopsis: "std++ is an extended \"Standard Library\" for Coq"
description: """
The key features of this library are as follows: The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data - It provides a great number of definitions and lemmas for common data
...@@ -17,3 +26,11 @@ The key features of this library are as follows: ...@@ -17,3 +26,11 @@ The key features of this library are as follows:
for proving compatibility of functions with respect to relations, and a solver for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations. `set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free. - It is entirely dependency- and axiom-free.
"""
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
opam-version: "1.2"
name: "coq-stdpp"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/iris/stdpp.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") }
]
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps fin_map_dom.
Section map_disjoint. Section map_disjoint.
Context `{FinMap K M}. Context `{FinMap K M}.
...@@ -11,3 +11,14 @@ Section map_disjoint. ...@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None. m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed. Proof. intros. solve_map_disjoint. Qed.
End map_disjoint. End map_disjoint.
Section map_dom.
Context `{FinMapDom K M D}.
Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
{[i; j]} dom D (<[i:=x]> (<[j:=y]> ( : M A))).
Proof. set_solver. Qed.
Lemma set_solver_dom_disjoint {A} (X : D) : dom D ( : M A) ## X.
Proof. set_solver. Qed.
End map_dom.
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
From stdpp Require prelude strings list.
(** Check that we always get the [length] function on lists, not on strings. *)
Module test1.
Import stdpp.base.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.base.
Check length.
End test1.
Module test2.
Import stdpp.prelude.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test2.
Module test3.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test3.
Module test4.
Import stdpp.list.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.list.
Check length.
End test4.
From stdpp Require Import gmultiset.
Section test.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Lemma test1 x y X : {[x]} ({[y]} X) .
Proof. multiset_solver. Qed.
Lemma test2 x y X : {[x]} ({[y]} X) = {[y]} ({[x]} X).
Proof. multiset_solver. Qed.
Lemma test3 x : {[x]} @{gmultiset A} .
Proof. multiset_solver. Qed.
Lemma test4 x y z X Y :
{[z]} X = {[y]} Y
{[x]} ({[z]} X) = {[y]} ({[x]} Y).
Proof. multiset_solver. Qed.
Lemma test5 X x : X = {[x]} X @{gmultiset A} .
Proof. multiset_solver. Qed.
End test.
From stdpp Require Import base tactics.
(** Test parsing of variants of [(≡)] notation. *)
Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (@{A})} (x : A) :
x @{A} x (@{A}) x x (x .) x (. x) x
((x @{A} x)) ((@{A})) x x ((x .)) x ((. x)) x
( x @{A} x) ( x .) x
(x @{A} x ) (@{A} ) x x (. x ) x.
Proof. naive_solver. Qed.
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
le
: nat → nat → Prop
lt
: nat → nat → Prop
From stdpp Require base numbers prelude.
(** Check that we always get the [le] and [lt] functions on [nat]. *)
Module test1.
Import stdpp.base.
Check le.
Check lt.
End test1.
Module test2.
Import stdpp.prelude.
Check le.
Check lt.
End test2.
Module test3.
Import stdpp.numbers.
Check le.
Check lt.
End test3.
Module test4.
Import stdpp.list.
Check le.
Check lt.
End test4.
From stdpp Require Import sets.
Lemma foo `{Set_ A C} (x : A) (X Y : C) : x X Y x X.
Proof. intros Hx. set_unfold in Hx. tauto. Qed.
From stdpp Require Import namespaces strings.
Lemma test1 (N1 N2 : namespace) :
N1 ## N2 N1 @{coPset} N2.
Proof. solve_ndisj. Qed.
Lemma test2 (N1 N2 : namespace) :
N1 ## N2 N1.@"x" @{coPset} N1.@"y" N2.
Proof. solve_ndisj. Qed.
Lemma test3 (N : namespace) :
N @{coPset} N.@"x".
Proof. solve_ndisj. Qed.
Lemma test4 (N : namespace) :
N @{coPset} N.@"x" N.@"y".
Proof. solve_ndisj. Qed.
Lemma test5 (N1 N2 : namespace) :
N1 N2 @{coPset} N1.@"x" N2 N1.@"y".
Proof. solve_ndisj. Qed.
The command has indeed failed with message:
Failed to progress.
The command has indeed failed with message:
Failed to progress.
The command has indeed failed with message:
Failed to progress.
From stdpp Require Import tactics.
Goal forall P1 P2 P3 P4 (P: Prop),
P1 (Is_true (P2 || P3)) P4
(P1 P)
(P2 P)
(P3 P)
(P4 P)
P.
Proof.
intros * HH X1 X2 X3 X4.
destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
P1 P2
P3 P4
(P1 P3 P)
(P1 P4 P)
(P2 P3 P)
(P2 P4 P)
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
id (P1 P2)
id (P3 P4)
(P1 P3 P)
(P1 P4 P)
(P2 P3 P)
(P2 P4 P)
P.
Proof.
intros * HH1 HH2 X1 X2 X3 X4.
Fail progress destruct_or?.
Fail progress destruct_or!.
destruct_or! HH1; destruct_or! HH2;
[ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4,
P1 (Is_true (P2 && P3)) P4
P1 P2 P3.
Proof.
intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
destruct_and?. Fail destruct_and!. assumption.
Qed.
From stdpp Require Import tactics telescopes. From stdpp Require Import tactics telescopes.
Local Unset Mangle Names. (* for stable goal printing *)
Section accessor. Section accessor.
(* This is like Iris' accessors, but in Prop. Just to play with telescopes. *) (* This is like Iris' accessors, but in Prop. Just to play with telescopes. *)
Definition accessor {X : tele} (α β γ : X Prop) : Prop := Definition accessor {X : tele} (α β γ : X Prop) : Prop :=
......
This diff is collapsed.
(** This file implements a type [binder] with elements [BAnon] for the
anonymous binder, and [BNamed] for named binders. This type is isomorphic to
[option string], but we use a special type so that we can define [BNamed] as
a coercion.
This library is used in various Iris developments, like heap-lang, LambdaRust,
Iron, Fairis. *)
From stdpp Require Export strings.
From stdpp Require Import sets countable finite fin_maps.
From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
Declare Scope binder_scope.
Delimit Scope binder_scope with binder.
Inductive binder := BAnon | BNamed :> string binder.
Bind Scope binder_scope with binder.
Notation "<>" := BAnon : binder_scope.
Instance binder_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Instance binder_inhabited : Inhabited binder := populate BAnon.
Instance binder_countable : Countable binder.
Proof.
refine (inj_countable'
(λ b, match b with BAnon => None | BNamed s => Some s end)
(λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
Qed.
(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [b], respectively [bs], are the binders that are being
added. *)
Definition cons_binder (b : binder) (ss : list string) : list string :=
match b with BAnon => ss | BNamed s => s :: ss end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
Infix "+b+" := app_binder (at level 60, right associativity).
Instance set_unfold_cons_binder s b ss P :
SetUnfoldElemOf s ss P SetUnfoldElemOf s (b :b: ss) (BNamed s = b P).
Proof.
constructor. rewrite <-(set_unfold (s ss) P).
destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed.
Instance set_unfold_app_binder s bs ss P Q :
SetUnfoldElemOf (BNamed s) bs P SetUnfoldElemOf s ss Q
SetUnfoldElemOf s (bs +b+ ss) (P Q).
Proof.
intros HinP HinQ.
constructor. rewrite <-(set_unfold (s ss) Q), <-(set_unfold (BNamed s bs) P).
clear HinP HinQ.
induction bs; set_solver.
Qed.
Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
Instance cons_binder_Permutation b : Proper (() ==> ()) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
Instance app_binder_Permutation : Proper (() ==> () ==> ()) app_binder.
Proof.
assert ( bs, Proper (() ==> ()) (app_binder bs)).
{ intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
Qed.
Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
match b with BAnon => m | BNamed s => delete s m end.
Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
match b with BAnon => m | BNamed s => <[s:=x]> m end.
Instance: Params (@binder_insert) 4 := {}.
Section binder_delete_insert.
Context `{FinMap string M}.
Global Instance binder_insert_proper `{Equiv A} b :
Proper (() ==> () ==> (@{M A})) (binder_insert b).
Proof. destruct b; solve_proper. Qed.
Lemma binder_delete_empty {A} b : binder_delete b =@{M A} .
Proof. destruct b; simpl; eauto using delete_empty. Qed.
Lemma lookup_binder_delete_None {A} (m : M A) b s :
binder_delete b m !! s = None b = BNamed s m !! s = None.
Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
Lemma binder_insert_fmap {A B} (f : A B) (x : A) b (m : M A) :
f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
Lemma binder_delete_insert {A} b s x (m : M A) :
b BNamed s binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
Lemma binder_delete_delete {A} b s (m : M A) :
binder_delete b (delete s m) = delete s (binder_delete b m).
Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
End binder_delete_insert.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements boolsets as functions into Prop. *) (** This file implements boolsets as functions into Prop. *)
From stdpp Require Export prelude. From stdpp Require Export prelude.
Set Default Proof Using "Type". From stdpp Require Import options.
Record boolset (A : Type) : Type := BoolSet { boolset_car : A bool }. Record boolset (A : Type) : Type := BoolSet { boolset_car : A bool }.
Arguments BoolSet {_} _ : assert. Arguments BoolSet {_} _ : assert.
...@@ -19,15 +17,16 @@ Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2, ...@@ -19,15 +17,16 @@ Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x). BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2, Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)). BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Instance boolset_set `{EqDecision A} : Set_ A (boolset A). Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof. Proof.
split; [split| |]. split; [split; [split| |]|].
- by intros x ?. - by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)). - by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro. - split; [apply orb_prop_elim | apply orb_prop_intro].
- split. apply andb_prop_elim. apply andb_prop_intro. - split; [apply andb_prop_elim | apply andb_prop_intro].
- intros X Y x; unfold elem_of, boolset_elem_of; simpl. - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto. destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
Qed. Qed.
Instance boolset_elem_of_dec {A} : RelDecision (@{boolset A}). Instance boolset_elem_of_dec {A} : RelDecision (@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined. Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
......
(** This file implements the type [coGset A] of finite/cofinite sets
of elements of any countable type [A].
Note that [coGset positive] cannot represent all elements of [coPset]
(e.g., [coPset_suffixes], [coPset_l], and [coPset_r] construct
infinite sets that cannot be represented). *)
From stdpp Require Export sets countable.
From stdpp Require Import decidable finite gmap coPset.
From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
Inductive coGset `{Countable A} :=
| FinGSet (X : gset A)
| CoFinGset (X : gset A).
Arguments coGset _ {_ _} : assert.
Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Proof. solve_decision. Defined.
Instance coGset_countable `{Countable A} : Countable (coGset A).
Proof.
apply (inj_countable'
(λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
(λ s, match s with inl X => FinGSet X | inr X => CoFinGset X end)).
by intros [].
Qed.
Section coGset.
Context `{Countable A}.
Global Instance coGset_elem_of : ElemOf A (coGset A) := λ x X,
match X with FinGSet X => x X | CoFinGset X => x X end.
Global Instance coGset_empty : Empty (coGset A) := FinGSet .
Global Instance coGset_top : Top (coGset A) := CoFinGset .
Global Instance coGset_singleton : Singleton A (coGset A) := λ x,
FinGSet {[x]}.
Global Instance coGset_union : Union (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => CoFinGset (X Y)
| FinGSet X, CoFinGset Y => CoFinGset (Y X)
| CoFinGset X, FinGSet Y => CoFinGset (X Y)
end.
Global Instance coGset_intersection : Intersection (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => CoFinGset (X Y)
| FinGSet X, CoFinGset Y => FinGSet (X Y)
| CoFinGset X, FinGSet Y => FinGSet (Y X)
end.
Global Instance coGset_difference : Difference (coGset A) := λ X Y,
match X, Y with
| FinGSet X, FinGSet Y => FinGSet (X Y)
| CoFinGset X, CoFinGset Y => FinGSet (Y X)
| FinGSet X, CoFinGset Y => FinGSet (X Y)
| CoFinGset X, FinGSet Y => CoFinGset (X Y)
end.
Global Instance coGset_set : TopSet A (coGset A).
Proof.
split; [split; [split| |]|].
- by intros ??.
- intros x y. unfold elem_of, coGset_elem_of; simpl.
by rewrite elem_of_singleton.
- intros [X|X] [Y|Y] x; unfold elem_of, coGset_elem_of, coGset_union; simpl.
+ set_solver.
+ by rewrite not_elem_of_difference, (comm ()).
+ by rewrite not_elem_of_difference.
+ by rewrite not_elem_of_intersection.
- intros [] [];
unfold elem_of, coGset_elem_of, coGset_intersection; set_solver.
- intros [X|X] [Y|Y] x;
unfold elem_of, coGset_elem_of, coGset_difference; simpl.
+ set_solver.
+ rewrite elem_of_intersection. destruct (decide (x Y)); tauto.
+ set_solver.
+ rewrite elem_of_difference. destruct (decide (x Y)); tauto.
- done.
Qed.
End coGset.
Instance coGset_elem_of_dec `{Countable A} : RelDecision (@{coGset A}) :=
λ x X,
match X with
| FinGSet X => decide_rel elem_of x X
| CoFinGset X => not_dec (decide_rel elem_of x X)
end.
Section infinite.
Context `{Countable A, Infinite A}.
Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
Proof.
intros [X|X] [Y|Y]; rewrite elem_of_equiv;
unfold elem_of, coGset_elem_of; simpl; intros HXY.
- f_equal. by apply leibniz_equiv.
- by destruct (exist_fresh (X Y)) as [? [? ?%HXY]%not_elem_of_union].
- by destruct (exist_fresh (X Y)) as [? [?%HXY ?]%not_elem_of_union].
- f_equal. apply leibniz_equiv; intros x. by apply not_elem_of_iff.
Qed.
Global Instance coGset_equiv_dec : RelDecision (@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
Defined.
Global Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Global Instance coGset_subseteq_dec : RelDecision (@{coGset A}).
Proof.
refine (λ X Y, cast_if (decide (X Y = Y)));
abstract (by rewrite subseteq_union_L).
Defined.
Definition coGset_finite (X : coGset A) : bool :=
match X with FinGSet _ => true | CoFinGset _ => false end.
Lemma coGset_finite_spec X : set_finite X coGset_finite X.
Proof.
destruct X as [X|X];
unfold set_finite, elem_of at 1, coGset_elem_of; simpl.
- split; [done|intros _]. exists (elements X). set_solver.
- split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
by destruct (exist_fresh (X Y)) as [? [?%HXY ?]%not_elem_of_union].
Qed.
Global Instance coGset_finite_dec (X : coGset A) : Decision (set_finite X).
Proof.
refine (cast_if (decide (coGset_finite X)));
abstract (by rewrite coGset_finite_spec).
Defined.
End infinite.
(** * Pick elements from infinite sets *)
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
fresh (match X with FinGSet _ => | CoFinGset X => X end).
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X coGpick X X.
Proof.
unfold coGpick.
destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
by intros _; apply is_fresh.
Qed.
(** * Conversion to and from gset *)
Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
match X with FinGSet X => X | CoFinGset _ => end.
Definition gset_to_coGset `{Countable A} : gset A coGset A := FinGSet.
Section to_gset.
Context `{Countable A}.
Lemma elem_of_gset_to_coGset (X : gset A) x : x gset_to_coGset X x X.
Proof. done. Qed.
Context `{Infinite A}.
Lemma elem_of_coGset_to_gset (X : coGset A) x :
set_finite X x coGset_to_gset X x X.
Proof. rewrite coGset_finite_spec. by destruct X. Qed.
Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
Proof. by rewrite coGset_finite_spec. Qed.
End to_gset.
(** * Conversion to coPset *)
Definition coGset_to_coPset (X : coGset positive) : coPset :=
match X with
| FinGSet X => gset_to_coPset X
| CoFinGset X => gset_to_coPset X
end.
Lemma elem_of_coGset_to_coPset X x : x coGset_to_coPset X x X.
Proof.
destruct X as [X|X]; simpl.
- by rewrite elem_of_gset_to_coPset.
- by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True ()).
Qed.
(** * Inefficient conversion to arbitrary sets with a top element *)
(** This shows that, when [A] is countable, [coGset A] is initial
among sets with [∪], [∩], [∖], [∅], [{[_]}], and [⊤]. *)
Definition coGset_to_top_set `{Countable A, Empty C, Singleton A C, Union C,
Top C, Difference C} (X : coGset A) : C :=
match X with
| FinGSet X => list_to_set (elements X)
| CoFinGset X => list_to_set (elements X)
end.
Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
x @{C} coGset_to_top_set X x X.
Proof. destruct X; set_solver. Qed.
(** * Domain of finite maps *)
Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
gset_to_coGset (dom _ m).
Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
Proof.
split; try apply _. intros B m i. unfold dom, coGset_dom.
by rewrite elem_of_gset_to_coGset, elem_of_dom.
Qed.
Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
Typeclasses Opaque coGset_dom.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements the type [coPset] of efficient finite/cofinite sets (** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are: of positive binary naturals [positive]. These sets are:
...@@ -13,7 +11,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond ...@@ -13,7 +11,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *) to the decision function that map bitstrings to bools. *)
From stdpp Require Export sets. From stdpp Require Export sets.
From stdpp Require Import pmap gmap mapset. From stdpp Require Import pmap gmap mapset.
Set Default Proof Using "Type". From stdpp Require Import options.
Local Open Scope positive_scope. Local Open Scope positive_scope.
(** * The tree data structure *) (** * The tree data structure *)
...@@ -169,9 +167,9 @@ Instance coPset_difference : Difference coPset := λ X Y, ...@@ -169,9 +167,9 @@ Instance coPset_difference : Difference coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 coPset_opp_raw t2) coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _). (t1 coPset_opp_raw t2) coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
Instance coPset_set : Set_ positive coPset. Instance coPset_top_set : TopSet positive coPset.
Proof. Proof.
split; [split| |]. split; [split; [split| |]|].
- by intros ??. - by intros ??.
- intros p q. apply coPset_elem_of_singleton. - intros p q. apply coPset_elem_of_singleton.
- intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl. - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
...@@ -181,8 +179,13 @@ Proof. ...@@ -181,8 +179,13 @@ Proof.
- intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl. - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
by rewrite coPset_elem_of_intersection, by rewrite coPset_elem_of_intersection,
coPset_elem_of_opp, andb_True, negb_True. coPset_elem_of_opp, andb_True, negb_True.
- done.
Qed. Qed.
(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
Hint Resolve coPset_top_subseteq : core.
Instance coPset_leibniz : LeibnizEquiv coPset. Instance coPset_leibniz : LeibnizEquiv coPset.
Proof. Proof.
intros X Y; rewrite elem_of_equiv; intros HXY. intros X Y; rewrite elem_of_equiv; intros HXY.
...@@ -204,11 +207,6 @@ Proof. ...@@ -204,11 +207,6 @@ 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.
(** * Top *)
Lemma coPset_top_subseteq (X : coPset) : X .
Proof. done. Qed.
Hint Resolve coPset_top_subseteq : core.
(** * Finite sets *) (** * Finite sets *)
Fixpoint coPset_finite (t : coPset_raw) : bool := Fixpoint coPset_finite (t : coPset_raw) : bool :=
match t with match t with
...@@ -318,11 +316,11 @@ Proof. ...@@ -318,11 +316,11 @@ Proof.
Qed. Qed.
(** * Conversion to and from gsets of positives *) (** * Conversion to and from gsets of positives *)
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m. Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
Proof. done. Qed. Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
Definition coPset_to_gset (X : coPset) : gset positive := Definition coPset_to_gset (X : coPset) : gset positive :=
let 'Mapset m := coPset_to_Pset X in let 'Mapset m := coPset_to_Pset X in
Mapset (GMap m (bool_decide_pack _ (coPset_to_gset_wf m))). Mapset (GMap m (coPset_to_gset_wf m)).
Definition gset_to_coPset (X : gset positive) : coPset := Definition gset_to_coPset (X : gset positive) : coPset :=
let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t Pset_to_coPset_wf _ Ht. let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t Pset_to_coPset_wf _ Ht.
......
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From Coq.QArith Require Import QArith_base Qcanon. From Coq.QArith Require Import QArith_base Qcanon.
From stdpp Require Export list numbers. From stdpp Require Export list numbers list_numbers fin.
Set Default Proof Using "Type". From stdpp Require Import options.
Local Open Scope positive. Local Open Scope positive.
Class Countable A `{EqDecision A} := { Class Countable A `{EqDecision A} := {
...@@ -14,24 +12,34 @@ Hint Mode Countable ! - : typeclass_instances. ...@@ -14,24 +12,34 @@ Hint Mode Countable ! - : typeclass_instances.
Arguments encode : simpl never. Arguments encode : simpl never.
Arguments decode : simpl never. Arguments decode : simpl never.
Definition encode_nat `{Countable A} (x : A) : nat := Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
Instance encode_inj `{Countable A} : Inj (=) (=) encode.
Proof. Proof.
intros x y Hxy; apply (inj Some). intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode. by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed. Qed.
Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed. Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x. Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
Proof. Proof.
pose proof (Pos2Nat.is_pos (encode x)). pose proof (Pos2Nat.is_pos (encode x)).
unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia. unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
by rewrite Pos2Nat.id, decode_encode. by rewrite Pos2Nat.id, decode_encode.
Qed. Qed.
Definition encode_Z `{Countable A} (x : A) : Z :=
Zpos (encode x).
Definition decode_Z `{Countable A} (i : Z) : option A :=
match i with Zpos i => decode i | _ => None end.
Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
Proof. apply decode_encode. Qed.
(** * Choice principles *) (** * Choice principles *)
Section choice. Section choice.
Context `{Countable A} (P : A Prop). Context `{Countable A} (P : A Prop).
...@@ -45,7 +53,7 @@ Section choice. ...@@ -45,7 +53,7 @@ Section choice.
intros [x Hx]. cut ( i p, intros [x Hx]. cut ( i p,
i encode x 1 + encode x = p + i Acc choose_step p). i encode x 1 + encode x = p + i Acc choose_step p).
{ intros help. by apply (help (encode x)). } { intros help. by apply (help (encode x)). }
induction i as [|i IH] using Pos.peano_ind; intros p ??. intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
{ constructor. intros j. assert (p = encode x) by lia; subst. { constructor. intros j. assert (p = encode x) by lia; subst.
inversion 1 as [? Hd|?? Hd]; subst; inversion 1 as [? Hd|?? Hd]; subst;
rewrite decode_encode in Hd; congruence. } rewrite decode_encode in Hd; congruence. }
...@@ -102,6 +110,11 @@ Section inj_countable'. ...@@ -102,6 +110,11 @@ Section inj_countable'.
Next Obligation. intros x. by f_equal/=. Qed. Next Obligation. intros x. by f_equal/=. Qed.
End inj_countable'. End inj_countable'.
(** ** Empty *)
Program Instance Empty_set_countable : Countable Empty_set :=
{| encode u := 1; decode p := None |}.
Next Obligation. by intros []. Qed.
(** ** Unit *) (** ** Unit *)
Program Instance unit_countable : Countable unit := Program Instance unit_countable : Countable unit :=
{| encode u := 1; decode p := Some () |}. {| encode u := 1; decode p := Some () |}.
...@@ -246,7 +259,7 @@ Next Obligation. ...@@ -246,7 +259,7 @@ Next Obligation.
by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id. by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
Qed. Qed.
Global Program Instance Qc_countable : Countable Qc := Program Instance Qc_countable : Countable Qc :=
inj_countable inj_countable
(λ p : Qc, let 'Qcmake (x # y) _ := p return _ in (x,y)) (λ p : Qc, let 'Qcmake (x # y) _ := p return _ in (x,y))
(λ q : Z * positive, let '(x,y) := q return _ in Some (Q2Qc (x # y))) _. (λ q : Z * positive, let '(x,y) := q return _ in Some (Q2Qc (x # y))) _.
...@@ -254,7 +267,7 @@ Next Obligation. ...@@ -254,7 +267,7 @@ Next Obligation.
intros [[x y] Hcan]. f_equal. apply Qc_is_canon. simpl. by rewrite Hcan. intros [[x y] Hcan]. f_equal. apply Qc_is_canon. simpl. by rewrite Hcan.
Qed. Qed.
Global Program Instance Qp_countable : Countable Qp := Program Instance Qp_countable : Countable Qp :=
inj_countable inj_countable
Qp_car Qp_car
(λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _. (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
...@@ -263,8 +276,18 @@ Next Obligation. ...@@ -263,8 +276,18 @@ Next Obligation.
case_match; [|done]. f_equal. by apply Qp_eq. case_match; [|done]. f_equal. by apply Qp_eq.
Qed. Qed.