...
 
Commits (10)
image: ralfjung/opam-ci:latest
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template
stage: build
tags:
- fp
script:
- git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
......@@ -29,9 +29,15 @@ variables:
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
VALIDATE: "1"
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
<<: *template
variables:
......
......@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.9\b" > /dev/null && echo 1)
COQ_BROKEN=
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
......
......@@ -38,7 +38,7 @@ Notably:
This version is known to compile with:
- Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1
- Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
## Installing via opam
......
Subproject commit fb4a01dacbd489e6a4c50c2659486f589ba470d3
......@@ -16,6 +16,11 @@ Instance collection_filter
of_list (filter P (elements X)).
Typeclasses Opaque collection_filter.
Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A B) (X : C) : D :=
of_list (f <$> elements X).
Typeclasses Opaque collection_map.
Section fin_collection.
Context `{FinCollection A C}.
Implicit Types X Y : C.
......@@ -248,6 +253,39 @@ Section filter.
End leibniz_equiv.
End filter.
(** * Map *)
Section map.
Context `{Collection B D}.
Lemma elem_of_map (f : A B) (X : C) y :
y collection_map (D:=D) f X x, y = f x x X.
Proof.
unfold collection_map. rewrite elem_of_of_list, elem_of_list_fmap.
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 collection_map (D:=D) f X) ( y, x = f y P y).
Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
Global Instance collection_map_proper :
Proper (pointwise_relation _ (=) ==> () ==> ()) (collection_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
Global Instance collection_map_mono :
Proper (pointwise_relation _ (=) ==> () ==> ()) (collection_map (C:=C) (D:=D)).
Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
Lemma elem_of_map_1 (f : A B) (X : C) (y : B) :
y collection_map (D:=D) f X x, y = f x x X.
Proof. set_solver. Qed.
Lemma elem_of_map_2 (f : A B) (X : C) (x : A) :
x X f x collection_map (D:=D) f X.
Proof. set_solver. Qed.
Lemma elem_of_map_2_alt (f : A B) (X : C) (x : A) (y : B) :
x X y = f x y collection_map (D:=D) f X.
Proof. set_solver. Qed.
End map.
(** * Decision procedures *)
Lemma set_Forall_elements P X : set_Forall P X Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
......