From 61f3b3f59df0daa8917f6cf86248ef39c6e9f813 Mon Sep 17 00:00:00 2001
From: Filip Sieczkowski <filips@cs.au.dk>
Date: Tue, 7 Oct 2014 11:12:19 +0200
Subject: [PATCH] More README, renamed library to ModuRes

---
 .dir-locals.el                         |  2 +-
 Makefile                               | 30 +++++++++++++-------------
 README.txt                             | 10 +++++----
 core_lang.v                            |  2 +-
 iris.v                                 |  8 ++++++-
 lang.v                                 |  2 +-
 lib/{recdom => ModuRes}/.dir-locals.el |  2 +-
 lib/{recdom => ModuRes}/BI.v           |  0
 lib/{recdom => ModuRes}/CBUltInst.v    |  0
 lib/{recdom => ModuRes}/CSetoid.v      |  0
 lib/{recdom => ModuRes}/Constr.v       |  0
 lib/{recdom => ModuRes}/Finmap.v       |  0
 lib/{recdom => ModuRes}/Makefile       | 16 +++++++-------
 lib/{recdom => ModuRes}/MetricCore.v   |  0
 lib/{recdom => ModuRes}/MetricRec.v    |  0
 lib/{recdom => ModuRes}/PCBUltInst.v   |  0
 lib/{recdom => ModuRes}/PCM.v          |  0
 lib/{recdom => ModuRes}/Predom.v       |  0
 lib/{recdom => ModuRes}/PreoMet.v      |  0
 lib/{recdom => ModuRes}/TOTInst.v      |  0
 lib/{recdom => ModuRes}/UPred.v        |  0
 world_prop.v                           |  6 +++---
 22 files changed, 43 insertions(+), 35 deletions(-)
 rename lib/{recdom => ModuRes}/.dir-locals.el (82%)
 rename lib/{recdom => ModuRes}/BI.v (100%)
 rename lib/{recdom => ModuRes}/CBUltInst.v (100%)
 rename lib/{recdom => ModuRes}/CSetoid.v (100%)
 rename lib/{recdom => ModuRes}/Constr.v (100%)
 rename lib/{recdom => ModuRes}/Finmap.v (100%)
 rename lib/{recdom => ModuRes}/Makefile (92%)
 rename lib/{recdom => ModuRes}/MetricCore.v (100%)
 rename lib/{recdom => ModuRes}/MetricRec.v (100%)
 rename lib/{recdom => ModuRes}/PCBUltInst.v (100%)
 rename lib/{recdom => ModuRes}/PCM.v (100%)
 rename lib/{recdom => ModuRes}/Predom.v (100%)
 rename lib/{recdom => ModuRes}/PreoMet.v (100%)
 rename lib/{recdom => ModuRes}/TOTInst.v (100%)
 rename lib/{recdom => ModuRes}/UPred.v (100%)

diff --git a/.dir-locals.el b/.dir-locals.el
index 79f36369..ee845344 100644
--- a/.dir-locals.el
+++ b/.dir-locals.el
@@ -3,6 +3,6 @@
 
 ((coq-mode
   (coq-load-path
-   (rec "lib/recdom/" "RecDom"))))
+   (rec "lib/ModuRes/" "ModuRes"))))
 
 
diff --git a/Makefile b/Makefile
index 28798520..85dbe463 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.4pl3     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.4pl4     ##
 #############################################################################
 
 # WARNING
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile lib/recdom/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/recdom/ RecDom 
+# coq_makefile lib/ModuRes/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/ModuRes/ ModuRes -o Makefile
 #
 
 .DEFAULT_GOAL := all
@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-COQLIBS?=-I . -R lib/recdom/ RecDom
-COQDOCLIBS?=-R lib/recdom/ RecDom
+COQLIBS?=-I . -R lib/ModuRes/ ModuRes
+COQDOCLIBS?=-R lib/ModuRes/ ModuRes
 
 ##########################
 #                        #
@@ -108,7 +108,7 @@ endif
 #                                     #
 #######################################
 
-all: ./lib/recdom/ $(VOFILES)
+all: $(VOFILES) ./lib/ModuRes/
 
 spec: $(VIFILES)
 
@@ -142,7 +142,7 @@ beautify: $(VFILES:=.beautified)
 	@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 opt byte archclean clean install userinstall depend html validate ./lib/recdom/
