.ackrc

+# Configuration file for the 'ack' search utility
+# See https://beyondgrep.com/ for details.
+
+# Ignore misc files generated by the build process
+--ignore-file=ext:glob,aux
\ No newline at end of file

analysis/apa/bertogna_fp_comp.v

@@ -310,7 +310,7 @@ Module ResponseTimeIterationFP.
         rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
         intros hp_idx idx LThp LT NEQ HP.
         rewrite ltn_neqAle; apply/andP; split; first by done.
-        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem).
+        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
       Qed.
       
     End HighPriorityTasks.

analysis/global/basic/bertogna_fp_comp.v

@@ -304,7 +304,7 @@ Module ResponseTimeIterationFP.
         rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
         intros hp_idx idx LThp LT NEQ HP.
         rewrite ltn_neqAle; apply/andP; split; first by done.
-        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem).
+        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
       Qed.
 
     End HighPriorityTasks.

analysis/global/jitter/bertogna_fp_comp.v

@@ -306,7 +306,7 @@ Module ResponseTimeIterationFP.
         rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
         intros hp_idx idx LThp LT NEQ HP.
         rewrite ltn_neqAle; apply/andP; split; first by done.
-        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem).
+        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
       Qed.
       
     End HighPriorityTasks.

analysis/global/parallel/bertogna_fp_comp.v

@@ -304,7 +304,7 @@ Module ResponseTimeIterationFP.
         rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
         intros hp_idx idx LThp LT NEQ HP.
         rewrite ltn_neqAle; apply/andP; split; first by done.
-        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem).
+        by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
       Qed.
       
     End HighPriorityTasks.

behavior/arrival/arrival_sequence.v

+From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
+From rt.behavior Require Export time job.
+From rt.util Require Import all.
+
+
+(* Definitions and properties of job arrival sequences. *)
+
+(* We begin by defining a job arrival sequence. *)
+Section ArrivalSequenceDef.
+
+  (* Given any job type with decidable equality, ... *)
+  Variable Job: JobType.
+
+  (* ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
+  Definition arrival_sequence := instant -> seq Job.
+
+End ArrivalSequenceDef.
+
+(* Next, we define properties of jobs in a given arrival sequence. *)
+Section JobProperties.
+
+  (* Consider any job arrival sequence. *)
+  Context {Job: JobType}.
+  Variable arr_seq: arrival_sequence Job.
+
+  (* First, we define the sequence of jobs arriving at time t. *)
+  Definition jobs_arriving_at (t : instant) := arr_seq t.
+
+  (* Next, we say that job j arrives at a given time t iff it belongs to the
+       corresponding sequence. *)
+  Definition arrives_at (j : Job) (t : instant) := j \in jobs_arriving_at t.
+
+  (* Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
+       whether it belongs to the arrival sequence. *)
+  Definition arrives_in (j : Job) := exists t, j \in jobs_arriving_at t.
+
+End JobProperties.
+
+(* Definition of a generic type of parameter for job_arrival *)
+
+Class JobArrival (J : JobType) := job_arrival : J -> instant.
+
+(* Next, we define properties of a valid arrival sequence. *)
+Section ArrivalSequenceProperties.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (* We say that arrival times are consistent if any job that arrives in the sequence
+       has the corresponding arrival time. *)
+  Definition arrival_times_are_consistent :=
+    forall j t,
+      arrives_at arr_seq j t -> job_arrival j = t.
+
+  (* We say that the arrival sequence is a set iff it doesn't contain duplicate jobs
+       at any given time. *)
+  Definition arrival_sequence_is_a_set := forall t, uniq (jobs_arriving_at arr_seq t).
+
+End ArrivalSequenceProperties.
+
+(* Next, we define properties of job arrival times. *)
+Section PropertiesOfArrivalTime.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* Let j be any job. *)
+  Variable j: Job.
+
+  (* We say that job j has arrived at time t iff it arrives at some time t_0 with t_0 <= t. *)
+  Definition has_arrived (t : instant) := job_arrival j <= t.
+
+  (* Next, we say that job j arrived before t iff it arrives at some time t_0 with t_0 < t. *)
+  Definition arrived_before (t : instant) := job_arrival j < t.
+
+  (* Finally, we say that job j arrives between t1 and t2 iff it arrives at some time t with
+       t1 <= t < t2. *)
+  Definition arrived_between (t1 t2 : instant) := t1 <= job_arrival j < t2.
+
+End PropertiesOfArrivalTime.
+
+(* In this section, we define arrival sequence prefixes, which are useful
+     to define (computable) properties over sets of jobs in the schedule. *)
+Section ArrivalSequencePrefix.
+
+  (* Assume that job arrival times are known. *)
+  Context {Job: JobType}.
+  Context `{JobArrival Job}.
+
+  (* Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (* By concatenation, we construct the list of jobs that arrived in the interval [t1, t2). *)
+  Definition jobs_arrived_between (t1 t2 : instant) :=
+    \cat_(t1 <= t < t2) jobs_arriving_at arr_seq t.
+
+  (* Based on that, we define the list of jobs that arrived up to time t, ...*)
+  Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.
+
+  (* ...and the list of jobs that arrived strictly before time t. *)
+  Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.
+
+  (* In this section, we prove some lemmas about arrival sequence prefixes. *)
+  Section Lemmas.
+
+    (* We begin with basic lemmas for manipulating the sequences. *)
+    Section Basic.
+
+      (* First, we show that the set of arriving jobs can be split
+           into disjoint intervals. *)
+      Lemma job_arrived_between_cat:
+        forall t1 t t2,
+          t1 <= t ->
+          t <= t2 ->
+          jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
+      Proof.
+        unfold jobs_arrived_between; intros t1 t t2 GE LE.
+          by rewrite (@big_cat_nat _ _ _ t).
+      Qed.
+
+      Lemma jobs_arrived_between_mem_cat:
+        forall j t1 t t2,
+          t1 <= t ->
+          t <= t2 ->
+          j \in jobs_arrived_between t1 t2 =
+                (j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
+      Proof.
+          by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
+      Qed.
+
+      Lemma jobs_arrived_between_sub:
+        forall j t1 t1' t2 t2',
+          t1' <= t1 ->
+          t2 <= t2' ->
+          j \in jobs_arrived_between t1 t2 ->
+                j \in jobs_arrived_between t1' t2'.
+      Proof.
+        intros j t1 t1' t2 t2' GE1 LE2 IN.
+        move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
+                                   last by rewrite /jobs_arrived_between big_geq // in IN.
+        rewrite /jobs_arrived_between.
+        rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
+        rewrite mem_cat; apply/orP; right.
+        rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
+          by rewrite mem_cat; apply/orP; left.
+      Qed.
+
+    End Basic.
+
+    (* Next, we relate the arrival prefixes with job arrival times. *)
+    Section ArrivalTimes.
+
+      (* Assume that job arrival times are consistent. *)
+      Hypothesis H_arrival_times_are_consistent:
+        arrival_times_are_consistent arr_seq.
+
+      (* First, we prove that if a job belongs to the prefix (jobs_arrived_before t),
+         then it arrives in the arrival sequence. *)
+      Lemma in_arrivals_implies_arrived:
+        forall j t1 t2,
+          j \in jobs_arrived_between t1 t2 ->
+                arrives_in arr_seq j.
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        intros j t1 t2 IN.
+        apply mem_bigcat_nat_exists in IN.
+        move: IN => [arr [IN _]].
+          by exists arr.
+      Qed.
+
+      (* Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2),
+         then it indeed arrives between t1 and t2. *)
+      Lemma in_arrivals_implies_arrived_between:
+        forall j t1 t2,
+          j \in jobs_arrived_between t1 t2 ->
+                arrived_between j t1 t2.
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        intros j t1 t2 IN.
+        apply mem_bigcat_nat_exists in IN.
+        move: IN => [t0 [IN /= LT]].
+          by apply CONS in IN; rewrite /arrived_between IN.
+      Qed.
+
+      (* Similarly, if a job belongs to the prefix (jobs_arrived_before t),
+           then it indeed arrives before time t. *)
+      Lemma in_arrivals_implies_arrived_before:
+        forall j t,
+          j \in jobs_arrived_before t ->
+                arrived_before j t.
+      Proof.
+        intros j t IN.
+        Fail suff: arrived_between j 0 t by rewrite /arrived_between /=.
+        have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
+        by rewrite /arrived_between /=.
+      Qed.
+
+      (* Similarly, we prove that if a job from the arrival sequence arrives before t,
+         then it belongs to the sequence (jobs_arrived_before t). *)
+      Lemma arrived_between_implies_in_arrivals:
+        forall j t1 t2,
+          arrives_in arr_seq j ->
+          arrived_between j t1 t2 ->
+          j \in jobs_arrived_between t1 t2.
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        move => j t1 t2 [a_j ARRj] BEFORE.
+        have SAME := ARRj; apply CONS in SAME; subst a_j.
+          by apply mem_bigcat_nat with (j := (job_arrival j)).
+      Qed.
+
+      (* Next, we prove that if the arrival sequence doesn't contain duplicate jobs,
+         the same applies for any of its prefixes. *)
+      Lemma arrivals_uniq :
+        arrival_sequence_is_a_set arr_seq ->
+        forall t1 t2, uniq (jobs_arrived_between t1 t2).
+      Proof.
+        rename H_arrival_times_are_consistent into CONS.
+        unfold jobs_arrived_up_to; intros SET t1 t2.
+        apply bigcat_nat_uniq; first by done.
+        intros x t t' IN1 IN2.
+          by apply CONS in IN1; apply CONS in IN2; subst.
+      Qed.
+
+    End ArrivalTimes.
+
+  End Lemmas.
+
+End ArrivalSequencePrefix.

behavior/job.v

+From mathcomp Require Export eqtype.
+
+(* Throughout the library we assume that jobs have decidable equality *)
+
+Definition JobType := eqType.

behavior/schedule/ideal.v

+From rt.behavior Require Export schedule.schedule.
+
+(** First let us define the notion of an ideal schedule state,
+ *  as done in Prosa so far: either a job is scheduled or the system is idle.
+ *)
+
+Section State.
+
+  Variable Job: eqType.
+
+  Definition processor_state := option Job.
+
+  Instance pstate_instance : ProcessorState Job (option Job) :=
+    {
+      scheduled_in j s := s == Some j;
+      service_in j s   := s == Some j
+    }.
+  Proof.
+      by move=> j [j'->|].
+  Qed.
+End State.

behavior/schedule/multiprocessor.v

+From mathcomp Require Export fintype.
+From rt.behavior.schedule Require Export schedule.
+
+Section Schedule.
+
+  Variable Job: eqType.
+  Variable processor_state: Type.
+  Context `{ProcessorState Job processor_state}.
+
+  Definition processor (num_cpus: nat) := 'I_num_cpus.
+
+  Variable num_cpus : nat.
+
+  Definition identical_state := processor num_cpus -> processor_state.
+
+  Instance multiproc_state : ProcessorState Job (identical_state) :=
+    {
+      scheduled_in j s := [exists cpu, scheduled_in j (s cpu)];
+      service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
+    }.
+  Proof.
+    move=> j s /existsP Hsched.
+    apply/eqP.
+    rewrite sum_nat_eq0.
+    apply/forallP=>/= c.
+    rewrite service_implies_scheduled//.
+    case: (boolP (scheduled_in _ _))=>//= Habs.
+    exfalso; apply: Hsched.
+      by exists c.
+  Qed.
+End Schedule.

behavior/schedule/schedule.v

+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.behavior Require Export arrival.arrival_sequence.
+
+(* We define the notion of a generic processor state. The processor state type
+ * determines aspects of the execution environment are modeled (e.g., overheads, spinning).
+ * In the most simple case (i.e., Ideal.processor_state), at any time,
+ * either a particular job is either scheduled or it is idle. *)
+Class ProcessorState (Job : eqType) (State : Type) :=
+  {
+    (* For a given processor state, the [scheduled_in] predicate checks whether a given
+     * job is running in that state. *)
+    scheduled_in: Job -> State -> bool;
+    (* For a given processor state, the [service_in] function determines how much
+     * service a given job receives in that state. *)
+    service_in: Job -> State -> nat;
+    (* For a given processor state, a job does not receive service if it is not scheduled
+     * in that state *)
+    service_implies_scheduled :
+      forall j s, scheduled_in j s = false -> service_in j s = 0
+  }.
+
+(* A schedule maps an instant to a processor state *)
+Definition schedule (PState : Type) := instant -> PState.
+
+(* Definition of a generic type of parameter relating jobs to a discrete cost *)
+
+Class JobCost (J : JobType) := job_cost : J -> nat.
+
+Section Service.
+  Context {Job : eqType} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  Variable sched : schedule PState.
+
+  (* First, we define whether a job j is scheduled at time t, ... *)
+  Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
+
+  (* ... and the instantaneous service received by
+           job j at time t. *)
+  Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+
+  (* Based on the notion of instantaneous service, we define the
+           cumulative service received by job j during any interval [t1, t2). *)
+  Definition service_during (j : Job) (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) service_at j t.
+
+  (* Using the previous definition, we define the cumulative service
+           received by job j up to time t, i.e., during interval [0, t). *)
+  Definition service (j : Job) (t : instant) := service_during j 0 t.
+
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (* Next, we say that job j has completed by time t if it received enough
+           service in the interval [0, t). *)
+  Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
+
+  (* Job j is pending at time t iff it has arrived but has not yet completed. *)
+  Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
+
+  (* Job j is pending earlier and at time t iff it has arrived before time t
+           and has not been completed yet. *)
+  Definition pending_earlier_and_at (j : Job) (t : instant) :=
+    arrived_before j t && ~~ completed_by j t.
+
+  (* Job j is backlogged at time t iff it is pending and not scheduled. *)
+  Definition backlogged (j : Job) (t : instant) := pending j t && ~~ scheduled_at j t.
+
+  (* Let's define the remaining cost of job j as the amount of service
+         that has to be received for its completion. *)
+  Definition remaining_cost j t :=
+    job_cost j - service j t.
+
+  (* In this section, we define properties of valid schedules. *)
+  Section ValidSchedules.
+
+    Variable (arr_seq : arrival_sequence Job).
+
+    (* We define whether jobs come from some arrival sequence... *)
+    Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
+      forall j t, scheduled_at j t -> arrives_in arr_seq j.
+
+    (* ..., whether a job can only be scheduled if it has arrived ... *)
+    Definition jobs_must_arrive_to_execute :=
+      forall j t, scheduled_at j t -> has_arrived j t.
+
+    (* ... and whether a job cannot be scheduled after it completes. *)
+    Definition completed_jobs_dont_execute :=
+      forall j t, service j t <= job_cost j.
+
+  End ValidSchedules.
+End Service.

behavior/schedule/spin.v

+From rt.behavior.schedule Require Export schedule.
+
+(** Next we define a processor state that includes the possibility of spinning,
+ *  where spinning jobs do not progress (= don't get service).  *)
+Section State.
+
+  Variable Job: eqType.
+
+  Inductive processor_state :=
+    Idle
+  | Spin (j : Job)
+  | Progress (j : Job).
+
+  Section Service.
+
+    Variable j : Job.
+
+    Definition scheduled_in (s : processor_state) : bool :=
+      match s with
+      | Idle        => false
+      | Spin j'     => j' == j
+      | Progress j' => j' == j
+      end.
+
+    Definition service_in (s : processor_state) : nat :=
+      match s with
+      | Idle        => 0
+      | Spin j'     => 0
+      | Progress j' => j' == j
+      end.
+
+  End Service.
+
+  Instance pstate_instance : ProcessorState Job (processor_state) :=
+    {
+      scheduled_in := scheduled_in;
+      service_in   := service_in
+    }.
+  Proof.
+    by move=> j [|j'|j']//=->.
+  Qed.
+End State.

behavior/schedule/varspeed.v

+From rt.behavior.schedule Require Export schedule.
+
+(** Next, let us define a schedule with variable execution speed. *)
+Section State.
+
+  Variable Job: eqType.
+
+  Inductive processor_state :=
+    Idle
+  | Progress (j : Job) (speed : nat).
+
+  Section Service.
+
+    Variable j : Job.
+
+    Definition scheduled_in (s : processor_state) : bool :=
+      match s with
+      | Idle => false
+      | Progress j' _  => j' == j
+      end.
+
+    Definition service_in (s : processor_state) : nat :=
+      match s with
+      | Idle => 0
+      | Progress j' s  => if j' == j then s else 0
+      end.
+
+  End Service.
+
+  Instance pstate_instance : ProcessorState Job processor_state :=
+    {
+      scheduled_in := scheduled_in;
+      service_in   := service_in
+    }.
+  Proof.
+      by move=> j []//= j' s->.
+  Qed.
+End State.

behavior/task.v

+From rt.behavior Require Export job.
+
+(* Throughout the library we assume that jobs have decidable equality *)
+
+Definition TaskType := eqType.
+
+(* Definition of a generic type of parameter relating jobs to tasks *)
+
+Class JobTask (T : TaskType) (J : JobType) := job_task : J -> T.
\ No newline at end of file

behavior/time.v

+(* Time is defined as a natural number. *)
+
+Definition duration := nat.
+Definition instant  := nat.

create_makefile.sh

@@ -10,7 +10,7 @@ fi
 
 # Compile all *.v files (except the ones that define the decidable equality). Those
 # are directly included in other files.
-coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
+coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -name "*eqdec*.v" ! -path "./.git/*" -print) -o Makefile
 
 # Fix the 'make validate' command. It doesn't handle the library prefix properly
 # and cause clashes for files with the same name. This forces full filenames and

implementation/apa/schedule.v

@@ -408,7 +408,7 @@ Module ConcreteScheduler.
                 in BUG; des;
                 first by rewrite BUG in NOTSCHED.
               move: BUG => /andP [_ /negP HP].
-              by apply HP, order_sorted_rcons with (s := l'); try by done.
+              by apply HP, order_sorted_rcons with (xs := l'); try by done.
             }
             move: (IHl cpu CAN) => [j_old IN]; clear IHl LAST.
             by eapply replace_first_previous in IN; des;
@@ -467,7 +467,7 @@ Module ConcreteScheduler.
           }
           {
             subst j_last.
-            by apply order_sorted_rcons with (s := l').
+            by apply order_sorted_rcons with (xs := l').
           }
           {
             subst j_last; clear IHl.
@@ -485,7 +485,7 @@ Module ConcreteScheduler.
                 move: SHOULD => /andP [CAN' /negP HP].
                 unfold prev in IN'.
                 apply scheduler_job_in_mapping in IN'.
-                by exfalso; apply HP, order_sorted_rcons with (s := l').
+                by exfalso; apply HP, order_sorted_rcons with (xs := l').
               }
               {
                 destruct [exists cpu, ((cpu, Some j) \in prev)] eqn:EX.
@@ -497,7 +497,7 @@ Module ConcreteScheduler.
                       in IN''; des;
                     first by specialize (NOTSCHED cpu'); rewrite IN'' in NOTSCHED.
                   move: IN'' => /andP [_ /negP HP].
-                  by exfalso; apply HP, order_sorted_rcons with (s := l').
+                  by exfalso; apply HP, order_sorted_rcons with (xs := l').
                 }
                 {
                   apply negbT in EX; rewrite negb_exists in EX.
@@ -529,7 +529,7 @@ Module ConcreteScheduler.
               }
               {
                 move: BUG => /andP [_ /negP HP].
-                by apply HP, order_sorted_rcons with (s := l'); try by done.
+                by apply HP, order_sorted_rcons with (xs := l'); try by done.
               }
             }
             {

util/find_seq.v

@@ -51,9 +51,11 @@ Section find_seq.
   Proof.
     intros.
     apply /negP /negP /hasPn.
-    intros. apply find_uniql with (x:=x) in H;auto.
-    case (x0==x)eqn:XX;move/eqP in XX;last trivial.
-    rewrite -XX in H0. by subst.
+    unfold prop_in1. intros.
+    apply find_uniql with (x:=x) in H; last by assumption.
+    case (x0==x) eqn:XX; last trivial.
+    move/eqP in XX.
+    rewrite XX in H1; by contradiction.
   Qed.
 
   Lemma findP_in_seq:

util/sorting.v

 Require Import rt.util.tactics rt.util.induction rt.util.list.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
-(* Lemmas about sorted lists. *)
+(** * Sorting *)
+(** In this modeule we prove a few lemmas about sorted sequences. *)
 Section Sorting.
-  
-  Lemma prev_le_next :
-    forall (T: Type) (F: T->nat) r (x0: T) i k,
-      (forall i, i < (size r).-1 -> F (nth x0 r i) <= F (nth x0 r i.+1)) ->
-      (i + k <= (size r).-1) ->
-      F (nth x0 r i) <= F (nth x0 r (i+k)).
-  Proof.
-    intros T F r x0 i k ALL SIZE.
-    generalize dependent i. generalize dependent k.
-    induction k; intros; first by rewrite addn0 leqnn.
-    specialize (IHk i.+1); exploit IHk; [by rewrite addSnnS | intro LE].
-    apply leq_trans with (n := F (nth x0 r (i.+1)));
-      last by rewrite -addSnnS.
-    apply ALL, leq_trans with (n := i + k.+1); last by ins.
-    by rewrite addnS ltnS leq_addr.
-  Qed.
 
-  Lemma sort_ordered:
-    forall {T: eqType} (leT: rel T) (s: seq T) x0 idx,
-      sorted leT s ->
-      idx < (size s).-1 ->
-      leT (nth x0 s idx) (nth x0 s idx.+1).
-  Proof.
-    intros T leT s x0 idx SORT LT.
-    induction s; first by rewrite /= ltn0 in LT.
-    simpl in SORT, LT; move: SORT => /pathP SORT.
-    by simpl; apply SORT.
-  Qed.
-  
-  Lemma sorted_rcons_prefix :
-    forall {T: eqType} (leT: rel T) s x,
-      sorted leT (rcons s x) ->
-      sorted leT s.
-  Proof.
-    intros T leT s x SORT; destruct s; simpl; first by ins.
-    rewrite rcons_cons /= rcons_path in SORT.
-    by move: SORT => /andP [PATH _].
-  Qed.
+  Section SortedImplLeIdx.
+    
+    (* Consider an arbitrary type T... *)
+    Variable T: eqType.
 
-  Lemma order_sorted_rcons :
-    forall {T: eqType} (leT: rel T) (s: seq T) (x last: T),
-      transitive leT ->
-      sorted leT (rcons s last) ->
-      x \in s ->
-      leT x last.
-  Proof.
-    intros T leT s x last TRANS SORT IN.
-    induction s; first by rewrite in_nil in IN.
-    simpl in SORT; move: IN; rewrite in_cons; move => /orP IN.
-    destruct IN as [HEAD | TAIL];
-      last by apply IHs; [by apply path_sorted in SORT| by ins].
-    move: HEAD => /eqP HEAD; subst a.
-    apply order_path_min in SORT; last by ins.
-    move: SORT => /allP SORT.
-    by apply SORT; rewrite mem_rcons in_cons; apply/orP; left.
-  Qed.
-  
-  Lemma sorted_lt_idx_implies_rel :
-    forall {T: eqType} (leT: rel T) (s: seq T) x0 i1 i2,
-      transitive leT ->
-      sorted leT s ->
-      i1 < i2 ->
-      i2 < size s ->
-      leT (nth x0 s i1) (nth x0 s i2).
-  Proof.
-    intros T leT s x0 i1 i2 TRANS SORT LE LEsize.
-    generalize dependent i2; rewrite leq_as_delta.
-    intros delta LT.
-    destruct s; first by rewrite ltn0 in LT.
-    simpl in SORT.
-    induction delta;
-      first by rewrite /= addn0 ltnS in LT; rewrite /= -addnE addn0; apply/pathP.
-    {
-      rewrite /transitive (TRANS (nth x0 (s :: s0) (i1.+1 + delta))) //;
-        first by apply IHdelta, leq_ltn_trans with (n := i1.+1 + delta.+1); [rewrite leq_add2l|].
-      rewrite -[delta.+1]addn1 addnA addn1.
-      move: SORT => /pathP SORT; apply SORT.
-      by rewrite /= -[delta.+1]addn1 addnA addn1 ltnS in LT.
-    }
-  Qed.
+    (* ... and some binary relation leT (≺) on it. *)
+    Variable leT: rel T.
+    Notation "x ≺ y" := (leT x y) (at level 30).
+    Let sorted xs := sorted leT xs.
+    
+    (* Next, let xs be a sequence of elements of type T. *)
+    Variable xs: seq T.
+    
+    (* Since Coq requires all functions to be total, we 
+       need to specify a default value for cases when 
+       an index exceeds the size of the sequence. *)
+    Variable default: T.
+    Let nth := nth default.
 
-  Lemma sorted_rel_implies_le_idx :
-    forall {T: eqType} (leT: rel T) (s: seq T) x0 i1 i2,
-      uniq s ->
-      antisymmetric_over_list leT s ->
-      transitive leT ->
-      sorted leT s ->
-      leT (nth x0 s i1) (nth x0 s i2) ->
-      i1 < size s ->
-      i2 < size s ->
-      i1 <= i2.
-  Proof.
-    intros T leT s x0 i1 i2 UNIQ ANTI TRANS SORT REL SIZE1 SIZE2.
-    generalize dependent i2.
-    induction i1; first by done.
-    {
-      intros i2 REL SIZE2.
-      feed IHi1; first by apply ltn_trans with (n := i1.+1).
-      apply leq_trans with (n := i1.+1); first by done.
-      rewrite ltn_neqAle; apply/andP; split.
+    (* Next, let's introduce a notation for the nth element of a sequence. *)
+    Notation "xs [| n |]" := (nth xs n) (at level 10).
+    
+    (* We prove that, given the fact that sequence xs is sorted, 
+       the i'th element of xs is ≺ than the i+1'th element. *)
+    Lemma sort_ordered:
+      forall (idx: nat),
+        sorted xs ->
+        idx < (size xs).-1 ->
+        xs[|idx|] ≺ xs[|idx.+1|].
+    Proof.
+      intros idx SORT LT.
+      induction xs; first by rewrite /= ltn0 in LT.
+      simpl in SORT, LT; move: SORT => /pathP SORT.
+        by simpl; apply SORT.
+    Qed.
+
+    (* Next we prove that the prefix of a sorted sequence is also sorted. *)
+    Lemma sorted_rcons_prefix:
+      forall x,
+        sorted (rcons xs x) ->
+        sorted xs.
+    Proof.
+      intros x SORT; destruct xs; simpl; first by ins.
+      rewrite rcons_cons /= rcons_path in SORT.
+        by move: SORT => /andP [PATH _].
+    Qed.
+
+    (* Let's assume that relation leT (≺) is transitive. *)
+    Hypothesis H_leT_is_transitive: transitive leT.
+    
+    (* Given the fact that sequence xs is sorted, we prove that 
+       the last elements of the sequence is the max. element. *) 
+    Lemma order_sorted_rcons:
+      forall (x lst: T),
+        sorted (rcons xs lst) ->
+        x \in xs ->
+        x ≺ lst.
+    Proof.
+      intros x last SORT IN.
+      induction xs as [ | a xs']; [ | clear xs; rename xs' into xs]; first by rewrite in_nil in IN.
+      simpl in SORT; move: IN; rewrite in_cons; move => /orP IN.
+      destruct IN as [HEAD | TAIL];
+        last by apply IHxs'; [by apply path_sorted in SORT| by ins].
+      move: HEAD => /eqP HEAD; subst a.
+      apply order_path_min in SORT; last by ins.
+      move: SORT => /allP SORT.
+        by apply SORT; rewrite mem_rcons in_cons; apply/orP; left.
+    Qed.
+
+    (* Next, we prove that for sorted sequence xs and for any
+       two indices i1 and i2, i1 < i2 implies xs[|i1|] ≺ xs[|i2|]. *) 
+    Lemma sorted_lt_idx_implies_rel:
+      forall  i1 i2,
+        sorted xs ->
+        i1 < i2 ->
+        i2 < size xs ->
+        xs[|i1|] ≺ xs [|i2|].
+    Proof.
+      intros i1 i2 SORT LE LEsize.
+      generalize dependent i2; rewrite leq_as_delta.
+      intros delta LT.
+      destruct xs as [ | a xs']; [ | clear xs; rename xs' into xs]; first by rewrite ltn0 in LT.
+      simpl in SORT.
+      induction delta;
+        first by rewrite /= addn0 ltnS in LT; rewrite /= -addnE addn0; apply/pathP.
       {
-        apply/eqP; red; intro BUG; subst.
-        assert (REL': leT (nth x0 s i2) (nth x0 s i2.+1)).
-          by apply sorted_lt_idx_implies_rel; rewrite // ltnSn.
-        rewrite /antisymmetric_over_list in ANTI.
-        exploit (ANTI (nth x0 s i2) (nth x0 s i2.+1)); rewrite ?mem_nth //.
-        move => /eqP EQ; rewrite nth_uniq in EQ; try (by done).
-        by rewrite -[_ == _]negbK in EQ; move: EQ => /negP EQ; apply EQ; apply/eqP.
+        rewrite /transitive (H_leT_is_transitive (nth (a :: xs) (i1.+1 + delta))) //;
+                first by apply IHdelta, leq_ltn_trans with (n := i1.+1 + delta.+1); [rewrite leq_add2l| ].
+        rewrite -[delta.+1]addn1 addnA addn1.
+        move: SORT => /pathP SORT; apply SORT.
+          by rewrite /= -[delta.+1]addn1 addnA addn1 ltnS in LT.
       }
+    Qed.
+
+    (* Finally, assuming that (1) xs is sorted and contains
+       no duplicates, (2) ≺ is antisymmetric and transitive,
+       we prove that x[|i1|] ≺ x[|i2|] implies i1 ≤ i2. *)
+    Lemma sorted_rel_implies_le_idx:
+      forall i1 i2,
+        uniq xs ->
+        antisymmetric_over_list leT xs ->
+        sorted xs ->
+        xs[|i1|] ≺ xs[|i2|] ->
+        i1 < size xs ->
+        i2 < size xs ->
+        i1 <= i2.
+    Proof.
+      intros i1 i2 UNIQ ANTI SORT REL SIZE1 SIZE2.
+      generalize dependent i2.
+      induction i1; first by done.
       {
-        apply IHi1; last by done.
-        rewrite /transitive (TRANS (nth x0 s i1.+1)) //.
-        by apply sorted_lt_idx_implies_rel; try (by done); apply ltnSn.
+        intros i2 REL SIZE2.
+        feed IHi1; first by apply ltn_trans with (n := i1.+1).
+        apply leq_trans with (n := i1.+1); first by done.
+        rewrite ltn_neqAle; apply/andP; split.
+        {
+          apply/eqP; red; intro BUG; subst.
+          assert (REL': leT (nth xs i2) (nth xs i2.+1)).
+            by apply sorted_lt_idx_implies_rel; rewrite // ltnSn.
+            rewrite /antisymmetric_over_list in ANTI.
+            exploit (ANTI (nth xs i2) (nth xs i2.+1)); rewrite ?mem_nth //.
+            move => /eqP EQ; rewrite nth_uniq in EQ; try (by done).
+              by rewrite -[_ == _]negbK in EQ; move: EQ => /negP EQ; apply EQ; apply/eqP.
+        }
+        {
+          apply IHi1; last by done.
+          rewrite /transitive (H_leT_is_transitive (nth xs i1.+1)) //.
+            by apply sorted_lt_idx_implies_rel; try (by done); apply ltnSn.
+        }
       }
-    }
-  Qed.
+    Qed.
+
+  End SortedImplLeIdx.
 
+  (* Let F be a function from some type to natural numbers. Then for a 
+     sequence xs, the fact that [∀ i: F(xs[i]) ≤ F(xs[i+1])] implies that 
+     [forall i k: F(xs[i]) ≤ F(xs[i + k])]. *) 
+  Lemma prev_le_next:
+    forall {T: Type} (F: T -> nat) (xs: seq T) (def: T) (i k: nat),
+      (forall i, i < (size xs).-1 -> F (nth def xs i) <= F (nth def xs i.+1)) ->
+      (i + k <= (size xs).-1) ->
+      F (nth def xs i) <= F (nth def xs (i+k)).
+  Proof.
+    intros T F r x i k ALL SIZE.
+    generalize dependent i. generalize dependent k.
+    induction k; intros; first by rewrite addn0 leqnn.
+    specialize (IHk i.+1); exploit IHk; [by rewrite addSnnS | intro LE].
+    apply leq_trans with (n := F (nth x r (i.+1)));
+      last by rewrite -addSnnS.
+    apply ALL, leq_trans with (n := i + k.+1); last by ins.
+      by rewrite addnS ltnS leq_addr.
+  Qed.
+  
 End Sorting.
\ No newline at end of file