From 4ee47809d19e46a547d6738ed744c13bc4186dc5 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 13 Sep 2021 12:24:35 +0200
Subject: [PATCH] clean up util/minmax.v
---
.../edf/nonpr_reg/response_time_bound.v | 2 +-
.../nonpr_reg/response_time_bound.v | 4 +-
results/edf/rta/bounded_nps.v | 2 +-
results/fixed_priority/rta/bounded_nps.v | 2 +-
util/minmax.v | 175 ++++++++----------
5 files changed, 86 insertions(+), 99 deletions(-)
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index b595a2b20..38ac2964c 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -194,7 +194,7 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
{ apply /bigmax_leq_seqP.
intros j' JINB NOTHEP.
apply leq_bigmax_cond_seq with
- (i0 := (job_task j')) (F := fun tsk => task_max_nps tsk - 1).
+ (x := (job_task j')) (F := fun tsk => task_max_nps tsk - 1).
{ apply H_all_jobs_from_taskset.
apply mem_bigcat_nat_exists in JINB.
by inversion JINB as [ta' [JIN' _]]; exists ta'. }
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index c6ab4c026..db018f269 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -179,7 +179,7 @@ Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
{ apply /bigmax_leq_seqP.
intros j' JINB NOTHEP.
apply leq_bigmax_cond_seq with
- (i0 := (job_task j')) (F := fun tsk => task_max_nps tsk - 1); last by done.
+ (x := (job_task j')) (F := fun tsk => task_max_nps tsk - 1); last by done.
apply H_all_jobs_from_taskset.
apply mem_bigcat_nat_exists in JINB.
by inversion JINB as [ta' [JIN' _]]; exists ta'.
@@ -289,4 +289,4 @@ Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
End Analysis.
-End RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
\ No newline at end of file
+End RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 2423eacc1..ae2a10202 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -175,7 +175,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
by apply H_valid_model_with_bounded_nonpreemptive_segments.
- apply /bigmax_leq_seqP.
intros j' JINB NOTHEP.
- apply leq_bigmax_cond_seq with (i0 := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1).
+ apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1).
{ apply H_all_jobs_from_taskset.
apply mem_bigcat_nat_exists in JINB.
by inversion JINB as [ta' [JIN' _]]; exists ta'. }
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 1137186a3..751d7fabd 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -153,7 +153,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
{ apply /bigmax_leq_seqP.
intros j' JINB NOTHEP.
apply leq_bigmax_cond_seq with
- (i0 := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1); last by done.
+ (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1); last by done.
apply H_all_jobs_from_taskset.
apply mem_bigcat_nat_exists in JINB.
by inversion JINB as [ta' [JIN' _]]; exists ta'.
diff --git a/util/minmax.v b/util/minmax.v
index 141ed69eb..736d5cdc5 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -1,128 +1,115 @@
Require Export prosa.util.notation prosa.util.nat prosa.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-(* Additional lemmas about max. *)
+(** Additional lemmas about [BigMax]. *)
Section ExtraLemmas.
- Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
- i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
- Proof.
- intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
- Qed.
-
- Lemma bigmax_sup_seq:
- forall (T: eqType) (i: T) r (P: pred T) m F,
- i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
- Proof.
- intros.
- induction r.
- - by rewrite in_nil in H.
- move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
- {
- clear IHr; subst a.
- rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
- apply leq_trans with (F i); first by done.
- by rewrite H0 leq_maxl.
- }
- {
- apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
- rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
-
- have Ob: a == a; first by done.
- by rewrite Ob leq_maxr.
- }
- Qed.
+ (** Given a function [F], a predicate [P], and a sequence [xs], we
+ show that [F x <= max { F i | ∀ i ∈ xs, P i}] for any [x] in
+ [xs]. *)
+ Lemma leq_bigmax_cond_seq :
+ forall {X : eqType} (F : X -> nat) (P : pred X) (xs : seq X) (x : X),
+ x \in xs -> P x -> F x <= \max_(i <- xs | P i) F i.
+ Proof. by intros * IN Px; rewrite (big_rem x) //= Px leq_maxl. Qed.
- Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
- reflect (forall i, i \in r -> P i -> F i <= m)
- (\max_(i <- r | P i) F i <= m).
+ (** Next, we show that the fact [max { F i | ∀ i ∈ xs, P i} <= m] for
+ some [m] is equivalent to the fact that [∀ x ∈ xs, P x -> F x <= m]. *)
+ Lemma bigmax_leq_seqP :
+ forall {X : eqType} (F : X -> nat) (P : pred X) (xs : seq X) (m : nat),
+ reflect (forall x, x \in xs -> P x -> F x <= m)
+ (\max_(x <- xs | P x) F x <= m).
Proof.
- apply: (iffP idP) => leFm => [i IINR Pi|];
- first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
- rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
- by intros; rewrite geq_max; apply/andP; split.
- by move: m2 => /andP [M1IN Pm1]; apply: leFm.
+ intros *.
+ apply: (iffP idP) => leFm => [i IINR Pi|].
+ - by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
+ - rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
+ + by intros; rewrite geq_max; apply/andP; split.
+ + by move: m2 => /andP [M1IN Pm1]; apply: leFm.
Qed.
- Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
- (forall i, i \in r -> P i -> F1 i <= F2 i) ->
- \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
+ (** Given two functions [F1] and [F2], a predicate [P], and sequence
+ [xs], we show that if [F1 x <= F2 x] for any [x \in xs] such that
+ [P x], then [max] of [{F1 x | ∀ x ∈ xs, P x}] is bounded by the
+ [max] of [{F2 x | ∀ x ∈ xs, P x}]. *)
+ Lemma leq_big_max :
+ forall {X : eqType} (F1 F2 : X -> nat) (P : pred X) (xs : seq X),
+ (forall x, x \in xs -> P x -> F1 x <= F2 x) ->
+ \max_(x <- xs | P x) F1 x <= \max_(x <- xs | P x) F2 x.
Proof.
- intros; apply /bigmax_leq_seqP; intros.
- specialize (H i); feed_n 2 H; try(done).
- rewrite (big_rem i) //=; rewrite H1.
- by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
+ intros * ALL; apply /bigmax_leq_seqP; intros * IN Px.
+ specialize (ALL x); feed_n 2 ALL; try done.
+ rewrite (big_rem x) //=; rewrite Px.
+ by apply leq_trans with (F2 x); [ | rewrite leq_maxl].
Qed.
- Lemma bigmax_ord_ltn_identity n :
- n > 0 ->
- \max_(i < n) i < n.
+ (** We show that for a positive [n], [max] of [{0, …, n-1}] is
+ smaller than [n]. *)
+ Lemma bigmax_ord_ltn_identity :
+ forall (n : nat),
+ n > 0 ->
+ \max_(i < n) i < n.
Proof.
- intros LT.
- destruct n; first by rewrite ltn0 in LT.
- clear LT.
- induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
+ intros [ | n] POS; first by rewrite ltn0 in POS.
+ clear POS; induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
rewrite big_ord_recr /=.
- by unfold maxn at 1; rewrite IHn.
+ by rewrite /maxn IHn.
Qed.
-
- Lemma bigmax_ltn_ord n (P : pred nat) (i0: 'I_n) :
+
+ (** We state the next lemma in terms of _ordinals_. Given a natural
+ number [n], a predicate [P], and an ordinal [i0 ∈ {0, …, n-1}]
+ satisfying [P], we show that [max {i | P i} < n]. Note that the
+ element satisfying [P] is needed to prove that [{i | P i}] is
+ not empty. *)
+ Lemma bigmax_ltn_ord :
+ forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 ->
\max_(i < n | P i) i < n.
Proof.
- intros LT.
+ intros n P i0 Pi.
destruct n; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
rewrite big_mkcond.
apply leq_ltn_trans with (n := \max_(i < n.+1) i).
- {
- apply/bigmax_leqP; ins.
+ - apply/bigmax_leqP; ins.
destruct (P i); last by done.
by apply leq_bigmax_cond.
- }
- by apply bigmax_ord_ltn_identity.
+ - by apply bigmax_ord_ltn_identity.
Qed.
- Lemma bigmax_pred n (P : pred nat) (i0: 'I_n) :
- P (i0) ->
- P (\max_(i < n | P i) i).
+ (** Finally, we show that, given a natural number [n], a predicate
+ [P], and an ordinal [i0 ∈ {0, …, n-1}] satisfying [P],
+ [max {i | P i} < n] also satisfies [P]. *)
+ Lemma bigmax_pred :
+ forall (n : nat) (P : pred nat) (i0 : 'I_n),
+ P i0 ->
+ P (\max_(i < n | P i) i).
Proof.
- intros PRED.
+ intros * Pi0.
induction n.
- {
- destruct i0 as [i0 P0].
- by move: (P0) => P1; rewrite ltn0 in P1.
- }
- rewrite big_mkcond big_ord_recr /=. destruct (P n) eqn:Pn.
- {
- destruct n; first by rewrite big_ord0 maxn0.
- unfold maxn at 1.
- destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
- | true => @nat_of_ord (S n) i
- | false => O
- end) < n.+1) eqn:Pi; first by rewrite Pi.
- exfalso.
- apply negbT in Pi; move: Pi => /negP BUG.
- apply BUG.
- apply leq_ltn_trans with (n := \max_(i < n.+1) i).
- {
- apply/bigmax_leqP; ins.
- destruct (P i); last by done.
- by apply leq_bigmax_cond.
+ { by destruct i0 as [i0 P0]; move: (P0) => P1; rewrite ltn0 in P1. }
+ { rewrite big_mkcond big_ord_recr /=.
+ destruct (P n) eqn:Pn.
+ { destruct n; first by rewrite big_ord0 maxn0.
+ unfold maxn at 1.
+ destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
+ | true => @nat_of_ord (S n) i
+ | false => O
+ end) < n.+1) eqn:Pi; first by rewrite Pi.
+ exfalso.
+ apply negbT in Pi; move: Pi => /negP BUG; apply: BUG.
+ apply leq_ltn_trans with (n := \max_(i < n.+1) i).
+ { apply/bigmax_leqP; rewrite //= => i _.
+ by destruct (P i); first apply leq_bigmax_cond.
+ }
+ { by apply bigmax_ord_ltn_identity. }
}
- by apply bigmax_ord_ltn_identity.
- }
- {
- rewrite maxn0.
- rewrite -big_mkcond /=.
- have LT: i0 < n.
- {
+ { rewrite maxn0 -big_mkcond /=.
+ have LT: i0 < n; last by rewrite (IHn (Ordinal LT)).
rewrite ltn_neqAle; apply/andP; split;
last by rewrite -ltnS; apply ltn_ord.
apply/negP; move => /eqP BUG.
- by rewrite -BUG PRED in Pn.
+ by rewrite -BUG Pi0 in Pn.
}
- by rewrite (IHn (Ordinal LT)).
}
Qed.
-
-End ExtraLemmas.
\ No newline at end of file
+
+End ExtraLemmas.
--
GitLab