...
 
Commits (144)
# 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_PINS: "coq version 8.11.dev"
CI_COQCHK: "1"
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.2"
OPAM_PKG: "coq-stdpp"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
TIMING_CONF: "coq-8.10.2"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.1"
OPAM_PINS: "coq version 8.9.1"
build-coq.8.8.0:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
OPAM_PINS: "coq version 8.8.2"
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"
......@@ -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.
......
......@@ -45,7 +45,7 @@ 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
......@@ -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
opam-version: "1.2"
name: "coq-stdpp"
synopsis: "This project contains an extended \"Standard Library\" for Coq called coq-std++"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
......@@ -10,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") }
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9.1" & < "8.12~") | (= "dev") }
]
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.
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.
......@@ -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).
Global Instance listset_difference: Difference (listset A) :=
λ '(Listset l) '(Listset k), Listset (list_difference l k).
Instance listset_set: Set_ A (listset A).
Proof.
......@@ -69,10 +69,10 @@ Qed.
End listset.
Instance listset_ret: MRet listset := λ A x, {[ x ]}.
Instance listset_fmap: FMap listset := λ A B f l,
let (l') := l in Listset (f <$> l').
Instance listset_bind: MBind listset := λ A B f l,
let (l') := l in Listset (mbind (listset_car f) l').
Instance listset_fmap: FMap listset := λ A B f '(Listset l),
Listset (f <$> l).
Instance listset_bind: MBind listset := λ A B f '(Listset l),
Listset (mbind (listset_car f) l).
Instance listset_join: MJoin listset := λ A, mbind id.
Instance listset_set_monad : MonadSet listset.
......
......@@ -21,17 +21,17 @@ Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l.
Instance listset_nodup_empty: Empty C := ListsetNoDup [] (@NoDup_nil_2 _).
Instance listset_nodup_singleton: Singleton A C := λ x,
ListsetNoDup [x] (NoDup_singleton x).
Instance listset_nodup_union: Union C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
Instance listset_nodup_intersection: Intersection C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_intersection _ k' Hl).
Instance listset_nodup_difference: Difference C := λ l k,
let (l',Hl) := l in let (k',Hk) := k
in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
Instance listset_nodup_union: Union C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
Instance listset_nodup_intersection: Intersection C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_intersection _ k Hl).
Instance listset_nodup_difference: Difference C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_difference _ k Hl).
Instance: Set_ A C.
Instance listset_nodup_set: Set_ A C.
Proof.
split; [split | | ].
- by apply not_elem_of_nil.
......@@ -42,7 +42,7 @@ Proof.
Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
Global Instance: FinSet A C.
Global Instance listset_nodup_fin_set: FinSet A C.
Proof. split. apply _. done. by intros [??]. Qed.
End list_set.
......
......@@ -66,35 +66,37 @@ Section namespace.
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
(** 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.