Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/stdpp
  • johannes/stdpp
  • proux1/stdpp
  • dosualdo/stdpp
  • benoit/coq-stdpp
  • dfrumin/coq-stdpp
  • haidang/stdpp
  • amintimany/coq-stdpp
  • swasey/coq-stdpp
  • simongregersen/stdpp
  • proux/stdpp
  • janno/coq-stdpp
  • amaurremi/coq-stdpp
  • msammler/stdpp
  • tchajed/stdpp
  • YaZko/stdpp
  • maximedenes/stdpp
  • jakobbotsch/stdpp
  • Blaisorblade/stdpp
  • simonspies/stdpp
  • lepigre/stdpp
  • devilhena/stdpp
  • simonfv/stdpp
  • jihgfee/stdpp
  • snyke7/stdpp
  • Armael/stdpp
  • gmalecha/stdpp
  • olaure01/stdpp
  • sarahzrf/stdpp
  • atrieu/stdpp
  • herbelin/stdpp
  • arthuraa/stdpp
  • lgaeher/stdpp
  • mrhaandi/stdpp
  • mattam82/stdpp
  • Quarkbeast/stdpp
  • aa755/stdpp
  • gmevel/stdpp
  • lstefane/stdpp
  • jung/stdpp
  • vsiles/stdpp
  • dlesbre/stdpp
  • bergwerf/stdpp
  • marijnvanwezel/stdpp
  • ivanbakel/stdpp
  • tperami/stdpp
  • adamAndMath/stdpp
  • Villetaneuse/stdpp
  • sanjit/stdpp
  • yiyunliu/stdpp
  • thomas-lamiaux/stdpp
  • Tragicus/stdpp
  • kbedarka/stdpp
