Merge branch 'master' of git.fp.mpi-sws.org:nowbook

Makefile

+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.4pl3     ##
+#############################################################################
+
+# 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 lib/recdom/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/recdom/ RecDom 
+#
+
+.DEFAULT_GOAL := all
+
+# 
+# This Makefile may take arguments passed as environment variables:
+# COQBIN to specify the directory where Coq binaries resides;
+# 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)
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+COQLIBS?=-I . -R lib/recdom/ RecDom
+COQDOCLIBS?=-R lib/recdom/ RecDom
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+
+OPT?=
+COQDEP?=$(COQBIN)coqdep -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?=$(COQBIN)coqc
+GALLINA?=$(COQBIN)gallina
+COQDOC?=$(COQBIN)coqdoc
+COQCHK?=$(COQBIN)coqchk
+
+##################
+#                #
+# 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
+endif
+
+######################
+#                    #
+# Files dispatching. #
+#                    #
+######################
+
+VFILES:=core_lang.v\
+  iris.v\
+  lang.v\
+  masks.v\
+  world_prop.v
+
+-include $(addsuffix .d,$(VFILES))
+.SECONDARY: $(addsuffix .d,$(VFILES))
+
+VOFILES:=$(VFILES:.v=.vo)
+VOFILESINC=$(filter $(wildcard ./*),$(VOFILES)) 
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+#                                     #
+# Definition of the toplevel targets. #
+#                                     #
+#######################################
+
+all: ./lib/recdom/ $(VOFILES)
+
+spec: $(VIFILES)
+
+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 opt byte archclean clean install userinstall depend html validate ./lib/recdom/
+
+###################
+#                 #
+# Subdirectories. #
+#                 #
+###################
+
+./lib/recdom/:
+	cd ./lib/recdom/ ; $(MAKE) all
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+userinstall:
+	+$(MAKE) USERINSTALL=true install
+
+install:
+	install -d $(DSTROOT)$(COQLIBINSTALL)/RecDom; \
+	for i in $(VOFILESINC); do \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/`basename $$i`; \
+	done
+	(cd ./lib/recdom/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/recdom/ install)
+
+install-doc:
+	install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+	for i in html/*; do \
+	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$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)
+
+archclean:
+	rm -f *.cmx *.o
+	(cd ./lib/recdom/ ; $(MAKE) archclean)
+
+printenv:
+	@$(COQBIN)coqtop -config
+	@echo CAMLC =	$(CAMLC)
+	@echo CAMLOPTC =	$(CAMLOPTC)
+	@echo PP =	$(PP)
+	@echo COQFLAGS =	$(COQFLAGS)
+	@echo COQLIBINSTALL =	$(COQLIBINSTALL)
+	@echo COQDOCINSTALL =	$(COQDOCINSTALL)
+
+###################
+#                 #
+# Implicit rules. #
+#                 #
+###################
+
+%.vo %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+	$(GALLINA) $<
+
+%.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+%.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+%.g.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+	$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@
+
+%.v.d: %.v
+	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.v.beautified:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+

iris.v

@@ -1155,6 +1155,37 @@ Qed.
       - simpl comp_list; now erewrite comm, pcm_op_unit by apply _.
     Qed.
 
+    Program Definition cons_pred (φ : value -=> Prop): value -n> Props :=
+      n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
+    Next Obligation.
+      firstorder.
+    Qed.
+    Next Obligation.
+      intros x y  H_xy P n r. simpl. rewrite H_xy. tauto.
+    Qed.
+    Next Obligation.
+      intros x y H_xy P m r. simpl in H_xy. destruct n.
+      - intros LEZ. exfalso. omega.
+      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+    Qed.
+
+    Theorem soundness_obs m e (φ : value -=> Prop) n e' tp σ σ'
+            (HT  : valid (ht m (ownS σ) e (cons_pred φ)))
+            (HSN : stepn n ([e], σ) (e' :: tp, σ'))
+            (HV : is_value e') :
+        φ (exist _ e' HV).
+    Proof.
+      edestruct (soundness _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) 1 HT HSN) as [w' [r' [s' [H_wle [H_phi _] ] ] ] ].
+      - simpl. hnf. exists (pcm_unit _).
+        rewrite pcm_op_unit by intuition. reflexivity.
+      - rewrite Plus.plus_comm. simpl. split.
+        + admit. (* TODO: rewrite comm. does not work though?? *)
+        + exists (fdEmpty (V:=res)). simpl. split; [reflexivity|].
+          intros i _. split; [tauto|].
+          intros _ _ [].
+      - exact H_phi.
+    Qed.
+
   End Soundness.
 
   Section HoareTripleProperties.