From 9884f13e5e144ef6688c1157cfa8e392eb592b1e Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 4 Sep 2018 17:37:08 +0200
Subject: [PATCH] Add lemmas about pick and make it easier to use
---
.../susp/dynamic/jitter/rta_by_reduction.v | 4 +-
.../susp/dynamic/jitter/taskset_membership.v | 6 +-
util/pick.v | 147 +++++++++++++-----
3 files changed, 110 insertions(+), 47 deletions(-)
diff --git a/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v b/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
index 21ebe100f..aadfaeda9 100644
--- a/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
+++ b/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
@@ -188,8 +188,8 @@ Module RTAByReduction.
{
intros j_hp ARRhp OTHERhp.
rewrite /actual_response_time.
- apply pick_min_holds; last by intros r RESP _.
- exists (Ordinal (ltnSn (R (job_task j_hp)))).
+ apply pick_min_holds; last by intros r _ RESP _.
+ exists (R (job_task j_hp)); split; first by done.
by apply RESPhp; try (by done); [by apply FROM | rewrite /other_hep_task -H_job_of_tsk].
}
{
diff --git a/analysis/uni/susp/dynamic/jitter/taskset_membership.v b/analysis/uni/susp/dynamic/jitter/taskset_membership.v
index 40a2fb460..f16e79e95 100644
--- a/analysis/uni/susp/dynamic/jitter/taskset_membership.v
+++ b/analysis/uni/susp/dynamic/jitter/taskset_membership.v
@@ -133,7 +133,7 @@ Module TaskSetMembership.
intros j_hp ARRhp HP.
rewrite /actual_response_time.
apply pick_min_holds; last by done.
- exists (Ordinal (ltnSn (R (job_task j_hp)))). simpl.
+ exists (R (job_task j_hp)); split; first by done.
by apply RESPhp; try (by done); first by apply FROM.
Qed.
@@ -153,14 +153,14 @@ Module TaskSetMembership.
rewrite /actual_response_time.
apply pick_min_holds;
last by intros x RESPx _ MINx; rewrite -ltnS in LT; apply (MINx (Ordinal LT)).
- exists (Ordinal (ltnSn (R (job_task j_hp)))).
+ exists (R (job_task j_hp)); split; first by done.
by apply RESPhp; try (by done); first by apply FROM.
}
{
apply leq_trans with (n := (R (job_task j_hp))); last by apply ltnW.
rewrite -ltnS /actual_response_time.
apply pick_min_ltn.
- exists (Ordinal (ltnSn (R (job_task j_hp)))). simpl.
+ exists (R (job_task j_hp)); split; first by done.
by apply RESPhp; try (by done); first by apply FROM.
}
Qed.
diff --git a/util/pick.v b/util/pick.v
index 3cc3a0929..dea4dcce3 100644
--- a/util/pick.v
+++ b/util/pick.v
@@ -11,17 +11,18 @@ Definition arg_pred_nat n (P: pred 'I_n) ord :=
Definition pred_min_nat n (P: pred 'I_n) := arg_pred_nat n P leq.
Definition pred_max_nat n (P: pred 'I_n) := arg_pred_nat n P (fun x y => geq x y).
+Definition to_pred_ord n (P: pred nat) := (fun x:'I_n => P (nat_of_ord x)).
(** Defining Pick functions *)
(* (pick_any n P) returns some number < n that satisfies P, or 0 if it cannot be found. *)
-Definition pick_any n (P: pred 'I_n) := default0 (pick P).
+Definition pick_any n (P: pred nat) := default0 (pick (to_pred_ord n P)).
(* (pick_min n P) returns the smallest number < n that satisfies P, or 0 if it cannot be found. *)
-Definition pick_min n (P: pred 'I_n) := default0 (pick (pred_min_nat n P)).
+Definition pick_min n (P: pred nat) := default0 (pick (pred_min_nat n (to_pred_ord n P))).
(* (pick_max n P) returns the largest number < n that satisfies P, or 0 if it cannot be found. *)
-Definition pick_max n (P: pred 'I_n) := default0 (pick (pred_max_nat n P)).
+Definition pick_max n (P: pred nat) := default0 (pick (pred_max_nat n (to_pred_ord n P))).
(** Improved notation *)
@@ -30,27 +31,27 @@ Definition pick_max n (P: pred 'I_n) := default0 (pick (pred_max_nat n P)).
[pick-min x <= N | P], [pick-min x < N | P]
[pick-max x <= N | P], [pick-max x < N | P]. *)
Notation "[ 'pick-any' x <= N | P ]" :=
- (pick_any N.+1 (fun x : 'I_N.+1 => P%B))
+ (pick_any N.+1 (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick-any' x < N | P ]" :=
- (pick_any N (fun x : 'I_N => P%B))
+ (pick_any N (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick-min' x <= N | P ]" :=
- (pick_min N.+1 (fun x : 'I_N.+1 => P%B))
+ (pick_min N.+1 (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick-min' x < N | P ]" :=
- (pick_min N (fun x : 'I_N => P%B))
+ (pick_min N (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick-max' x <= N | P ]" :=
- (pick_max N.+1 (fun x : 'I_N.+1 => P%B))
+ (pick_max N.+1 (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick-max' x < N | P ]" :=
- (pick_max N (fun x : 'I_N => P%B))
+ (pick_max N (fun x : nat => P%B))
(at level 0, x ident, only parsing) : form_scope.
(** Lemmas about pick_any *)
@@ -58,11 +59,11 @@ Notation "[ 'pick-max' x < N | P ]" :=
Section PickAny.
Variable n: nat.
- Variable p: pred 'I_n.
+ Variable p: pred nat.
Variable P: nat -> Prop.
- Hypothesis EX: exists x:'I_n, p x.
+ Hypothesis EX: exists x, x < n /\ p x.
Hypothesis HOLDS: forall x, p x -> P x.
@@ -73,8 +74,8 @@ Section PickAny.
rewrite /pick_any /default0.
case: pickP; first by intros x PRED; apply HOLDS.
intros NONE; red in NONE; exfalso.
- move: EX => [x PRED].
- by specialize (NONE x); rewrite PRED in NONE.
+ move: EX => [x [LTN PRED]].
+ by specialize (NONE (Ordinal LTN)); rewrite /to_pred_ord /= PRED in NONE.
Qed.
End PickAny.
@@ -83,12 +84,12 @@ End PickAny.
Section PickMin.
Variable n: nat.
- Variable p: pred 'I_n.
+ Variable p: pred nat.
Variable P: nat -> Prop.
(* Assume that there is some number < n that satisfies p. *)
- Hypothesis EX: exists x:'I_n, p x.
+ Hypothesis EX: exists x, x < n /\ p x.
Section Bound.
@@ -99,12 +100,12 @@ Section PickMin.
case: pickP.
{
move => x /andP [PRED /forallP ALL].
- by rewrite /default0.
+ by rewrite /default0.
}
{
intros NONE; red in NONE; exfalso.
- move: EX => [x PRED]; clear EX.
- set argmin := arg_min x p id.
+ move: EX => [x [LT PRED]]; clear EX.
+ set argmin := arg_min (Ordinal LT) p id.
specialize (NONE argmin).
suff ARGMIN: (pred_min_nat n p) argmin by rewrite ARGMIN in NONE.
rewrite /argmin; case: arg_minP; first by done.
@@ -120,9 +121,9 @@ Section PickMin.
Hypothesis MIN:
forall x,
- p x ->
x < n ->
- (forall y, p y -> x <= y) ->
+ p x ->
+ (forall y, y < n -> p y -> x <= y) ->
P x.
(* Next, we show that any property P of (pick_min n p) can be proven by showing
@@ -133,70 +134,71 @@ Section PickMin.
case: pickP.
{
move => x /andP [PRED /forallP ALL].
- apply MIN; try (by done).
- by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
+ apply MIN; [by rewrite /default0 | by done |].
+ intros y LTy Py; specialize (ALL (Ordinal LTy)).
+ by move: ALL => /implyP ALL; apply ALL.
}
{
intros NONE; red in NONE; exfalso.
- move: EX => [x PRED]; clear EX.
- set argmin := arg_min x p id.
+ move: EX => [x [LT PRED]]; clear EX.
+ set argmin := arg_min (Ordinal LT) p id.
specialize (NONE argmin).
suff ARGMIN: (pred_min_nat n p) argmin by rewrite ARGMIN in NONE.
rewrite /argmin; case: arg_minP; first by done.
intros y Py MINy.
apply/andP; split; first by done.
- by apply/forallP; intros y0; apply/implyP; intros Py0; apply MINy.
+ by apply/forallP; intros y0; apply/implyP; intros Py0; apply MINy.
}
Qed.
End Minimum.
-
+
End PickMin.
(** Lemmas about pick_max *)
Section PickMax.
Variable n: nat.
- Variable p: pred 'I_n.
+ Variable p: pred nat.
Variable P: nat -> Prop.
(* Assume that there is some number < n that satisfies p. *)
- Hypothesis EX: exists x:'I_n, p x.
+ Hypothesis EX: exists x, x < n /\ p x.
Section Bound.
- (* First, we show that (pick_max n p) < n. *)
+ (* First, we show that (pick_max n p) < n... *)
Lemma pick_max_ltn: pick_max n p < n.
Proof.
rewrite /pick_max /odflt /oapp.
case: pickP.
{
move => x /andP [PRED /forallP ALL].
- by rewrite /default0.
+ by rewrite /default0.
}
{
intros NONE; red in NONE; exfalso.
- move: EX => [x PRED]; clear EX.
- set argmax := arg_max x p id.
+ move: EX => [x [LT PRED]]; clear EX.
+ set argmax := arg_max (Ordinal LT) p id.
specialize (NONE argmax).
suff ARGMAX: (pred_max_nat n p) argmax by rewrite ARGMAX in NONE.
rewrite /argmax; case: arg_maxP; first by done.
intros y Py MAXy.
apply/andP; split; first by done.
- by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
+ by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
}
Qed.
End Bound.
-
+
Section Maximum.
Hypothesis MAX:
forall x,
- p x ->
x < n ->
- (forall y, p y -> x >= y) ->
+ p x ->
+ (forall y, y < n -> p y -> x >= y) ->
P x.
(* Next, we show that any property P of (pick_max n p) can be proven by showing that
@@ -207,22 +209,83 @@ Section PickMax.
case: pickP.
{
move => x /andP [PRED /forallP ALL].
- apply MAX; try (by done).
- by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
+ apply MAX; [by rewrite /default0 | by rewrite /default0 |].
+ intros y LTy Py; specialize (ALL (Ordinal LTy)).
+ by move: ALL => /implyP ALL; apply ALL.
}
{
intros NONE; red in NONE; exfalso.
- move: EX => [x PRED]; clear EX.
- set argmax := arg_max x p id.
+ move: EX => [x [LT PRED]]; clear EX.
+ set argmax := arg_max (Ordinal LT) p id.
specialize (NONE argmax).
suff ARGMAX: (pred_max_nat n p) argmax by rewrite ARGMAX in NONE.
rewrite /argmax; case: arg_maxP; first by done.
intros y Py MAXy.
apply/andP; split; first by done.
- by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
+ by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
}
Qed.
End Maximum.
+
+End PickMax.
+
+Section Predicate.
+
+ Variable n: nat.
+ Variable p: pred nat.
+
+ Hypothesis EX: exists x, x < n /\ p x.
+
+ (* Here we prove that pick_any satiesfies the predicate p, ... *)
+ Lemma pick_any_pred: p (pick_any n p).
+ Proof.
+ by apply pick_any_holds.
+ Qed.
+
+ (* ...and the same holds for pick_min... *)
+ Lemma pick_min_pred: p (pick_min n p).
+ Proof.
+ by apply pick_min_holds.
+ Qed.
+
+ (* ...and pick_max. *)
+ Lemma pick_max_pred: p (pick_max n p).
+ Proof.
+ by apply pick_max_holds.
+ Qed.
+
+End Predicate.
+
+Section PickMinCompare.
+
+ Variable n: nat.
+ Variable p1 p2: pred nat.
+
+ Hypothesis EX1 : exists x, x < n /\ p1 x.
+ Hypothesis EX2 : exists x, x < n /\ p2 x.
+
+ Hypothesis OUT:
+ forall x y, x < n -> y < n -> p1 x -> p2 y -> ~~ p1 y -> x <= y.
+
+ Lemma pick_min_compare: pick_min n p1 <= pick_min n p2.
+ Proof.
+ set m1:= pick_min _ _.
+ set m2:= pick_min _ _.
+ case IN: (p1 m2).
+ {
+ apply pick_min_holds; first by done.
+ intros x Px LTN ALL.
+ by apply ALL; first by apply pick_min_ltn.
+ }
+ {
+ apply (OUT m1 m2).
+ - by apply pick_min_ltn.
+ - by apply pick_min_ltn.
+ - by apply pick_min_pred.
+ - by apply pick_min_pred.
+ - by apply negbT.
+ }
+ Qed.
-End PickMax.
\ No newline at end of file
+End PickMinCompare.
\ No newline at end of file
--
GitLab