Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
6cb786f2
Commit
6cb786f2
authored
Dec 02, 2019
by
Sergey Bozhko
Committed by
Björn Brandenburg
Dec 10, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
address spellchecking issues in util
parent
fbcbb997
Changes
9
Show whitespace changes
Inline
Sidebyside
Showing
9 changed files
with
71 additions
and
72 deletions
+71
72
util/epsilon.v
util/epsilon.v
+1
1
util/list.v
util/list.v
+15
16
util/nat.v
util/nat.v
+8
8
util/nondecreasing.v
util/nondecreasing.v
+22
22
util/rewrite_facilities.v
util/rewrite_facilities.v
+12
12
util/search_arg.v
util/search_arg.v
+7
7
util/seqset.v
util/seqset.v
+1
1
util/sum.v
util/sum.v
+3
3
util/tactics.v
util/tactics.v
+2
2
No files found.
util/epsilon.v
View file @
6cb786f2
Section
Epsilon
.
(*
ε
is defined as the smallest positive number. *)
(*
[ε]
is defined as the smallest positive number. *)
Definition
ε
:
=
1
.
End
Epsilon
.
\ No newline at end of file
util/list.v
View file @
6cb786f2
...
...
@@ 43,7 +43,7 @@ Section Last0.
Proof
.
by
intros
;
rewrite
nth_last
.
Qed
.
(** We prove that for any nonempty sequence [xs] there is a sequence [xsh]
such that [xsh ++ [::last0 x] =
xs
]. *)
such that [xsh ++ [::last0 x] =
[xs]
]. *)
Lemma
last0_ex_cat
:
forall
x
xs
,
xs
<>
[
::
]
>
...
...
@@ 81,7 +81,7 @@ End Last0.
(** Additional lemmas about max0. *)
Section
Max0
.
(** We prove that
max0 (x::xs) is equal to max {x, max0 xs}
. *)
(** We prove that
[max0 (x::xs)] is equal to [max {x, max0 xs}]
. *)
Lemma
max0_cons
:
forall
x
xs
,
max0
(
x
::
xs
)
=
maxn
x
(
max0
xs
).
Proof
.
have
L
:
forall
s
x
xs
,
foldl
maxn
s
(
x
::
xs
)
=
maxn
x
(
foldl
maxn
s
xs
).
...
...
@@ 206,9 +206,9 @@ Section Max0.
(** Let's introduce the notion of the nth element of a sequence. *)
Notation
"xs [ n ]"
:
=
(
nth
0
xs
n
)
(
at
level
30
).
(** If any
n'th element of a sequence xs
is lessthanorequalto
n'th element of ys, then max of xs is lessthanorequalto max
of ys
. *)
(** If any
element of a sequence [xs]
is lessthanorequalto
the corresponding element of a sequence [ys], then max of
[xs] is lessthanorequalto max of [ys]
. *)
Lemma
max_of_dominating_seq
:
forall
(
xs
ys
:
seq
nat
),
(
forall
n
,
xs
[
n
]
<=
ys
[
n
])
>
...
...
@@ 254,7 +254,7 @@ End Max0.
(* Additional lemmas about rem for lists. *)
Section
RemList
.
(* We prove that if
x lies in xs excluding y, then x also lies in xs
. *)
(* We prove that if
[x] lies in [xs] excluding [y], then [x] also lies in [xs]
. *)
Lemma
rem_in
:
forall
(
T
:
eqType
)
(
x
y
:
T
)
(
xs
:
seq
T
),
x
\
in
rem
y
xs
>
x
\
in
xs
.
...
...
@@ 272,8 +272,8 @@ Section RemList.
}
Qed
.
(* We prove that if we remove an element
x for which P x
from
a filter, then the size of the filter decreases by
1
. *)
(* We prove that if we remove an element
[x] for which [P x]
from
a filter, then the size of the filter decreases by
[1]
. *)
Lemma
filter_size_rem
:
forall
(
T
:
eqType
)
(
x
:
T
)
(
xs
:
seq
T
)
(
P
:
T
>
bool
),
(
x
\
in
xs
)
>
...
...
@@ 300,8 +300,7 @@ End RemList.
(* Additional lemmas about sequences. *)
Section
AdditionalLemmas
.
(* First, we show that if [n > 0], then [n]'th element of a sequence
[x::xs] is equal to [n1]'th element of sequence [xs]. *)
(* First, we show that if [n > 0], then [nth (x::xs) n = nth xs (n1)]. *)
Lemma
nth0_cons
:
forall
x
xs
n
,
n
>
0
>
...
...
@@ 332,8 +331,8 @@ Section AdditionalLemmas.
by
apply
eq_S
.
Qed
.
(* Next, we prove that
x ∈ xs implies that xs
can be split
into two parts such that
xs = xsl ++ [::x] ++ xsr
. *)
(* Next, we prove that
[x ∈ xs] implies that [xs]
can be split
into two parts such that
[xs = xsl ++ [::x] ++ [xsr]]
. *)
Lemma
in_cat
:
forall
{
X
:
eqType
}
(
x
:
X
)
(
xs
:
list
X
),
x
\
in
xs
>
exists
xsl
xsr
,
xs
=
xsl
++
[
::
x
]
++
xsr
.
...
...
@@ 347,8 +346,8 @@ Section AdditionalLemmas.
by
subst
;
exists
(
a
::
xsl
),
xsr
.
Qed
.
(* We prove that for any two sequences
xs and ys the fact that xs is a sub
sequence
of
ys implies that the size of xs is at most the size of ys
. *)
(* We prove that for any two sequences
[xs] and [ys] the fact that [xs] is a sub
sequence
of
[ys] implies that the size of [xs] is at most the size of [ys]
. *)
Lemma
subseq_leq_size
:
forall
{
X
:
eqType
}
(
xs
ys
:
seq
X
),
uniq
xs
>
...
...
@@ 413,7 +412,7 @@ Section AdditionalLemmas.
End
AdditionalLemmas
.
(** Function [rem] from
ssreflect
removes only the first occurrence of
(** Function [rem] from
[ssreflect]
removes only the first occurrence of
an element in a sequence. We define function [rem_all] which
removes all occurrences of an element in a sequence. *)
Fixpoint
rem_all
{
X
:
eqType
}
(
x
:
X
)
(
xs
:
seq
X
)
:
=
...
...
@@ 423,7 +422,7 @@ Fixpoint rem_all {X : eqType} (x : X) (xs : seq X) :=
if
a
==
x
then
rem_all
x
xs
else
a
::
rem_all
x
xs
end
.
(** Additional lemmas about
rem_all
for lists. *)
(** Additional lemmas about
[rem_all]
for lists. *)
Section
RemAllList
.
(** First we prove that [x ∉ rem_all x xs]. *)
...
...
util/nat.v
View file @
6cb786f2
...
...
@@ 30,7 +30,7 @@ Section NatLemmas.

by
apply
leq_trans
with
(
m
+
p
)
;
first
rewrite
leq_addl
.
Qed
.
(* Simplify
n + a  b + b  a = n if n >= b
. *)
(* Simplify
[n + a  b + b  a = n] if [n >= b]
. *)
Lemma
subn_abba
:
forall
n
a
b
,
n
>=
b
>
...
...
@@ 97,20 +97,20 @@ End Interval.
Section
NatOrderLemmas
.
(* Mimic the way implicit arguments are used in
ssreflect
. *)
(* Mimic the way implicit arguments are used in
[ssreflect]
. *)
Set
Implicit
Arguments
.
Unset
Strict
Implicit
.
(*
ltn_leq_trans: Establish that m < p if m < n and n <= p
, to mirror the
lemma
leq_ltn_trans in ssrnat
.
(*
[ltn_leq_trans]: Establish that [m < p] if [m < n] and [n <= p]
, to mirror the
lemma
[leq_ltn_trans] in [ssrnat]
.
NB: There is a good reason for this lemma to be "missing" in
ssrnat

since
m < n is defined as m.+1 <= n, ltn_leq_trans
is just
m.+1 <= n > n <= p > m.+1 <= p, that is (@leq_trans n m.+1 p)
.
NB: There is a good reason for this lemma to be "missing" in
[ssrnat]

since
[m < n] is defined as [m.+1 <= n], [ltn_leq_trans]
is just
[m.+1 <= n > n <= p > m.+1 <= p], that is [@leq_trans n m.+1 p]
.
Nonetheless we introduce it here because an additional (even though
arguably redundant) lemma doesn't hurt, and for newcomers the apparent
absence of the mirror case of
leq_ltn_trans
can be somewhat confusing. *)
absence of the mirror case of
[leq_ltn_trans]
can be somewhat confusing. *)
Lemma
ltn_leq_trans
n
m
p
:
m
<
n
>
n
<=
p
>
m
<
p
.
Proof
.
exact
(@
leq_trans
n
m
.+
1
p
).
Qed
.
...
...
util/nondecreasing.v
View file @
6cb786f2
...
...
@@ 13,8 +13,8 @@ Section NondecreasingSequence.
(** In this section we provide the notion of a nondecreasing sequence. *)
Section
Definitions
.
(** We say that a sequence
xs is nondecincreasing iff for any two indices n1 and n2
such that [n1 <= n2 < size
xs] condition [xs[n1] <= xs
[n2]] holds. *)
(** We say that a sequence
[xs] is nondecreasing iff for any two indices [n1] and [n2]
such that [n1 <= n2 < size
[xs]] condition [[xs][n1] <= [xs]
[n2]] holds. *)
Definition
nondecreasing_sequence
(
xs
:
seq
nat
)
:
=
forall
n1
n2
,
n1
<=
n2
<
size
xs
>
...
...
@@ 29,7 +29,7 @@ Section NondecreasingSequence.
(** For a nondecreasing sequence we define the notion of
distances between neighboring elements of the sequence. *)
(** Example:
Consider the following sequence of natural numbers:
xs
= [:: 1; 10; 10; 17; 20; 41].
Consider the following sequence of natural numbers:
[xs]
= [:: 1; 10; 10; 17; 20; 41].
Then [drop 1 xs] is equal to [:: 10; 10; 17; 20; 41].
Then [zip xs (drop 1 xs)] is equal to [:: (1,10); (10,10); (10,17); (17,20); (20,41)]
And after the mapping [map (fun '(x1, x2) => x2  x1)] we end up with [:: 9; 0; 7; 3; 21]. *)
...
...
@@ 254,8 +254,8 @@ Section NondecreasingSequence.
Qed
.
(** Alternatively, consider an arbitrary natural number x that is
bounded by the first and the last element of a sequence
xs
. Then
there is an index n such that
xs[n] <= x < x[n+1
]. *)
bounded by the first and the last element of a sequence
[xs]
. Then
there is an index n such that
[xs[n] <= x < x[n+1]
]. *)
Lemma
belonging_to_segment_of_seq_is_total
:
forall
(
xs
:
seq
nat
)
(
x
:
nat
),
2
<=
size
xs
>
...
...
@@ 293,7 +293,7 @@ Section NondecreasingSequence.
}
Qed
.
(** Note that the last element of a nondecreasing sequence is the max element. *)
(** Note that the last element of a non

decreasing sequence is the max element. *)
Lemma
last_is_max_in_nondecreasing_seq
:
forall
(
xs
:
seq
nat
)
(
x
:
nat
),
nondecreasing_sequence
xs
>
...
...
@@ 324,8 +324,8 @@ Section NondecreasingSequence.
End
NonDecreasingSequence
.
(** * Properties of
Undup
of NonDecreasing Sequence *)
(** In this section we prove a few lemmas about
undup
of nondecreasing sequences. *)
(** * Properties of
[Undup]
of NonDecreasing Sequence *)
(** In this section we prove a few lemmas about
[undup]
of nondecreasing sequences. *)
Section
Undup
.
(** First we prove that [undup x::x::xs] is equal to [undup x::xs]. *)
...
...
@@ 443,7 +443,7 @@ Section NondecreasingSequence.
(** In this section we prove a few lemmas about function [distances]. *)
Section
Distances
.
(** We begin
g
with a simple lemma that helps us unfold [distances]
(** We begin with a simple lemma that helps us unfold [distances]
of lists with two consecutive cons [x0::x1::xs]. *)
Lemma
distances_unfold_2cons
:
forall
x0
x1
xs
,
...
...
@@ 546,8 +546,8 @@ Section NondecreasingSequence.
Qed
.
(** Note that the distancesfunction has the expected behavior indeed. I.e. an element
on the
nth position
of the distancesequence is equal to the difference between
n+1th and nth elements
. *)
on the
position [n]
of the distancesequence is equal to the difference between
elements on positions [n+1] and [n]
. *)
Lemma
function_of_distances_is_correct
:
forall
(
xs
:
seq
nat
)
(
n
:
nat
),
(
distances
xs
)[
n
]
=
xs
[
n
.+
1
]

xs
[
n
].
...
...
@@ 689,9 +689,9 @@ Section NondecreasingSequence.

eapply
L
with
(
indx
:
=
indy
)
(
indy
:
=
indx
)
(
x
:
=
y
)
(
y
:
=
x
)
;
eauto
.
Qed
.
(** Given a non
decreasing sequence xs
with length n, we show that the difference
between the last element of
xs
and the last element of the distancessequence
of
xs is equal to the (n2)'th element of xs
. *)
(** Given a non
decreasing sequence [xs]
with length n, we show that the difference
between the last element of
[xs]
and the last element of the distancessequence
of
[xs] is equal to [xs[n2]]
. *)
Lemma
last_seq_minus_last_distance_seq
:
forall
(
xs
:
seq
nat
),
nondecreasing_sequence
xs
>
...
...
@@ 718,8 +718,8 @@ Section NondecreasingSequence.
by
rewrite
addn1
.
Qed
.
(** The max element of the distancessequence of a sequence
xs
is bounded
by the last element of
xs. Note that all elements of xs
are positive.
(** The max element of the distancessequence of a sequence
[xs]
is bounded
by the last element of
[xs]. Note that all elements of [xs]
are positive.
Thus they all lie within the interval [0, last xs]. *)
Lemma
max_distance_in_seq_le_last_element_of_seq
:
forall
(
xs
:
seq
nat
),
...
...
@@ 765,7 +765,7 @@ Section NondecreasingSequence.
}
Qed
.
(** Let
xs
be a nondecreasing sequence. We prove that
(** Let
[xs]
be a nondecreasing sequence. We prove that
distances of sequence [[seq ρ < index_iota 0 k.+1  ρ \in xs]]
coincide with sequence [[seq x < distances xs  0 < x]]]. *)
Lemma
distances_iota_filtered
:
...
...
@@ 810,7 +810,7 @@ Section NondecreasingSequence.
}
Qed
.
(** Let
xs
again be a nondecreasing sequence. We prove that
(** Let
[xs]
again be a nondecreasing sequence. We prove that
distances of sequence [undup xs] coincide with
sequence of positive distances of [xs]. *)
Lemma
distances_positive_undup
:
...
...
@@ 847,10 +847,10 @@ Section NondecreasingSequence.
Qed
.
(** Consider two non
decreasing sequences xs and ys
and assume that
(1) first element of
xs is at most the first element of ys
and
(2) distancessequences of
xs
is dominated by distancessequence of
ys. Then xs is dominated by ys
. *)
(** Consider two non
decreasing sequences [xs] and [ys]
and assume that
(1) first element of
[xs] is at most the first element of [ys]
and
(2) distancessequences of
[xs]
is dominated by distancessequence of
[ys]. Then [xs] is dominated by [ys]
. *)
Lemma
domination_of_distances_implies_domination_of_seq
:
forall
(
xs
ys
:
seq
nat
),
first0
xs
<=
first0
ys
>
...
...
util/rewrite_facilities.v
View file @
6cb786f2
...
...
@@ 78,27 +78,27 @@ Section RewriteFacilities.
(*
(* Simplifying some relatively sophisticated
expressions can be quite tedious. *)
Goal f ((a == b) && f false) = f false.
Proof.
(* Things like
simpl/compute
make no sense here. *)
[Goal f ((a == b) && f false) = f false.]
[Proof.]
(* Things like
[simpl/compute]
make no sense here. *)
(* One can use [replace] to generate a new goal. *)
replace (a == b) with false; last first.
[replace (a == b) with false; last first.]
(* However, this leads to a "loss of focus". Moreover,
the resulting goal is not so trivial to prove. *)
{ apply/eqP; rewrite eq_sym eqbF_neg.
by apply/eqP; intros EQ; subst b; apply H_npb. }
by rewrite Bool.andb_false_l.
Abort.
[{ apply/eqP; rewrite eq_sym eqbF_neg.]
[ by apply/eqP; intros EQ; subst b; apply H_npb. }]
[ by rewrite Bool.andb_false_l.]
[Abort.]
*)
(*
(* The second attempt. *)
Goal f ((a == b) && f false) = f false.
[Goal f ((a == b) && f false) = f false.]
(* With the lemmas above one can compose multiple
transformations in a single rewrite. *)
by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))
Bool.andb_false_l.
Qed.
[ by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))]
[ Bool.andb_false_l.]
[Qed.]
*)
End
Example
.
...
...
util/search_arg.v
View file @
6cb786f2
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
fintype
.
Require
Import
rt
.
util
.
tactics
.
(** This file introduces a function called
search_arg
that allows finding the
(** This file introduces a function called
[search_arg]
that allows finding the
argument within a given range for which a function is minimal w.r.t. to a
given order while satisfying a given predicate, along with lemmas
establishing the basic properties of
search_arg
.
establishing the basic properties of
[search_arg]
.
Note that while this is quite similar to [arg min ...] / [arg max ...] in
ssreflect (fintype
), this function is subtly different in that it possibly
[ssreflect] ([fintype]
), this function is subtly different in that it possibly
returns None and that it does not require the last element in the given
range to satisfy the predicate. In contrast,
ssreflect
's notion of
extremum in
fintype
uses the upper bound of the search space as the
range to satisfy the predicate. In contrast,
[ssreflect]
's notion of
extremum in
[fintype]
uses the upper bound of the search space as the
default value, which is rather unnatural when searching through a schedule.
*)
...
...
@@ 42,7 +42,7 @@ Section ArgSearch.
(** In the following, we establish basic properties of [search_arg]. *)
(* To begin, we observe that the search yields
None
iff predicate [P] does
(* To begin, we observe that the search yields
[None]
iff predicate [P] does
not hold for any of the points in the search interval. *)
Lemma
search_arg_none
:
forall
a
b
,
...
...
@@ 151,7 +151,7 @@ Section ArgSearch.
Hypothesis
R_total
:
total
R
.
(* ...then [search_arg] yields an extremum w.r.t. to [a, b), that is, if
[search_arg] yields a point x, then [R (f x) (f y)] holds for any
y
in the
[search_arg] yields a point x, then [R (f x) (f y)] holds for any
[y]
in the
search range [a, b) that satisfies [P]. *)
Lemma
search_arg_extremum
:
forall
a
b
x
,
...
...
util/seqset.v
View file @
6cb786f2
...
...
@@ 12,7 +12,7 @@ Section SeqSet.
_
:
uniq
_set_seq
(* no duplicates *)
}.
(* Now we add the
ssreflect
boilerplate code. *)
(* Now we add the
[ssreflect]
boilerplate code. *)
Canonical
Structure
setSubType
:
=
[
subType
for
_set_seq
].
Definition
set_eqMixin
:
=
[
eqMixin
of
set
by
<
:
].
Canonical
Structure
set_eqType
:
=
EqType
set
set_eqMixin
.
...
...
util/sum.v
View file @
6cb786f2
...
...
@@ 107,7 +107,7 @@ Section ExtraLemmas.
by
apply
sum0
.
Qed
.
(* We prove that if any element of a set r is bounded by constant
const
,
(* We prove that if any element of a set r is bounded by constant
[const]
,
then the sum of the whole set is bounded by [const * size r]. *)
Lemma
sum_majorant_constant
:
forall
(
T
:
eqType
)
(
r
:
seq
T
)
(
P
:
pred
T
)
F
const
,
...
...
@@ 138,10 +138,10 @@ Section ExtraLemmas.
}
Qed
.
(* We prove that if for any element x of a set
xs
the following two statements hold
(* We prove that if for any element x of a set
[xs]
the following two statements hold
(1) [F1 x] is less than or equal to [F2 x] and (2) the sum [F1 x_1, ..., F1 x_n]
is equal to the sum of [F2 x_1, ..., F2 x_n], then [F1 x] is equal to [F2 x] for
any element x of
xs
. *)
any element x of
[xs]
. *)
Lemma
sum_majorant_eqn
:
forall
(
T
:
eqType
)
xs
F1
F2
(
P
:
pred
T
),
(
forall
x
,
x
\
in
xs
>
P
x
>
F1
x
<=
F2
x
)
>
...
...
util/tactics.v
View file @
6cb786f2
From
mathcomp
Require
Import
ssreflect
ssrbool
ssrnat
eqtype
bigop
.
(** Lemmas & tactics adopted (with permission) from
V. Vafeiadis' Vbase.v
. *)
(** Lemmas & tactics adopted (with permission) from
[V. Vafeiadis' Vbase.v]
. *)
Lemma
neqP
:
forall
(
T
:
eqType
)
(
x
y
:
T
),
reflect
(
x
<>
y
)
(
x
!=
y
).
Proof
.
intros
;
case
eqP
;
constructor
;
auto
.
Qed
.
...
...
@@ 11,7 +11,7 @@ Ltac ins := simpl in *; try done; intros.
(** ** Exploiting a hypothesis *)
(* ************************************************************************** *)
(** Exploit an assumption (adapted from
CompCert
). *)
(** Exploit an assumption (adapted from
[CompCert]
). *)
Ltac
exploit
x
:
=
refine
((
fun
x
y
=>
y
x
)
(
x
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
)
_
)
...
...
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