53 results
Show changes
Commits on Source (142)
......@@ -45,10 +45,10 @@ variables:
## Build jobs
# The newest version runs with timing.
build-coq.8.19.0:
build-coq.8.20.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.19.0"
OPAM_PINS: "coq version 8.20.1"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
CI_COQCHK: "1"
......@@ -59,21 +59,27 @@ build-coq.8.19.0:
interruptible: false
# The newest version also runs in MRs, without timing.
build-coq.8.19.0-mr:
build-coq.8.20.1-mr:
<<: *template
<<: *only_mr
variables:
OPAM_PINS: "coq version 8.19.0"
OPAM_PINS: "coq version 8.20.1"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
# Also ensure Dune works.
build-coq.8.19.0-dune:
build-coq.8.20.1-dune:
<<: *template
variables:
OPAM_PINS: "coq version 8.19.0 dune version 3.15.2"
OPAM_PINS: "coq version 8.20.1 dune version 3.15.2"
MAKE_TARGET: "dune"
build-coq.8.19.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.19.1"
DENY_WARNINGS: "1"
# The oldest version runs in MRs, without name mangling.
build-coq.8.18.0:
<<: *template
......
......@@ -3,6 +3,62 @@ API-breaking change is listed.
## std++ master
- Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
- Add lemma `lookup_total_fmap`.
- Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
`head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
- Rename `map_filter_empty_iff` to `map_empty_filter` and add
`map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
`length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
- Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
`StronglySorted_app_2`. Rename lemmas
`elem_of_StronglySorted_app``StronglySorted_app_1_elem_of`,
`StronglySorted_app_inv_l``StronglySorted_app_1_l`
`StronglySorted_app_inv_r``StronglySorted_app_1_r`. (by Marijn van Wezel)
- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
- Split up `stdpp.list` into smaller files. Users should keep importing
`stdpp.list`; the organization into smaller modules is considered an
implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
and also considered part of the list module, so existing imports should be
updated.
- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
functions; they existed solely to facilitate the proofs of decidability of
`submseteq` and `≡ₚ`, which have been refactored.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# length
s/\bmap_filter_empty_iff\b/map_empty_filter/g
# StronglySorted
s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
EOF
```
## std++ 1.11.0 (2024-10-30)
The highlights of this release include:
* support for building with dune
* stronger versions of the induction principles for `map_fold`, exposing the order in
which elements are processed
std++ 1.11 supports Coq 8.18, 8.19 and 8.20.
Coq 8.16 and 8.17 are no longer supported.
This release of std++ was managed by Jesper Bengtson, Ralf Jung,
and Robbert Krebbers, with contributions from Andres Erbsen, Lennard Gäher,
Léo Stefanesco, Marijn van Wezel, Paolo G. Giarrusso, Pierre Roux,
Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Yannick Zakowski,
and Yiyun Liu. Thanks a lot to everyone involved!
**Detailed list of changes:**
- Generalize `foldr_comm_acc`, `map_fold_comm_acc`, `set_fold_comm_acc`, and
`gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
- Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
......@@ -11,6 +67,133 @@ API-breaking change is listed.
- Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
`difference_union_intersection_L`. (by Léo Stefanesco)
- Make the build script compatible with BSD systems. (by Yiyun Liu)
- Rename lemmas `X_length` into `length_X`, see the sed script below for an
overview. This follows https://github.com/coq/coq/pull/18564.
- Redefine `map_imap` so its closure argument can contain recursive
occurrences of a `Fixpoint`.
- Add lemma `fmap_insert_inv`.
- Rename `minimal_exists` to `minimal_exists_elem_of` and
`minimal_exists_L` to `minimal_exists_elem_of_L`.
Add new `minimal_exists` lemma. (by Lennard Gäher)
- Generalize `map_relation R P Q` to have the key (extra argument `K`) in the
predicates `R`, `P` and `Q`.
- Generalize `map_included R` to a predicate `R : K → A → B → Prop`, i.e., (a)
to have the key, and (b) to have different types `A` and `B`.
- Add `map_Forall2` and some basic lemmas about it.
- Rename `map_not_Forall2` into `map_not_relation`.
- Replace the induction principle `map_fold_ind` for `map_fold` with a stronger
version:
+ The main new induction principle is `map_first_key_ind`, which is meant
to be used together with the lemmas `map_fold_insert_first_key` and
`map_to_list_insert_first_key` (and others about `map_first_key`). This
induction scheme reflects all these operations (induction, `map_fold`,
`map_to_list`) process the map in the same order.
+ The new primitive induction principle `map_fold_fmap_ind` is only relevant
for implementers of `FinMap` instances.
+ The lemma `map_fold_foldr` has been strengthened to (a) drop the
commutativity requirement and (b) give an equality (`=`) instead of being
generic over a relation `R`.
+ The lemma `map_to_list_fmap` has been strengthened to give an equality (`=`)
instead of a permutation (`≡ₚ`).
+ The lemmas `map_fold_comm_acc_strong` and `map_fold_comm_acc` have been
strengthened to only require commutativity w.r.t. the operation being
pulled out of the accumulator, not commutativity of
the folded function itself.
- Add lemmas `Sorted_unique_strong` and `StronglySorted_unique_strong` that only
require anti-symmetry for the elements that are in the list.
- Rename `foldr_cons_permute` into `foldr_cons_permute_strong` and strengthen
(a) from function `f : A → A → A` to `f : A → B → B`, and (b) to only require
associativity/commutativity for the elements that are in the list.
- Rename `foldr_cons_permute_eq` into `foldr_cons_permute`.
- Various improvements to the support of strings:
+ Add string literal notation "my string" to `std_scope`, and no longer
globally open `string_scope`.
+ Move all definitions and lemmas about strings/ascii into the modules
`String`/`Ascii`, i.e., rename `string_rev_app``String.rev_app`,
`string_rev``String.rev`, `is_nat``Ascii.is_nat`,
`is_space``Ascii.is_space` and `words``String.words`.
+ The file `std.strings` no longer exports the `String` module, it only
exports the `string` type, its constructors, induction principles, and
notations (in `string_scope`). Similar to the number types (`nat`, `N`,
`Z`), importing the `String` module yourself is discouraged, rather use
`String.function` and `String.lemma`.
+ Add `String.le` and some theory about it (decidability, proof irrelevance,
total order).
- Add lemmas `foldr_idemp_strong` and `foldr_idemp`.
- Add lemmas `set_fold_union_strong` and `set_fold_union`.
- Add lemmas `map_fold_union_strong`, `map_fold_union`,
`map_fold_disj_union_strong`, `map_fold_disj_union` and `map_fold_proper`.
- Add `gmultiset_map` and associated lemmas. (by Marijn van Wezel)
- Add `CProd` type class for Cartesian products; with instances for `list`,
`gset`, `boolset`, `MonadSet` (i.e., `propset`, `listset`); and `set_solver`
tactic support. (by Thibaut Pérami)
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# length
s/\bnil_length\b/length_nil/g
s/\bcons_length\b/length_cons/g
s/\bapp_length\b/length_app/g
s/\bmap_to_list_length\b/length_map_to_list/g
s/\bseq_length\b/length_seq/g
s/\bseqZ_length\b/length_seqZ/g
s/\bjoin_length\b/length_join/g
s/\bZ_to_little_endian_length\b/length_Z_to_little_endian/g
s/\balter_length\b/length_alter/g
s/\binsert_length\b/length_insert/g
s/\binserts_length\b/length_inserts/g
s/\breverse_length\b/length_reverse/g
s/\btake_length\b/length_take/g
s/\btake_length_le\b/length_take_le/g
s/\btake_length_ge\b/length_take_ge/g
s/\bdrop_length\b/length_drop/g
s/\breplicate_length\b/length_replicate/g
s/\bresize_length\b/length_resize/g
s/\brotate_length\b/length_rotate/g
s/\breshape_length\b/length_reshape/g
s/\bsublist_alter_length\b/length_sublist_alter/g
s/\bmask_length\b/length_mask/g
s/\bfilter_length\b/length_filter/g
s/\bfilter_length_lt\b/length_filter_lt/g
s/\bfmap_length\b/length_fmap/g
s/\bmapM_length\b/length_mapM/g
s/\bset_mapM_length\b/length_set_mapM/g
s/\bimap_length\b/length_imap/g
s/\bzip_with_length\b/length_zip_with/g
s/\bzip_with_length_l\b/length_zip_with_l/g
s/\bzip_with_length_l_eq\b/length_zip_with_l_eq/g
s/\bzip_with_length_r\b/length_zip_with_r/g
s/\bzip_with_length_r_eq\b/length_zip_with_r_eq/g
s/\bzip_with_length_same_l\b/length_zip_with_same_l/g
s/\bzip_with_length_same_r\b/length_zip_with_same_r/g
s/\bnatset_to_bools_length\b/length_natset_to_bools/g
s/\bvec_to_list_length\b/length_vec_to_list/g
s/\bfresh_list_length\b/length_fresh_list/g
s/\bbv_to_little_endian_length\b/length_bv_to_little_endian/g
s/\bbv_seq_length\b/length_bv_seq/g
s/\bbv_to_bits_length\b/length_bv_to_bits/g
# renaming of minimal_exists
s/\bminimal_exists_L\b/minimal_exists_elem_of_L/g
s/\bminimal_exists\b/minimal_exists_elem_of/g
# map_relation
s/\bmap_not_Forall2\b/map_not_relation/g
# map_fold
s/\bmap_fold_ind2\b/map_fold_weak_ind/g
# foldr_cons_permute
s/\bfoldr_cons_permute\b/foldr_cons_permute_strong/g
s/\bfoldr_cons_permute_eq\b/foldr_cons_permute/g
# strings
s/\bstring_rev_app\b/String.rev_app/g
s/\bstring_rev\b/String.rev/g
s/\bis_nat\b/Ascii.is_nat/g
s/\bis_space\b/Ascii.is_space/g
s/\bwords\b/String.words/g
EOF
```
## std++ 1.10.0 (2024-04-12)
......
......@@ -4,6 +4,11 @@ NO_TEST:=
# use MAKE_REF=1 to generate new reference files
MAKE_REF:=
# Only test reference output on known versions of Coq, to avoid blocking
# Coq CI when they change the printing a little.
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
# Run tests interleaved with main build. They have to be in the same target for this.
real-all: style $(if $(NO_TEST),,test)
......@@ -24,10 +29,6 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
# These versions of Coq are known to have different output so we don't test them.
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
......@@ -44,14 +45,15 @@ tests/.coqdeps.d: $(TESTFILES)
# - Cleanup, and mark as done for make.
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
$(HIDE)REF=$*".ref" && \
echo "COQTEST$(if $(COQ_NOREF), [ref diff ignored],$(if $(MAKE_REF), [make ref],)) $< (ref: $$REF)" && \
echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
TMPFILE="$$(mktemp)" && \
unset OCAMLRUNPARAM && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
mv "$$TMPFILE".new "$$TMPFILE" && \
$(if $(COQ_NOREF), (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) , \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") \
$(if $(COQ_REF),\
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
true \
) && \
rm -f "$$TMPFILE" && \
touch $@
......@@ -43,7 +43,7 @@ Notably:
This version is known to compile with:
- Coq version 8.18.0 / 8.19.0
- Coq version 8.18.0 / 8.19.1 / 8.20.1
Generally we always aim to support the last two stable Coq releases. Support for
older versions will be dropped when it is convenient.
......
......@@ -7,6 +7,11 @@
# Custom flags (to be kept in sync with the dune file at the root of the repo).
# Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
# We can't do this migration yet until we require Coq 9.0
-arg -w -arg -deprecated-from-Coq
-arg -w -arg -deprecated-dirpath-Coq
stdpp/options.v
stdpp/base.v
......@@ -47,6 +52,11 @@ stdpp/lexico.v
stdpp/propset.v
stdpp/decidable.v
stdpp/list.v
stdpp/list_basics.v
stdpp/list_relations.v
stdpp/list_monad.v
stdpp/list_misc.v
stdpp/list_tactics.v
stdpp/list_numbers.v
stdpp/functions.v
stdpp/hlist.v
......
#!/bin/bash
#!/bin/sh
set -e
## A simple shell script checking for some common Coq issues.
......
......@@ -33,7 +33,7 @@ tags: [
]
depends: [
"coq" { (>= "8.18" & < "8.20~") | (= "dev") }
"coq" { (>= "8.18" & < "9.1~") | (= "dev") }
]
build: ["./make-package" "stdpp" "-j%{jobs}%"]
......
......@@ -4,4 +4,5 @@
(flags ; Configure the coqc flags.
(:standard ; Keeping the default flags.
; Add custom flags (to be kept in sync with _CoqProject).
-w -argument-scope-delimiter)))))
-w -argument-scope-delimiter
-w -notation-incompatible-prefix)))))
......@@ -1050,6 +1050,15 @@ Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope.
Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope.
(** The operation [cprod X Y] gives the Cartesian product of set-like structures
[X] and [Y], i.e., [cprod X Y := { (x,y) | x ∈ X, y ∈ Y }]. The implementation/
instance depends on the representation of the set. *)
Class CProd A B C := cprod : A B C.
Global Hint Mode CProd ! ! - : typeclass_instances.
Global Instance: Params (@cprod) 4 := {}.
(** We do not have a notation for [cprod] (yet) since this operation seems
not commonly enough used. *)
Class Singleton A B := singleton: A B.
Global Hint Mode Singleton - ! : typeclass_instances.
Global Instance: Params (@singleton) 3 := {}.
......@@ -1113,6 +1122,11 @@ Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
Definition disj_union_list `{Empty A} `{DisjUnion A} : list A A := fold_right () ∅.
Global Arguments disj_union_list _ _ _ !_ / : assert.
(* There is no "big" version of [⊎] in unicode, we thus use [⋃+]. *)
Notation "⋃+ l" := (disj_union_list l) (at level 20, format "⋃+ l") : stdpp_scope.
Class SingletonMS A B := singletonMS: A B.
Global Hint Mode SingletonMS - ! : typeclass_instances.
Global Instance: Params (@singletonMS) 3 := {}.
......
......@@ -17,6 +17,10 @@ Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Global Instance boolset_cprod {A B} :
CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof.
split; [split; [split| |]|].
......@@ -31,6 +35,19 @@ Qed.
Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
x cprod X1 X2 x.1 X1 x.2 X2.
Proof. apply andb_True. Qed.
Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
SetUnfoldElemOf x.1 X1 P SetUnfoldElemOf x.2 X2 Q
SetUnfoldElemOf x (cprod X1 X2) (P Q).
Proof.
intros ??; constructor.
by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
(set_unfold_elem_of x.2 X2 Q).
Qed.
Global Typeclasses Opaque boolset_elem_of.
Global Opaque boolset_empty boolset_singleton boolset_union
boolset_intersection boolset_difference.
boolset_intersection boolset_difference boolset_cprod.
......@@ -313,6 +313,18 @@ Qed.
(** ** Generic trees *)
Local Close Scope positive.
(** This type can help you construct a [Countable] instance for an arbitrary
(even recursive) inductive datatype. The idea is tht you make [T] something like
[T1 + T2 + ...], covering all the data types that can be contained inside your
type.
- Each non-recursive constructor to a [GenLeaf]. Different constructors must use
different variants of [T] to ensure they remain distinguishable!
- Each recursive constructor to a [GenNode] where the [nat] is a (typically
small) constant representing the constructor itself, and then all the data in
the constructor (recursive or otherwise) is put into child nodes.
This data type is the same as [GenTree.tree] in mathcomp, see
https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
Inductive gen_tree (T : Type) : Type :=
| GenLeaf : T gen_tree T
| GenNode : nat list (gen_tree T) gen_tree T.
......@@ -355,7 +367,7 @@ Proof.
induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
- simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
by (by rewrite reverse_length).
by (by rewrite length_reverse).
Qed.
Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
......
......@@ -177,6 +177,25 @@ Proof.
- simpl. by rewrite dom_insert, IH.
Qed.
Lemma map_first_key_dom {A B} (m1 : M A) (m2 : M B) i :
dom m1 dom m2 map_first_key m1 i map_first_key m2 i.
Proof.
intros Hm. apply map_first_key_dom'. intros j.
by rewrite <-!elem_of_dom, Hm.
Qed.
Lemma map_first_key_dom_L {A B} (m1 : M A) (m2 : M B) i :
dom m1 = dom m2 map_first_key m1 i map_first_key m2 i.
Proof. intros Hm. apply map_first_key_dom. by rewrite Hm. Qed.
Lemma map_Forall2_dom {A B} (P : K A B Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 dom m1 dom m2.
Proof.
revert m2. induction m1 as [|i x1 m1 ? IH] using map_ind; intros m2.
{ intros ->%map_Forall2_empty_inv_l. by rewrite !dom_empty. }
intros (x2 & m2' & -> & ? & ? & ?)%map_Forall2_insert_inv_l; last done.
by rewrite !dom_insert, IH by done.
Qed.
(** Alternative definition of [dom] in terms of [map_to_list]. *)
Lemma dom_alt {A} (m : M A) :
dom m list_to_set (map_to_list m).*1.
......@@ -314,6 +333,7 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Section leibniz.
Context `{!LeibnizEquiv D}.
Lemma dom_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 (filter P m) = X.
......@@ -348,6 +368,9 @@ Section leibniz.
Proof. unfold_leibniz; apply dom_difference. Qed.
Lemma dom_fmap_L {A B} (f : A B) (m : M A) : dom (f <$> m) = dom m.
Proof. unfold_leibniz; apply dom_fmap. Qed.
Lemma map_Forall2_dom_L {A B} (P : K A B Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 dom m1 = dom m2.
Proof. unfold_leibniz. apply map_Forall2_dom. Qed.
Lemma dom_imap_L {A B} (f: K A option B) (m: M A) X :
( i, i X x, m !! i = Some x is_Some (f i x))
dom (map_imap f m) = X.
......
This diff is collapsed.
......@@ -194,7 +194,7 @@ Qed.
Lemma size_union X Y : X ## Y size (X Y) = size X + size Y.
Proof.
intros. unfold size, set_size. simpl. rewrite <-app_length.
intros. unfold size, set_size. simpl. rewrite <-length_app.
apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements.
......@@ -298,28 +298,112 @@ Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
Lemma set_fold_singleton {B} (f : A B B) (b : B) (a : A) :
set_fold f b ({[a]} : C) = f a b.
Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
(** The following lemma shows that folding over two sets separately (using the
result of the first fold as input for the second fold) is equivalent to folding
over the union, *if* the function is idempotent for the elements that will be
processed twice ([X ∩ Y]) and does not care about the order in which elements
are processed.
This is a generalization of [set_fold_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
Lemma set_fold_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) X Y :
( x, Proper (R ==> R) (f x))
( x b',
(** This is morally idempotence for elements of [X ∩ Y] *)
x X Y
(** We cannot write this in the usual direction of idempotence properties
(i.e., [R (f x (f x b'))) (f x b')]) because [R] is not symmetric. *)
R (f x b') (f x (f x b')))
( x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 X Y x2 X Y x1 x2
R (f x1 (f x2 b')) (f x2 (f x1 b')))
X ## Y
R (set_fold f b (X Y)) (set_fold f (set_fold f b X) Y).
Proof.
intros ? Hf Hdisj. unfold set_fold; simpl.
rewrite <-foldr_app. apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
(** This lengthy proof involves various steps by transitivity of [R].
Roughly, we show that the LHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y)
and the RHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∩ Y) ++ elements (Y ∖ X)
These steps are justified by lemma [foldr_permutation]. In the middle we
remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp_strong].
Most of the proof work concerns the side conditions of [foldr_permutation]
and [foldr_idemp_strong], which require relating results about lists and
sets. *)
intros ?.
assert ( b1 b2 l, R b1 b2 R (foldr f b1 l) (foldr f b2 l)) as Hff.
{ intros b1 b2 l Hb. induction l as [|x l]; simpl; [done|]. by f_equiv. }
intros Hfidemp Hfcomm. unfold set_fold; simpl.
trans (foldr f b (elements (Y X) ++ elements (X Y) ++ elements (X Y))).
{ apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x X)), (decide (x Y)); set_solver. }
trans (foldr f (foldr f b (elements (X Y) ++ elements (X Y)))
(elements (Y X) ++ elements (X Y))).
{ rewrite !foldr_app. apply Hff. apply (foldr_idemp_strong (flip R)).
- solve_proper.
- intros j a b' ?%elem_of_list_lookup_2. apply Hfidemp. set_solver.
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
by eapply Hj, NoDup_lookup. }
trans (foldr f (foldr f b (elements (X Y) ++ elements (X Y))) (elements Y)).
{ apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. assert (NoDup (elements (Y X) ++ elements (X Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x X)); set_solver. }
apply Hff. apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
+ intros ->. assert (NoDup (elements (X Y) ++ elements (X Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- by rewrite elements_disj_union, (comm (++)).
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x Y)); set_solver.
Qed.
Lemma set_fold_union (f : A A A) (b : A) X Y :
IdemP (=) f
Comm (=) f
Assoc (=) f
set_fold f b (X Y) = set_fold f (set_fold f b X) Y.
Proof.
intros. apply (set_fold_union_strong _ _ _ _ _ _).
- intros x b' _. by rewrite (assoc_L f), (idemp f).
- intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) X Y :
( x, Proper (R ==> R) (f x))
( x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 X Y x2 X Y x1 x2
R (f x1 (f x2 b')) (f x2 (f x1 b')))
X ## Y
R (set_fold f b (X Y)) (set_fold f (set_fold f b X) Y).
Proof. intros. apply set_fold_union_strong; set_solver. Qed.
Lemma set_fold_disj_union (f : A A A) (b : A) X Y :
Comm (=) f
Assoc (=) f
......@@ -345,7 +429,7 @@ Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
(** * Minimal elements *)
Lemma minimal_exists R `{!Transitive R, x y, Decision (R x y)} (X : C) :
Lemma minimal_exists_elem_of R `{!Transitive R, x y, Decision (R x y)} (X : C) :
X x, x X minimal R x X.
Proof.
pattern X; apply set_ind; clear X.
......@@ -361,10 +445,20 @@ Proof.
exists x; split; [set_solver|].
rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
x y, Decision (R x y)} (X : C) :
X x, x X minimal R x X.
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
Lemma minimal_exists R `{!Transitive R,
x y, Decision (R x y)} `{!Inhabited A} (X : C) :
x, minimal R x X.
Proof.
destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
- edestruct (minimal_exists_elem_of R X) as (x & Hel & Hmin); first set_solver.
exists x. done.
- exists inhabitant. intros y Hel. set_solver.
Qed.
(** * Filter *)
Lemma elem_of_filter (P : A Prop) `{!∀ x, Decision (P x)} X x :
......@@ -701,7 +795,7 @@ Section infinite.
Forall_fresh X xs Y X Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n.
Lemma length_fresh_list n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed.
Lemma fresh_list_is_fresh n X x : x fresh_list n X x X.
Proof.
......@@ -726,5 +820,5 @@ Lemma size_set_seq `{FinSet nat C} start len :
Proof.
rewrite <-list_to_set_seq, size_list_to_set.
2:{ apply NoDup_seq. }
rewrite seq_length. done.
rewrite length_seq. done.
Qed.
......@@ -120,7 +120,7 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
Proof.
intros. apply submseteq_length_Permutation.
- by apply finite_inj_submseteq.
- rewrite fmap_length. by apply Nat.eq_le_incl.
- rewrite length_fmap. by apply Nat.eq_le_incl.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B Surj (=) f.
......@@ -146,7 +146,7 @@ Proof.
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- intros [f ?]. unfold card. rewrite <-(fmap_length f).
- intros [f ?]. unfold card. rewrite <-(length_fmap f).
by apply submseteq_length, (finite_inj_submseteq f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
......@@ -216,7 +216,7 @@ Section enc_finite.
split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
Qed.
Lemma enc_finite_card : card A = c.
Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
End enc_finite.
(** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
......@@ -262,7 +262,7 @@ Next Obligation.
apply elem_of_list_fmap. eauto using elem_of_enum.
Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap. Qed.
Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
......@@ -297,7 +297,7 @@ Next Obligation.
[left|right]; (eexists; split; [done|apply elem_of_enum]).
Qed.
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.
Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := a enum A; (a,.) <$> enum B |}.
......@@ -315,7 +315,7 @@ Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
unfold card; simpl. induction (enum A); simpl; auto.
rewrite app_length, fmap_length. auto.
rewrite length_app, length_fmap. auto.
Qed.
Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
......@@ -343,18 +343,18 @@ Proof.
unfold card; simpl. induction n as [|n IH]; simpl; [done|].
rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
by rewrite app_length, fmap_length, IH.
by rewrite length_app, length_fmap, IH.
Qed.
Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
Proof.
refine (bijective_finite (λ v : vec A n, vec_to_list v vec_to_list_length _)).
refine (bijective_finite (λ v : vec A n, vec_to_list v length_vec_to_list _)).
- abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
- abstract (intros [l <-]; exists (list_to_vec l);
apply (sig_eq_pi _), vec_to_list_to_vec).
Defined.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof. unfold card; simpl. rewrite fmap_length. apply vec_card. Qed.
Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
Fixpoint fin_enum (n : nat) : list (fin n) :=
match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
......@@ -369,7 +369,7 @@ Next Obligation.
rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
Qed.
Lemma fin_card n : card (fin n) = n.
Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
(* shouldn’t be an instance (cycle with [sig_finite]): *)
Lemma finite_sig_dec `{!EqDecision A} (P : A Prop) `{Finite (sig P)} x :
......@@ -415,7 +415,7 @@ Section sig_finite.
split; [by destruct p | apply elem_of_enum].
Qed.
Lemma sig_card : card (sig P) = length (filter P (enum A)).
Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
End sig_finite.
Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A B) :
......
......@@ -63,6 +63,7 @@ Global Arguments GNodes {A P} _.
Record gmap_key K `{Countable K} (q : positive) :=
GMapKey { _ : encode (A:=K) <$> decode q = Some q }.
Add Printing Constructor gmap_key.
Global Arguments GMapKey {_ _ _ _} _.
Lemma gmap_key_encode `{Countable K} (k : K) : gmap_key K (encode k).
......@@ -71,6 +72,7 @@ Global Instance gmap_key_pi `{Countable K} q : ProofIrrel (gmap_key K q).
Proof. intros [?] [?]. f_equal. apply (proof_irrel _). Qed.
Record gmap K `{Countable K} A := GMap { gmap_car : gmap_dep A (gmap_key K) }.
Add Printing Constructor gmap.
Global Arguments GMap {_ _ _ _} _.
Global Arguments gmap_car {_ _ _ _} _.
......@@ -442,45 +444,68 @@ Section gmap_merge.
Qed.
End gmap_merge.
Section gmap_fold.
Context {A B} (f : positive A B B).
Local Lemma gmap_dep_fold_GNode {P} i y (ml : gmap_dep A P~0) mx mr :
GNode_valid ml mx mr
gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
(gmap_dep_fold f i~0
match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
Proof. by destruct ml, mx as [[]|], mr. Qed.
Local Lemma gmap_dep_fold_GNode {A B} (f : positive A B B)
{P} i y (ml : gmap_dep A P~0) mx mr :
gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
(gmap_dep_fold f i~0
match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
Proof. by destruct ml, mx as [[]|], mr. Qed.
Local Lemma gmap_dep_fold_ind {P} (Q : B gmap_dep A P Prop) (b : B) j :
Q b GEmpty
( i p x mt r, gmap_dep_lookup i mt = None
Q r mt
Q (f (Pos.reverse_go i j) x r) (gmap_dep_partial_alter (λ _, Some x) i p mt))
mt, Q (gmap_dep_fold f j b mt) mt.
Proof.
intros Hemp Hinsert mt. revert Q b j Hemp Hinsert.
induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
intros Q b j Hemp Hinsert; [done|].
rewrite gmap_dep_fold_GNode by done.
apply (IHr (λ y mt, Q y (GNode ml mx mt))).
{ apply (IHl (λ y mt, Q y (GNode mt mx GEmpty))).
{ destruct mx as [[p x]|]; [|done].
replace (GNode GEmpty (Some (p,x)) GEmpty) with
(gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
by apply Hinsert. }
intros i p x mt r ??.
replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
Local Lemma gmap_dep_fold_ind {A} {P} (Q : gmap_dep A P Prop) :
Q GEmpty
( i p x mt,
gmap_dep_lookup i mt = None
( j A' B (f : positive A' B B) (g : A A') b x',
gmap_dep_fold f j b
(gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
= f (Pos.reverse_go i j) x' (gmap_dep_fold f j b (gmap_dep_fmap g mt)))
Q mt Q (gmap_dep_partial_alter (λ _, Some x) i p mt))
mt, Q mt.
Proof.
intros Hemp Hinsert mt. revert Q Hemp Hinsert.
induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
intros Q Hemp Hinsert; [done|].
apply (IHr (λ mt, Q (GNode ml mx mt))).
{ apply (IHl (λ mt, Q (GNode mt mx GEmpty))).
{ destruct mx as [[p x]|]; [|done].
replace (GNode GEmpty (Some (p,x)) GEmpty) with
(gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
by apply Hinsert. }
intros i p x mt r ? Hfold.
replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
by (by destruct mt, mx as [[]|]).
apply Hinsert.
- by rewrite gmap_dep_lookup_GNode.
- intros j A' B f g b x'.
replace (gmap_dep_partial_alter (λ _, Some x') (i~0) p
(gmap_dep_fmap g (GNode mt mx GEmpty)))
with (GNode (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
(prod_map id g <$> mx) GEmpty)
by (by destruct mt, mx as [[]|]).
replace (gmap_dep_fmap g (GNode mt mx GEmpty))
with (GNode (gmap_dep_fmap g mt) (prod_map id g <$> mx) GEmpty)
by (by destruct mt, mx as [[]|]).
apply Hinsert; by rewrite ?gmap_dep_lookup_GNode. }
intros i p x mt r ??.
replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
rewrite !gmap_dep_fold_GNode; simpl; auto.
- done. }
intros i p x mt r ? Hfold.
replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
by (by destruct ml, mx as [[]|], mt).
apply Hinsert.
- by rewrite gmap_dep_lookup_GNode.
- intros j A' B f g b x'.
replace (gmap_dep_partial_alter (λ _, Some x') (i~1) p
(gmap_dep_fmap g (GNode ml mx mt)))
with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx)
(gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt)))
by (by destruct ml, mx as [[]|], mt).
apply Hinsert; by rewrite ?gmap_dep_lookup_GNode.
Qed.
End gmap_fold.
replace (gmap_dep_fmap g (GNode ml mx mt))
with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx) (gmap_dep_fmap g mt))
by (by destruct ml, mx as [[]|], mt).
rewrite !gmap_dep_fold_GNode; simpl; auto.
- done.
Qed.
(** Instance of the finite map type class *)
Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
......@@ -494,11 +519,16 @@ Proof.
- intros A b f [mt] i. apply gmap_dep_lookup_fmap.
- intros A B f [mt] i. apply gmap_dep_lookup_omap.
- intros A B C f [mt1] [mt2] i. apply gmap_dep_lookup_merge.
- intros A B P f b Hemp Hinsert [mt].
apply (gmap_dep_fold_ind _ (λ r mt, P r (GMap mt))); clear mt; [done|].
intros i [Hk] x mt r ??; simpl. destruct (fmap_Some_1 _ _ _ Hk) as (k&->&->).
assert (GMapKey Hk = gmap_key_encode k) as -> by (apply proof_irrel).
by apply (Hinsert _ _ (GMap mt)).
- done.
- intros A P Hemp Hins [mt].
apply (gmap_dep_fold_ind (λ mt, P (GMap mt))); clear mt; [done|].
intros i [Hk] x mt ? Hfold. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk'&->).
assert (GMapKey Hk = gmap_key_encode k) as Hkk by (apply proof_irrel).
rewrite Hkk in Hfold |- *. clear Hk Hkk.
apply (Hins k x (GMap mt)); [done|]. intros A' B f g b x'.
trans ((match decode (encode k) with Some k => f k x' | None => id end)
(map_fold f b (g <$> GMap mt))); [apply (Hfold 1)|].
by rewrite Hk'.
Qed.
Global Program Instance gmap_countable
......@@ -581,10 +611,10 @@ Section curry_uncurry.
Lemma lookup_gmap_uncurry (m : gmap K1 (gmap K2 A)) i j :
gmap_uncurry m !! (i,j) = m !! i ≫= (.!! j).
Proof.
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
apply (map_fold_weak_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_weak_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. }
......@@ -598,7 +628,7 @@ Section curry_uncurry.
Lemma lookup_gmap_curry (m : gmap (K1 * K2) A) i j :
gmap_curry m !! i ≫= (.!! j) = m !! (i, j).
Proof.
apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
apply (map_fold_weak_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 [->|].
......@@ -611,8 +641,8 @@ Section curry_uncurry.
Lemma lookup_gmap_curry_None (m : gmap (K1 * K2) A) i :
gmap_curry m !! i = None ( j, m !! (i, j) = None).
Proof.
apply (map_fold_ind (λ mr m, mr !! i = None ( j, m !! (i, j) = None)));
[done|].
apply (map_fold_weak_ind
(λ mr m, mr !! i = None ( j, m !! (i, j) = None))); [done|].
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
- split; [by rewrite lookup_partial_alter|].
......@@ -793,4 +823,25 @@ Section gset.
Qed.
End gset.
Section gset_cprod.
Context `{Countable A, Countable B}.
Global Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) :=
λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
x cprod X Y x.1 X x.2 Y.
Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
Global Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
SetUnfoldElemOf x.1 X P SetUnfoldElemOf x.2 Y Q
SetUnfoldElemOf x (cprod X Y) (P Q).
Proof using.
intros ??; constructor.
by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
(set_unfold_elem_of x.2 Y Q).
Qed.
End gset_cprod.
Global Typeclasses Opaque gset.
......@@ -61,12 +61,19 @@ Section definitions.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom X.
Definition gmultiset_map `{Countable B} (f : A B)
(X : gmultiset A) : gmultiset B :=
GMultiSet $ map_fold
(λ x n, partial_alter (Some from_option (Pos.add n) n) (f x))
(gmultiset_car X).
End definitions.
Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom gmultiset_map.
Section basic_lemmas.
Context `{Countable A}.
......@@ -152,6 +159,13 @@ Section basic_lemmas.
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
Lemma gmultiset_elem_of_dom x X : x dom X x X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
End basic_lemmas.
(** * A solver for multisets *)
......@@ -292,6 +306,9 @@ Section multiset_unfold.
intros ??; constructor. rewrite gmultiset_elem_of_intersection.
by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_gmultiset_dom x X :
SetUnfoldElemOf x (dom X) (x X).
Proof. constructor. apply gmultiset_elem_of_dom. Qed.
End multiset_unfold.
(** Step 3: instantiate hypotheses *)
......@@ -485,6 +502,9 @@ Section more_lemmas.
Global Instance list_to_set_disj_perm :
Proper (() ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof. induction 1; multiset_solver. Qed.
Lemma list_to_set_disj_replicate n x :
list_to_set_disj (replicate n x) =@{gmultiset A} n *: {[+ x +]}.
Proof. induction n; multiset_solver. Qed.
(** Properties of the elements operation *)
Lemma gmultiset_elements_empty : elements ( : gmultiset A) = [].
......@@ -544,12 +564,6 @@ Section more_lemmas.
exists (x,n); split; [|by apply elem_of_map_to_list].
apply elem_of_replicate; auto with lia.
Qed.
Lemma gmultiset_elem_of_dom x X : x dom X x X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
(** Properties of the set_fold operation *)
Lemma gmultiset_set_fold_empty {B} (f : A B B) (b : B) :
......@@ -640,7 +654,7 @@ Section more_lemmas.
Lemma gmultiset_size_disj_union X Y : size (X Y) = size X + size Y.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite gmultiset_elements_disj_union, app_length.
by rewrite gmultiset_elements_disj_union, length_app.
Qed.
Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
Proof.
......@@ -655,15 +669,17 @@ Section more_lemmas.
Local Lemma gmultiset_subseteq_alt X Y :
X Y
map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
map_relation (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
(gmultiset_car X) (gmultiset_car Y).
Proof.
apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation Pos.le
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
refine (λ X Y, cast_if (decide (map_relation
(λ _, Pos.le) (λ _ _, False) (λ _ _, True)
(gmultiset_car X) (gmultiset_car Y))));
by rewrite gmultiset_subseteq_alt.
Defined.
......@@ -774,3 +790,120 @@ Section more_lemmas.
apply Hinsert, IH; multiset_solver.
Qed.
End more_lemmas.
(** * Map *)
Section map.
Context `{Countable A, Countable B}.
Context (f : A B).
Lemma gmultiset_map_alt X :
gmultiset_map f X = list_to_set_disj (f <$> elements X).
Proof.
destruct X as [m]. unfold elements, gmultiset_map. simpl.
induction m as [|x n m ?? IH] using map_first_key_ind; [done|].
rewrite map_to_list_insert_first_key, map_fold_insert_first_key by done.
csimpl. rewrite fmap_app, fmap_replicate, list_to_set_disj_app, <-IH.
apply gmultiset_eq; intros y.
rewrite multiplicity_disj_union, list_to_set_disj_replicate.
rewrite multiplicity_scalar_mul, multiplicity_singleton'.
unfold multiplicity; simpl. destruct (decide (y = f x)) as [->|].
- rewrite lookup_partial_alter; simpl. destruct (_ !! f x); simpl; lia.
- rewrite lookup_partial_alter_ne by done. lia.
Qed.
Lemma gmultiset_map_empty : gmultiset_map f = ∅.
Proof. done. Qed.
Lemma gmultiset_map_disj_union X Y :
gmultiset_map f (X Y) = gmultiset_map f X gmultiset_map f Y.
Proof.
apply gmultiset_eq; intros x.
rewrite !gmultiset_map_alt, gmultiset_elements_disj_union, fmap_app.
by rewrite list_to_set_disj_app.
Qed.
Lemma gmultiset_map_singleton x :
gmultiset_map f {[+ x +]} = {[+ f x +]}.
Proof.
rewrite gmultiset_map_alt, gmultiset_elements_singleton.
multiset_solver.
Qed.
Lemma elem_of_gmultiset_map X y :
y gmultiset_map f X x, y = f x x X.
Proof.
rewrite gmultiset_map_alt, elem_of_list_to_set_disj, elem_of_list_fmap.
by setoid_rewrite gmultiset_elem_of_elements.
Qed.
Lemma multiplicity_gmultiset_map X x :
Inj (=) (=) f
multiplicity (f x) (gmultiset_map f X) = multiplicity x X.
Proof.
intros. induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
rewrite gmultiset_map_disj_union, gmultiset_map_singleton,
!multiplicity_disj_union.
multiset_solver.
Qed.
Global Instance gmultiset_map_inj :
Inj (=) (=) f Inj (=) (=) (gmultiset_map f).
Proof.
intros ? X Y HXY. apply gmultiset_eq; intros x.
by rewrite <-!(multiplicity_gmultiset_map _ _ _), HXY.
Qed.
Global Instance set_unfold_gmultiset_map X (P : A Prop) y :
( x, SetUnfoldElemOf x X (P x))
SetUnfoldElemOf y (gmultiset_map f X) ( x, y = f x P x).
Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.
Global Instance multiset_unfold_map x X n :
Inj (=) (=) f
MultisetUnfold x X n
MultisetUnfold (f x) (gmultiset_map f X) n.
Proof.
intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
Qed.
End map.
(** * Big disjoint unions *)
Section disj_union_list.
Context `{Countable A}.
Implicit Types X Y : gmultiset A.
Implicit Types Xs Ys : list (gmultiset A).
Lemma gmultiset_disj_union_list_nil :
⋃+ (@nil (gmultiset A)) = ∅.
Proof. done. Qed.
Lemma gmultiset_disj_union_list_cons X Xs :
⋃+ (X :: Xs) = X ⋃+ Xs.
Proof. done. Qed.
Lemma gmultiset_disj_union_list_singleton X :
⋃+ [X] = X.
Proof. simpl. by rewrite (right_id_L _). Qed.
Lemma gmultiset_disj_union_list_app Xs1 Xs2 :
⋃+ (Xs1 ++ Xs2) = ⋃+ Xs1 ⋃+ Xs2.
Proof.
induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id_L _)|].
by rewrite IH, (assoc_L _).
Qed.
Lemma elem_of_gmultiset_disj_union_list Xs x :
x ⋃+ Xs X, X Xs x X.
Proof. induction Xs; multiset_solver. Qed.
Lemma multiplicity_gmultiset_disj_union_list x Xs :
multiplicity x (⋃+ Xs) = sum_list (multiplicity x <$> Xs).
Proof.
induction Xs as [|X Xs IH]; [done|]; simpl.
by rewrite multiplicity_disj_union, IH.
Qed.
Global Instance gmultiset_disj_union_list_proper :
Proper (() ==> (=)) (@disj_union_list (gmultiset A) _ _).
Proof. induction 1; multiset_solver. Qed.
End disj_union_list.
......@@ -45,7 +45,7 @@ Section search_infinite.
split; [done|]. apply elem_of_list_filter; naive_solver lia. }
intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
intros n1; constructor; intros n2 [Hn Hs].
apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
Qed.
Definition search_infinite_go (xs : list B) (n : nat)
......@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
Next Obligation.
intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
apply elem_of_list_fmap. eexists; split; [|done].
unfold fresh. by rewrite replicate_length.
unfold fresh. by rewrite length_replicate.
Qed.
Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
......
This diff is collapsed.
This diff is collapsed.