Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
RTPROOFS
PROSA  Formally Proven Schedulability Analysis
Commits
4d5282fa
Commit
4d5282fa
authored
Apr 08, 2022
by
Björn Brandenburg
Browse files
protect TODO comments from spell checker
parent
165a18f2
Pipeline
#69077
passed with stage
in 18 minutes and 16 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
util/sum.v
View file @
4d5282fa
...
...
@@ 35,8 +35,8 @@ Section SumsOverSequences.
(** We start showing that having every member of [r] equal to zero is equivalent to
having the sum of all the elements of [r] equal to zero, and viceversa. *)
(* TODO: PR MathComp
this should probably be named sum_nat_eq0,
but there is already a sum_nat_eq0 that is less generic? *)
this should probably be named
[
sum_nat_eq0
]
,
but there is already a
[
sum_nat_eq0
]
that is less generic? *)
Lemma
sum_nat_eq0_nat
:
(
\
sum_
(
i
<
r

P
i
)
F
i
==
0
)
=
all
(
fun
x
=>
F
x
==
0
)
[
seq
x
<
r

P
x
].
Proof
.
...
...
@@ 90,7 +90,7 @@ Section SumsOverSequences.
guarantee that the set inclusion [r <= rs] implies the actually
required multiset inclusion. *)
(* TODO: PR MathComp
 add a condition P i *)
 add a condition
[
P i
]
*)
Lemma
leq_sum_sub_uniq
(
rs
:
seq
I
)
:
uniq
r
>
{
subset
r
<=
rs
}
>
\
sum_
(
i
<
r
)
F
i
<=
\
sum_
(
i
<
rs
)
F
i
.
...
...
@@ 132,7 +132,7 @@ Section SumsOverSequences.
(** In the same way, if [E1] equals [E2] in all the points considered above, then also the two
sums will be identical. *)
(* TODO: PR MathComp
 generalize as eq_big_seq_cond (nothing specific to addn here)
 generalize as
[
eq_big_seq_cond
]
(nothing specific to
[
addn
]
here)
 replace == with = ? *)
Lemma
eq_sum_seq
:
(
forall
i
,
i
\
in
r
>
P
i
>
E1
i
==
E2
i
)
>
...
...
@@ 147,7 +147,7 @@ Section SumsOverSequences.
points, then the sum of [E] conditioned by [P2] will dominate
the sum of [E] conditioned by [P1]. *)
(* TODO: PR MathComp
 maybe leq_sum_seq above should be leq_sum_seqr and this one leq_sum_seql *)
 maybe
[
leq_sum_seq
]
above should be
[
leq_sum_seqr
]
and this one
[
leq_sum_seql
]
*)
Lemma
leq_sum_seq_pred
:
(
forall
i
,
i
\
in
r
>
P1
i
>
P2
i
)
>
\
sum_
(
i
<
r

P1
i
)
E
i
<=
\
sum_
(
i
<
r

P2
i
)
E
i
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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