+.PHONY: all opt byte archclean clean install userinstall depend html validate ./lib/ModuRes/
 
 ###################
 #                 #
@@ -150,8 +150,8 @@ beautify: $(VFILES:=.beautified)
 #                 #
 ###################
 
-./lib/recdom/:
-	cd ./lib/recdom/ ; $(MAKE) all
+./lib/ModuRes/:
+	cd ./lib/ModuRes/ ; $(MAKE) all
 
 ####################
 #                  #
@@ -169,27 +169,27 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install:
-	install -d $(DSTROOT)$(COQLIBINSTALL)/RecDom; \
+	install -d $(DSTROOT)$(COQLIBINSTALL)/ModuRes; \
 	for i in $(VOFILESINC); do \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/`basename $$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/`basename $$i`; \
 	done
-	(cd ./lib/recdom/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/recdom/ install)
+	(cd ./lib/ModuRes/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/ModuRes/ install)
 
 install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+	install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
 	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
 	done
 
 clean:
 	rm -f $(VOFILES) $(VIFILES) $(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
-	(cd ./lib/recdom/ ; $(MAKE) clean)
+	(cd ./lib/ModuRes/ ; $(MAKE) clean)
 
 archclean:
 	rm -f *.cmx *.o
-	(cd ./lib/recdom/ ; $(MAKE) archclean)
+	(cd ./lib/ModuRes/ ; $(MAKE) archclean)
 
 printenv:
 	@$(COQBIN)coqtop -config
diff --git a/README.txt b/README.txt
index eb476e8c..a2154985 100644
--- a/README.txt
+++ b/README.txt
@@ -53,14 +53,16 @@ CONTENTS
   
   * masks.v introduces some lemmas about masks
   
-  * world_prop.v uses the aforementioned Coq library to construct the
-    domain for Iris propositions
+  * world_prop.v uses the ModuRes Coq library to construct the domain
+    for Iris propositions
   
   * iris.v is the main file and contains the actual logic and the
     proof of the rules for view shifts and Hoare triples
 
-  It uses a Coq library in lib/ by Sieczkowski et al. to solve the
-  recursive domain equation (see the paper for a reference).
+  The development uses ModuRes, a Coq library in by Sieczkowski et
+  al. to solve the recursive domain equation (see the paper for a
+  reference) and prove some of the standard separation logic rules. It
+  is located in the lib/ subdirectory.
 
 
 REQUIREMENTS
diff --git a/core_lang.v b/core_lang.v
index d1d427d9..62b061a0 100644
--- a/core_lang.v
+++ b/core_lang.v
@@ -1,4 +1,4 @@
-Require Import RecDom.PCM.
+Require Import ModuRes.PCM.
 
 Module Type CORE_LANG.
   Delimit Scope lang_scope with lang.
diff --git a/iris.v b/iris.v
index 95f3c00c..a433c8d3 100644
--- a/iris.v
+++ b/iris.v
@@ -1,5 +1,5 @@
 Require Import world_prop core_lang lang masks.
-Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Module Iris (RL : PCM_T) (C : CORE_LANG).
 
@@ -215,6 +215,12 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
     intros w n r; simpl; unfold const; reflexivity.
   Qed.
 
+  Lemma box_disj p q :
+    □ (p ∨ q) == □ p ∨ □ q.
+  Proof.
+    intros w n r; reflexivity.
+  Qed.
+
   (** Ghost state ownership **)
   Lemma ownL_sc (u t : option RL.res) :
     ownL (u · t)%pcm == ownL u * ownL t.
diff --git a/lang.v b/lang.v
index 5f09ade3..5a33d268 100644
--- a/lang.v
+++ b/lang.v
@@ -1,5 +1,5 @@
 Require Import List.
-Require Import RecDom.PCM.
+Require Import ModuRes.PCM.
 Require Import core_lang.
 
 (******************************************************************)
diff --git a/lib/recdom/.dir-locals.el b/lib/ModuRes/.dir-locals.el
similarity index 82%
rename from lib/recdom/.dir-locals.el
rename to lib/ModuRes/.dir-locals.el
index 82ea871d..44673b5a 100644
--- a/lib/recdom/.dir-locals.el
+++ b/lib/ModuRes/.dir-locals.el
@@ -3,6 +3,6 @@
 
 ((coq-mode
   (coq-load-path
-   (rec "./" "RecDom"))))
+   (rec "./" "ModuRes"))))
 
 
diff --git a/lib/recdom/BI.v b/lib/ModuRes/BI.v
similarity index 100%
rename from lib/recdom/BI.v
rename to lib/ModuRes/BI.v
diff --git a/lib/recdom/CBUltInst.v b/lib/ModuRes/CBUltInst.v
similarity index 100%
rename from lib/recdom/CBUltInst.v
rename to lib/ModuRes/CBUltInst.v
diff --git a/lib/recdom/CSetoid.v b/lib/ModuRes/CSetoid.v
similarity index 100%
rename from lib/recdom/CSetoid.v
rename to lib/ModuRes/CSetoid.v
diff --git a/lib/recdom/Constr.v b/lib/ModuRes/Constr.v
similarity index 100%
rename from lib/recdom/Constr.v
rename to lib/ModuRes/Constr.v
diff --git a/lib/recdom/Finmap.v b/lib/ModuRes/Finmap.v
similarity index 100%
rename from lib/recdom/Finmap.v
rename to lib/ModuRes/Finmap.v
diff --git a/lib/recdom/Makefile b/lib/ModuRes/Makefile
similarity index 92%
rename from lib/recdom/Makefile
rename to lib/ModuRes/Makefile
index dc09c4a1..0affb728 100644
--- a/lib/recdom/Makefile
+++ b/lib/ModuRes/Makefile
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.4pl3     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.4pl4     ##
 #############################################################################
 
 # WARNING
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -R . RecDom BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile 
+# coq_makefile -R . ModuRes BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-COQLIBS?= -R . RecDom
-COQDOCLIBS?=-R . RecDom
+COQLIBS?= -R . ModuRes
+COQDOCLIBS?=-R . ModuRes
 
 ##########################
 #                        #
@@ -168,14 +168,14 @@ userinstall:
 
 install:
 	for i in $(VOFILES); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i; \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i; \
 	done
 
 install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+	install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
 	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
 	done
 
 clean:
diff --git a/lib/recdom/MetricCore.v b/lib/ModuRes/MetricCore.v
similarity index 100%
rename from lib/recdom/MetricCore.v
rename to lib/ModuRes/MetricCore.v
diff --git a/lib/recdom/MetricRec.v b/lib/ModuRes/MetricRec.v
similarity index 100%
rename from lib/recdom/MetricRec.v
rename to lib/ModuRes/MetricRec.v
diff --git a/lib/recdom/PCBUltInst.v b/lib/ModuRes/PCBUltInst.v
similarity index 100%
rename from lib/recdom/PCBUltInst.v
rename to lib/ModuRes/PCBUltInst.v
diff --git a/lib/recdom/PCM.v b/lib/ModuRes/PCM.v
similarity index 100%
rename from lib/recdom/PCM.v
rename to lib/ModuRes/PCM.v
diff --git a/lib/recdom/Predom.v b/lib/ModuRes/Predom.v
similarity index 100%
rename from lib/recdom/Predom.v
rename to lib/ModuRes/Predom.v
diff --git a/lib/recdom/PreoMet.v b/lib/ModuRes/PreoMet.v
similarity index 100%
rename from lib/recdom/PreoMet.v
rename to lib/ModuRes/PreoMet.v
diff --git a/lib/recdom/TOTInst.v b/lib/ModuRes/TOTInst.v
similarity index 100%
rename from lib/recdom/TOTInst.v
rename to lib/ModuRes/TOTInst.v
diff --git a/lib/recdom/UPred.v b/lib/ModuRes/UPred.v
similarity index 100%
rename from lib/recdom/UPred.v
rename to lib/ModuRes/UPred.v
diff --git a/world_prop.v b/world_prop.v
index 9e785644..103ead16 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -1,8 +1,8 @@
 (** In this file, we show how we can use the solution of the recursive
     domain equations to build a higher-order separation logic *)
-Require Import RecDom.PreoMet RecDom.MetricRec RecDom.CBUltInst.
-Require Import RecDom.Finmap RecDom.Constr.
-Require Import RecDom.PCM RecDom.UPred RecDom.BI.
+Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
+Require Import ModuRes.Finmap ModuRes.Constr.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
 
 Module WorldProp (Res : PCM_T).
 
-- 
GitLab