From bc38ff74ee56e08cf8c467900bcf878cdc4ba459 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Wed, 8 Sep 2021 18:07:18 +0200
Subject: [PATCH] remove [util.counting.v] lemma [count_filter_fun] is
equivalent to ssreflect's [size_filter]
---
analysis/abstract/abstract_seq_rta.v | 2 +-
.../uni/limited/abstract_RTA/abstract_seq_rta.v | 4 ++--
classic/util/counting.v | 4 +---
util/all.v | 1 -
util/counting.v | 15 ---------------
5 files changed, 4 insertions(+), 22 deletions(-)
delete mode 100644 util/counting.v
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index e652e58b7..196493031 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -585,7 +585,7 @@ Section Sequential_Abstract_RTA.
{ by move: ARR => [t ARR]; rewrite subnKC //; feed (H_arrival_times_are_consistent j t); try (subst t). }
have Fact1: 1 <= number_of_task_arrivals arr_seq tsk (t1 + A) (t1 + A + ε).
{ rewrite /number_of_task_arrivals /task_arrivals_between /arrival_sequence.arrivals_between.
- by rewrite -count_filter_fun -has_count; apply/hasP; exists j; last rewrite TSK.
+ by rewrite size_filter -has_count; apply/hasP; exists j; last rewrite TSK.
}
rewrite (@num_arrivals_of_task_cat _ _ _ _ _ (t1 + A)); last by apply/andP; split; rewrite leq_addr //.
rewrite mulnDr.
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index 12041b462..d0bd64b51 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -494,7 +494,7 @@ Module AbstractSeqRTA.
}
have Fact1: num_arrivals_of_task job_task arr_seq tsk (t1 + A) (t1 + A + ε) >= 1.
{ rewrite /num_arrivals_of_task /arrivals_of_task_between.
- rewrite -count_filter_fun -has_count; apply/hasP.
+ rewrite size_filter -has_count; apply/hasP.
by exists j; last rewrite /is_job_of_task TSK.
}
have Fact2: job_cost j <= task_workload_between (t1 + A) (t1 + A + ε).
@@ -636,4 +636,4 @@ Module AbstractSeqRTA.
End Sequential_Abstract_RTA.
End AbstractSeqRTA.
-
\ No newline at end of file
+
diff --git a/classic/util/counting.v b/classic/util/counting.v
index d4e23a53d..03f4b6251 100644
--- a/classic/util/counting.v
+++ b/classic/util/counting.v
@@ -1,5 +1,3 @@
-Require Export prosa.util.counting.
-
Require Import prosa.classic.util.tactics prosa.classic.util.ord_quantifier.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
@@ -103,4 +101,4 @@ Section Counting.
}
Qed.
-End Counting.
\ No newline at end of file
+End Counting.
diff --git a/util/all.v b/util/all.v
index cdc1a9d95..20dc35795 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,7 +1,6 @@
Require Export prosa.util.tactics.
Require Export prosa.util.notation.
Require Export prosa.util.bigcat.
-Require Export prosa.util.counting.
Require Export prosa.util.div_mod.
Require Export prosa.util.list.
Require Export prosa.util.nat.
diff --git a/util/counting.v b/util/counting.v
deleted file mode 100644
index 0fec37401..000000000
--- a/util/counting.v
+++ /dev/null
@@ -1,15 +0,0 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
-(* Additional lemmas about counting. *)
-Section Counting.
-
- Lemma count_filter_fun :
- forall (T: eqType) (l: seq T) P,
- count P l = size (filter P l).
- Proof.
- intros T l P.
- induction l; simpl; first by done.
- by destruct (P a); [by rewrite add1n /=; f_equal | by rewrite add0n].
- Qed.
-
-End Counting.
\ No newline at end of file
--
GitLab