Commit 1d874525 authored by Ulrich's avatar Ulrich

finished the box case

parent 23a593fd
......@@ -12,8 +12,6 @@ Require Export dnegmod.KIbox_Rules.
(*** Hilbert-style system for IPC *)
Reserved Notation "G '|--' A" (at level 79).
Require Export Coq.Lists.List.
Export ListNotations.
......@@ -108,7 +106,18 @@ intros. split.
eapply hilMP; try apply IHKIbox2.
eapply hilA3.
+ eapply hil_ded; trivial.
+ admit.
+ clear H H1. generalize dependent h.
induction F; intros.
* eapply hilNorm; trivial.
* eapply hil_ded in IHKIbox.
assert (hil Z G (|[]| a)) as H1.
apply H0; simpl; left; trivial.
assert (hil Z G (|[]| (a ->> h))) as H2.
apply IHF. intros. apply H0. simpl; right; trivial. apply IHKIbox.
pose proof (hilKax Z G a h) as K.
eapply hilMP; try apply H1.
eapply hilMP; try apply H2.
apply K.
- intro H. induction H; eauto 3 with KIboxDB.
+ eapply hilbert_axiom.
+ do 2 eapply KIbox_impI. eapply box_andI; perm_contained.
......@@ -120,7 +129,7 @@ intros. split.
+ do 2 eapply KIbox_impI.
eapply (KIbox_boxIE _ _ _ [A; A ->> B]).
* intros. inversion H; subst.
** contained (|[]| f).
** inversion H0; subst. try contained (|[]| (A ->> B)). inversion H1.
contained (|[]| f).
inversion H0; subst. try contained (|[]| (A ->> B)). inversion H1.
* eapply KIbox_impE; try contained (A ->> B); try contained A.
Admitted.
\ No newline at end of file
Qed.
......@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# WARNING
......@@ -19,11 +19,17 @@
.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.
# VERBOSE to disable the short display of compilation rules.
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
# Here is a hack to make $(eval $(shell works:
define donewline
......@@ -33,14 +39,27 @@ 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?= -R . dnegmod
COQDOCLIBS?=-R . dnegmod
COQLIBS?=\
-R "." dnegmod
COQCHKLIBS?=\
-R "." dnegmod
COQDOCLIBS?=\
-R "." dnegmod
##########################
# #
......@@ -50,14 +69,15 @@ COQDOCLIBS?=-R . dnegmod
OPT?=
COQDEP?=$(COQBIN)coqdep -c
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
COQC?=$(TIMER) "$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
##################
# #
......@@ -66,12 +86,13 @@ COQCHK?=$(COQBIN)coqchk
##################
ifdef USERINSTALL
XDG_DATA_HOME?=$(HOME)/.local/share
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
COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL="${DOCDIR}user-contrib"
COQTOPINSTALL="${COQLIB}toploop"
endif
######################
......@@ -80,22 +101,33 @@ endif
# #
######################
VFILES:=External/IPC/MyPermutations.v\
Summary.v\
DNTrans.v\
KIbox_Rules.v\
VFILES:=IntModalSetup.v\
KIbox_NaturalDeduction.v\
IntModalSetup.v
KIbox_Rules.v\
HilbertStyleEquivalence.v\
DNTrans.v\
Summary.v\
External/IPC/MyPermutations.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))
VOFILES:=$(VFILES:.v=.vo)
VO=vo
VOFILES:=$(VFILES:.v=.$(VO))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
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
......@@ -110,8 +142,12 @@ endif
all: $(VOFILES)
spec: $(VIFILES)
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)
......@@ -135,14 +171,14 @@ all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(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
.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
####################
# #
......@@ -160,37 +196,73 @@ userinstall:
+$(MAKE) USERINSTALL=true install
install:
for i in $(VOFILES); do \
install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/dnegmod/$$i`; \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/dnegmod/$$i; \
cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/dnegmod/$$i`"; \
install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/dnegmod/$$i; \
done
install-doc:
install -d $(DSTROOT)$(COQDOCINSTALL)/dnegmod/html
install -d "$(DSTROOT)"$(COQDOCINSTALL)/dnegmod/html
for i in html/*; do \
install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/dnegmod/$$i;\
install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/dnegmod/$$i;\
done
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
uninstall_me.sh: Makefile
echo '#!/bin/sh' > $@
printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/dnegmod && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "dnegmod" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/dnegmod \\\n' >> "$@"
printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find dnegmod/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
chmod +x $@
uninstall: uninstall_me.sh
sh $<
.merlin:
@echo 'FLG -rectypes' > .merlin
@echo "B $(COQLIB)kernel" >> .merlin
@echo "B $(COQLIB)lib" >> .merlin
@echo "B $(COQLIB)library" >> .merlin
@echo "B $(COQLIB)parsing" >> .merlin
@echo "B $(COQLIB)pretyping" >> .merlin
@echo "B $(COQLIB)interp" >> .merlin
@echo "B $(COQLIB)printing" >> .merlin
@echo "B $(COQLIB)intf" >> .merlin
@echo "B $(COQLIB)proofs" >> .merlin
@echo "B $(COQLIB)tactics" >> .merlin
@echo "B $(COQLIB)tools" >> .merlin
@echo "B $(COQLIB)ltacprof" >> .merlin
@echo "B $(COQLIB)toplevel" >> .merlin
@echo "B $(COQLIB)stm" >> .merlin
@echo "B $(COQLIB)grammar" >> .merlin
@echo "B $(COQLIB)config" >> .merlin
@echo "B $(COQLIB)ltac" >> .merlin
@echo "B $(COQLIB)engine" >> .merlin
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
- rm -rf html mlihtml uninstall_me.sh
archclean:
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)
@"$(COQBIN)coqtop" -config
@echo 'OCAMLFIND = $(OCAMLFIND)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
Makefile: _CoqProject
mv -f $@ $@.bak
$(COQBIN)coq_makefile -f $< -o $@
"$(COQBIN)coq_makefile" -f $< -o $@
###################
......@@ -199,32 +271,37 @@ Makefile: _CoqProject
# #
###################
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
$(VOFILES): %.vo: %.v
$(SHOW)COQC $<
$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(GLOBFILES): %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $<
%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
$(VFILES:.v=.vio): %.vio: %.v
$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
%.g: %.v
$(GFILES): %.g: %.v
$(GALLINA) $<
%.tex: %.v
$(VFILES:.v=.tex): %.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
%.html: %.v %.glob
$(HTMLFILES): %.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
%.g.tex: %.v
$(VFILES:.v=.g.tex): %.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob
$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
$(GHTMLFILES): %.g.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
%.v.d: %.v
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
$(addsuffix .d,$(VFILES)): %.v.d: %.v
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
$(addsuffix .beautified,$(VFILES)): %.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
# WARNING
#
......
......@@ -2,6 +2,7 @@
IntModalSetup.v
KIbox_NaturalDeduction.v
KIbox_Rules.v
HilbertStyleEquivalence.v
DNTrans.v
Summary.v
External/IPC/MyPermutations.v
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment