_CoqProject

--R . prosa -arg "-w -notation-overriden,-parsing"
+-R . prosa -arg "-w -notation-overriden,-parsing,-projection-no-head-constant"

classic/analysis/apa/interference_bound_edf.v

@@ -274,7 +274,7 @@ Module InterferenceBoundEDF.
           \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
            \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
         Proof.
-          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
+          by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Note that both sequences have the same set of elements. *)
@@ -282,7 +282,7 @@ Module InterferenceBoundEDF.
           forall j,
             (j \in interfering_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)

classic/analysis/apa/workload_bound.v

@@ -231,7 +231,7 @@ Module WorkloadBound.
            \sum_(i <- sorted_jobs) service_during sched i t1 t2.
         Proof.
           unfold workload_joblist; fold scheduled_jobs.
-          rewrite (eq_big_perm sorted_jobs) /= //.
+          rewrite (perm_big sorted_jobs) /= //.
           by rewrite -(perm_sort earlier_arrival).
         Qed.
 
@@ -240,7 +240,7 @@ Module WorkloadBound.
           forall j,
             (j \in scheduled_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Remember that all jobs in the sorted sequence is an

classic/analysis/global/basic/interference_bound_edf.v

@@ -260,7 +260,7 @@ Module InterferenceBoundEDF.
           \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
            \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
         Proof.
-          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
+          by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Note that both sequences have the same set of elements. *)
@@ -268,7 +268,7 @@ Module InterferenceBoundEDF.
           forall j,
             (j \in interfering_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)

classic/analysis/global/basic/workload_bound.v

@@ -234,7 +234,7 @@ Module WorkloadBound.
            \sum_(i <- sorted_jobs) service_during sched i t1 t2.
         Proof.
           unfold workload_joblist; fold scheduled_jobs.
-          rewrite (eq_big_perm sorted_jobs) /= //.
+          rewrite (perm_big sorted_jobs) /= //.
           by rewrite -(perm_sort earlier_arrival).
         Qed.
 
@@ -243,7 +243,7 @@ Module WorkloadBound.
           forall j,
             (j \in scheduled_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Remember that all jobs in the sorted sequence is an

classic/analysis/global/jitter/interference_bound_edf.v

@@ -271,7 +271,7 @@ Module InterferenceBoundEDFJitter.
           \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
            \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
         Proof.
-          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
+          by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Note that both sequences have the same set of elements. *)
@@ -279,7 +279,7 @@ Module InterferenceBoundEDFJitter.
           forall j,
             (j \in interfering_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)

classic/analysis/global/jitter/workload_bound.v

@@ -241,7 +241,7 @@ Module WorkloadBoundJitter.
            \sum_(i <- sorted_jobs) service_during sched i t1 t2.
         Proof.
           unfold workload_joblist; fold scheduled_jobs.
-          rewrite (eq_big_perm sorted_jobs) /= //.
+          rewrite (perm_big sorted_jobs) /= //.
           by rewrite -(perm_sort earlier_arrival).
         Qed.
 
@@ -250,7 +250,7 @@ Module WorkloadBoundJitter.
           forall j,
             (j \in scheduled_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Remember that all jobs in the sorted sequence is an

classic/analysis/global/parallel/interference_bound_edf.v

@@ -286,7 +286,7 @@ Module InterferenceBoundEDF.
           \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
            \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
         Proof.
-          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
+          by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Note that both sequences have the same set of elements. *)
@@ -294,7 +294,7 @@ Module InterferenceBoundEDF.
           forall j,
             (j \in interfering_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)

classic/analysis/global/parallel/workload_bound.v

@@ -169,7 +169,7 @@ Module WorkloadBound.
            \sum_(i <- sorted_jobs) service_during sched i t1 t2.
         Proof.
           unfold workload_joblist; fold scheduled_jobs.
-          rewrite (eq_big_perm sorted_jobs) /= //.
+          rewrite (perm_big sorted_jobs) /= //.
           by rewrite -(perm_sort earlier_arrival).
         Qed.
 
