diff --git a/Makefile b/Makefile
deleted file mode 100644
index a3182f76705c73c28681e216b71c247212239cb5..0000000000000000000000000000000000000000
--- a/Makefile
+++ /dev/null
@@ -1,337 +0,0 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.5rc1 ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject -o Makefile
-#
-
-.DEFAULT_GOAL := all
-
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# TIMECMD set a command to log .v compilation time;
-# TIMED if non empty, use the default time command as TIMECMD;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-TIMED=
-TIMECMD=
-STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
-
-vo_to_obj = $(addsuffix .o,\
- $(filter-out Warning: Error:,\
- $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
-
-##########################
-# #
-# Libraries definitions. #
-# #
-##########################
-
-COQLIBS?=-Q "." ""
-COQDOCLIBS?=-Q "." ""
-
-##########################
-# #
-# Variables definitions. #
-# #
-##########################
-
-
-OPT?=
-COQDEP?="$(COQBIN)coqdep" -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(TIMER) "$(COQBIN)coqc"
-GALLINA?="$(COQBIN)gallina"
-COQDOC?="$(COQBIN)coqdoc"
-COQCHK?="$(COQBIN)coqchk"
-COQMKTOP?="$(COQBIN)coqmktop"
-
-##################
-# #
-# Install Paths. #
-# #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?="$(HOME)/.local/share"
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL="${COQLIB}user-contrib"
-COQDOCINSTALL="${DOCDIR}user-contrib"
-COQTOPINSTALL="${COQLIB}toploop"
-endif
-
-######################
-# #
-# Files dispatching. #
-# #
-######################
-
-VFILES:=barrier/heap_lang.v\
- iris/parameter.v\
- iris/hoare.v\
- iris/resources.v\
- iris/pviewshifts.v\
- iris/language.v\
- iris/weakestpre.v\
- iris/ownership.v\
- iris/wsat.v\
- iris/viewshifts.v\
- iris/namespace.v\
- iris/lifting.v\
- iris/hoare_lifting.v\
- iris/adequacy.v\
- iris/model.v\
- modures/excl.v\
- modures/ra.v\
- modures/agree.v\
- modures/cofe_solver.v\
- modures/dra.v\
- modures/base.v\
- modures/cofe.v\
- modures/logic.v\
- modures/fin_maps.v\
- modures/auth.v\
- modures/sts.v\
- modures/cmra.v\
- modures/option.v\
- prelude/error.v\
- prelude/list.v\
- prelude/decidable.v\
- prelude/sets.v\
- prelude/lexico.v\
- prelude/co_pset.v\
- prelude/zmap.v\
- prelude/nmap.v\
- prelude/numbers.v\
- prelude/finite.v\
- prelude/listset_nodup.v\
- prelude/prelude.v\
- prelude/tactics.v\
- prelude/base.v\
- prelude/gmap.v\
- prelude/streams.v\
- prelude/listset.v\
- prelude/collections.v\
- prelude/relations.v\
- prelude/strings.v\
- prelude/natmap.v\
- prelude/orders.v\
- prelude/countable.v\
- prelude/pretty.v\
- prelude/hashset.v\
- prelude/proof_irrel.v\
- prelude/mapset.v\
- prelude/fin_collections.v\
- prelude/stringmap.v\
- prelude/pmap.v\
- prelude/vector.v\
- prelude/fin_maps.v\
- prelude/bsets.v\
- prelude/fin_map_dom.v\
- prelude/option.v
-
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(VFILES))
-else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(VFILES))
-endif
-endif
-
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-VO=vo
-VOFILES:=$(VFILES:.v=.$(VO))
-GLOBFILES:=$(VFILES:.v=.glob)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES=$(call vo_to_obj,$(VOFILES))
-ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
-NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ifeq '$(HASNATDYNLINK)' 'true'
-HASNATDYNLINK_OR_EMPTY := yes
-else
-HASNATDYNLINK_OR_EMPTY :=
-endif
-
-#######################################
-# #
-# Definition of the toplevel targets. #
-# #
-#######################################
-
-all: $(VOFILES)
-
-quick: $(VOFILES:.vo=.vio)
-
-vio2vo:
- $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-checkproofs:
- $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
- $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
- for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
- @echo 'Do not do "make clean" until you are sure that everything went well!'
- @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-byte:
- $(MAKE) all "OPT:=-byte"
-
-opt:
- $(MAKE) all "OPT:=-opt"
-
-userinstall:
- +$(MAKE) USERINSTALL=true install
-
-install:
- cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
- install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)//$$i`"; \
- install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)//$$i; \
- done
-
-install-doc:
- install -d "$(DSTROOT)"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/html
- for i in html/*; do \
- install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/$$i;\
- done
-
-uninstall_me.sh: Makefile
- echo '#!/bin/sh' > $@
- printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/ && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
- printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT) \\\n' >> "$@"
- printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
- printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find $(INSTALLDEFAULTROOT)/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
- chmod +x $@
-
-uninstall: uninstall_me.sh
- sh $<
-
-clean::
- rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
- find . -name .coq-native -type d -empty -delete
- rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
- rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- - rm -rf html mlihtml uninstall_me.sh
-
-cleanall:: clean
- rm -f $(patsubst %.v,.%.aux,$(VFILES))
-
-archclean::
- rm -f *.cmx *.o
-
-printenv:
- @"$(COQBIN)coqtop" -config
- @echo 'CAMLC = $(CAMLC)'
- @echo 'CAMLOPTC = $(CAMLOPTC)'
- @echo 'PP = $(PP)'
- @echo 'COQFLAGS = $(COQFLAGS)'
- @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
- @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
-
-Makefile: _CoqProject
- mv -f $@ $@.bak
- "$(COQBIN)coq_makefile" -f $< -o $@
-
-
-###################
-# #
-# Implicit rules. #
-# #
-###################
-
-$(VOFILES): %.vo: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-$(GLOBFILES): %.glob: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-$(VFILES:.v=.vio): %.vio: %.v
- $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*
-
-$(GFILES): %.g: %.v
- $(GALLINA) $<
-
-$(VFILES:.v=.tex): %.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-$(HTMLFILES): %.html: %.v %.glob
- $(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-$(VFILES:.v=.g.tex): %.g.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-$(GHTMLFILES): %.g.html: %.v %.glob
- $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
-
-$(addsuffix .d,$(VFILES)): %.v.d: %.v
- $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-$(addsuffix .beautified,$(VFILES)): %.v.beautified:
- $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
diff --git a/configure b/configure
new file mode 100755
index 0000000000000000000000000000000000000000..eeb3f9d750a6878ff23b94a0ad9a642f575b4267
--- /dev/null
+++ b/configure
@@ -0,0 +1,2 @@
+#!/bin/sh
+coq_makefile -f _CoqProject -o Makefile
diff --git a/iris/model.v b/iris/model.v
index 6097d19157b9355f616a80fb4db55f8ddf56b761..61b2f1566a4e73bd0e7bead9e68a045f1fc45004 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -2,26 +2,32 @@ Require Export modures.logic iris.resources.
Require Import modures.cofe_solver.
Module iProp.
-Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ A).
+Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
(f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
- uPredC_map (resRA_map (f.1)).
+ uPredC_map (resRA_map (laterC_map (f.1))).
Definition result Σ : solution (F Σ).
Proof.
apply (solver.result _ (@map Σ)).
- * by intros A B r n ?; rewrite /uPred_holds /= res_map_id.
- * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?;
- rewrite /= /uPred_holds /= res_map_compose.
- * by intros A1 A2 B1 B2 n f f' [??] r;
- apply upredC_map_ne, resRA_map_contractive.
+ * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
+ rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
+ * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
+ rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
+ rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
+ by rewrite -later_map_compose.
+ * intros A1 A2 B1 B2 n f f' [??] P.
+ by apply upredC_map_ne, resRA_map_ne, laterC_map_contractive.
Qed.
End iProp.
(* Solution *)
Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
-Notation res' Σ := (res Σ (iPreProp Σ)).
-Notation icmra' Σ := (icmra Σ (laterC (iPreProp Σ))).
-Definition iProp (Σ : iParam) : cofeT := uPredC (resRA Σ (iPreProp Σ)).
+Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
+Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
+Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
+Notation iPst Σ := (exclRA (istateC Σ)).
+Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
+Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
@@ -34,3 +40,7 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
+
+Module Test. (* Make sure we got the notations right. *)
+ Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+End Test.
diff --git a/iris/ownership.v b/iris/ownership.v
index c49a468813eefa5e51a8025c0241f5dec2e55f61..68f99ad9ed2a43029f8a4c980358cfcac86a168f 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -4,7 +4,7 @@ Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
Arguments inv {_} _ _%I.
Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : icmra' Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
+Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
Instance: Params (@inv) 2.
Instance: Params (@ownP) 1.
Instance: Params (@ownG) 1.
@@ -13,10 +13,10 @@ Typeclasses Opaque inv ownG ownP.
Section ownership.
Context {Σ : iParam}.
-Implicit Types r : res' Σ.
+Implicit Types r : iRes Σ.
Implicit Types σ : istate Σ.
Implicit Types P : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
(* Invariants *)
Global Instance inv_contractive i : Contractive (@inv Σ i).
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index 2e83581e4ebd8cd3bb40cfdff8105749fa8d3c7f..81ee2f4eec368916dff1dd9f5a644d6597aa6a31 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -29,7 +29,7 @@ Instance: Params (@pvs) 3.
Section pvs.
Context {Σ : iParam}.
Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
Transparent uPred_holds.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
@@ -96,7 +96,7 @@ Proof.
* by rewrite -(left_id_L ∅ (∪) Ef).
* apply uPred_weaken with r n; auto.
Qed.
-Lemma pvs_updateP E m (P : icmra' Σ → Prop) :
+Lemma pvs_updateP E m (P : iGst Σ → Prop) :
m â‡: P → ownG m ⊑ pvs E E (∃ m', â– P m' ∧ ownG m').
Proof.
intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
diff --git a/iris/resources.v b/iris/resources.v
index 73996b11c75bf4522335b6e173bdc6eba81066b9..067b47e22eb219dccc9386f73c6d5fa2f3132875 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -1,9 +1,9 @@
Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
Record res (Σ : iParam) (A : cofeT) := Res {
- wld : mapRA positive (agreeRA (laterC A));
+ wld : mapRA positive (agreeRA A);
pst : exclRA (istateC Σ);
- gst : icmra Σ (laterC A);
+ gst : icmra Σ A;
}.
Add Printing Constructor res.
Arguments Res {_ _} _ _ _.
@@ -137,7 +137,7 @@ Canonical Structure resRA : cmraT :=
Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : icmra Σ (laterC A)) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A :=
Res (wld r) (pst r) m.
Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
@@ -167,9 +167,9 @@ End res.
Arguments resRA : clear implicits.
Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
- Res (agree_map (later_map f) <$> (wld r))
+ Res (agree_map f <$> (wld r))
(pst r)
- (icmra_map Σ (laterC_map f) (gst r)).
+ (icmra_map Σ f (gst r)).
Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) :
(∀ n, Proper (dist n ==> dist n) f) →
∀ n, Proper (dist n ==> dist n) (@res_map Σ _ _ f).
@@ -178,20 +178,22 @@ Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r.
Proof.
constructor; simpl; [|done|].
* rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
- rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
- by rewrite later_map_id.
- * rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
- by rewrite later_map_id.
+ by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
+ * by rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
Qed.
Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) :
res_map (g ◎ f) r ≡ res_map g (res_map f r).
Proof.
constructor; simpl; [|done|].
* rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
- rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
- by rewrite later_map_compose.
- * rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
- by rewrite later_map_compose.
+ by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
+ * by rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
+Qed.
+Lemma res_map_ext {Σ A B} (f g : A -n> B) :
+ (∀ r, f r ≡ g r) -> ∀ r : res Σ A, res_map f r ≡ res_map g r.
+Proof.
+ move=>H r. split; simpl;
+ [apply map_fmap_setoid_ext; intros; apply agree_map_ext | | apply icmra_map_ext]; done.
Qed.
Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
CofeMor (res_map f : resRA Σ A → resRA Σ B).
@@ -203,10 +205,10 @@ Proof.
intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
* by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed.
-Instance resRA_map_contractive {Σ A B} : Contractive (@resRA_map Σ A B).
+Lemma resRA_map_ne {Σ A B} (f g : A -n> B) n :
+ f ={n}= g → resRA_map (Σ := Σ) f ={n}= resRA_map g.
Proof.
- intros n f g ? r; constructor; simpl; [|done|].
- * by apply (mapRA_map_ne _ (agreeRA_map (laterC_map f))
- (agreeRA_map (laterC_map g))), agreeRA_map_ne, laterC_map_contractive.
- * by apply icmra_map_ne, laterC_map_contractive.
+ intros ? r. split; simpl;
+ [apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne
+ | | apply icmra_map_ne]; done.
Qed.
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index de7568c0ea834f0ec9303f3cc5881fc6cf32196f..a090f5f85fe5109f780a1947396385de47d7de59 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -16,7 +16,7 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
Section vs.
Context {Σ : iParam}.
Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
Import uPred.
Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
@@ -85,7 +85,7 @@ Proof.
intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
apply vs_close.
Qed.
-Lemma vs_updateP E m (P : icmra' Σ → Prop) :
+Lemma vs_updateP E m (P : iGst Σ → Prop) :
m â‡: P → ownG m >{E}> (∃ m', â– P m' ∧ ownG m').
Proof. by intros; apply vs_alt, pvs_updateP. Qed.
Lemma vs_update E m m' : m ⇠m' → ownG m >{E}> ownG m'.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 3e9a5088b8266b24a59103ce360de16eb1a1d020..e866cba4422e5d65240a894b5e8678a5f1cfa53a 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -7,8 +7,8 @@ Local Hint Extern 10 (✓{_} _) =>
repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
solve_validN.
-Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
- (k : nat) (rf : res' Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
+Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
+ (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
wf_safe : reducible e1 σ1;
wp_step e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
@@ -18,7 +18,7 @@ Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
∀ e', ef = Some e' → Qfork e' k r2'
}.
CoInductive wp_pre {Σ} (E : coPset)
- (Q : ival Σ → iProp Σ) : iexpr Σ → nat → res' Σ → Prop :=
+ (Q : ival Σ → iProp Σ) : iexpr Σ → nat → iRes Σ → Prop :=
| wp_pre_0 e r : wp_pre E Q e 0 r
| wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
| wp_pre_step n r1 e1 :
diff --git a/iris/wsat.v b/iris/wsat.v
index ac5f7e5019d34b59c08b3779ef48d9d1489b3f82..a9afb6facf148e02209c15dbb595ae259154af8f 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -5,7 +5,7 @@ Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
Record wsat_pre {Σ} (n : nat) (E : coPset)
- (σ : istate Σ) (rs : gmap positive (res' Σ)) (r : res' Σ) := {
+ (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
wsat_pre_valid : ✓{S n} r;
wsat_pre_state : pst r ≡ Excl σ;
wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
@@ -19,7 +19,7 @@ Arguments wsat_pre_state {_ _ _ _ _ _} _.
Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _.
Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
-Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : res' Σ) : Prop :=
+Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop :=
match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
Instance: Params (@wsat) 4.
Arguments wsat : simpl never.
@@ -27,8 +27,8 @@ Arguments wsat : simpl never.
Section wsat.
Context {Σ : iParam}.
Implicit Types σ : istate Σ.
-Implicit Types r : res' Σ.
-Implicit Types rs : gmap positive (res' Σ).
+Implicit Types r : iRes Σ.
+Implicit Types rs : gmap positive (iRes Σ).
Implicit Types P : iProp Σ.
Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ).
@@ -120,7 +120,7 @@ Proof.
split; [done|exists rs].
by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : icmra' Σ → Prop) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
m1 ≼{S n} gst r → m1 â‡: P →
wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
Proof.
diff --git a/modures/cmra.v b/modures/cmra.v
index 7b2b4127583f87d7990ccb5bda87ff74641e719b..39ea086c82a135ef625896f8088e57e78a7fbc1b 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -105,6 +105,13 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
validN_preserving n x : ✓{n} x → ✓{n} (f x)
}.
+Instance compose_cmra_monotone {A B C : cmraT} (f : A -n> B) (g : B -n> C) :
+ CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ◎ f).
+Proof.
+ split.
+ - move=> n x y Hxy /=. eapply includedN_preserving, includedN_preserving; done.
+ - move=> n x Hx /=. eapply validN_preserving, validN_preserving; done.
+Qed.
(** * Updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
diff --git a/modures/logic.v b/modures/logic.v
index e9b058004387d504d26062b8098abf09f30b655e..a8d29109913dbdf6de2a7fcec86245c8106e4d8e 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -54,20 +54,31 @@ Instance uPred_holds_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_holds_ne, equiv_dist. Qed.
(** functor *)
-Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1)
- `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
- (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
+Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
+ `{!CMRAMonotone f} (P : uPred M1) :
+ uPred M2 := {| uPred_holds n x := P n (f x) |}.
+Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
+Next Obligation. intros M1 M2 f _ P x; apply uPred_0. Qed.
Next Obligation.
naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Qed.
-Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 → M1)
- `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :
+Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
+ `{!CMRAMonotone f} :
Proper (dist n ==> dist n) (uPred_map f).
Proof.
by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
Qed.
+Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
+Proof. by intros x n ?. Qed.
+Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+ `{!CMRAMonotone f} `{!CMRAMonotone g}
+ (P : uPred M3):
+ uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
+Proof. by intros x n Hx. Qed.
+Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
+ `{!CMRAMonotone f} `{!CMRAMonotone g}:
+ (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. move=> H x P n Hx /=. by rewrite /uPred_holds /= H. Qed.
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)