...
 
Commits (158)
# Enable syntax highlighting.
*.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......
......@@ -18,61 +18,48 @@ variables:
paths:
- opamroot/
only:
- master
- /^ci/
- master@iris/stdpp
- /^ci/@iris/stdpp
except:
- triggers
- schedules
- api
## Build jobs
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.9.0:
build-coq.8.11.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-stdpp"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.1"
OPAM_PINS: "coq version 8.11.dev"
CI_COQCHK: "1"
build-coq.8.8.0:
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
OPAM_PINS: "coq version 8.10.2"
OPAM_PKG: "coq-stdpp"
# DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.10.2"
tags:
- fp-timing
build-coq.8.7.2:
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
OPAM_PINS: "coq version 8.9.1"
build-coq.8.7.1:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
OPAM_PINS: "coq version 8.8.2"
build-coq.8.7.0:
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.0"
OPAM_PINS: "coq version 8.7.2"
......@@ -3,20 +3,101 @@ API-breaking change is listed.
## std++ master
Numerous functions and theorems have been renamed.
- Consistently use `set` instead of `collection`.
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection`
is called `SemiSet`, and `FinCollection` is called `FinSet`, and
`CollectionMonad` is called `MonadSet`.
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`,
respectively.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise
`bset` into `boolset`.
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map`
instead of the former `map_of_list`.
The following `sed` script should get you a long way:
- Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
`dom_map_filter` for the version with the equality. This follows the naming
convention for similar lemmas.
- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
- Disambiguate Haskell-style notations for partially applied operators. For
example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
prefix, as done in VST. A sed script to perform the renaming can be found at:
https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
## std++ 1.2.1 (released 2019-08-29)
This release of std++ received contributions by Dan Frumin, Michael Sammler,
Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
Rodolphe Lepigre, and Simon Spies.
Noteworthy additions and changes:
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
- Make `solve_ndisj` tactic more powerful.
- Add type class `Involutive`.
- Improve `naive_solver` performance in case the goal is trivially solvable.
- Add a bunch of new lemmas for list, set, and map operations.
- Rename `lookup_imap` into `map_lookup_imap`.
## std++ 1.2.0 (released 2019-04-26)
Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
std++ 1.1 if you have to use Coq 8.6. The repository moved to a new location at
https://gitlab.mpi-sws.org/iris/stdpp and automatically generated Coq-doc of
master is available at https://plv.mpi-sws.org/coqdoc/stdpp/.
This release of std++ received contributions by Dan Frumin, Hai Dang, Jan-Oliver
Kaiser, Mackie Loeffel, Maxime Dénès, Ralf Jung, Robbert Krebbers, and Tej
Chajed.
New features:
- New notations `=@{A}`, `≡@{A}`, `∈@{A}`, `∉@{A}`, `##@{A}`, `⊆@{A}`, `⊂@{A}`,
`⊑@{A}`, `≡ₚ@{A}` for being explicit about the type.
- A definition of basic telescopes `tele` and some theory about them.
- A simple type class based canceler `NatCancel` for natural numbers.
- A type `binder` for anonymous and named binders to be used in program language
definitions with string-based binders.
- More results about `set_fold` on sets and multisets.
- Notions of infinite and finite predicates/sets and basic theory about them.
- New operation `map_seq`.
- The symmetric and reflexive/transitive/symmetric closure of a relation (`sc`
and `rtsc`, respectively).
- Different notions of confluence (diamond property, confluence, local
confluence) and the relations between these.
- A `size` function for finite maps and prove some properties.
- More results about `Qp` fractions.
- More miscellaneous results about sets, maps, lists, multisets.
- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
and `tc_to_bool`.
- Generalize `gset_to_propset` to `set_to_propset` for any `SemiSet`.
Changes:
- Consistently use `lia` instead of `omega` everywhere.
- Consistently block `simpl` on all `Z` operations.
- The `Infinite` class is now defined using a function `fresh : list A → A`
that given a list `xs`, gives an element `fresh xs ∉ xs`.
- Make `default` an abbreviation for `from_option id` (instead of just swapping
the argument order of `from_option`).
- More efficient `Countable` instance for `list` that is linear instead of
exponential.
- Improve performance of `set_solver` significantly by introducing specialized
type class `SetUnfoldElemOf` for propositions involving `∈`.
- Make `gset` a `Definition` instead of a `Notation` to improve performance.
- Use `disj_union` (notation `⊎`) for disjoint union on multisets (that adds the
multiplicities). Repurpose `∪` on multisets for the actual union (that takes
the max of the multiplicities).
Naming:
- Consistently use the `set` prefix instead of the `collection` prefix for
definitions and lemmas.
- Renaming of classes:
+ `Collection` into `Set_` (`_` since `Set` is a reserved keyword)
+ `SimpleCollection` into `SemiSet`
+ `FinCollection` into `FinSet`
+ `CollectionMonad` into `MonadSet`
- Types:
+ `set A := A → Prop` into `propset`
+ `bset := A → bool` into `boolset`.
- Files:
+ `collections.v` into `sets.v`
+ `fin_collections.v` into `fin_sets.v`
+ `bset` into `boolset`
+ `set` into `propset`
- Consistently use the naming scheme `X_to_Y` for conversion functions, e.g.
`list_to_map` instead of the former `map_of_list`.
The following `sed` script should perform most of the renaming:
```
sed '
......
......@@ -9,7 +9,7 @@ all: Makefile.coq
clean: Makefile.coq
+@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
rm -f Makefile.coq
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......@@ -29,14 +29,8 @@ 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 itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
......@@ -45,11 +45,11 @@ Notably:
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.7.2 / 8.8.2 / 8.9.1 / 8.10.2
## 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:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -79,3 +79,9 @@ your account. Then you can fork the
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
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
# "Declare Scope" does not exist yet in 8.9
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
theories/base.v
theories/tactics.v
theories/option.v
......@@ -44,3 +45,4 @@ theories/infinite.v
theories/nat_cancel.v
theories/namespaces.v
theories/telescopes.v
theories/binders.v
This project contains an extended "Standard Library" for Coq called coq-std++.
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
opam-version: "1.2"
opam-version: "2.0"
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"]
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: "This project contains an extended \"Standard Library\" for Coq called coq-std++"
description: """
This project contains an extended "Standard Library" for Coq called coq-std++.
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
"""
depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") }
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9.1" & < "8.12~") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
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.
This diff is collapsed.
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** 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.
Inductive binder := BAnon | BNamed :> string binder.
Bind Scope binder_scope with binder.
Delimit 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)).
{ 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; auto 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.
......@@ -318,11 +318,11 @@ Proof.
Qed.
(** * Conversion to and from gsets of positives *)
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
Proof. done. Qed.
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
Definition coPset_to_gset (X : coPset) : gset positive :=
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 :=
let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t Pset_to_coPset_wf _ Ht.
......
......@@ -18,14 +18,14 @@ 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_inj `{Countable A} : Inj (=) (=) encode.
Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Proof.
intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed.
Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
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.
pose proof (Pos2Nat.is_pos (encode x)).
unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
......@@ -102,6 +102,11 @@ Section inj_countable'.
Next Obligation. intros x. by f_equal/=. Qed.
End inj_countable'.
(** ** Empty *)
Program Instance Empty_set_countable : Countable Empty_set :=
{| encode u := 1; decode p := None |}.
Next Obligation. by intros []. Qed.
(** ** Unit *)
Program Instance unit_countable : Countable unit :=
{| encode u := 1; decode p := Some () |}.
......@@ -264,7 +269,7 @@ Next Obligation.
Qed.
(** ** Generic trees *)
Close Scope positive.
Local Close Scope positive.
Inductive gen_tree (T : Type) : Type :=
| GenLeaf : T gen_tree T
......
......@@ -91,6 +91,13 @@ Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Lemma bool_decide_decide P `{!Decision P} :
bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
(if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
......@@ -108,14 +115,29 @@ Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack : core.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ¬P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
(P Q) bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed.
Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true P.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_true_2 P `{!Decision P}: P bool_decide P = true.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false ¬P.
Proof. apply bool_decide_eq_false. Qed.
Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P bool_decide P = false.
Proof. apply bool_decide_eq_false. Qed.
(** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2.
Notation bool_decide_false := bool_decide_eq_false_2.
(** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
......@@ -135,7 +157,7 @@ Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x.
Proof. apply dsig_eq; reflexivity. Qed.
(** * Instances of Decision *)
(** * Instances of [Decision] *)
(** Instances of [Decision] for operators of propositional logic. *)
Instance True_dec: Decision True := left I.
Instance False_dec: Decision False := right (False_rect False).
......@@ -162,6 +184,8 @@ Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
Instance Empty_set_eq_dec : EqDecision Empty_set.
Proof. solve_decision. Defined.
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
......@@ -192,3 +216,11 @@ Proof. destruct (decide Q); tauto. Qed.
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
(** * Instances of [RelDecision] *)
Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
RelDecision (flip R) := λ x y, decide_rel R y x.
(** We do not declare this as an actual instance since Coq can unify [flip ?R]
with any relation. Coq's standard library is carrying out the same approach for
the [Reflexive], [Transitive], etc, instance of [flip]. *)
Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
......@@ -11,15 +11,22 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
OMap M, Merge M, A, FinMapToList K A (M A), EqDecision K,
ElemOf K D, Empty D, Singleton K D,
Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M;
finmap_dom_set :>> Set_ K D;
finmap_dom_map :> FinMap K M;
finmap_dom_set :> Set_ K D;
elem_of_dom {A} (m : M A) i : i dom D m is_Some (m !! i)
}.
Section fin_map_dom.
Context `{FinMapDom K M D}.
Lemma dom_map_filter {A} (P : K * A Prop) `{! x, Decision (P x)} (m : M A):
Lemma dom_map_filter {A} (P : K * A Prop) `{! x, Decision (P x)} (m : M A) X :
( i, i X x, m !! i = Some x P (i, x))
dom D (filter P m) X.
Proof.
intros HX i. rewrite elem_of_dom, HX.
unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
Qed.
Lemma dom_map_filter_subseteq {A} (P : K * A Prop) `{! x, Decision (P x)} (m : M A):
dom D (filter P m) dom D m.
Proof.
intros ?. rewrite 2!elem_of_dom.
......@@ -119,8 +126,23 @@ Proof.
eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
(singleton_finite (C:=D)).
Qed.
Global Instance dom_proper `{!Equiv A} : Proper ((@{M A}) ==> ()) (dom D).
Proof.
intros m1 m2 EQm. apply elem_of_equiv. intros i.
rewrite !elem_of_dom, EQm. done.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
Proper ((@{M A}) ==> (=)) (dom D) | 0.
Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Context `{!LeibnizEquiv D}.
Lemma dom_map_filter_L {A} (P : K * A Prop) `{! x, Decision (P x)} (m : M A) X :
( i, i X x, m !! i = Some x P (i, x))
dom D (filter P m) = X.
Proof. unfold_leibniz. apply dom_map_filter. Qed.
Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
Proof. unfold_leibniz; apply dom_empty. Qed.
Lemma dom_empty_inv_L {A} (m : M A) : dom D m = m = .
......@@ -145,12 +167,12 @@ Proof. unfold_leibniz; apply dom_fmap. Qed.
End fin_map_dom.
Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
dom D (map_seq start xs) set_seq start (length xs).
dom D (map_seq start (M:=M A) xs) set_seq start (length xs).
Proof.
revert start. induction xs as [|x xs IH]; intros start; simpl.
- by rewrite dom_empty.
- by rewrite dom_insert, IH.
Qed.
Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
dom D (map_seq start xs) = set_seq start (length xs).
dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
Proof. unfold_leibniz. apply dom_seq. Qed.
This diff is collapsed.
......@@ -60,8 +60,8 @@ Defined.
(** * The [elements] operation *)
Global Instance set_unfold_elements X x P :
SetUnfold (x X) P SetUnfold (x elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold (x X) P). Qed.
SetUnfoldElemOf x X P SetUnfoldElemOf x (elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed.
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Proof.
......@@ -224,6 +224,11 @@ Proof.
rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. set_solver. apply IH. set_solver.
Qed.
Lemma set_fold_ind_L `{!LeibnizEquiv C}
{B} (P : B C Prop) (f : A B B) (b : B) :
P b ( x X r, x X P r X P (f x r) ({[ x ]} X))
X, P (set_fold f b X) X.
Proof. apply set_fold_ind. by intros ?? -> ?? ->%leibniz_equiv. Qed.
Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
......@@ -278,9 +283,9 @@ Section filter.
by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
Qed.
Global Instance set_unfold_filter X Q :
SetUnfold (x X) Q SetUnfold (x filter P X) (P x Q).
SetUnfoldElemOf x X Q SetUnfoldElemOf x (filter P X) (P x Q).
Proof.
intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x X) Q).
intros ??; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
Qed.
Lemma filter_empty : filter P (:C) .
......@@ -316,8 +321,8 @@ Section map.
by setoid_rewrite elem_of_elements.
Qed.
Global Instance set_unfold_map (f : A B) (X : C) (P : A Prop) :
( y, SetUnfold (y X) (P y))
SetUnfold (x set_map (D:=D) f X) ( y, x = f y P y).
( y, SetUnfoldElemOf y X (P y))
SetUnfoldElemOf x (set_map (D:=D) f X) ( y, x = f y P y).
Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
Global Instance set_map_proper :
......@@ -396,7 +401,7 @@ Section infinite.
(** Properties about the [fresh] operation on finite sets *)
Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
Proof. unfold fresh, set_fresh. solve_proper. Qed.
Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
Lemma is_fresh X : fresh X X.
Proof.
......
......@@ -18,41 +18,41 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x,
Pos.of_nat $ S $ default 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.
Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
destruct (list_find_Some (x =) xs i y); naive_solver.
destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed.
Hint Immediate finite_countable : typeclass_instances.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
list_find P (enum A) = decode_nat fst.
Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
- destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
- apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed.
Lemma encode_decode A `{finA: Finite A} i :
i < card A x, decode_nat i = Some x encode_nat x = i.
i < card A x : A, decode_nat i = Some x encode_nat x = i.
Proof.
destruct finA as [xs Hxs HA].
unfold encode_nat, decode_nat, encode, decode, card; simpl.
intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
exists x. rewrite !Nat2Pos.id by done; simpl.
destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto.
destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
rewrite Hj; csimpl; eauto using NoDup_lookup.
destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
split; [done|]; rewrite Hj; simpl.
apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup.
Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
find P = Some x P x.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
......@@ -60,13 +60,13 @@ Proof.
rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i y); naive_solver.
Qed.
Lemma find_is_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
Lemma find_is_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
P x y, find P = Some y P y.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
exists y. by rewrite !Nat2Pos.id by done.
rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
apply list_find_Some in Hi; naive_solver.
Qed.
Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
......@@ -246,6 +246,12 @@ Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.
Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
Next Obligation. intros []. Qed.
Lemma Empty_set_card : card Empty_set = 0.
Proof. done. Qed.
Program Instance unit_finite : Finite () := {| enum := [tt] |}.
Next Obligation. apply NoDup_singleton. Qed.
Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
......@@ -276,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
{| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
......@@ -306,10 +312,10 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
fix go n :=
match n with
| 0 => [[]eq_refl]
| S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
| S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
end.
Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
{| enum := list_enum (enum A) n |}.
Next Obligation.
intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
......@@ -335,7 +341,7 @@ Next Obligation.
- rewrite elem_of_app. eauto.
Qed.
Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof.
unfold card; simpl. induction n as [|n IH]; simpl; auto.
rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
......
......@@ -9,11 +9,11 @@ From stdpp Require Import pmap mapset propset.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
to codes of actual elements of the countable type. *)
Definition gmap_wf `{Countable K} {A} : Pmap A Prop :=
map_Forall (λ p _, encode <$> decode p = Some p).
Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : Prop :=
bool_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
Record gmap K `{Countable K} A := GMap {
gmap_car : Pmap A;
gmap_prf : bool_decide (gmap_wf gmap_car)
gmap_prf : gmap_wf K gmap_car
}.
Arguments GMap {_ _ _ _} _ _ : assert.
Arguments gmap_car {_ _ _ _} _ : assert.
......@@ -30,50 +30,53 @@ Proof.
Defined.
(** * Operations on the data structure *)
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
let (m,_) := m in m !! encode i.
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
λ i '(GMap m _), m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap I.
Global Opaque gmap_empty.
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A option A) m i :
gmap_wf m gmap_wf (partial_alter f (encode i) m).
gmap_wf K m gmap_wf K (partial_alter f (encode (A:=K) i) m).
Proof.
unfold gmap_wf; rewrite !bool_decide_spec.
intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
- rewrite decode_encode; eauto.
- rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i m,
let (m,Hm) := m in GMap (partial_alter f (encode i) m)
(bool_decide_pack _ (gmap_partial_alter_wf f m i
(bool_decide_unpack _ Hm))).
PartialAlter K A (gmap K A) := λ f i '(GMap m Hm),
GMap (partial_alter f (encode i) m) (gmap_partial_alter_wf f m i Hm).
Lemma gmap_fmap_wf `{Countable K} {A B} (f : A B) m :
gmap_wf m gmap_wf (f <$> m).
Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f m,
let (m,Hm) := m in GMap (f <$> m)
(bool_decide_pack _ (gmap_fmap_wf f m (bool_decide_unpack _ Hm))).
gmap_wf K m gmap_wf K (f <$> m).
Proof.
unfold gmap_wf; rewrite !bool_decide_spec.
intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
Qed.
Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
GMap (f <$> m) (gmap_fmap_wf f m Hm).
Lemma gmap_omap_wf `{Countable K} {A B} (f : A option B) m :
gmap_wf m gmap_wf (omap f m).
Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
let (m,Hm) := m in GMap (omap f m)
(bool_decide_pack _ (gmap_omap_wf f m (bool_decide_unpack _ Hm))).
gmap_wf K m gmap_wf K (omap f m).
Proof.
unfold gmap_wf; rewrite !bool_decide_spec.
intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
Qed.
Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
GMap (omap f m) (gmap_omap_wf f m Hm).
Lemma gmap_merge_wf `{Countable K} {A B C}
(f : option A option B option C) m1 m2 :
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
gmap_wf m1 gmap_wf m2 gmap_wf (merge f' m1 m2).
gmap_wf K m1 gmap_wf K m2 gmap_wf K (merge f' m1 m2).
Proof.
intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
intros f'; unfold gmap_wf; rewrite !bool_decide_spec.
intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
Qed.
Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
let (m,_) := m in omap (λ ix : positive * A,
let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
GMap (merge f' m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
(** * Instantiation of the finite map interface *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
......@@ -130,7 +133,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') .
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
map_fold (λ '(i1, i2) x,
partial_alter (Some <[i2:=x]> default ) i1) .
Section curry_uncurry.
......@@ -139,12 +142,12 @@ Section curry_uncurry.
(* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
a consequence of Coq bug #5735 *)
Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (!! j).
gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (.!! j).
Proof.
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (!! j))).
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (.!! j))).
{ by rewrite !lookup_empty. }
clear m; intros i' m2 m m12 Hi' IH.
apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (!! j))).
apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (.!! j))).
{ rewrite IH. destruct (decide (i' = i)) as [->|].
- rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
- by rewrite lookup_insert_ne by done. }
......@@ -156,9 +159,9 @@ Section curry_uncurry.
Qed.
Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
(gmap_uncurry m !! i : option (gmap K2 A)) = (!! j) = m !! (i, j).
(gmap_uncurry m !! i : option (gmap K2 A)) = (.!! j) = m !! (i, j).
Proof.
apply (map_fold_ind (λ mr m, mr !! i = (!! j) = m !! (i, j))).
apply (map_fold_ind (λ mr m, mr !! i = (.!! j) = m !! (i, j))).
{ by rewrite !lookup_empty. }
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
......@@ -202,7 +205,7 @@ Section curry_uncurry.
intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
- destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
+ f_equal. apply map_eq. intros j.
trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (!! j)).
trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (.!! j)).
{ by rewrite Hcurry. }
by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
+ rewrite lookup_gmap_uncurry_None in Hcurry.
......@@ -237,11 +240,6 @@ Section gset.
Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
Definition gset_to_propset (X : gset K) : propset K :=
{[ x | x X ]}.
Lemma elem_of_gset_to_propset (X : gset K) x : x gset_to_propset X x X.
Proof. done. Qed.
Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
(λ _, x) <$> mapset_car X.
......@@ -284,6 +282,13 @@ Section gset.
- by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
- by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
Qed.
Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
dom _ (gset_to_gmap x X) = X.
Proof.
induction X as [| y X not_in IH] using set_ind_L.
- rewrite gset_to_gmap_empty, dom_empty_L; done.
- rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
Qed.
End gset.
Typeclasses Opaque gset.
......@@ -136,10 +136,11 @@ Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y
Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
SetUnfold (x X) P SetUnfold (x Y) Q SetUnfold (x X Y) (P Q).
SetUnfoldElemOf x X P SetUnfoldElemOf x Y Q
SetUnfoldElemOf x (X Y) (P Q).
Proof.
intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
by rewrite <-(set_unfold (x X) P), <-(set_unfold (x Y) Q).
by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
Qed.
(* Algebraic laws *)
......@@ -217,12 +218,12 @@ Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ().
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ).
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X .).
Proof.
intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
rewrite !multiplicity_disj_union. lia.
Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) ( X).
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (. X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z).
......
......@@ -129,7 +129,7 @@ Definition remove_dups_fast (l : list A) : list A :=
| [x] => [x]
| _ =>
let n : Z := length l in
elements (foldr (λ x, ({[ x ]} )) l :
elements (foldr (λ x, ({[ x ]} .)) l :
hashset (λ x, hash x `mod` (2 * n))%Z)
end.
Lemma elem_of_remove_dups_fast l x : x remove_dups_fast l x l.
......
......@@ -35,7 +35,7 @@ Section search_infinite.
Lemma search_infinite_R_wf xs : wf (R xs).
Proof.
revert xs. assert (help : xs n n',
Acc (R (filter ( f n') xs)) n n' < n Acc (R xs) n).
Acc (R (filter (. f n') xs)) n n' < n Acc (R xs) n).
{ induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
split; [done|]. apply elem_of_list_filter; naive_solver lia. }
intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
......@@ -127,9 +127,9 @@ Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
inj_infinite inr (maybe inr) (λ _, eq_refl).
Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
inj_infinite (,inhabitant) (Some fst) (λ _, eq_refl).
inj_infinite (., inhabitant) (Some fst) (λ _, eq_refl).
Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
inj_infinite (inhabitant,) (Some snd) (λ _, eq_refl).
inj_infinite (inhabitant ,.) (Some snd) (λ _, eq_refl).
(** Instance for lists *)
Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
......
This diff is collapsed.
......@@ -15,8 +15,8 @@ Context {A : Type}.
Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, x listset_car l.
Global Instance listset_empty: Empty (listset A) := Listset [].
Global Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
Global Instance listset_union: Union (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (l' ++ k').
Global Instance listset_union: Union (listset A) := λ '(Listset l) '(Listset k),
Listset (l ++ k).
Global Opaque listset_singleton listset_empty.
Global Instance listset_simple_set : SemiSet A (listset A).
......@@ -45,10 +45,10 @@ Proof using Aeq.
refine (λ x X, cast_if (decide (x listset_car X))); done.
Defined.
Global Instance listset_intersection: Intersection (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_intersection l' k').
Global Instance listset_difference: Difference (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_difference l' k').
Global Instance listset_intersection: Intersection (listset A) :=
λ '(Listset l) '(Listset k), Listset (list_intersection l k).