@@ -178,7 +178,7 @@ Module WorkloadBound.
           forall j,
             (j \in scheduled_jobs) = (j \in sorted_jobs).
         Proof.
-          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
+          by apply perm_mem; rewrite -(perm_sort earlier_arrival).
         Qed.
 
         (* Remember that all jobs in the sorted sequence is an

classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v

@@ -215,7 +215,7 @@ Module SustainabilitySingleCostProperties.
         }
         destruct (sched_susp t) eqn:SCHEDs; last by case: SCHED => SAME; subst.
         move: SCHEDs => /eqP SCHEDs; apply FROM in SCHEDs.
-        case: SCHED; case: ifP; first by move => /andP [PEND _]; case => <-.
+        case: ifP SCHED; first by move => /andP [PEND _]; case => <-.
         by move => NOTPEND; case => <-.
       Qed.
 
@@ -236,7 +236,7 @@ Module SustainabilitySingleCostProperties.
           by eapply in_arrivals_implies_arrived_before in IN; eauto.
         }
         destruct (sched_susp t) eqn:SCHEDs; last by case: SCHED => SAME; subst.
-        case: SCHED; case: ifP;
+        case: ifP SCHED;
           first by move => /andP [PEND _]; case => <-; apply MUST; apply/eqP.
         by move => NOTPEND; case => <-.
       Qed.
@@ -364,7 +364,7 @@ Module SustainabilitySingleCostProperties.
         }
         destruct (sched_susp t) eqn:SCHEDs;
           last by case: SCHED => SAME; subst; rewrite SUSP in NOTSUSP.
-        case: SCHED; case: ifP; last by move => _; case => SAME; subst; rewrite SUSP in NOTSUSP.
+        case: ifP SCHED; last by move => _; case => SAME; subst; rewrite SUSP in NOTSUSP.
         move: SCHEDs; move => /eqP SCHEDs /andP [/andP [PEND NOTSUSPs] _]; case => SAME; subst.
         by rewrite -/suspended SUSP in NOTSUSPs.
       Qed.
@@ -731,4 +731,4 @@ Module SustainabilitySingleCostProperties.
     
   End ReductionProperties.
   
-End SustainabilitySingleCostProperties.
\ No newline at end of file
+End SustainabilitySingleCostProperties.

classic/model/schedule/uni/limited/schedule.v

@@ -3,6 +3,10 @@ Require Import prosa.classic.model.arrival.basic.job.
 Require Import prosa.classic.model.schedule.uni.service
                prosa.classic.model.schedule.uni.schedule.
 
