diff --git a/.gitignore b/.gitignore
index bdb3108122dfc5be1fb0370483837d395c0524bd..d192c02799c5c98832458e9f76acc7ae1890be31 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@
*.glob
*.vo
*.html
+*.aux
diff --git a/Makefile b/Makefile
index eee18ff8e634826c5cc1dfaebbaeecfb1fe1d609..f00672eacc07f5cff53eeff0d55ff11bce98b08f 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.4pl4 ##
+## // # Makefile automagically generated by coq_makefile V8.5pl1 ##
#############################################################################
# WARNING
@@ -14,14 +14,15 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -R . rt ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/exists.v ./util/induction.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
+# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/exists.v ./util/induction.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -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.
@@ -33,14 +34,25 @@ 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 . rt
-COQDOCLIBS?=-R . rt
+COQLIBS?=\
+ -R "." rt
+COQDOCLIBS?=\
+ -R "." rt
##########################
# #
@@ -50,14 +62,15 @@ COQDOCLIBS?=-R . rt
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 +79,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
######################
@@ -159,15 +173,25 @@ VFILES:=util/fixedpoint.v\
model/jitter/response_time.v\
model/jitter/platform_fp.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
@@ -182,8 +206,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)
@@ -214,7 +242,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
+.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
####################
# #
@@ -232,33 +260,72 @@ userinstall:
+$(MAKE) USERINSTALL=true install
install:
- for i in $(VOFILES); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/rt/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/rt/$$i; \
+ cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
+ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/rt/$$i`"; \
+ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/rt/$$i; \
done
install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/rt/html
+ install -d "$(DSTROOT)"$(COQDOCINSTALL)/rt/html
for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/rt/$$i;\
+ install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/rt/$$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)/rt && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "rt" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+ printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/rt \\\n' >> "$@"
+ printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
+ printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find rt/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) toplevel" >> .merlin
+ @echo "B $(COQLIB) stm" >> .merlin
+ @echo "B $(COQLIB) grammar" >> .merlin
+ @echo "B $(COQLIB) config" >> .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
+
+cleanall:: clean
+ rm -f $(patsubst %.v,.%.aux,$(VFILES))
-archclean:
+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 '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 $@
+
###################
# #
@@ -266,31 +333,34 @@ printenv:
# #
###################
-%.vo %.glob: %.v
+$(VOFILES): %.vo: %.v
+ $(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
+ $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-%.v.beautified:
+$(addsuffix .beautified,$(VFILES)): %.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
# WARNING
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..dcdf97e03d88df736a8e2720bf6fb99636751905
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1 @@
+-R . rt
\ No newline at end of file
diff --git a/analysis/basic/bertogna_edf_comp.v b/analysis/basic/bertogna_edf_comp.v
index 8edd7cf42499b20bbb4a794ed81c076d4fb6ddc4..d9493644e86d3a567ec61e0984c3510492750c81 100755
--- a/analysis/basic/bertogna_edf_comp.v
+++ b/analysis/basic/bertogna_edf_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_edf_theory.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
@@ -238,7 +237,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
- by apply/(zipP (fun x y => snd x <= snd y)).
+ by apply/(zipP t (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
@@ -247,8 +246,8 @@ Module ResponseTimeIterationEDF.
unfold transitive, all_le.
move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
apply/andP; split; first by rewrite ZIPxy -ZIPyz.
- move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
- move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
+ move: LExy => /(zipP _ (fun x y => snd x <= snd y)) LExy.
+ move: LEyz => /(zipP _ (fun x y => snd x <= snd y)) LEyz.
assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
by rewrite ZIPxy.
assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
@@ -259,21 +258,22 @@ Module ResponseTimeIterationEDF.
apply size0nil in SIZExy; symmetry in SIZEyz.
by apply size0nil in SIZEyz; subst.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (t, 0) | by rewrite SIZExy -SIZEyz|].
+ rewrite -SIZExy in SIZEyz.
+ have ZIP := zipP t (fun x y => snd x <= snd y) _ _ SIZEyz.
+ apply/ZIP.
intros i LTi.
+ specialize (LExy t); specialize (LEyz t).
exploit LExy; first by rewrite SIZExy.
{
- rewrite size_zip -SIZEyz -SIZExy minnn in LTi.
- by rewrite size_zip -SIZExy minnn; apply LTi.
+ rewrite size_zip -SIZExy minnn.
+ rewrite size_zip -SIZEyz minnn in LTi; apply LTi.
}
- instantiate (1 := t); intro LE.
- exploit LEyz; first by apply SIZEyz.
+ intro LE.
+ exploit LEyz; first by rewrite -SIZExy.
{
- rewrite size_zip SIZExy SIZEyz minnn in LTi.
- by rewrite size_zip SIZEyz minnn; apply LTi.
+ by rewrite size_zip -SIZExy -size_zip; apply LTi.
}
- by instantiate (1 := t); intro LE'; apply (leq_trans LE).
+ by intro LE'; apply (leq_trans LE).
Qed.
(* At any step of the iteration, the corresponding list
@@ -294,8 +294,8 @@ Module ResponseTimeIterationEDF.
by rewrite iterSr IHstep.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].
+ apply/(zipP (tsk0,0) (fun x y => snd x <= snd y));
+ first by rewrite edf_claimed_bounds_size size_map.
intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
@@ -349,10 +349,9 @@ Module ResponseTimeIterationEDF.
apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
rename UNZIP' into SIZE.
rewrite size_map [size (unzip1 _)]size_map in SIZE.
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (p0,0) | by done |].
+ apply/(zipP p0 (fun x y => snd x <= snd y)); first by done.
intros i LTi.
exploit LE; first by rewrite 2!size_map in SIZE.
@@ -420,7 +419,7 @@ Module ResponseTimeIterationEDF.
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
@@ -614,6 +613,8 @@ Module ResponseTimeIterationEDF.
k <= max_steps ts ->
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
Proof.
+ have INC := bertogna_edf_comp_f_increases.
+ have MONO := bertogna_edf_comp_iteration_monotonic.
rename H_at_least_one_task into NONEMPTY.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_valid_task_parameters into VALID.
@@ -661,12 +662,12 @@ Module ResponseTimeIterationEDF.
}
rewrite -2!big_seq_cond.
- have LT := bertogna_edf_comp_f_increases step (ltnW LE).
- have MONO := bertogna_edf_comp_iteration_monotonic step.
+ have LT := INC step (ltnW LE).
+ specialize (MONO step).
move: LT => /andP [_ LT]; move: LT => /hasP LT.
destruct LT as [[x1 x2] INzip LT]; simpl in *.
- move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
+ move: MONO => /andP [_ /(zipP _ (fun x y => snd x <= snd y)) MONO].
rewrite 2!(big_nth (elem, 0)).
apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
last by rewrite size_map.
@@ -940,6 +941,9 @@ Module ResponseTimeIterationEDF.
Theorem taskset_schedulable_by_edf_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (edf_analysis_yields_response_time_bounds).
+ have DL := (edf_claimed_bounds_le_deadline ts).
+ have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
edf_schedulable,
@@ -953,10 +957,6 @@ Module ResponseTimeIterationEDF.
H_test_succeeds into TEST.
move => tsk INtsk j JOBtsk.
- have RLIST := (edf_analysis_yields_response_time_bounds).
- have DL := (edf_claimed_bounds_le_deadline ts).
- have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
-
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j JOBtsk.
diff --git a/analysis/basic/bertogna_edf_theory.v b/analysis/basic/bertogna_edf_theory.v
index beb2917777f805ad5787205ec92ea31cfaea6d32..b76bc4784d570fc6e6c1487efbe411aa755fd732 100644
--- a/analysis/basic/bertogna_edf_theory.v
+++ b/analysis/basic/bertogna_edf_theory.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.platform rt.model.basic.response_time.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF.
@@ -284,8 +283,8 @@ Module ResponseTimeAnalysisEDF.
| by apply JOBtsk | by apply BACK | ].
{
intros j0 tsk0 TSK0 LE.
- cut (tsk0 \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP -TSK0 FROMTS].
- move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ cut (tsk0 \in unzip1 rt_bounds = true); last by rewrite UNZIP -TSK0 FROMTS.
+ move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done).
{
rewrite leq_add2l TSK0.
@@ -362,6 +361,7 @@ Module ResponseTimeAnalysisEDF.
Lemma bertogna_edf_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
+ have DIFFTASK := bertogna_edf_interference_by_different_tasks.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
@@ -397,7 +397,7 @@ Module ResponseTimeAnalysisEDF.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold jldp_can_interfere_with.
- apply bertogna_edf_interference_by_different_tasks with (t := t); [by auto | by done |].
+ apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
@@ -416,8 +416,8 @@ Module ResponseTimeAnalysisEDF.
H_all_jobs_from_taskset into FROMTS,
H_all_previous_jobs_completed_on_time into BEFOREok.
intros t j0 LEt LE.
- cut ((job_task j0) \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP FROMTS].
- move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
+ move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done.
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
@@ -442,6 +442,8 @@ Module ResponseTimeAnalysisEDF.
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
+ have COMP := bertogna_edf_all_previous_jobs_complete_by_their_period.
+ have INV := bertogna_edf_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk,
@@ -515,7 +517,7 @@ Module ResponseTimeAnalysisEDF.
(job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t);
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
intros j0 tsk0 TSK0 LE.
- by apply (bertogna_edf_all_previous_jobs_complete_by_their_period t); rewrite ?TSK0.
+ by apply (COMP t); rewrite ?TSK0.
}
by subst j2; apply SEQ with (j := j1) (t := t).
}
@@ -549,9 +551,8 @@ Module ResponseTimeAnalysisEDF.
eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
rewrite leq_subLR count_predC size_filter.
- apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
- first by rewrite bertogna_edf_scheduling_invariant.
- by rewrite count_filter.
+ by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ [by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
@@ -624,9 +625,12 @@ Module ResponseTimeAnalysisEDF.
\sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
Proof.
+ have GE_COST := bertogna_edf_R_other_ge_cost.
+ have EXCEEDS := bertogna_edf_minimum_exceeds_interference.
+ have ALLBUSY := bertogna_edf_all_cpus_busy.
+ have TOOMUCH := bertogna_edf_too_much_interference.
rename H_rt_bounds_contains_all_tasks into UNZIP,
H_response_time_is_fixed_point into REC.
- have GE_COST := bertogna_edf_R_other_ge_cost.
apply leq_trans with (n := \sum_(tsk_other <- ts_interf) minn (x tsk_other) (R - task_cost tsk + 1));
last first.
{
@@ -654,11 +658,10 @@ Module ResponseTimeAnalysisEDF.
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
- apply bertogna_edf_minimum_exceeds_interference.
+ apply EXCEEDS.
apply leq_trans with (n := X * num_cpus);
- last by rewrite bertogna_edf_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_edf_too_much_interference.
+ last by rewrite ALLBUSY.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
@@ -669,6 +672,9 @@ Module ResponseTimeAnalysisEDF.
(tsk_other, R_other) \in rt_bounds /\
(minn (x tsk_other) (R - task_cost tsk + 1) > interference_bound tsk_other R_other).
Proof.
+ have SUM := bertogna_edf_sum_exceeds_total_interference.
+ have BOUND := bertogna_edf_workload_bounds_interference.
+ have EDFBOUND := bertogna_edf_specific_bound_holds.
rename H_rt_bounds_contains_all_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_other, R_other) := tup in
@@ -679,7 +685,6 @@ Module ResponseTimeAnalysisEDF.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_edf_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold I, total_interference_bound_edf.
@@ -692,11 +697,11 @@ Module ResponseTimeAnalysisEDF.
unfold interference_bound; rewrite leq_min; apply/andP; split;
last by rewrite geq_minr.
apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
- by apply bertogna_edf_workload_bounds_interference.
+ by apply BOUND.
}
{
apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
- by apply bertogna_edf_specific_bound_holds.
+ by apply EDFBOUND.
}
}
move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MIN].
diff --git a/analysis/basic/bertogna_fp_comp.v b/analysis/basic/bertogna_fp_comp.v
index 8a1019fcfec7202c16b6d1bbe2be73e034d065d5..dfa823f813dfcdf1e1ed3fd1a5abd4ba5a3c62e6 100644
--- a/analysis/basic/bertogna_fp_comp.v
+++ b/analysis/basic/bertogna_fp_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_fp_theory.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
@@ -444,6 +443,7 @@ Module ResponseTimeIterationFP.
k <= max_steps tsk ->
f k > k + task_cost tsk - 1.
Proof.
+ have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
@@ -457,15 +457,12 @@ Module ResponseTimeIterationFP.
{
intros LT.
specialize (IHk (ltnW LT)).
- apply leq_ltn_trans with (n := f k);
- last by apply bertogna_fp_comp_f_increases, ltnW.
+ apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk; last first.
- {
- apply leq_trans with (n := task_cost tsk); last by apply leq_addl.
- by apply PARAMS.
- }
+ rewrite subh1 in IHk;
+ last by apply leq_trans with (n := task_cost tsk);
+ [by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
@@ -476,6 +473,8 @@ Module ResponseTimeIterationFP.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
+ have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
+ have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
@@ -493,18 +492,19 @@ Module ResponseTimeIterationFP.
move: EX => /forall_inP EX.
rewrite leqNgt in LE; move: LE => /negP LE.
exfalso; apply LE.
- have TOOMUCH := bertogna_fp_comp_rt_grows_too_much _ (max_steps tsk).
- exploit TOOMUCH; [| by apply leqnn |].
+
+ assert (DIFF: forall k : nat, k <= max_steps tsk -> f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
- by exploit (EX (Ordinal LEk)); [by done | intro DIFF].
- }
- unfold max_steps at 1.
+ by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
+ }
+ exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite subh1; last by apply PARAMS2.
- by rewrite -addnBA // subnn addn0.
+ rewrite -addnBA // subnn addn0 subn1 prednK //.
+ intros LT; apply (leq_ltn_trans LT).
+ by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
@@ -657,7 +657,7 @@ Module ResponseTimeIterationFP.
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done).
{
- cut (NTH idx \in hp_bounds); [intros IN | by apply mem_nth].
+ cut (NTH idx \in hp_bounds = true); [intros IN | by apply mem_nth].
by rewrite -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
}
{
@@ -688,15 +688,15 @@ Module ResponseTimeIterationFP.
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (fp_analysis_yields_response_time_bounds).
+ have UNZIP := (fp_claimed_bounds_unzip ts).
+ have DL := (fp_claimed_bounds_le_deadline ts).
+
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
move => tsk INtsk j JOBtsk.
- have RLIST := (fp_analysis_yields_response_time_bounds).
- have UNZIP := (fp_claimed_bounds_unzip ts).
- have DL := (fp_claimed_bounds_le_deadline ts).
-
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: exists R, (tsk, R) \in rt_bounds).
diff --git a/analysis/basic/bertogna_fp_theory.v b/analysis/basic/bertogna_fp_theory.v
index 5fce53b10dadb037e09211adee31817d20ce53c7..250e35f2efb9053d3e0b9d49a694c2b3156c1f4f 100644
--- a/analysis/basic/bertogna_fp_theory.v
+++ b/analysis/basic/bertogna_fp_theory.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.response_time rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
@@ -159,7 +158,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [_ IN].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -171,7 +170,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [INTERF _].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -289,7 +288,7 @@ Module ResponseTimeAnalysisFP.
{
intros j_other tsk_other JOBother INTERF.
move: UNZIP => UNZIP.
- cut (tsk_other \in unzip1 hp_bounds); last first.
+ cut (tsk_other \in unzip1 hp_bounds = true); last first.
{
rewrite -UNZIP mem_filter; apply/andP; split; first by done.
by rewrite -JOBother; apply FROMTS.
@@ -301,7 +300,8 @@ Module ResponseTimeAnalysisFP.
rewrite leq_add2l.
apply leq_trans with (n := task_deadline tsk_other); first by apply NOMISS.
apply RESTR.
- cut (tsk_other \in unzip1 hp_bounds); last by apply/mapP; exists (tsk_other, R').
+ cut (tsk_other \in unzip1 hp_bounds = true);
+ last by apply/mapP; exists (tsk_other, R').
by rewrite -UNZIP mem_filter; move => /andP [_ IN'].
}
}
@@ -372,6 +372,7 @@ Module ResponseTimeAnalysisFP.
Lemma bertogna_fp_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
+ have DIFFTASK := bertogna_fp_interference_by_different_tasks.
rename H_work_conserving into WORK, H_enforces_FP_policy into FP,
H_all_jobs_from_taskset into FROMTS, H_job_of_tsk into JOBtsk.
unfold sporadic_task_model in *.
@@ -399,7 +400,7 @@ Module ResponseTimeAnalysisFP.
rewrite -JOBtsk; apply FP with (t := t); try by done.
by apply/existsP; exists cpu; apply/eqP.
}
- apply bertogna_fp_interference_by_different_tasks with (t := t); [by auto | by done |].
+ apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
@@ -414,7 +415,8 @@ Module ResponseTimeAnalysisFP.
forall delta,
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
- Proof.
+ Proof.
+ have INV := bertogna_fp_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk,
@@ -563,9 +565,8 @@ Module ResponseTimeAnalysisFP.
eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
rewrite leq_subLR count_predC size_filter.
- apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
- first by rewrite bertogna_fp_scheduling_invariant.
- by rewrite count_filter.
+ by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ [by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
@@ -640,6 +641,9 @@ Module ResponseTimeAnalysisFP.
total_interference_bound_fp task_cost task_period tsk hp_bounds
R higher_eq_priority.
Proof.
+ have EXCEEDS := bertogna_fp_minimum_exceeds_interference.
+ have ALLBUSY := bertogna_fp_all_cpus_busy.
+ have TOOMUCH := bertogna_fp_too_much_interference.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_recurrence_holds into REC.
apply leq_trans with (n := \sum_(tsk_k <- ts_interf) minn (x tsk_k) (R - task_cost tsk + 1));
@@ -657,11 +661,9 @@ Module ResponseTimeAnalysisFP.
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
- apply bertogna_fp_minimum_exceeds_interference.
- apply leq_trans with (n := X * num_cpus);
- last by rewrite bertogna_fp_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_fp_too_much_interference.
+ apply EXCEEDS.
+ apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 6) After concluding that the sum of the minimum exceeds (R - e_i + 1),
@@ -673,6 +675,8 @@ Module ResponseTimeAnalysisFP.
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
Proof.
+ have SUM := bertogna_fp_sum_exceeds_total_interference.
+ have INTERFk := bertogna_fp_tsk_other_interferes.
rename H_hp_bounds_has_interfering_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_k, R_k) := tup in
@@ -682,7 +686,6 @@ Module ResponseTimeAnalysisFP.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_fp_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold total_interference_bound_fp.
@@ -691,7 +694,7 @@ Module ResponseTimeAnalysisFP.
apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
specialize (ALL (tsk_k, R_k) HPk).
rewrite -leqNgt in ALL.
- have INTERFk := bertogna_fp_tsk_other_interferes tsk_k R_k HPk.
+ specialize (INTERFk tsk_k R_k HPk).
fold (can_interfere_with_tsk); rewrite INTERFk.
by apply ALL.
}
@@ -707,6 +710,8 @@ Module ResponseTimeAnalysisFP.
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk R.
Proof.
+ have WORKLOAD := bertogna_fp_workload_bounds_interference.
+ have EX := bertogna_fp_exists_task_that_exceeds_bound.
rename H_response_time_bounds_ge_cost into GE_COST,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_recurrence_holds into REC,
@@ -743,10 +748,10 @@ Module ResponseTimeAnalysisFP.
apply negbT in NOTCOMP; exfalso.
(* We derive a contradiction using the previous lemmas. *)
- have EX := bertogna_fp_exists_task_that_exceeds_bound j JOBtsk NOTCOMP BEFOREok.
+ specialize (EX j JOBtsk NOTCOMP BEFOREok).
destruct EX as [tsk_k [R_k [HPk LTmin]]].
unfold minn at 1 in LTmin.
- have WORKLOAD := bertogna_fp_workload_bounds_interference j tsk_k R_k HPk.
+ specialize (WORKLOAD j tsk_k R_k HPk).
destruct (W task_cost task_period tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
move: LTmin => /andP [BUG _]; des.
diff --git a/analysis/basic/interference_bound.v b/analysis/basic/interference_bound.v
index d38bb4d3276908c190d2dbd0cbbf73430fcd3302..63229dee756439782224ada2545ffea7a6c154cc 100644
--- a/analysis/basic/interference_bound.v
+++ b/analysis/basic/interference_bound.v
@@ -1,8 +1,7 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.basic.workload_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
diff --git a/analysis/basic/interference_bound_edf.v b/analysis/basic/interference_bound_edf.v
index 23c108885d0141598dca1121e291e5681a46cbc3..bf569094fe92c4d5e7aa0739082d1c804cf431df 100644
--- a/analysis/basic/interference_bound_edf.v
+++ b/analysis/basic/interference_bound_edf.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
rt.model.basic.interference rt.model.basic.interference_edf.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDF.
@@ -634,6 +633,8 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 <= interference_bound.
Proof.
+ have ONE := interference_bound_edf_simpl_when_there's_one_job.
+ have SLACK := interference_bound_edf_interference_of_j_fst_limited_by_slack.
rename H_many_jobs into NUM, H_only_one_job into SIZE.
unfold interference_caused_by, interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
@@ -645,8 +646,7 @@ Module InterferenceBoundEDF.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite SIZE.
}
- rewrite interference_bound_edf_simpl_when_there's_one_job.
- by apply interference_bound_edf_interference_of_j_fst_limited_by_slack.
+ by rewrite ONE; apply SLACK.
Qed.
End InterferenceSingleJob.
@@ -806,7 +806,7 @@ Module InterferenceBoundEDF.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite INnth INnth0.
}
- by rewrite subh3 // addnC -INnth.
+ by rewrite subh3 // addnC /p_k -INnth.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
@@ -814,14 +814,14 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k >= num_mid_jobs.+1.
Proof.
- rename H_valid_task_parameters into TASK_PARAMS,
- H_tsk_k_in_task_set into INk.
- unfold valid_sporadic_taskset, is_valid_sporadic_task,
- interference_bound, edf_specific_interference_bound in *.
have DIST := interference_bound_edf_many_periods_in_between.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
interference_bound_edf_j_fst_completed_on_time.
+ rename H_valid_task_parameters into TASK_PARAMS,
+ H_tsk_k_in_task_set into INk.
+ unfold valid_sporadic_taskset, is_valid_sporadic_task,
+ interference_bound, edf_specific_interference_bound in *.
rewrite leqNgt; apply/negP; unfold not; intro LTnk; unfold n_k in LTnk.
rewrite ltn_divLR in LTnk; last by specialize (TASK_PARAMS tsk_k INk); des.
apply (leq_trans LTnk) in DIST; rewrite ltn_subRL in DIST.
@@ -876,8 +876,8 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Proof.
- rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
+ rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
[by rewrite SIZE ltnS leqNgt NK in NUM | by done].
Qed.
diff --git a/analysis/basic/interference_bound_fp.v b/analysis/basic/interference_bound_fp.v
index 6facd93a09b6a9e7accb6044315e26295c3204a2..35052c7e523e468f7b721b04179d16da3c2f60c1 100644
--- a/analysis/basic/interference_bound_fp.v
+++ b/analysis/basic/interference_bound_fp.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
diff --git a/analysis/basic/workload_bound.v b/analysis/basic/workload_bound.v
index 4658f11cb61633716a0034b4281c3e27de01d99a..70b0436acfbbfd5e0a2cce2a5215bce47f6648f4 100644
--- a/analysis/basic/workload_bound.v
+++ b/analysis/basic/workload_bound.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.schedulability.
-Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
diff --git a/analysis/jitter/bertogna_edf_comp.v b/analysis/jitter/bertogna_edf_comp.v
index dfba24def0b4b548f819eb2bbc569d1cdf56ea76..cf5a0572b4a53b25ad4b394a815fd3daa3a9815b 100755
--- a/analysis/jitter/bertogna_edf_comp.v
+++ b/analysis/jitter/bertogna_edf_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.analysis.jitter.bertogna_edf_theory.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
@@ -292,7 +291,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
- by apply/(zipP (fun x y => snd x <= snd y)).
+ by apply/(zipP t (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
@@ -301,8 +300,8 @@ Module ResponseTimeIterationEDF.
unfold transitive, all_le.
move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
apply/andP; split; first by rewrite ZIPxy -ZIPyz.
- move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
- move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
+ move: LExy => /(zipP _ (fun x y => snd x <= snd y)) LExy.
+ move: LEyz => /(zipP _ (fun x y => snd x <= snd y)) LEyz.
assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
by rewrite ZIPxy.
assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
@@ -313,21 +312,22 @@ Module ResponseTimeIterationEDF.
apply size0nil in SIZExy; symmetry in SIZEyz.
by apply size0nil in SIZEyz; subst.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (t, 0) | by rewrite SIZExy -SIZEyz|].
+ specialize (LExy t); specialize (LEyz t).
+ apply/(zipP t (fun x y => snd x <= snd y));
+ first by rewrite SIZExy -SIZEyz.
intros i LTi.
exploit LExy; first by rewrite SIZExy.
{
rewrite size_zip -SIZEyz -SIZExy minnn in LTi.
by rewrite size_zip -SIZExy minnn; apply LTi.
}
- instantiate (1 := t); intro LE.
+ intro LE.
exploit LEyz; first by apply SIZEyz.
{
rewrite size_zip SIZExy SIZEyz minnn in LTi.
by rewrite size_zip SIZEyz minnn; apply LTi.
}
- by instantiate (1 := t); intro LE'; apply (leq_trans LE).
+ by intro LE'; apply (leq_trans LE).
Qed.
(* At any step of the iteration, the corresponding list
@@ -348,8 +348,8 @@ Module ResponseTimeIterationEDF.
by rewrite iterSr IHstep.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].
+ apply/(zipP (tsk0,0) (fun x y => snd x <= snd y));
+ first by rewrite edf_claimed_bounds_size size_map.
intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
@@ -403,10 +403,9 @@ Module ResponseTimeIterationEDF.
apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
rename UNZIP' into SIZE.
rewrite size_map [size (unzip1 _)]size_map in SIZE.
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (p0,0) | by done |].
+ apply/(zipP p0 (fun x y => snd x <= snd y)); first by done.
intros i LTi.
exploit LE; first by rewrite 2!size_map in SIZE.
@@ -474,7 +473,7 @@ Module ResponseTimeIterationEDF.
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
@@ -669,6 +668,8 @@ Module ResponseTimeIterationEDF.
k <= max_steps ts ->
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
Proof.
+ have LT := bertogna_edf_comp_f_increases.
+ have MONO := bertogna_edf_comp_iteration_monotonic.
rename H_at_least_one_task into NONEMPTY.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_valid_task_parameters into VALID.
@@ -716,12 +717,12 @@ Module ResponseTimeIterationEDF.
}
rewrite -2!big_seq_cond.
- have LT := bertogna_edf_comp_f_increases step (ltnW LE).
- have MONO := bertogna_edf_comp_iteration_monotonic step.
+ specialize (LT step (ltnW LE)).
+ specialize (MONO step).
move: LT => /andP [_ LT]; move: LT => /hasP LT.
destruct LT as [[x1 x2] INzip LT]; simpl in *.
- move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
+ move: MONO => /andP [_ /(zipP _ (fun x y => snd x <= snd y)) MONO].
rewrite 2!(big_nth (elem, 0)).
apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
last by rewrite size_map.
@@ -1034,6 +1035,9 @@ Module ResponseTimeIterationEDF.
Theorem taskset_schedulable_by_edf_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (edf_analysis_yields_response_time_bounds).
+ have DL := (edf_claimed_bounds_le_deadline ts).
+ have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
edf_schedulable,
@@ -1045,12 +1049,7 @@ Module ResponseTimeIterationEDF.
H_jobs_execute_after_jitter into AFTER,
H_all_jobs_from_taskset into ALLJOBS,
H_test_succeeds into TEST.
-
move => tsk INtsk j JOBtsk.
- have RLIST := (edf_analysis_yields_response_time_bounds).
- have DL := (edf_claimed_bounds_le_deadline ts).
- have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
-
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j JOBtsk.
diff --git a/analysis/jitter/bertogna_edf_theory.v b/analysis/jitter/bertogna_edf_theory.v
index ceaa3f3b4be86ba63492dd9b5c7f2dd8d9eec301..3ea4ad152dadba7bda035b648a224d03303bdadd 100644
--- a/analysis/jitter/bertogna_edf_theory.v
+++ b/analysis/jitter/bertogna_edf_theory.v
@@ -1,4 +1,3 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference
@@ -6,7 +5,7 @@ Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arr
rt.model.jitter.priority rt.model.jitter.platform rt.model.jitter.response_time.
Require Import rt.analysis.jitter.workload_bound
rt.analysis.jitter.interference_bound_edf.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDFJitter.
@@ -300,8 +299,8 @@ Module ResponseTimeAnalysisEDFJitter.
| by apply JOBtsk | by apply BACK | ].
{
intros j0 tsk0 TSK0 LE.
- cut (tsk0 \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP -TSK0 FROMTS].
- move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ cut (tsk0 \in unzip1 rt_bounds = true); last by rewrite UNZIP -TSK0 FROMTS.
+ move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk0 + R0); try (by done).
{
rewrite -addnA leq_add2l TSK0.
@@ -404,6 +403,7 @@ Module ResponseTimeAnalysisEDFJitter.
Lemma bertogna_edf_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
+ have DIFFTASK := bertogna_edf_interference_by_different_tasks.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
@@ -434,7 +434,7 @@ Module ResponseTimeAnalysisEDFJitter.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold jldp_can_interfere_with.
- apply bertogna_edf_interference_by_different_tasks with (t := t); [by auto | by done |].
+ apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
@@ -456,8 +456,8 @@ Module ResponseTimeAnalysisEDFJitter.
H_all_previous_jobs_completed_on_time into BEFOREok.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
intros t j0 LEt LE.
- cut ((job_task j0) \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP FROMTS].
- move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
+ move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 +
task_jitter (job_task j0) + R0); first by done.
{
@@ -489,15 +489,15 @@ Module ResponseTimeAnalysisEDFJitter.
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
+ have COMP := bertogna_edf_all_previous_jobs_complete_by_their_period.
+ have INV := bertogna_edf_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_sporadic_tasks into SPO,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
- H_constrained_deadlines into CONSTR,
- H_sequential_jobs into SEQ.
+ H_constrained_deadlines into CONSTR, H_sequential_jobs into SEQ.
unfold sporadic_task_model in *.
move => delta /andP [HAS LT].
rewrite -has_count in HAS.
@@ -562,8 +562,7 @@ Module ResponseTimeAnalysisEDFJitter.
(task_deadline0 := task_deadline) (tsk0 := tsk) (job_task0 := job_task) (sched0 := sched)
(j0 := j) (t0 := t);
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
- intros j0 tsk0 TSK0 LE.
- by apply (bertogna_edf_all_previous_jobs_complete_by_their_period t); rewrite ?TSK0.
+ by intros j0 tsk0 TSK0 LE; apply (COMP t); rewrite ?TSK0.
}
by subst j2; apply SEQ with (j := j1) (t := t).
}
@@ -596,9 +595,8 @@ Module ResponseTimeAnalysisEDFJitter.
eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
rewrite leq_subLR count_predC size_filter.
- apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
- first by rewrite bertogna_edf_scheduling_invariant.
- by rewrite count_filter.
+ by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ [by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
@@ -671,9 +669,12 @@ Module ResponseTimeAnalysisEDFJitter.
\sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
Proof.
+ have GE_COST := bertogna_edf_R_other_ge_cost.
+ have EXCEEDS := bertogna_edf_minimum_exceeds_interference.
+ have ALLBUSY := bertogna_edf_all_cpus_busy.
+ have TOOMUCH := bertogna_edf_too_much_interference.
rename H_rt_bounds_contains_all_tasks into UNZIP,
H_response_time_is_fixed_point into REC.
- have GE_COST := bertogna_edf_R_other_ge_cost.
apply leq_trans with (n := \sum_(tsk_other <- ts_interf) minn (x tsk_other) (R - task_cost tsk + 1));
last first.
{
@@ -701,11 +702,9 @@ Module ResponseTimeAnalysisEDFJitter.
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
- apply bertogna_edf_minimum_exceeds_interference.
- apply leq_trans with (n := X * num_cpus);
- last by rewrite bertogna_edf_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_edf_too_much_interference.
+ apply EXCEEDS.
+ apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
@@ -716,6 +715,9 @@ Module ResponseTimeAnalysisEDFJitter.
(tsk_other, R_other) \in rt_bounds /\
(minn (x tsk_other) (R - task_cost tsk + 1) > interference_bound tsk_other R_other).
Proof.
+ have SUM := bertogna_edf_sum_exceeds_total_interference.
+ have BOUND := bertogna_edf_workload_bounds_interference.
+ have EDFBOUND := bertogna_edf_specific_bound_holds.
rename H_rt_bounds_contains_all_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_other, R_other) := tup in
@@ -726,7 +728,6 @@ Module ResponseTimeAnalysisEDFJitter.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_edf_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold I, total_interference_bound_edf.
@@ -738,12 +739,12 @@ Module ResponseTimeAnalysisEDFJitter.
{
unfold interference_bound; rewrite leq_min; apply/andP; split;
last by rewrite geq_minr.
- apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
- by apply bertogna_edf_workload_bounds_interference.
+ by apply leq_trans with (n := x tsk_k);
+ [by rewrite geq_minl | by apply BOUND].
}
{
apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
- by apply bertogna_edf_specific_bound_holds.
+ by apply EDFBOUND.
}
}
move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MIN].
@@ -766,6 +767,9 @@ Module ResponseTimeAnalysisEDFJitter.
Theorem bertogna_cirinei_response_time_bound_edf :
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
+ have EXISTS := bertogna_edf_exists_task_that_exceeds_bound.
+ have BASICBOUND := bertogna_edf_workload_bounds_interference.
+ have EDFBOUND := bertogna_edf_specific_bound_holds.
rename H_valid_job_parameters into JOBPARAMS.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
intros j JOBtsk.
@@ -806,15 +810,15 @@ Module ResponseTimeAnalysisEDFJitter.
apply negbT in NOTCOMP; exfalso.
(* Next, we derive a contradiction using the previous lemmas. *)
- exploit (bertogna_edf_exists_task_that_exceeds_bound tsk' R' INbounds j JOBtsk NOTCOMP).
+ exploit (EXISTS tsk' R' INbounds j JOBtsk NOTCOMP).
{
by ins; apply IH with (tsk := tsk_other) (R := R_other).
}
intro EX; destruct EX as [tsk_other [R_other [HP LTmin]]].
unfold interference_bound_edf, interference_bound_generic in LTmin.
rewrite minnAC in LTmin; apply min_lt_same in LTmin.
- have BASICBOUND := bertogna_edf_workload_bounds_interference tsk' R' j JOBtsk BEFOREok tsk_other R_other HP.
- have EDFBOUND := bertogna_edf_specific_bound_holds tsk' R' INbounds j JOBtsk BEFOREok tsk_other R_other HP.
+ specialize (BASICBOUND tsk' R' j JOBtsk BEFOREok tsk_other R_other HP).
+ specialize (EDFBOUND tsk' R' INbounds j JOBtsk BEFOREok tsk_other R_other HP).
unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
{
by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin.
diff --git a/analysis/jitter/bertogna_fp_comp.v b/analysis/jitter/bertogna_fp_comp.v
index 09ab5892e97f4ccb2f99597d59a62098fb27ae8f..5a60ea7f15cb7d53993fd7d48476f49e6ce78550 100644
--- a/analysis/jitter/bertogna_fp_comp.v
+++ b/analysis/jitter/bertogna_fp_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.analysis.jitter.bertogna_fp_theory.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
@@ -449,6 +448,7 @@ Module ResponseTimeIterationFP.
k <= max_steps tsk ->
f k > k + task_cost tsk - 1.
Proof.
+ have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
@@ -463,14 +463,12 @@ Module ResponseTimeIterationFP.
intros LT.
specialize (IHk (ltnW LT)).
apply leq_ltn_trans with (n := f k);
- last by apply bertogna_fp_comp_f_increases, ltnW.
+ last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk; last first.
- {
- apply leq_trans with (n := task_cost tsk); last by apply leq_addl.
- by apply PARAMS.
- }
+ rewrite subh1 in IHk;
+ last by apply leq_trans with (n := task_cost tsk);
+ [by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
@@ -481,6 +479,8 @@ Module ResponseTimeIterationFP.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
+ have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
+ have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
@@ -498,18 +498,19 @@ Module ResponseTimeIterationFP.
move: EX => /forall_inP EX.
rewrite leqNgt in LE; move: LE => /negP LE.
exfalso; apply LE.
- have TOOMUCH := bertogna_fp_comp_rt_grows_too_much _ (max_steps tsk).
- exploit TOOMUCH; [| by apply leqnn |].
+
+ assert (DIFF: forall k : nat, k <= max_steps tsk -> f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
- by exploit (EX (Ordinal LEk)); [by done | intro DIFF].
- }
- unfold max_steps at 1.
+ by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
+ }
+ exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite subh1; last by apply PARAMS2.
- by rewrite -addnBA // subnn addn0.
+ rewrite -addnBA // subnn addn0 subn1 prednK //.
+ intros LT; apply (leq_ltn_trans LT).
+ by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
@@ -665,7 +666,8 @@ Module ResponseTimeIterationFP.
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(job_jitter0 := job_jitter) (higher_eq_priority := higher_priority); try (by done).
{
- cut (NTH idx \in hp_bounds); [intros IN | by apply mem_nth].
+ cut (NTH idx \in hp_bounds = true);
+ [intros IN | by apply mem_nth].
by rewrite -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
}
{
@@ -702,15 +704,15 @@ Module ResponseTimeIterationFP.
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (fp_analysis_yields_response_time_bounds).
+ have UNZIP := (fp_claimed_bounds_unzip ts).
+ have DL := (fp_claimed_bounds_le_deadline ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable,
valid_sporadic_job_with_jitter, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
move => tsk INtsk j JOBtsk.
- have RLIST := (fp_analysis_yields_response_time_bounds).
- have UNZIP := (fp_claimed_bounds_unzip ts).
- have DL := (fp_claimed_bounds_le_deadline ts).
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: exists R, (tsk, R) \in rt_bounds).
diff --git a/analysis/jitter/bertogna_fp_theory.v b/analysis/jitter/bertogna_fp_theory.v
index ac6124dc519f8f270bc1c77365ee93006c9c67b6..1f78d2a488f176aad2d8e6be18c1ed6f8e3a1666 100644
--- a/analysis/jitter/bertogna_fp_theory.v
+++ b/analysis/jitter/bertogna_fp_theory.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.platform_fp
rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority
rt.model.jitter.response_time rt.model.jitter.interference.
Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound_fp.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
@@ -168,7 +167,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [_ IN].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -180,7 +179,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [INTERF _].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -303,7 +302,7 @@ Module ResponseTimeAnalysisFP.
{
intros j_other tsk_other JOBother INTERF.
move: UNZIP => UNZIP.
- cut (tsk_other \in unzip1 hp_bounds); last first.
+ cut (tsk_other \in unzip1 hp_bounds = true); last first.
{
rewrite -UNZIP mem_filter; apply/andP; split; first by done.
by rewrite -JOBother; apply FROMTS.
@@ -394,6 +393,7 @@ Module ResponseTimeAnalysisFP.
Lemma bertogna_fp_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
+ have DIFFTASK := bertogna_fp_interference_by_different_tasks.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
@@ -427,7 +427,7 @@ Module ResponseTimeAnalysisFP.
rewrite -JOBtsk; apply FP with (t := t); try by done.
by apply/existsP; exists cpu; apply/eqP.
}
- apply bertogna_fp_interference_by_different_tasks with (t := t); [by auto | by done |].
+ apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
@@ -443,6 +443,7 @@ Module ResponseTimeAnalysisFP.
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
+ have INV := bertogna_fp_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_valid_job_parameters into JOBPARAMS,
@@ -599,9 +600,8 @@ Module ResponseTimeAnalysisFP.
eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
rewrite leq_subLR count_predC size_filter.
- apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
- first by rewrite bertogna_fp_scheduling_invariant.
- by rewrite count_filter.
+ by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ [by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
@@ -676,6 +676,9 @@ Module ResponseTimeAnalysisFP.
total_interference_bound_fp task_cost task_period task_jitter tsk hp_bounds
R higher_eq_priority.
Proof.
+ have EXCEEDS := bertogna_fp_minimum_exceeds_interference.
+ have ALLBUSY := bertogna_fp_all_cpus_busy.
+ have TOOMUCH := bertogna_fp_too_much_interference.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_recurrence_holds into REC.
apply leq_trans with (n := \sum_(tsk_k <- ts_interf) minn (x tsk_k) (R - task_cost tsk + 1));
@@ -695,11 +698,9 @@ Module ResponseTimeAnalysisFP.
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
- apply bertogna_fp_minimum_exceeds_interference.
- apply leq_trans with (n := X * num_cpus);
- last by rewrite bertogna_fp_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_fp_too_much_interference.
+ apply EXCEEDS.
+ apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 7) After concluding that the sum of the minimum exceeds (R' - e_i + 1),
@@ -711,6 +712,8 @@ Module ResponseTimeAnalysisFP.
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
Proof.
+ have SUM := bertogna_fp_sum_exceeds_total_interference.
+ have INTERFk := bertogna_fp_tsk_other_interferes.
rename H_hp_bounds_has_interfering_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_k, R_k) := tup in
@@ -720,7 +723,6 @@ Module ResponseTimeAnalysisFP.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_fp_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold total_interference_bound_fp.
@@ -729,7 +731,7 @@ Module ResponseTimeAnalysisFP.
apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
specialize (ALL (tsk_k, R_k) HPk).
rewrite -leqNgt in ALL.
- have INTERFk := bertogna_fp_tsk_other_interferes tsk_k R_k HPk.
+ specialize (INTERFk tsk_k R_k HPk).
fold (can_interfere_with_tsk); rewrite INTERFk.
by apply ALL.
}
@@ -745,6 +747,8 @@ Module ResponseTimeAnalysisFP.
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
+ have EX := bertogna_fp_exists_task_that_exceeds_bound.
+ have WORKLOAD := bertogna_fp_workload_bounds_interference.
rename H_valid_job_parameters into PARAMS.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
intros j JOBtsk.
@@ -781,10 +785,10 @@ Module ResponseTimeAnalysisFP.
apply negbT in NOTCOMP; exfalso.
(* We derive a contradiction using the previous lemmas. *)
- have EX := bertogna_fp_exists_task_that_exceeds_bound j JOBtsk NOTCOMP BEFOREok.
+ specialize (EX j JOBtsk NOTCOMP BEFOREok).
destruct EX as [tsk_k [R_k [HPk LTmin]]].
unfold minn at 1 in LTmin.
- have WORKLOAD := bertogna_fp_workload_bounds_interference j tsk_k R_k HPk.
+ specialize (WORKLOAD j tsk_k R_k HPk).
destruct (W_jitter task_cost task_period task_jitter tsk_k R_k R < R - task_cost tsk + 1);
rewrite leq_min in LTmin;
last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
diff --git a/analysis/jitter/interference_bound.v b/analysis/jitter/interference_bound.v
index 2e30af266e90a3a28a3fa407f6e5157aa3aa4c8d..41df7e005d041cffd16bcd3742acf153e3005d6a 100644
--- a/analysis/jitter/interference_bound.v
+++ b/analysis/jitter/interference_bound.v
@@ -1,9 +1,8 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule
rt.model.jitter.interference rt.model.jitter.priority.
Require Import rt.analysis.jitter.workload_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundJitter.
diff --git a/analysis/jitter/interference_bound_edf.v b/analysis/jitter/interference_bound_edf.v
index 525ebeb7ea0b9a92a82885da1471f1664ec0ac28..124063581b81453cde8ae327821e3b29d4fa4dca 100644
--- a/analysis/jitter/interference_bound_edf.v
+++ b/analysis/jitter/interference_bound_edf.v
@@ -1,11 +1,10 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
rt.model.jitter.interference rt.model.jitter.interference_edf.
Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDFJitter.
@@ -704,6 +703,8 @@ Module InterferenceBoundEDFJitter.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 <= interference_bound.
Proof.
+ have ONE := interference_bound_edf_simpl_when_there's_one_job.
+ have SLACK := interference_bound_edf_interference_of_j_fst_limited_by_slack.
rename H_many_jobs into NUM, H_only_one_job into SIZE.
unfold interference_caused_by, interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
@@ -715,8 +716,7 @@ Module InterferenceBoundEDFJitter.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite SIZE.
}
- rewrite interference_bound_edf_simpl_when_there's_one_job.
- by apply interference_bound_edf_interference_of_j_fst_limited_by_slack.
+ by rewrite ONE; apply SLACK.
Qed.
End InterferenceSingleJob.
@@ -886,7 +886,7 @@ Module InterferenceBoundEDFJitter.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite INnth INnth0.
}
- by rewrite subh3 // addnC -INnth.
+ by rewrite subh3 // addnC /p_k -INnth.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
@@ -894,14 +894,14 @@ Module InterferenceBoundEDFJitter.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k >= num_mid_jobs.+1.
Proof.
+ have AFTERt1 :=
+ interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
+ interference_bound_edf_j_fst_completed_on_time.
rename H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in *.
have DIST := interference_bound_edf_many_periods_in_between.
- have AFTERt1 :=
- interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
- interference_bound_edf_j_fst_completed_on_time.
rewrite leqNgt; apply/negP; unfold not; intro LTnk; unfold n_k in LTnk.
rewrite ltn_divLR in LTnk; last by specialize (TASK_PARAMS tsk_k INk); des.
apply (leq_trans LTnk) in DIST; rewrite ltn_subRL in DIST.
@@ -960,8 +960,8 @@ Module InterferenceBoundEDFJitter.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Proof.
- rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
+ rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
first by rewrite SIZE ltnS leqNgt NK in NUM.
by rewrite NK.
diff --git a/analysis/jitter/interference_bound_fp.v b/analysis/jitter/interference_bound_fp.v
index e24d658a33cc6774f892e169ec50e276e3cdfa18..b60d89c3d6651a5d73b827d6ce42ff9690fa8a21 100644
--- a/analysis/jitter/interference_bound_fp.v
+++ b/analysis/jitter/interference_bound_fp.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload
rt.model.jitter.interference.
Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
diff --git a/analysis/jitter/workload_bound.v b/analysis/jitter/workload_bound.v
index e6594b7f6586f09354a96629a635598da4180714..66bf9677b1cb382d3152e7e00c5f437cbd2b51e8 100644
--- a/analysis/jitter/workload_bound.v
+++ b/analysis/jitter/workload_bound.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.task_arrival rt.model.jitter.response_time
rt.model.jitter.schedulability rt.model.jitter.workload.
-Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBoundJitter.
@@ -659,12 +658,14 @@ Module WorkloadBoundJitter.
service_during sched (nth elem sorted_jobs i.+1) t1 t2
<= workload_bound.
Proof.
+ have MID := workload_bound_service_of_middle_jobs.
rename H_jobs_have_valid_parameters into JOBPARAMS.
unfold valid_sporadic_job_with_jitter in *; des.
unfold workload_bound, W_jitter; fold n_k.
move => NK; rewrite -NK.
rewrite -{2}addn1 mulnDl mul1n [_* _ + _]addnC addnA addn_minl.
- apply leq_add; last by apply workload_bound_service_of_middle_jobs.
+ apply leq_add; last first.
+ apply MID.
rewrite leq_min; apply/andP; split.
{
assert (SIZE: 0 < size sorted_jobs).
diff --git a/analysis/parallel/bertogna_edf_comp.v b/analysis/parallel/bertogna_edf_comp.v
index ffd6e4d5e757221ec30df5c9da9b99a69bc435d6..a0b40e4ecee8823be52b2558f08ff24a75e90bd7 100755
--- a/analysis/parallel/bertogna_edf_comp.v
+++ b/analysis/parallel/bertogna_edf_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.analysis.parallel.bertogna_edf_theory.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
@@ -239,7 +238,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
- by apply/(zipP (fun x y => snd x <= snd y)).
+ by apply/(zipP t (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
@@ -248,8 +247,8 @@ Module ResponseTimeIterationEDF.
unfold transitive, all_le.
move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
apply/andP; split; first by rewrite ZIPxy -ZIPyz.
- move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
- move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
+ move: LExy => /(zipP _ (fun x y => snd x <= snd y)) LExy.
+ move: LEyz => /(zipP _ (fun x y => snd x <= snd y)) LEyz.
assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
by rewrite ZIPxy.
assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
@@ -260,8 +259,8 @@ Module ResponseTimeIterationEDF.
apply size0nil in SIZExy; symmetry in SIZEyz.
by apply size0nil in SIZEyz; subst.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (t, 0) | by rewrite SIZExy -SIZEyz|].
+ apply/(zipP t (fun x y => snd x <= snd y));
+ first by rewrite SIZExy -SIZEyz.
intros i LTi.
exploit LExy; first by rewrite SIZExy.
{
@@ -295,8 +294,8 @@ Module ResponseTimeIterationEDF.
by rewrite iterSr IHstep.
}
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].
+ apply/(zipP (tsk0,0) (fun x y => snd x <= snd y));
+ first by rewrite edf_claimed_bounds_size size_map.
intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
@@ -350,10 +349,9 @@ Module ResponseTimeIterationEDF.
apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
rename UNZIP' into SIZE.
rewrite size_map [size (unzip1 _)]size_map in SIZE.
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
- apply/(zipP (fun x y => snd x <= snd y));
- [by apply (p0,0) | by done |].
+ apply/(zipP p0 (fun x y => snd x <= snd y)); first by done.
intros i LTi.
exploit LE; first by rewrite 2!size_map in SIZE.
@@ -421,7 +419,7 @@ Module ResponseTimeIterationEDF.
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
- move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
+ move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
@@ -615,6 +613,8 @@ Module ResponseTimeIterationEDF.
k <= max_steps ts ->
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
Proof.
+ have LT := bertogna_edf_comp_f_increases.
+ have MONO := bertogna_edf_comp_iteration_monotonic.
rename H_at_least_one_task into NONEMPTY.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_valid_task_parameters into VALID.
@@ -625,10 +625,7 @@ Module ResponseTimeIterationEDF.
by exists tsk0.
} destruct DUMMY as [elem _].
- induction step.
- {
- by rewrite addn1.
- }
+ induction step; first by rewrite addn1.
{
rewrite -addn1 ltn_add2r.
apply leq_ltn_trans with (n := \sum_(i <- f step) (let '(tsk, R) := i in R - task_cost tsk)).
@@ -662,12 +659,11 @@ Module ResponseTimeIterationEDF.
}
rewrite -2!big_seq_cond.
- have LT := bertogna_edf_comp_f_increases step (ltnW LE).
- have MONO := bertogna_edf_comp_iteration_monotonic step.
-
+ specialize (LT step (ltnW LE)).
+ specialize (MONO step).
move: LT => /andP [_ LT]; move: LT => /hasP LT.
destruct LT as [[x1 x2] INzip LT]; simpl in *.
- move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
+ move: MONO => /andP [_ /(zipP _ (fun x y => snd x <= snd y)) MONO].
rewrite 2!(big_nth (elem, 0)).
apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
last by rewrite size_map.
@@ -939,6 +935,9 @@ Module ResponseTimeIterationEDF.
Theorem taskset_schedulable_by_edf_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (edf_analysis_yields_response_time_bounds).
+ have DL := (edf_claimed_bounds_le_deadline ts).
+ have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
edf_schedulable,
@@ -952,10 +951,6 @@ Module ResponseTimeIterationEDF.
H_test_succeeds into TEST.
move => tsk INtsk j JOBtsk.
- have RLIST := (edf_analysis_yields_response_time_bounds).
- have DL := (edf_claimed_bounds_le_deadline ts).
- have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
-
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j JOBtsk.
diff --git a/analysis/parallel/bertogna_edf_theory.v b/analysis/parallel/bertogna_edf_theory.v
index e08261eff3bfd9d7a61ec94a099d899cc5078c26..8448eaf546f939352f1c84c1c972f12e63e2a21c 100644
--- a/analysis/parallel/bertogna_edf_theory.v
+++ b/analysis/parallel/bertogna_edf_theory.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.platform rt.model.basic.response_time.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound_edf.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF.
@@ -340,9 +339,11 @@ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by
\sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
x tsk_other > I tsk R.
Proof.
+ have GE_COST := bertogna_edf_R_other_ge_cost.
+ have ALLBUSY := bertogna_edf_all_cpus_busy.
+ have TOOMUCH := bertogna_edf_too_much_interference.
rename H_rt_bounds_contains_all_tasks into UNZIP,
H_response_time_is_fixed_point into REC.
- have GE_COST := bertogna_edf_R_other_ge_cost.
apply leq_trans with (n := \sum_(tsk_other <- ts_interf) x tsk_other);
last first.
{
@@ -368,9 +369,8 @@ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
- rewrite bertogna_edf_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_edf_too_much_interference.
+ rewrite ALLBUSY.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 3) After concluding that the sum of the minimum exceeds (R - e_i + 1),
@@ -381,6 +381,9 @@ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by
(tsk_other, R_other) \in rt_bounds /\
x tsk_other > interference_bound tsk_other R_other.
Proof.
+ have SUM := bertogna_edf_sum_exceeds_total_interference.
+ have BOUND := bertogna_edf_workload_bounds_interference.
+ have EDFBOUND := bertogna_edf_specific_bound_holds.
rename H_rt_bounds_contains_all_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_other, R_other) := tup in
@@ -390,7 +393,6 @@ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_edf_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold I, total_interference_bound_edf.
@@ -398,13 +400,8 @@ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by
apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
specialize (ALL (tsk_k, R_k) INBOUNDSk).
unfold interference_bound_edf; simpl in *.
- rewrite leq_min; apply/andP; split.
- {
- by apply bertogna_edf_workload_bounds_interference.
- }
- {
- by apply bertogna_edf_specific_bound_holds.
- }
+ by rewrite leq_min; apply/andP; split;
+ [by apply BOUND | by apply EDFBOUND].
}
move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MIN].
move: MIN => /andP [/andP [INts INTERFk] MINk].
diff --git a/analysis/parallel/bertogna_fp_comp.v b/analysis/parallel/bertogna_fp_comp.v
index 572d56f90af8c69a77b6feedc3f609550936c651..58beffe3dfbbd92ffbdc246df921df30255d25a6 100644
--- a/analysis/parallel/bertogna_fp_comp.v
+++ b/analysis/parallel/bertogna_fp_comp.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.analysis.parallel.bertogna_fp_theory.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
@@ -437,6 +436,7 @@ Module ResponseTimeIterationFP.
k <= max_steps tsk ->
f k > k + task_cost tsk - 1.
Proof.
+ have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
@@ -450,15 +450,12 @@ Module ResponseTimeIterationFP.
{
intros LT.
specialize (IHk (ltnW LT)).
- apply leq_ltn_trans with (n := f k);
- last by apply bertogna_fp_comp_f_increases, ltnW.
+ apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk; last first.
- {
- apply leq_trans with (n := task_cost tsk); last by apply leq_addl.
- by apply PARAMS.
- }
+ rewrite subh1 in IHk;
+ last by apply leq_trans with (n := task_cost tsk);
+ [by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
@@ -469,6 +466,8 @@ Module ResponseTimeIterationFP.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
+ have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
+ have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
@@ -486,18 +485,19 @@ Module ResponseTimeIterationFP.
move: EX => /forall_inP EX.
rewrite leqNgt in LE; move: LE => /negP LE.
exfalso; apply LE.
- have TOOMUCH := bertogna_fp_comp_rt_grows_too_much _ (max_steps tsk).
- exploit TOOMUCH; [| by apply leqnn |].
+
+ assert (DIFF: forall k : nat, k <= max_steps tsk -> f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
- by exploit (EX (Ordinal LEk)); [by done | intro DIFF].
- }
- unfold max_steps at 1.
+ by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
+ }
+ exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite subh1; last by apply PARAMS2.
- by rewrite -addnBA // subnn addn0.
+ rewrite -addnBA // subnn addn0 subn1 prednK //.
+ intros LT; apply (leq_ltn_trans LT).
+ by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
@@ -648,7 +648,8 @@ Module ResponseTimeIterationFP.
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done).
{
- cut (NTH idx \in hp_bounds); [intros IN | by apply mem_nth].
+ cut (NTH idx \in hp_bounds = true);
+ [intros IN | by apply mem_nth].
by rewrite -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
}
{
@@ -671,15 +672,15 @@ Module ResponseTimeIterationFP.
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
+ have RLIST := (fp_analysis_yields_response_time_bounds).
+ have UNZIP := (fp_claimed_bounds_unzip ts).
+ have DL := (fp_claimed_bounds_le_deadline ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
move => tsk INtsk j JOBtsk.
- have RLIST := (fp_analysis_yields_response_time_bounds).
- have UNZIP := (fp_claimed_bounds_unzip ts).
- have DL := (fp_claimed_bounds_le_deadline ts).
-
+
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: exists R, (tsk, R) \in rt_bounds).
diff --git a/analysis/parallel/bertogna_fp_theory.v b/analysis/parallel/bertogna_fp_theory.v
index a990c5ff6a0bf00224da838978d09826f35725e3..243cb9b33168511d13ef067c1cfe90ff06a2ffe9 100644
--- a/analysis/parallel/bertogna_fp_theory.v
+++ b/analysis/parallel/bertogna_fp_theory.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.response_time rt.model.basic.interference.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound_fp.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
@@ -149,7 +148,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [_ IN].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -161,7 +160,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
- cut (tsk_other \in ts_interf);
+ cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [INTERF _].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
@@ -337,6 +336,7 @@ Module ResponseTimeAnalysisFP.
x tsk_k > total_interference_bound_fp task_cost task_period tsk
hp_bounds R higher_eq_priority.
Proof.
+ have TOOMUCH := bertogna_fp_too_much_interference.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_recurrence_holds into REC.
apply leq_trans with (n := \sum_(tsk_k <- ts_interf) x tsk_k);
@@ -355,8 +355,7 @@ Module ResponseTimeAnalysisFP.
rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
rewrite bertogna_fp_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_fp_too_much_interference.
+ by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 3) After concluding that the sum of the minimum exceeds (R - e_i + 1),
@@ -366,6 +365,8 @@ Module ResponseTimeAnalysisFP.
(tsk_k, R_k) \in hp_bounds /\
x tsk_k > workload_bound tsk_k R_k.
Proof.
+ have INTERFk := bertogna_fp_tsk_other_interferes.
+ have SUM := bertogna_fp_sum_exceeds_total_interference.
rename H_hp_bounds_has_interfering_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_k, R_k) := tup in
@@ -374,7 +375,6 @@ Module ResponseTimeAnalysisFP.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_fp_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold total_interference_bound_fp.
@@ -383,7 +383,7 @@ Module ResponseTimeAnalysisFP.
apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
specialize (ALL (tsk_k, R_k) HPk).
rewrite -leqNgt in ALL.
- have INTERFk := bertogna_fp_tsk_other_interferes tsk_k R_k HPk.
+ specialize (INTERFk tsk_k R_k HPk).
fold (can_interfere_with_tsk); rewrite INTERFk.
unfold interference_bound_generic. by apply ALL.
}
@@ -399,6 +399,8 @@ Module ResponseTimeAnalysisFP.
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk R.
Proof.
+ have EX := bertogna_fp_exists_task_that_exceeds_bound.
+ have BOUND := bertogna_fp_workload_bounds_interference.
rename H_response_time_recurrence_holds into REC,
H_response_time_of_interfering_tasks_is_known into RESP,
H_hp_bounds_has_interfering_tasks into UNZIP,
@@ -433,10 +435,10 @@ Module ResponseTimeAnalysisFP.
apply negbT in NOTCOMP; exfalso.
(* We derive a contradiction using the previous lemmas. *)
- have EX := bertogna_fp_exists_task_that_exceeds_bound j JOBtsk NOTCOMP BEFOREok.
+ specialize (EX j JOBtsk NOTCOMP BEFOREok).
destruct EX as [tsk_k [R_k [HPk LTmin]]].
- have BUG := bertogna_fp_workload_bounds_interference j tsk_k R_k HPk.
- by apply (leq_ltn_trans BUG) in LTmin; rewrite ltnn in LTmin.
+ specialize (BOUND j tsk_k R_k HPk).
+ by apply (leq_ltn_trans BOUND) in LTmin; rewrite ltnn in LTmin.
Qed.
End ResponseTimeBound.
diff --git a/analysis/parallel/interference_bound.v b/analysis/parallel/interference_bound.v
index 1d4e69309e5b0bbc9da768d3c0c900123434e71c..63fed92913d98b4ac6e3698adff0d1c61510feeb 100644
--- a/analysis/parallel/interference_bound.v
+++ b/analysis/parallel/interference_bound.v
@@ -1,8 +1,7 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.parallel.workload_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
diff --git a/analysis/parallel/interference_bound_edf.v b/analysis/parallel/interference_bound_edf.v
index b7721cf74ff4aaa2dbda4011d03f418366c776ae..a06f5532dcb1a53c0bb5badbda1b264da8b81820 100644
--- a/analysis/parallel/interference_bound_edf.v
+++ b/analysis/parallel/interference_bound_edf.v
@@ -1,11 +1,10 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
rt.model.basic.interference rt.model.basic.interference_edf.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDF.
@@ -620,7 +619,7 @@ Module InterferenceBoundEDF.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite INnth INnth0.
}
- by rewrite subh3 // addnC -INnth.
+ by rewrite subh3 // addnC /p_k -INnth.
Qed.
Lemma interference_bound_edf_slack_le_delta:
@@ -648,13 +647,14 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_n_k_covers_all_jobs :
n_k >= num_mid_jobs.+2.
Proof.
+ have AFTERt1 :=
+ interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
+ interference_bound_edf_j_fst_completed_on_time.
+ have SLACK := interference_bound_edf_slack_le_delta.
rename H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in *.
- have AFTERt1 :=
- interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
- interference_bound_edf_j_fst_completed_on_time.
have DIST := interference_bound_edf_many_periods_in_between.
rewrite leqNgt; apply/negP; unfold not; rewrite ltnS; intro LTnk.
assert (BUG: a_lst - a_fst > D_i + R_k - D_k).
@@ -668,7 +668,6 @@ Module InterferenceBoundEDF.
- by rewrite dvdn_eq in DIV; move: DIV => /eqP DIV; rewrite DIV addn1.
- by rewrite -addn1; apply ltnW, ltn_ceil.
}
- have SLACK := interference_bound_edf_slack_le_delta.
rewrite leq_subLR in SLACK.
rewrite -(leq_add2r a_fst) subh1 in BUG;
last by apply interference_bound_edf_j_fst_before_j_lst.
diff --git a/analysis/parallel/interference_bound_fp.v b/analysis/parallel/interference_bound_fp.v
index 905e7e59fba70760548cb85fd723e933fe577e67..49ed78f3decee2a4f91708322b586af34c0b854f 100644
--- a/analysis/parallel/interference_bound_fp.v
+++ b/analysis/parallel/interference_bound_fp.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.interference.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
diff --git a/analysis/parallel/workload_bound.v b/analysis/parallel/workload_bound.v
index 008ef46ff5eb8bd9b19a59c9765f0155cf373888..6cae44aec99594d0e10902b2cf81a1892b311f03 100644
--- a/analysis/parallel/workload_bound.v
+++ b/analysis/parallel/workload_bound.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.schedulability.
-Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
diff --git a/create_makefile.sh b/create_makefile.sh
index a8cd7b5e76077e3def8f2ad6b929ab724dacb54f..25f27433e4f9f189d09e77cab48150eef6ee1ca8 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,6 +1,6 @@
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
-coq_makefile -R . rt $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
+coq_makefile -f _CoqProject $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and
diff --git a/implementation/basic/arrival_sequence.v b/implementation/basic/arrival_sequence.v
index c0143d317172063ff6ecd81f6b5e3386402bccf5..96089dc1546e8460cd92de5ebd0e643b98c7ec1c 100644
--- a/implementation/basic/arrival_sequence.v
+++ b/implementation/basic/arrival_sequence.v
@@ -1,9 +1,8 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.arrival_sequence rt.model.basic.job
rt.model.basic.task rt.model.basic.task_arrival.
Require Import rt.implementation.basic.task rt.implementation.basic.job.
-Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
Module ConcreteArrivalSequence.
diff --git a/implementation/basic/bertogna_edf_example.v b/implementation/basic/bertogna_edf_example.v
index 3d9af57d2d91ea1d092fc97e4e8e9d55f9960ee0..661197da575fd0778e82987f936aa91761d16bac 100644
--- a/implementation/basic/bertogna_edf_example.v
+++ b/implementation/basic/bertogna_edf_example.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task
rt.model.basic.schedule rt.model.basic.schedulability
@@ -10,7 +9,7 @@ Require Import rt.implementation.basic.job
rt.implementation.basic.task
rt.implementation.basic.schedule
rt.implementation.basic.arrival_sequence.
-Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Module ResponseTimeAnalysisEDF.
diff --git a/implementation/basic/job.v b/implementation/basic/job.v
index 0d0bf8128538720613ef6e211e51ffb64204bb74..db1a3c372939e72e20b185dc6382b143d96f3e4e 100644
--- a/implementation/basic/job.v
+++ b/implementation/basic/job.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.all.
Require Import rt.implementation.basic.task.
-Require Import ssreflect ssrbool ssrnat eqtype seq.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteJob.
diff --git a/implementation/basic/schedule.v b/implementation/basic/schedule.v
index c8c28fb75f49c31568595fd624de887f492fa2ef..c4ba99cc8467fe63b174ce1a5cb21710dbf71415 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/basic/schedule.v
@@ -1,8 +1,7 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.arrival_sequence rt.model.basic.schedule
rt.model.basic.platform rt.model.basic.priority.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
diff --git a/implementation/basic/task.v b/implementation/basic/task.v
index 4025b88383f2253c17a3fdb450066f87226e26aa..fe158837bc9def7383f85be212782bbc596ea5f9 100644
--- a/implementation/basic/task.v
+++ b/implementation/basic/task.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.all.
Require Import rt.model.basic.task.
-Require Import ssreflect ssrbool ssrnat eqtype seq.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteTask.
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/jitter/arrival_sequence.v
index b1382aa4a3832004358787bf2e47ced543856cd6..4a66266ea2b77ddf4a2239e775cacb0357091761 100644
--- a/implementation/jitter/arrival_sequence.v
+++ b/implementation/jitter/arrival_sequence.v
@@ -1,9 +1,8 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.arrival_sequence rt.model.jitter.job
rt.model.jitter.task rt.model.jitter.task_arrival.
Require Import rt.implementation.jitter.task rt.implementation.jitter.job.
-Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
Module ConcreteArrivalSequence.
diff --git a/implementation/jitter/bertogna_edf_example.v b/implementation/jitter/bertogna_edf_example.v
index 98746e9459e48893f8c3674a0321a235571fe4de..6cfdd6ac69d61c8a4135037adcf1ab2aa7dc8b14 100644
--- a/implementation/jitter/bertogna_edf_example.v
+++ b/implementation/jitter/bertogna_edf_example.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task
rt.model.jitter.schedule rt.model.jitter.schedulability
@@ -10,7 +9,7 @@ Require Import rt.implementation.jitter.job
rt.implementation.jitter.task
rt.implementation.jitter.schedule
rt.implementation.jitter.arrival_sequence.
-Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Module ResponseTimeAnalysisEDF.
diff --git a/implementation/jitter/job.v b/implementation/jitter/job.v
index d320385624e29efc0c8927caa86576e5c518b4b8..3eb0633ca68f781c5cd1404fedaa830410dd1783 100644
--- a/implementation/jitter/job.v
+++ b/implementation/jitter/job.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.implementation.jitter.task.
-Require Import ssreflect ssrbool ssrnat eqtype seq.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteJob.
diff --git a/implementation/jitter/schedule.v b/implementation/jitter/schedule.v
index cc099f56eddaa948ca21546e06abf7f9590d2324..d4fc05aa6b11a9d22f76aa0edcd485ed6265cbbc 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/jitter/schedule.v
@@ -1,8 +1,7 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.arrival_sequence rt.model.jitter.schedule
rt.model.jitter.platform rt.model.jitter.priority.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
diff --git a/implementation/jitter/task.v b/implementation/jitter/task.v
index d09078a25344273cd228aef9965f8cb341e05546..4e0238f398222124292718ef810c58c88b52cc74 100644
--- a/implementation/jitter/task.v
+++ b/implementation/jitter/task.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task.
-Require Import ssreflect ssrbool ssrnat eqtype seq.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteTask.
diff --git a/model/basic/arrival_sequence.v b/model/basic/arrival_sequence.v
index 660c5e9113a928152e5a73f08d4bd4bcc0f5686d..d84e7664dec68a015deeaf3a8d55ecc82fa63e43 100644
--- a/model/basic/arrival_sequence.v
+++ b/model/basic/arrival_sequence.v
@@ -1,6 +1,5 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all rt.model.basic.job rt.model.basic.task rt.model.basic.time.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* Definitions and properties of job arrival sequences. *)
Module ArrivalSequence.
diff --git a/model/basic/interference.v b/model/basic/interference.v
index 496342b6305ab1e44fe7ab16b68d4372bcc249f4..9cf6985e57ad2de5d835d72b9ce3e130f3f7def3 100644
--- a/model/basic/interference.v
+++ b/model/basic/interference.v
@@ -1,8 +1,7 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.workload.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
@@ -120,7 +119,6 @@ Module Interference.
by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
Qed.
-
Lemma job_interference_le_service :
forall j_other t1 t2,
job_interference j_other t1 t2 <= service_during sched j_other t1 t2.
@@ -187,7 +185,8 @@ Module Interference.
(* The sequential per-job interference bounds the actual interference. *)
Section BoundUsingPerJobInterference.
- Lemma interference_le_interference_joblist :
+
+ Lemma interference_le_interference_joblist :
forall tsk t1 t2,
task_interference tsk t1 t2 <= task_interference_joblist tsk t1 t2.
Proof.
diff --git a/model/basic/interference_edf.v b/model/basic/interference_edf.v
index fa427fa278ccf31149c11cfd7173e9136f0cd2ea..1058ed3ed750be87988a614fc2ee721c1f62409f 100644
--- a/model/basic/interference_edf.v
+++ b/model/basic/interference_edf.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference
rt.model.basic.arrival_sequence rt.model.basic.platform.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module InterferenceEDF.
diff --git a/model/basic/job.v b/model/basic/job.v
index e65f567224c2adf0f9fb964f78dc09aa31055441..f2fa9885261e5dfc4bdf46b1f260150f90273a52 100644
--- a/model/basic/job.v
+++ b/model/basic/job.v
@@ -1,6 +1,5 @@
-Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.model.basic.task.
-Require Import ssrnat ssrbool eqtype.
+From mathcomp Require Import ssrnat ssrbool eqtype.
(* Properties of different types of job: *)
Module Job.
diff --git a/model/basic/platform.v b/model/basic/platform.v
index b95db94caa3d96be28fe72be68de1de58d9501f3..f89ff7697319f22f16b75e399f151216fb51334d 100644
--- a/model/basic/platform.v
+++ b/model/basic/platform.v
@@ -1,8 +1,7 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
@@ -149,7 +148,7 @@ Module Platform.
rewrite -addn1 addnC [_ + 1]addnC -addnA.
apply leq_add; first by done.
rewrite eq_fun_ord_to_nat; unfold make_sequence at 2; rewrite EX /= add0n.
- apply leq_add; apply leq_sum; ins; unfold fun_ord_to_nat; des_eqrefl2; try done;
+ apply leq_add; apply leq_sum; ins; unfold fun_ord_to_nat; des_eqrefl; try done;
by unfold make_sequence; desf.
}
}
@@ -247,6 +246,7 @@ Module Platform.
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
Proof.
+ have UNIQ := platform_at_most_one_pending_job_of_each_task.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
@@ -265,7 +265,6 @@ Module Platform.
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs in *.
- have UNIQ := platform_at_most_one_pending_job_of_each_task.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{
apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
diff --git a/model/basic/platform_fp.v b/model/basic/platform_fp.v
index 4b434d6cf5402e0c33c096a863a23bf58ca8fa11..6befe703964baad39a7873e65c7fd76589d6a6df 100644
--- a/model/basic/platform_fp.v
+++ b/model/basic/platform_fp.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.interference
rt.model.basic.priority rt.model.basic.platform.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module PlatformFP.
@@ -175,6 +174,8 @@ Module PlatformFP.
Lemma platform_fp_cpus_busy_with_interfering_tasks :
count (scheduled_task_with_higher_eq_priority tsk) ts = num_cpus.
Proof.
+ have UNIQ := platform_fp_no_multiple_jobs_of_interfering_tasks.
+ have UNIQ' := platform_fp_no_multiple_jobs_of_tsk.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
@@ -196,8 +197,6 @@ Module PlatformFP.
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs,
can_interfere_with_tsk in *.
- have UNIQ := platform_fp_no_multiple_jobs_of_interfering_tasks.
- have UNIQ' := platform_fp_no_multiple_jobs_of_tsk.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{
apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
diff --git a/model/basic/priority.v b/model/basic/priority.v
index 8ea503b28b4434d9e6f4cd024bba2e61dda2f2dd..b96753c05474719c6d5b4354753c4c827ee9bda6 100644
--- a/model/basic/priority.v
+++ b/model/basic/priority.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
-Require Import ssreflect ssrbool eqtype ssrnat seq.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
(* Definitions of FP and JLFP/JLDP priority relations. *)
diff --git a/model/basic/response_time.v b/model/basic/response_time.v
index 5949f5f9042b835d2511f35a3446d033ab443532..68fd3a16d5ea435730189bc56b354e8278da1b02 100644
--- a/model/basic/response_time.v
+++ b/model/basic/response_time.v
@@ -1,8 +1,7 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Definition of response-time bound and some simple lemmas. *)
Module ResponseTime.
diff --git a/model/basic/schedulability.v b/model/basic/schedulability.v
index fd80738e96d68721d7b7969181a80c7439597a6f..88bdb99d3b43854356a6c419acad48e6e47e2318 100644
--- a/model/basic/schedulability.v
+++ b/model/basic/schedulability.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule.
-Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
(* Definitions of deadline miss. *)
Module Schedulability.
diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index 5246d415560869715ba629ddc9799e38eb367b26..47cfa1baa78ea77d0324bebb0074efb3650547f7 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all
rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Definition, properties and lemmas about schedules. *)
Module Schedule.
diff --git a/model/basic/task.v b/model/basic/task.v
index b3dcbec66085cd02e3cab2124880bd61938d116a..df65a6d58a6d3af7539050109ff51b0781064369 100644
--- a/model/basic/task.v
+++ b/model/basic/task.v
@@ -1,6 +1,5 @@
-Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.all.
-Require Import ssrnat ssrbool eqtype fintype seq.
+From mathcomp Require Import ssrnat ssrbool eqtype fintype seq.
(* Attributes of a valid sporadic task. *)
Module SporadicTask.
diff --git a/model/basic/task_arrival.v b/model/basic/task_arrival.v
index a9308b04d91e9d518f6945cfea27b4de322c5814..44a769db2d57c7f640a4f86e57aa8bd0242f3351 100644
--- a/model/basic/task_arrival.v
+++ b/model/basic/task_arrival.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
-Require Import ssreflect ssrbool eqtype ssrnat seq.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
(* Properties of the job arrival. *)
Module SporadicTaskArrival.
diff --git a/model/basic/workload.v b/model/basic/workload.v
index f80d0e83254adbe32331d2229971a2987953dde7..78f8f1a60cb4d494ea99aec7c87a32ab6635d148 100644
--- a/model/basic/workload.v
+++ b/model/basic/workload.v
@@ -1,9 +1,8 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.schedulability.
-Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module Workload.
diff --git a/model/jitter/arrival_sequence.v b/model/jitter/arrival_sequence.v
index 17e5f45edf4b60547fa71a919742921ad99ad417..316a75b8a6796c29c6aa5f64e58d34b07c0a8272 100644
--- a/model/jitter/arrival_sequence.v
+++ b/model/jitter/arrival_sequence.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* All definitions from arrival sequence can be safely imported. *)
Require Export rt.model.basic.arrival_sequence.
\ No newline at end of file
diff --git a/model/jitter/interference.v b/model/jitter/interference.v
index 583240d1b40b731d73af46ede2f6b77af7bb2b55..63dca9f75da1e18564d34a73523a09f0a3274e4b 100644
--- a/model/jitter/interference.v
+++ b/model/jitter/interference.v
@@ -1,9 +1,8 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.workload.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
diff --git a/model/jitter/interference_edf.v b/model/jitter/interference_edf.v
index 1277e3ee0cd395ce9c39a853074e59a018063e1d..6a9d4d1e2ac6358e3ef2edf5d300c4fef08b3231 100644
--- a/model/jitter/interference_edf.v
+++ b/model/jitter/interference_edf.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference
rt.model.jitter.arrival_sequence rt.model.jitter.platform.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module InterferenceEDF.
diff --git a/model/jitter/job.v b/model/jitter/job.v
index abf4244934f81fe3dbda2a0fbb9f1828cb184102..35e395f385918a895c36189c81207b6935823538 100644
--- a/model/jitter/job.v
+++ b/model/jitter/job.v
@@ -1,6 +1,5 @@
-Add LoadPath "../../" as rt.
Require Import rt.model.jitter.time rt.model.jitter.task.
-Require Import ssrnat ssrbool eqtype.
+From mathcomp Require Import ssrnat ssrbool eqtype.
Require Export rt.model.basic.job.
diff --git a/model/jitter/platform.v b/model/jitter/platform.v
index e02219128c675c696bcecf5640e1a481028f6083..ad283f800cb28ee2bf9cabd7a450bbe7046675c3 100644
--- a/model/jitter/platform.v
+++ b/model/jitter/platform.v
@@ -1,8 +1,7 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
@@ -151,7 +150,7 @@ Module Platform.
rewrite -addn1 addnC [_ + 1]addnC -addnA.
apply leq_add; first by done.
rewrite eq_fun_ord_to_nat; unfold make_sequence at 2; rewrite EX /= add0n.
- apply leq_add; apply leq_sum; ins; unfold fun_ord_to_nat; des_eqrefl2; try done;
+ apply leq_add; apply leq_sum; ins; unfold fun_ord_to_nat; des_eqrefl; try done;
by unfold make_sequence; desf.
}
}
@@ -254,6 +253,7 @@ Module Platform.
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
Proof.
+ have UNIQ := platform_at_most_one_pending_job_of_each_task.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
@@ -272,7 +272,6 @@ Module Platform.
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs in *.
- have UNIQ := platform_at_most_one_pending_job_of_each_task.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{
apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
diff --git a/model/jitter/platform_fp.v b/model/jitter/platform_fp.v
index 1df61ffee6305c54be66850aeccde26bdf1502e3..e330c42bc3a9f46ca6f73feb18cedfe4891317f1 100644
--- a/model/jitter/platform_fp.v
+++ b/model/jitter/platform_fp.v
@@ -1,9 +1,8 @@
-Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.task_arrival rt.model.jitter.interference
rt.model.jitter.priority rt.model.jitter.platform.
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module PlatformFP.
@@ -186,6 +185,8 @@ Module PlatformFP.
Lemma platform_fp_cpus_busy_with_interfering_tasks :
count (scheduled_task_with_higher_eq_priority tsk) ts = num_cpus.
Proof.
+ have UNIQ := platform_fp_no_multiple_jobs_of_interfering_tasks.
+ have UNIQ' := platform_fp_no_multiple_jobs_of_tsk.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
@@ -207,8 +208,6 @@ Module PlatformFP.
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs,
can_interfere_with_tsk in *.
- have UNIQ := platform_fp_no_multiple_jobs_of_interfering_tasks.
- have UNIQ' := platform_fp_no_multiple_jobs_of_tsk.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{
apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
diff --git a/model/jitter/priority.v b/model/jitter/priority.v
index c2f5a4aec091ded0e46f97935a150b2a8f2d8bef..1a59a29edafce6aaebc7a3beddd74ade26f6def6 100644
--- a/model/jitter/priority.v
+++ b/model/jitter/priority.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* Because we define EDF using the *actual job arrivals*, we can safely import the original of priority. *)
Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/jitter/response_time.v b/model/jitter/response_time.v
index 91a8aa5a06a73f4d2138658acabdd36e0f630626..673085f1b3bd8d6cb4d2b8e140bfd31dba564a76 100644
--- a/model/jitter/response_time.v
+++ b/model/jitter/response_time.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* Since jitter does not change the notion of response time, we keep
the original definitions. *)
diff --git a/model/jitter/schedulability.v b/model/jitter/schedulability.v
index ed5c6769e56240c28f8ff744aea9977d6802f1c3..7dfa86aff7d53b4d13f65d3892d07c3537c798ee 100644
--- a/model/jitter/schedulability.v
+++ b/model/jitter/schedulability.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* Jitter doesn't affect the notion of deadline miss, so we can safely
import the basic definitions. *)
diff --git a/model/jitter/schedule.v b/model/jitter/schedule.v
index f75c7a62ef4c2ae567c2f8fa13a94c85674962b7..a78068ba480014d8ebe99f9019d99bc54eb23d90 100644
--- a/model/jitter/schedule.v
+++ b/model/jitter/schedule.v
@@ -1,7 +1,6 @@
-Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.arrival_sequence.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Definition, properties and lemmas about schedules. *)
Module ScheduleWithJitter.
diff --git a/model/jitter/task.v b/model/jitter/task.v
index 84a6028779b4de90db6a309290abb53d3ff66ae4..73037fe62d05e1bad39faa106a7280ba9fc9b2b9 100644
--- a/model/jitter/task.v
+++ b/model/jitter/task.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* Since the worst-case jitter of a task is unbounded, we don't need to
define any specific properties for a task with jitter.*)
diff --git a/model/jitter/task_arrival.v b/model/jitter/task_arrival.v
index b050e784bd1f21e2203391b9975ccdaa40a00b95..d2db320ed8dc63fe098582e2b92df063e624b6a3 100644
--- a/model/jitter/task_arrival.v
+++ b/model/jitter/task_arrival.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* Interarrival times are specified by the environment and are based on the
original arrival times. We can import the original definitions. *)
diff --git a/model/jitter/time.v b/model/jitter/time.v
index 603a1f76e5817edeea5539ca8840a6b94ac07bd1..06ad193b5fb228c7d2d6cc05aad597669eb2ab1d 100644
--- a/model/jitter/time.v
+++ b/model/jitter/time.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* The definition of time is the same. *)
Require Export rt.model.basic.time.
\ No newline at end of file
diff --git a/model/jitter/workload.v b/model/jitter/workload.v
index 83d15b159a42b45365a777024e4f7159ceae647f..280cc69ebcb55ec9c71d1245988e9c433fefc734 100644
--- a/model/jitter/workload.v
+++ b/model/jitter/workload.v
@@ -1,4 +1,3 @@
-Add LoadPath "../../" as rt.
(* The workload of a task doesn't depend on jitter, so we keep the original definitions. *)
Require Export rt.model.basic.workload.
\ No newline at end of file
diff --git a/util/all.v b/util/all.v
index 440291a291c0b22d66ec424e8e27c34b76146591..5ee67b8a496cdb36670df403b243de2baf0747b5 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,4 +1,3 @@
-Add LoadPath ".." as rt.
Require Export rt.util.tactics.
Require Export rt.util.notation.
diff --git a/util/bigcat.v b/util/bigcat.v
index 69d30e8539857349b860efa7b718d19a9d83e734..c58d3dda7f439c1db75bc8968ed05cd0b9d65ada 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.notation rt.util.bigord.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about the big concatenation operator. *)
Section BigCatLemmas.
diff --git a/util/bigord.v b/util/bigord.v
index 419a9d228e586608f30ffc378f0bf55f1f8e7515..065a0f9767bcdfe7844299091fdf3a699da01dec 100644
--- a/util/bigord.v
+++ b/util/bigord.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about big operators over Ordinals that use Ordinal functions.
There is no support for them in ssreflect. *)
@@ -16,8 +15,7 @@ Section BigOrdFunOrd.
forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
(fun_ord_to_nat x0 f) x = f x.
Proof.
- ins; unfold fun_ord_to_nat.
- des_eqrefl2.
+ ins; unfold fun_ord_to_nat; des_eqrefl.
by f_equal; apply ord_inj.
by destruct x; ins; rewrite i in EQ.
Qed.
diff --git a/util/counting.v b/util/counting.v
index eb16fa66d1275e3076c7f68fa4051548df37a86b..3e6fe473a123091a5917f709d0d05114b2dfb94f 100644
--- a/util/counting.v
+++ b/util/counting.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.exists.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Additional lemmas about counting. *)
Section Counting.
diff --git a/util/divround.v b/util/divround.v
index 938a70023c20c573fb73ef746dbda159ae07fd0e..714a5223b2a6a611a0f1081d7dff4bc0ed81d051 100644
--- a/util/divround.v
+++ b/util/divround.v
@@ -1,5 +1,4 @@
-Add LoadPath ".." as rt.
-Require Import ssrbool ssrnat div.
+From mathcomp Require Import ssrbool ssrnat div.
Definition div_floor (x y: nat) : nat := x %/ y.
Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.
\ No newline at end of file
diff --git a/util/exists.v b/util/exists.v
index 27856c470946b2b398a81cce524a71fdf24d0c74..7dd564da3724ad6cd7a3d5d3c9ae8fdcdf1a5857 100644
--- a/util/exists.v
+++ b/util/exists.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
(* Lemmas about the finite existential for Ordinals: [exists x, P x]. *)
Section OrdExists.
diff --git a/util/fixedpoint.v b/util/fixedpoint.v
index 10fb78d401ea2027503f799d1857a5c94cbb9e65..b1d31d931c425bafc89ad04add409fa5dcb6d543 100644
--- a/util/fixedpoint.v
+++ b/util/fixedpoint.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.induction.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Section FixedPoint.
diff --git a/util/induction.v b/util/induction.v
index aef2dfe37505d4565ccf5ec9ad8d1d9cb9448c4f..70ea7b7b80449636b59b21f0e38347f50c02c847 100644
--- a/util/induction.v
+++ b/util/induction.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Induction lemmas for natural numbers. *)
Section NatInduction.
diff --git a/util/list.v b/util/list.v
index 94b71d51d4c7c3fb6fdbe9f75f084dde9c984230..6ff7ac78ab30156e527c7e02c5d3b0001201112a 100644
--- a/util/list.v
+++ b/util/list.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about lists without duplicates. *)
Section UniqList.
@@ -101,7 +100,7 @@ End UniqList.
(* Additional lemmas about list zip. *)
Section Zip.
- Lemma zipP {T: eqType} (P: _ -> _ -> bool) (X Y: seq T) x0:
+ Lemma zipP {T: eqType} (x0: T) (P: _ -> _ -> bool) (X Y: seq T):
size X = size Y ->
reflect (forall i, i < size (zip X Y) -> P (nth x0 X i) (nth x0 Y i))
(all (fun p => P (fst p) (snd p)) (zip X Y)).
diff --git a/util/nat.v b/util/nat.v
index 0880a188a50692a33d8856d2ffae2054988ab55b..35690a9a66c31e12b68a415e7d5842b03f04bfbb 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.divround rt.util.ssromega.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
(* Additional lemmas about natural numbers. *)
Section NatLemmas.
diff --git a/util/notation.v b/util/notation.v
index 17b0895c9bba4be3846e91aeec6c172107940a66..6787517bdebb9fa20643f64c7c96c7e731f39cce 100644
--- a/util/notation.v
+++ b/util/notation.v
@@ -1,5 +1,4 @@
-Add LoadPath ".." as rt.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Here we define a more verbose notation for projections of pairs... *)
Section Pair.
diff --git a/util/powerset.v b/util/powerset.v
index 44900176d607e1fdf4dc746f3c775a2d1257b59d..723fcfdae699e4795ac90abd4fd4dc7f03541a78 100644
--- a/util/powerset.v
+++ b/util/powerset.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple.
Section PowerSet.
diff --git a/util/sorting.v b/util/sorting.v
index d1f0d4f8b9ac3aa13912211a418b79b7dcce7dfc..e28d8003bcaff85a1ac8e26216945d627003a734 100644
--- a/util/sorting.v
+++ b/util/sorting.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.induction.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
(* Lemmas about sorted lists. *)
Section Sorting.
@@ -63,13 +62,14 @@ Section Sorting.
destruct s; first by rewrite ltn0 in LT.
simpl in SORT.
induction delta;
- first by rewrite /= addn0 ltnS in LT; rewrite addn0; apply/pathP.
+ first by rewrite /= addn0 ltnS in LT; rewrite /= -addnE addn0; apply/pathP.
{
rewrite /transitive (TRANS (nth x0 (s :: s0) (i1.+1 + delta))) //;
first by apply IHdelta, leq_ltn_trans with (n := i1.+1 + delta.+1); [rewrite leq_add2l|].
- rewrite -[delta.+1]addn1 addnA addn1; apply/pathP; first by done.
+ rewrite -[delta.+1]addn1 addnA addn1.
+ move: SORT => /pathP SORT; apply SORT.
by rewrite /= -[delta.+1]addn1 addnA addn1 ltnS in LT.
- }
+ }
Qed.
Lemma sorted_uniq_rel_implies_le_idx :
diff --git a/util/ssromega.v b/util/ssromega.v
index b5341a0d51bc02c2e2d1514114f0a774c9323a83..426d8d07311ec76f642e1eb75789b223e46fc9a6 100644
--- a/util/ssromega.v
+++ b/util/ssromega.v
@@ -1,4 +1,5 @@
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq Omega.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import Omega.
(* Taken from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)
diff --git a/util/sum.v b/util/sum.v
index 3242b0f6254bd0b695542e4c7ed5465deea57749..5180530b5cb4a1c9f59efe259d5e00398bdcc87d 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,6 +1,5 @@
-Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
-Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about arithmetic with sums. *)
Section SumArithmetic.
diff --git a/util/tactics.v b/util/tactics.v
index f94e0f0f7ba2905697488742aaf887cb34af1e19..cff319faa75bc1300d11d4577a0ded56fab883e6 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -11,7 +11,7 @@
(** Symbols starting with [vlib__] are internal. *)
-Require Import ssreflect ssrbool ssrnat eqtype bigop.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype bigop.
Open Scope bool_scope.
Open Scope list_scope.
@@ -175,7 +175,6 @@ Ltac clarsimp := intros; simpl in *; vlib__clarsimp1.
Ltac autos := clarsimp; auto with vlib.
-
(* ************************************************************************** *)
(** Destruct but give useful names *)
(* ************************************************************************** *)
@@ -289,31 +288,18 @@ Ltac des_if :=
Ltac des_eqrefl :=
match goal with
- | H: context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] |- _ =>
- let EQ := fresh "EQ" in
- let id' := fresh "x" in
- revert H;
- generalize (Logic.eq_refl X); generalize X at 1 3;
- intros id' EQ; destruct id'; intros H
- | |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
- let EQ := fresh "EQ" in
- let id' := fresh "x" in
- generalize (Logic.eq_refl X); generalize X at 1 3;
- intros id' EQ; destruct id'
- end.
-
-Ltac des_eqrefl2 :=
- match goal with
- | H: context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] |- _ =>
+ | H: context[match ?X with |true => _ | false => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
- generalize (Logic.eq_refl X); generalize X at 2 3;
+ generalize (Logic.eq_refl X);
+ try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'; intros H
- | |- context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] =>
+ | |- context[match ?X with |true => _ | false => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
- generalize (Logic.eq_refl X); generalize X at 2 3;
+ generalize (Logic.eq_refl X);
+ try (generalize X at 1 3); try (generalize X at 2 3);
intros id' EQ; destruct id'
end.