From 0727d647550c19e200a7f3d071ae1623d7133c22 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 2 Nov 2021 10:39:37 +0100
Subject: [PATCH] remove util/rewrite_facilities.v I think that this experiment
was not successful. These lemmas can be easily replaced by ssreflect tactics.
Also, they encourage to write proofs that are harder to maintain.
---
analysis/abstract/abstract_seq_rta.v | 25 +++--
.../facts/busy_interval/priority_inversion.v | 2 +-
analysis/facts/model/service_of_jobs.v | 2 +-
analysis/facts/preemption/job/limited.v | 2 +-
results/edf/rta/bounded_pi.v | 5 +-
results/fixed_priority/rta/bounded_pi.v | 5 +-
util/all.v | 1 -
util/rewrite_facilities.v | 106 ------------------
8 files changed, 21 insertions(+), 127 deletions(-)
delete mode 100644 util/rewrite_facilities.v
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index a6091baba..5e6fdf1f0 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -339,7 +339,7 @@ Section Sequential_Abstract_RTA.
Qed.
End Case1.
-
+
Section Case2.
(** Assume a job [j'] from another task is scheduled at time [t]. *)
@@ -363,13 +363,14 @@ Section Sequential_Abstract_RTA.
/service_of_jobs.service_of_jobs_at scheduled_at_def/=.
have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; rewrite scheduled_at_def; apply/eqP.
rewrite H_sched H_not_job_of_tsk; simpl.
- rewrite (negbTE (option_inj_neq (neqprop_to_neqbool
- (diseq (fun j => job_task j = tsk) _ _
- (neqbool_to_neqprop H_not_job_of_tsk) H_job_of_tsk)))) addn0.
+ have ->: Some j' == Some j = false; last rewrite addn0.
+ { apply/negP => /eqP CONTR; inversion CONTR; subst j'.
+ by move: (H_job_of_tsk) (H_not_job_of_tsk) => -> => /eqP NEQ; apply: NEQ. }
have ZERO: \sum_(i <- arrivals_between t1 (t1 + A + ε) | job_task i == tsk) (Some j' == Some i) = 0.
{ apply big1; move => j2 /eqP TSK2; apply/eqP; rewrite eqb0.
- apply option_inj_neq, neqprop_to_neqbool, (diseq (fun j => job_task j = tsk) _ _
- (neqbool_to_neqprop H_not_job_of_tsk) TSK2). }
+ apply/negP => /eqP EQ; inversion EQ; subst j'.
+ by move: TSK2 H_not_job_of_tsk => -> /negP.
+ }
rewrite ZERO ?addn0 add0n; simpl; clear ZERO.
case INT: (interference j t); last by done.
simpl; rewrite lt0b.
@@ -404,15 +405,17 @@ Section Sequential_Abstract_RTA.
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
/service_of_jobs.service_of_jobs_at scheduled_at_def/=.
have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; rewrite scheduled_at_def; apply/eqP.
- rewrite H_sched H_not_job_of_tsk addn0; simpl;
- rewrite [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) addn0.
+ rewrite H_sched H_not_job_of_tsk addn0; simpl.
+ have ->: Some j' == Some j = false by
+ apply/negP => /eqP EQ; inversion EQ; subst j'; move:H_j_neq_j' => /negP NEQ; apply: NEQ.
replace (interference j t) with true; last first.
{ have NEQT: t1 <= t < t2.
{ by move: H_t_in_interval => /andP [NEQ1 NEQ2]; apply/andP; split; last apply ltn_trans with (t1 + x). }
move: (H_work_conserving j t1 t2 t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval NEQT) => [Hn _].
apply/eqP;rewrite eq_sym eqb_id; apply/negPn/negP; intros CONTR; move: CONTR => /negP CONTR.
apply Hn in CONTR; rewrite scheduled_at_def in CONTR; simpl in CONTR.
- by rewrite H_sched [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) in CONTR. }
+ by move: CONTR; rewrite H_sched => /eqP EQ; inversion EQ; subst; move: H_j_neq_j' => /eqP.
+ }
rewrite big_mkcond; apply/sum_seq_gt0P; exists j'; split; last first.
{ by move: H_not_job_of_tsk => /eqP TSK; rewrite /job_of_task TSK eq_refl eq_refl. }
{ intros. have ARR:= arrives_after_beginning_of_busy_interval j j' _ _ _ _ _ t1 t2 _ t.
@@ -460,7 +463,7 @@ Section Sequential_Abstract_RTA.
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
/service_of_jobs.service_of_jobs_at scheduled_at_def.
- rewrite H_sched H_job_of_tsk neq_antirefl addn0; simpl.
+ rewrite H_sched H_job_of_tsk !eq_refl addn0 //=.
move: (H_work_conserving j _ _ t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval) => WORK.
feed WORK.
{ move: H_t_in_interval => /andP [NEQ1 NEQ2].
@@ -468,7 +471,7 @@ Section Sequential_Abstract_RTA.
move: WORK => [_ ZIJT].
feed ZIJT; first by rewrite scheduled_at_def H_sched; simpl.
move: ZIJT => /negP /eqP; rewrite eqb_negLR; simpl; move => /eqP ZIJT; rewrite ZIJT; simpl; rewrite add0n.
- rewrite !eq_refl; simpl; rewrite big_mkcond //=; apply/sum_seq_gt0P.
+ rewrite big_mkcond //=; apply/sum_seq_gt0P.
by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl].
Qed.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index ba5cf9dda..da20e1de8 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -591,7 +591,7 @@ Section PriorityInversionIsBounded.
move: (H_valid_model_with_bounded_nonpreemptive_segments) => CORR.
move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]].
exists t1; split.
- - by rewrite /preemption_time (eqbool_to_eqprop H_is_idle).
+ - by rewrite /preemption_time; move: H_is_idle => /eqP ->.
- by apply/andP; split; last rewrite leq_addr.
Qed.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 3a121ed20..5670cd93d 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -375,7 +375,7 @@ Section IdealModelLemmas.
destruct (t1 <= t2) eqn:LE; last first.
{ move: LE => /negP/negP; rewrite -ltnNge.
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.
- by rewrite (eqbool_to_eqprop LT) ltn0 in SERV.
+ by move: LT => /eqP -> in SERV; rewrite ltn0 in SERV.
}
have EX: exists δ, t2 = t1 + δ.
{ by exists (t2 - t1); rewrite subnKC // ltnW. }
diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index 9f86d27a1..8d5b95980 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -72,7 +72,7 @@ Section ModelWithLimitedPreemptions.
move: H_valid_limited_preemptions_job_model => [BEG [END _]].
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.
specialize (BEG j H_j_arrives).
- by rewrite /beginning_of_execution_in_preemption_points (eqbool_to_eqprop CONTR) in BEG.
+ by move: CONTR BEG => /eqP; rewrite /beginning_of_execution_in_preemption_points => ->.
Qed.
(** Next, we prove that the cost of a job is a preemption point. *)
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 9f04bb62a..43cd7c314 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -622,9 +622,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
rewrite /task_rbf_changes_at neq_ltn; apply/orP; left.
rewrite /task_rbf /rbf; erewrite task_rbf_0_zero; eauto 2.
rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk).
- - by eapply leq_trans; eauto 2;
- rewrite -(eqbool_to_eqprop H_job_of_tsk); apply H_valid_job_cost.
- - by eapply task_rbf_1_ge_task_cost; eauto using eqbool_to_eqprop.
+ - by eapply leq_trans; eauto 2; move: H_job_of_tsk => /eqP <-; apply H_valid_job_cost.
+ - by eapply task_rbf_1_ge_task_cost; eauto 2; apply/eqP.
}
{ apply/andP; split; first by done.
rewrite -[_ || _ ]Bool.negb_involutive negb_or; apply/negP; move => /andP [/negPn/eqP EQ1 /hasPn EQ2].
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 402a95200..3099f1223 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -198,11 +198,10 @@ Section AbstractRTAforFPwithArrivalCurves.
rewrite !Bool.negb_involutive negb_and Bool.negb_involutive.
move => HYP1 /orP [/negP HYP2| /eqP HYP2].
* by exfalso.
- * by subst s; rewrite scheduled_at_def //; apply eqprop_to_eqbool.
+ * by subst s; rewrite scheduled_at_def //; apply/eqP.
+ exfalso; clear HYP1 HYP2.
eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
- by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
- eauto 2 using eqprop_to_eqbool with basic_facts.
+ by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle; eauto 2 with basic_facts; apply/eqP.
- move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
/is_interference_from_another_hep_job HYP2 negb_or.
diff --git a/util/all.v b/util/all.v
index 20dc35795..2b76862d0 100644
--- a/util/all.v
+++ b/util/all.v
@@ -14,5 +14,4 @@ Require Export prosa.util.rel.
Require Export prosa.util.minmax.
Require Export prosa.util.supremum.
Require Export prosa.util.nondecreasing.
-Require Export prosa.util.rewrite_facilities.
Require Export prosa.util.setoid.
diff --git a/util/rewrite_facilities.v b/util/rewrite_facilities.v
deleted file mode 100644
index 584df5a1f..000000000
--- a/util/rewrite_facilities.v
+++ /dev/null
@@ -1,106 +0,0 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * Rewriting *)
-(** In this file we prove a few lemmas
- that simplify work with rewriting. *)
-Section RewriteFacilities.
-
- Lemma diseq:
- forall {X : Type} (p : X -> Prop) (x y : X),
- ~ p x -> p y -> x <> y.
- Proof. intros ? ? ? ? NP P EQ; subst; auto. Qed.
-
-
- Lemma eqprop_to_eqbool {X : eqType} {a b : X}: a = b -> a == b.
- Proof. by intros; apply/eqP. Qed.
-
- Lemma eqbool_true {X : eqType} {a b : X}: a == b -> a == b = true.
- Proof. by move =>/eqP EQ; subst b; rewrite eq_refl. Qed.
-
- Lemma eqbool_false {X : eqType} {a b : X}: a != b -> a == b = false.
- Proof. by apply negbTE. Qed.
-
-
- Lemma eqbool_to_eqprop {X : eqType} {a b : X}: a == b -> a = b.
- Proof. by intros; apply/eqP. Qed.
-
- Lemma neqprop_to_neqbool {X : eqType} {a b : X}: a <> b -> a != b.
- Proof. by intros; apply/eqP. Qed.
-
- Lemma neqbool_to_neqprop {X : eqType} {a b : X}: a != b -> a <> b.
- Proof. by intros; apply/eqP. Qed.
-
- Lemma neq_sym {X : eqType} {a b : X}:
- a != b -> b != a.
- Proof.
- intros NEQ; apply/eqP; intros EQ;
- subst b; move: NEQ => /eqP NEQ; auto. Qed.
-
- Lemma neq_antirefl {X : eqType} {a : X}:
- (a != a) = false.
- Proof. by apply/eqP. Qed.
-
-
- Lemma option_inj_eq {X : eqType} {a b : X}:
- a == b -> Some a == Some b.
- Proof. by move => /eqP EQ; apply/eqP; rewrite EQ. Qed.
-
- Lemma option_inj_neq {X : eqType} {a b : X}:
- a != b -> Some a != Some b.
- Proof.
- by move => /eqP NEQ;
- apply/eqP; intros CONTR;
- apply: NEQ; inversion_clear CONTR. Qed.
-
- (** Example *)
- (* As a motivation for this file, we consider the following example. *)
- Section Example.
-
- (* Let X be an arbitrary type ... *)
- Context {X : eqType}.
-
- (* ... f be an arbitrary function [bool -> bool] ... *)
- Variable f : bool -> bool.
-
- (* ... p be an arbitrary predicate on X ... *)
- Variable p : X -> Prop.
-
- (* ... and let a and b be two elements of X such that ... *)
- Variables a b : X.
-
- (* ... p holds for a and doesn't hold for b. *)
- Hypothesis H_pa : p a.
- Hypothesis H_npb : ~ p b.
-
- (* The following examples are commented out
- to expose the insides of the proofs. *)
-
- (*
- (* Simplifying some relatively sophisticated
- expressions can be quite tedious. *)
- [Goal f ((a == b) && f false) = f false.]
- [Proof.]
- (* Things like [simpl/compute] make no sense here. *)
- (* One can use [replace] to generate a new goal. *)
- [replace (a == b) with false; last first.]
- (* However, this leads to a "loss of focus". Moreover,
- the resulting goal is not so trivial to prove. *)
- [{ apply/eqP; rewrite eq_sym eqbF_neg.]
- [ by apply/eqP; intros EQ; subst b; apply H_npb. }]
- [ by rewrite Bool.andb_false_l.]
- [Abort.]
- *)
-
- (*
- (* The second attempt. *)
- [Goal f ((a == b) && f false) = f false.]
- (* With the lemmas above one can compose multiple
- transformations in a single rewrite. *)
- [ by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))]
- [ Bool.andb_false_l.]
- [Qed.]
- *)
-
- End Example.
-
-End RewriteFacilities.
--
GitLab