+(* Let's import definition of nonpreemptive schedule. *)
+Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
+
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* In this file, we provide additional definitions and 
@@ -132,9 +136,6 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
       (* In fully nonpreemptive model any job becomes nonpreemptive as soon as it receives one unit of service. *)
       Let job_lock_in_service (j: Job) := ε.
 
-      (* Let's import definition of nonpreemptive schedule. *)
-      Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
-
       (* Next, we assume that the schedule is fully nonpreemptive. *) 
       Hypothesis H_is_nonpreemptive_schedule: 
         NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.

classic/util/tactics.v

@@ -97,7 +97,7 @@ Lemma vlib__eqb_split : forall b1 b2 : bool, (b1 -> b2) -> (b2 -> b1) -> b1 = b2
 Proof. intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.
 
 Lemma vlib__beq_rewrite : forall (T : eqType) (x1 x2 : T), x1 == x2 -> x1 = x2.
-Proof. by intros until 0; case eqP. Qed.
+Proof. by intros *; case eqP. Qed.
 
 Lemma vlib__leq_split : forall x1 x2 x3, x1 <= x2 -> x2 <= x3 -> x1 <= x2 <= x3.
 Proof. by intros; apply/andP; split. Qed.
@@ -115,7 +115,7 @@ Create HintDb vlib_refl discriminated.
 Hint Resolve andP orP nandP norP negP vlib__internal_eqP neqP : vlib_refl.
 
 (* Add x <= y <= z splitting to the core hint database. *)
-Hint Immediate vlib__leq_split vlib__ltn_split1 vlib__ltn_split2.
+Hint Immediate vlib__leq_split vlib__ltn_split1 vlib__ltn_split2 : core.
 
 
 Ltac vlib__complaining_inj f H :=
@@ -381,4 +381,4 @@ Ltac split_conj X :=
       let x' := H in
       let y' := fresh H in
         destruct H as [x' y']
-  end.
\ No newline at end of file
+  end.

doc/guidelines.md

@@ -96,6 +96,43 @@ Guideline: do not name proof terms in type classes to prevent explicit dependenc
 
 - Document the tactics that you use in the [list of tactics](doc/tactics.md). For new users, it can be quite difficult to identify the right tactics to use. This list is intended to give novices a starting to point in the search for the "right" tools.
 
+### Forward vs backward reasoning
+Although the primary focus of Prosa is on the quality of the overall structure and the specifications, good proofs are short and readable. Since Coq tends to favor backward reasoning, try to adhere to it. Forward reasoning tends to be more verbose and to generate needlessly convoluted proof trees. To get an idea, read the following snippet:
+```
+(* Let's say A->B->C->D *)
+  Variable A B C D : Prop.
+  Hypothesis AB : A->B.
+  Hypothesis BC : B->C.
+  Hypothesis CD : C->D.
+
+  (* And we want to prove A->D *)
+  Lemma AD_backward:
+    A->D.
+  Proof.
+    intros.
+    apply CD.
+    apply BC.
+    now apply AB.
+  Qed.
+
+  Lemma AD_forward:
+    A->D.
+  Proof.
+    intros.
+    (* hmm, I have C->D. If only I had C... *) 
+    have I_need_C: C.
+    { (* hmm, I have B->C. If only I had B... *)
+      have I_need_B: B by apply AB.
+      feed BC.
+      apply I_need_B.
+      now apply BC.
+    }
+    feed CD.
+    apply I_need_C.
+    now apply CD.
+  Qed.
+  ```
+
 
 *To be continued… Merge requests welcome: please feel free to propose new advice and better guidelines.*
 

util/search_arg.v

@@ -170,7 +170,7 @@ Section ArgSearch.
       destruct (P (f n)) eqn:Pfn => //=.
     - rewrite <- REC in IND.
       destruct (R (f n) (f q)) eqn:REL => some_x_is;
-        move => y [/andP [a_le_y y_lt_Sn] Pfy];
+        move=> y /andP [a_le_y y_lt_Sn] Pfy;
         injection some_x_is => x_is; rewrite -{}x_is //;
         move: y_lt_Sn; rewrite ltnS;
         rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
@@ -185,13 +185,13 @@ Section ArgSearch.
       + move: (IND q REC y) => HOLDS.
         apply HOLDS => //.
         by apply /andP; split.
-    - move=> some_q_is y [/andP [a_le_y y_lt_Sn] Pfy].
+    - move=> some_q_is y /andP [a_le_y y_lt_Sn] Pfy.
       move: y_lt_Sn. rewrite ltnS.
       rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
       + exfalso. move: Pfn => /negP Pfn. by subst.
       + apply IND => //. by apply /andP; split.
     - move=> some_n_is. injection some_n_is => n_is.
-      move=> y [/andP [a_le_y y_lt_Sn] Pfy].
+      move=> y /andP [a_le_y y_lt_Sn] Pfy.
       move: y_lt_Sn. rewrite ltnS.
       rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
       + by rewrite -n_is EQ; apply (R_reflexive (f n)).
@@ -235,4 +235,4 @@ Section ExMinn.
       by move: MIN; rewrite leqNgt; move => /negP MIN; apply: MIN.
   Qed.
   
-End ExMinn.
\ No newline at end of file
+End ExMinn.