Commit 9bd265d8 authored by Vedant Chavda's avatar Vedant Chavda Committed by Björn Brandenburg

resolve warnings related to eq_big_perm

change it to perm_big
parent b1459e3c
......@@ -274,7 +274,7 @@ Module InterferenceBoundEDF.
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
(* Note that both sequences have the same set of elements. *)
......@@ -282,7 +282,7 @@ Module InterferenceBoundEDF.
forall j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
......
......@@ -231,7 +231,7 @@ Module WorkloadBound.
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (eq_big_perm sorted_jobs) /= //.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
......@@ -240,7 +240,7 @@ Module WorkloadBound.
forall j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Remember that all jobs in the sorted sequence is an
......
......@@ -260,7 +260,7 @@ Module InterferenceBoundEDF.
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
(* Note that both sequences have the same set of elements. *)
......@@ -268,7 +268,7 @@ Module InterferenceBoundEDF.
forall j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
......
......@@ -234,7 +234,7 @@ Module WorkloadBound.
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (eq_big_perm sorted_jobs) /= //.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
......@@ -243,7 +243,7 @@ Module WorkloadBound.
forall j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Remember that all jobs in the sorted sequence is an
......
......@@ -271,7 +271,7 @@ Module InterferenceBoundEDFJitter.
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
(* Note that both sequences have the same set of elements. *)
......@@ -279,7 +279,7 @@ Module InterferenceBoundEDFJitter.
forall j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
......
......@@ -241,7 +241,7 @@ Module WorkloadBoundJitter.
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (eq_big_perm sorted_jobs) /= //.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
......@@ -250,7 +250,7 @@ Module WorkloadBoundJitter.
forall j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Remember that all jobs in the sorted sequence is an
......
......@@ -286,7 +286,7 @@ Module InterferenceBoundEDF.
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
(* Note that both sequences have the same set of elements. *)
......@@ -294,7 +294,7 @@ Module InterferenceBoundEDF.
forall j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
......
......@@ -169,7 +169,7 @@ Module WorkloadBound.
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (eq_big_perm sorted_jobs) /= //.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
......@@ -178,7 +178,7 @@ Module WorkloadBound.
forall j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
(* Remember that all jobs in the sorted sequence is an
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment