From 9bd265d8851f5b0675fffd2480d5f590c18946de Mon Sep 17 00:00:00 2001
From: Vedant Chavda <f20180209@goa.bits-pilani.ac.in>
Date: Mon, 11 May 2020 15:11:44 +0200
Subject: [PATCH] resolve warnings related to eq_big_perm
change it to perm_big
---
classic/analysis/apa/interference_bound_edf.v | 4 ++--
classic/analysis/apa/workload_bound.v | 4 ++--
classic/analysis/global/basic/interference_bound_edf.v | 4 ++--
classic/analysis/global/basic/workload_bound.v | 4 ++--
classic/analysis/global/jitter/interference_bound_edf.v | 4 ++--
classic/analysis/global/jitter/workload_bound.v | 4 ++--
classic/analysis/global/parallel/interference_bound_edf.v | 4 ++--
classic/analysis/global/parallel/workload_bound.v | 4 ++--
8 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/classic/analysis/apa/interference_bound_edf.v b/classic/analysis/apa/interference_bound_edf.v
index bb672002a..0abd7cae5 100644
--- a/classic/analysis/apa/interference_bound_edf.v
+++ b/classic/analysis/apa/interference_bound_edf.v
@@ -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, ... *)
diff --git a/classic/analysis/apa/workload_bound.v b/classic/analysis/apa/workload_bound.v
index 1bb0671cf..35be6eb26 100644
--- a/classic/analysis/apa/workload_bound.v
+++ b/classic/analysis/apa/workload_bound.v
@@ -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
diff --git a/classic/analysis/global/basic/interference_bound_edf.v b/classic/analysis/global/basic/interference_bound_edf.v
index af8435fbc..8956d8a19 100644
--- a/classic/analysis/global/basic/interference_bound_edf.v
+++ b/classic/analysis/global/basic/interference_bound_edf.v
@@ -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, ... *)
diff --git a/classic/analysis/global/basic/workload_bound.v b/classic/analysis/global/basic/workload_bound.v
index cb3ce2214..833da3148 100644
--- a/classic/analysis/global/basic/workload_bound.v
+++ b/classic/analysis/global/basic/workload_bound.v
@@ -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
diff --git a/classic/analysis/global/jitter/interference_bound_edf.v b/classic/analysis/global/jitter/interference_bound_edf.v
index 110377974..a279e9f62 100644
--- a/classic/analysis/global/jitter/interference_bound_edf.v
+++ b/classic/analysis/global/jitter/interference_bound_edf.v
@@ -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, ... *)
diff --git a/classic/analysis/global/jitter/workload_bound.v b/classic/analysis/global/jitter/workload_bound.v
index 24a40fc2c..2e7309f0b 100644
--- a/classic/analysis/global/jitter/workload_bound.v
+++ b/classic/analysis/global/jitter/workload_bound.v
@@ -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
diff --git a/classic/analysis/global/parallel/interference_bound_edf.v b/classic/analysis/global/parallel/interference_bound_edf.v
index 1d02f843a..a20bc4299 100644
--- a/classic/analysis/global/parallel/interference_bound_edf.v
+++ b/classic/analysis/global/parallel/interference_bound_edf.v
@@ -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, ... *)
diff --git a/classic/analysis/global/parallel/workload_bound.v b/classic/analysis/global/parallel/workload_bound.v
index c85aa7918..9dd7fa8e2 100644
--- a/classic/analysis/global/parallel/workload_bound.v
+++ b/classic/analysis/global/parallel/workload_bound.v
@@ -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
--
GitLab