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

@@ -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.
 

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.
         

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. }

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. *)

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].

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.

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.

util/rewrite_facilities.v

-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.