Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rtproofs
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Sophie Quinton
rtproofs
Commits
9884f13e
Commit
9884f13e
authored
Sep 04, 2018
by
Felipe Cerqueira
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add lemmas about pick and make it easier to use
parent
258edf49
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
110 additions
and
47 deletions
+110
47
analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
+2
2
analysis/uni/susp/dynamic/jitter/taskset_membership.v
analysis/uni/susp/dynamic/jitter/taskset_membership.v
+3
3
util/pick.v
util/pick.v
+105
42
No files found.
analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
View file @
9884f13e
...
...
@@ 188,8 +188,8 @@ Module RTAByReduction.
{
intros
j_hp
ARRhp
OTHERhp
.
rewrite
/
actual_response_time
.
apply
pick_min_holds
;
last
by
intros
r
RESP
_
.
exists
(
Ordinal
(
ltnSn
(
R
(
job_task
j_hp
))))
.
apply
pick_min_holds
;
last
by
intros
r
_
RESP
_
.
exists
(
R
(
job_task
j_hp
))
;
split
;
first
by
done
.
by
apply
RESPhp
;
try
(
by
done
)
;
[
by
apply
FROM

rewrite
/
other_hep_task

H_job_of_tsk
].
}
{
...
...
analysis/uni/susp/dynamic/jitter/taskset_membership.v
View file @
9884f13e
...
...
@@ 133,7 +133,7 @@ Module TaskSetMembership.
intros
j_hp
ARRhp
HP
.
rewrite
/
actual_response_time
.
apply
pick_min_holds
;
last
by
done
.
exists
(
Ordinal
(
ltnSn
(
R
(
job_task
j_hp
)))).
simpl
.
exists
(
R
(
job_task
j_hp
))
;
split
;
first
by
done
.
by
apply
RESPhp
;
try
(
by
done
)
;
first
by
apply
FROM
.
Qed
.
...
...
@@ 153,14 +153,14 @@ Module TaskSetMembership.
rewrite
/
actual_response_time
.
apply
pick_min_holds
;
last
by
intros
x
RESPx
_
MINx
;
rewrite

ltnS
in
LT
;
apply
(
MINx
(
Ordinal
LT
)).
exists
(
Ordinal
(
ltnSn
(
R
(
job_task
j_hp
))))
.
exists
(
R
(
job_task
j_hp
))
;
split
;
first
by
done
.
by
apply
RESPhp
;
try
(
by
done
)
;
first
by
apply
FROM
.
}
{
apply
leq_trans
with
(
n
:
=
(
R
(
job_task
j_hp
)))
;
last
by
apply
ltnW
.
rewrite

ltnS
/
actual_response_time
.
apply
pick_min_ltn
.
exists
(
Ordinal
(
ltnSn
(
R
(
job_task
j_hp
)))).
simpl
.
exists
(
R
(
job_task
j_hp
))
;
split
;
first
by
done
.
by
apply
RESPhp
;
try
(
by
done
)
;
first
by
apply
FROM
.
}
Qed
.
...
...
util/pick.v
View file @
9884f13e
...
...
@@ 11,17 +11,18 @@ Definition arg_pred_nat n (P: pred 'I_n) ord :=
Definition
pred_min_nat
n
(
P
:
pred
'
I_n
)
:
=
arg_pred_nat
n
P
leq
.
Definition
pred_max_nat
n
(
P
:
pred
'
I_n
)
:
=
arg_pred_nat
n
P
(
fun
x
y
=>
geq
x
y
).
Definition
to_pred_ord
n
(
P
:
pred
nat
)
:
=
(
fun
x
:
'
I_n
=>
P
(
nat_of_ord
x
)).
(** Defining Pick functions *)
(* (pick_any n P) returns some number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_any
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
P
).
Definition
pick_any
n
(
P
:
pred
nat
)
:
=
default0
(
pick
(
to_pred_ord
n
P
)
).
(* (pick_min n P) returns the smallest number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_min
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
(
pred_min_nat
n
P
)).
Definition
pick_min
n
(
P
:
pred
nat
)
:
=
default0
(
pick
(
pred_min_nat
n
(
to_pred_ord
n
P
)
)).
(* (pick_max n P) returns the largest number < n that satisfies P, or 0 if it cannot be found. *)
Definition
pick_max
n
(
P
:
pred
'
I_n
)
:
=
default0
(
pick
(
pred_max_nat
n
P
)).
Definition
pick_max
n
(
P
:
pred
nat
)
:
=
default0
(
pick
(
pred_max_nat
n
(
to_pred_ord
n
P
)
)).
(** Improved notation *)
...
...
@@ 30,27 +31,27 @@ Definition pick_max n (P: pred 'I_n) := default0 (pick (pred_max_nat n P)).
[pickmin x <= N  P], [pickmin x < N  P]
[pickmax x <= N  P], [pickmax x < N  P]. *)
Notation
"[ 'pickany' x <= N  P ]"
:
=
(
pick_any
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
pick_any
N
.+
1
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickany' x < N  P ]"
:
=
(
pick_any
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
pick_any
N
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmin' x <= N  P ]"
:
=
(
pick_min
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
pick_min
N
.+
1
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmin' x < N  P ]"
:
=
(
pick_min
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
pick_min
N
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmax' x <= N  P ]"
:
=
(
pick_max
N
.+
1
(
fun
x
:
'
I_N
.+
1
=>
P
%
B
))
(
pick_max
N
.+
1
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
Notation
"[ 'pickmax' x < N  P ]"
:
=
(
pick_max
N
(
fun
x
:
'
I_N
=>
P
%
B
))
(
pick_max
N
(
fun
x
:
nat
=>
P
%
B
))
(
at
level
0
,
x
ident
,
only
parsing
)
:
form_scope
.
(** Lemmas about pick_any *)
...
...
@@ 58,11 +59,11 @@ Notation "[ 'pickmax' x < N  P ]" :=
Section
PickAny
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
p
:
pred
nat
.
Variable
P
:
nat
>
Prop
.
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
EX
:
exists
x
,
x
<
n
/\
p
x
.
Hypothesis
HOLDS
:
forall
x
,
p
x
>
P
x
.
...
...
@@ 73,8 +74,8 @@ Section PickAny.
rewrite
/
pick_any
/
default0
.
case
:
pickP
;
first
by
intros
x
PRED
;
apply
HOLDS
.
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
].
by
specialize
(
NONE
x
)
;
rewrite
PRED
in
NONE
.
move
:
EX
=>
[
x
[
LTN
PRED
]
].
by
specialize
(
NONE
(
Ordinal
LTN
))
;
rewrite
/
to_pred_ord
/=
PRED
in
NONE
.
Qed
.
End
PickAny
.
...
...
@@ 83,12 +84,12 @@ End PickAny.
Section
PickMin
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
p
:
pred
nat
.
Variable
P
:
nat
>
Prop
.
(* Assume that there is some number < n that satisfies p. *)
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
EX
:
exists
x
,
x
<
n
/\
p
x
.
Section
Bound
.
...
...
@@ 99,12 +100,12 @@ Section PickMin.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
by
rewrite
/
default0
.
by
rewrite
/
default0
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmin
:
=
arg_min
x
p
id
.
move
:
EX
=>
[
x
[
LT
PRED
]
]
;
clear
EX
.
set
argmin
:
=
arg_min
(
Ordinal
LT
)
p
id
.
specialize
(
NONE
argmin
).
suff
ARGMIN
:
(
pred_min_nat
n
p
)
argmin
by
rewrite
ARGMIN
in
NONE
.
rewrite
/
argmin
;
case
:
arg_minP
;
first
by
done
.
...
...
@@ 120,9 +121,9 @@ Section PickMin.
Hypothesis
MIN
:
forall
x
,
p
x
>
x
<
n
>
(
forall
y
,
p
y
>
x
<=
y
)
>
p
x
>
(
forall
y
,
y
<
n
>
p
y
>
x
<=
y
)
>
P
x
.
(* Next, we show that any property P of (pick_min n p) can be proven by showing
...
...
@@ 133,70 +134,71 @@ Section PickMin.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
apply
MIN
;
try
(
by
done
).
by
intros
y
Py
;
specialize
(
ALL
y
)
;
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
apply
MIN
;
[
by
rewrite
/
default0

by
done
].
intros
y
LTy
Py
;
specialize
(
ALL
(
Ordinal
LTy
)).
by
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmin
:
=
arg_min
x
p
id
.
move
:
EX
=>
[
x
[
LT
PRED
]
]
;
clear
EX
.
set
argmin
:
=
arg_min
(
Ordinal
LT
)
p
id
.
specialize
(
NONE
argmin
).
suff
ARGMIN
:
(
pred_min_nat
n
p
)
argmin
by
rewrite
ARGMIN
in
NONE
.
rewrite
/
argmin
;
case
:
arg_minP
;
first
by
done
.
intros
y
Py
MINy
.
apply
/
andP
;
split
;
first
by
done
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MINy
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MINy
.
}
Qed
.
End
Minimum
.
End
PickMin
.
(** Lemmas about pick_max *)
Section
PickMax
.
Variable
n
:
nat
.
Variable
p
:
pred
'
I_n
.
Variable
p
:
pred
nat
.
Variable
P
:
nat
>
Prop
.
(* Assume that there is some number < n that satisfies p. *)
Hypothesis
EX
:
exists
x
:
'
I_n
,
p
x
.
Hypothesis
EX
:
exists
x
,
x
<
n
/\
p
x
.
Section
Bound
.
(* First, we show that (pick_max n p) < n. *)
(* First, we show that (pick_max n p) < n.
..
*)
Lemma
pick_max_ltn
:
pick_max
n
p
<
n
.
Proof
.
rewrite
/
pick_max
/
odflt
/
oapp
.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
by
rewrite
/
default0
.
by
rewrite
/
default0
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmax
:
=
arg_max
x
p
id
.
move
:
EX
=>
[
x
[
LT
PRED
]
]
;
clear
EX
.
set
argmax
:
=
arg_max
(
Ordinal
LT
)
p
id
.
specialize
(
NONE
argmax
).
suff
ARGMAX
:
(
pred_max_nat
n
p
)
argmax
by
rewrite
ARGMAX
in
NONE
.
rewrite
/
argmax
;
case
:
arg_maxP
;
first
by
done
.
intros
y
Py
MAXy
.
apply
/
andP
;
split
;
first
by
done
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MAXy
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MAXy
.
}
Qed
.
End
Bound
.
Section
Maximum
.
Hypothesis
MAX
:
forall
x
,
p
x
>
x
<
n
>
(
forall
y
,
p
y
>
x
>=
y
)
>
p
x
>
(
forall
y
,
y
<
n
>
p
y
>
x
>=
y
)
>
P
x
.
(* Next, we show that any property P of (pick_max n p) can be proven by showing that
...
...
@@ 207,22 +209,83 @@ Section PickMax.
case
:
pickP
.
{
move
=>
x
/
andP
[
PRED
/
forallP
ALL
].
apply
MAX
;
try
(
by
done
).
by
intros
y
Py
;
specialize
(
ALL
y
)
;
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
apply
MAX
;
[
by
rewrite
/
default0

by
rewrite
/
default0
].
intros
y
LTy
Py
;
specialize
(
ALL
(
Ordinal
LTy
)).
by
move
:
ALL
=>
/
implyP
ALL
;
apply
ALL
.
}
{
intros
NONE
;
red
in
NONE
;
exfalso
.
move
:
EX
=>
[
x
PRED
]
;
clear
EX
.
set
argmax
:
=
arg_max
x
p
id
.
move
:
EX
=>
[
x
[
LT
PRED
]
]
;
clear
EX
.
set
argmax
:
=
arg_max
(
Ordinal
LT
)
p
id
.
specialize
(
NONE
argmax
).
suff
ARGMAX
:
(
pred_max_nat
n
p
)
argmax
by
rewrite
ARGMAX
in
NONE
.
rewrite
/
argmax
;
case
:
arg_maxP
;
first
by
done
.
intros
y
Py
MAXy
.
apply
/
andP
;
split
;
first
by
done
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MAXy
.
by
apply
/
forallP
;
intros
y0
;
apply
/
implyP
;
intros
Py0
;
apply
MAXy
.
}
Qed
.
End
Maximum
.
End
PickMax
.
Section
Predicate
.
Variable
n
:
nat
.
Variable
p
:
pred
nat
.
Hypothesis
EX
:
exists
x
,
x
<
n
/\
p
x
.
(* Here we prove that pick_any satiesfies the predicate p, ... *)
Lemma
pick_any_pred
:
p
(
pick_any
n
p
).
Proof
.
by
apply
pick_any_holds
.
Qed
.
(* ...and the same holds for pick_min... *)
Lemma
pick_min_pred
:
p
(
pick_min
n
p
).
Proof
.
by
apply
pick_min_holds
.
Qed
.
(* ...and pick_max. *)
Lemma
pick_max_pred
:
p
(
pick_max
n
p
).
Proof
.
by
apply
pick_max_holds
.
Qed
.
End
Predicate
.
Section
PickMinCompare
.
Variable
n
:
nat
.
Variable
p1
p2
:
pred
nat
.
Hypothesis
EX1
:
exists
x
,
x
<
n
/\
p1
x
.
Hypothesis
EX2
:
exists
x
,
x
<
n
/\
p2
x
.
Hypothesis
OUT
:
forall
x
y
,
x
<
n
>
y
<
n
>
p1
x
>
p2
y
>
~~
p1
y
>
x
<=
y
.
Lemma
pick_min_compare
:
pick_min
n
p1
<=
pick_min
n
p2
.
Proof
.
set
m1
:
=
pick_min
_
_
.
set
m2
:
=
pick_min
_
_
.
case
IN
:
(
p1
m2
).
{
apply
pick_min_holds
;
first
by
done
.
intros
x
Px
LTN
ALL
.
by
apply
ALL
;
first
by
apply
pick_min_ltn
.
}
{
apply
(
OUT
m1
m2
).

by
apply
pick_min_ltn
.

by
apply
pick_min_ltn
.

by
apply
pick_min_pred
.

by
apply
pick_min_pred
.

by
apply
negbT
.
}
Qed
.
End
PickMax
.
\ No newline at end of file
End
PickMinCompare
.
\ No newline at end of file
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment