Library rt.model.schedule.uni.susp.last_execution

Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* In this file, we show how to compute the time instant after the last
   execution of a job and prove several lemmas about that instant. This
   notion is crucial for defining suspension intervals. *)

Module LastExecution.

  Export Job UniprocessorSchedule.

  (* In this section we define the time after the last execution of a job (if exists). *)
  Section TimeAfterLastExecution.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.

    (* Consider any uniprocessor schedule. *)
    Variable sched: schedule Job.

    (* For simplicity, let's define some local names. *)
    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.

    Section Defs.

      (* Let j be any job in the arrival sequence. *)
      Variable j: Job.

      (* Next, we will show how to find the time after the most recent
         execution of a given job j in the interval [job_arrival j, t).
         (Note that this instant can be time t itself.) *)

      Variable t: time.

      (* Let scheduled_before denote whether job j was scheduled in the interval [0, t). *)
      Let scheduled_before :=
        [ t0: 'I_t, job_scheduled_at j t0].

      (* In case j was scheduled before, we define the last time in which j was scheduled. *)
      Let last_time_scheduled :=
        \max_(t_last < t | job_scheduled_at j t_last) t_last.

      (* Then, the time after the last execution of job j in the interval [0, t), if exists,
           (a) immediately after the last time in which job j was scheduled, or,
           (b) if j was never scheduled, at the arrival time of j. *)

      Definition time_after_last_execution :=
        if scheduled_before then
          last_time_scheduled + 1
        else job_arrival j.

    End Defs.

    (* Next, we prove lemmas about the time after the last execution. *)
    Section Lemmas.

      (* Assume that jobs do not execute before they arrived. *)
      Hypothesis H_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute job_arrival sched.

      (* Let j be any job. *)
      Variable j: Job.

      (* In this section, we show that the time after the last execution occurs
           no earlier than the arrival of the job. *)

      Section JobHasArrived.

        (* Then, the time following the last execution of job j in the
             interval [0, t) occurs no earlier than the arrival of j. *)

        Lemma last_execution_after_arrival:
            has_arrived job_arrival j (time_after_last_execution j t).
          unfold time_after_last_execution, has_arrived; intros t.
          case EX: [ _, _]; last by done.
          move: EX ⇒ /existsP [t0 SCHED].
          apply leq_trans with (n := t0 + 1);
            last by rewrite leq_add2r; apply leq_bigmax_cond.
          apply leq_trans with (n := t0); last by rewrite addn1.
            by apply H_jobs_must_arrive_to_execute.

      End JobHasArrived.

      (* Next, we establish the monotonicity of the function. *)
      Section Monotonicity.

        (* Let t1 be any time no earlier than the arrival of job j. *)
        Variable t1: time.
        Hypothesis H_after_arrival: has_arrived job_arrival j t1.

        (* Then, (time_after_last_execution j) grows monotonically
             after that point. *)

        Lemma last_execution_monotonic:
            t1 t2
            time_after_last_execution j t1 time_after_last_execution j t2.
          rename H_jobs_must_arrive_to_execute into ARR.
          intros t2 LE12.
          rewrite /time_after_last_execution.
          case EX1: [ _, _].
            move: EX1 ⇒ /existsP [t0 SCHED0].
            have EX2: [ t:'I_t2, job_scheduled_at j t].
              have LT: t0 < t2 by apply: (leq_trans _ LE12).
                by apply/existsP; (Ordinal LT).
            rewrite EX2 2!addn1.
            set m1 := \max_(_ < t1 | _)_.
            have LTm1: m1 < t2.
              apply: (leq_trans _ LE12).
                by apply bigmax_ltn_ord with (i0 := t0).
            apply leq_ltn_trans with (n := Ordinal LTm1); first by done.
              by apply leq_bigmax_cond, (bigmax_pred _ _ t0).
            case EX2: [ _, _]; last by done.
            move: EX2 ⇒ /existsP [t0 SCHED0].
            set m2 := \max_(_ < t2 | _)_.
            rewrite addn1 ltnW // ltnS.
            have SCHED2: scheduled_at sched j m2 by apply (bigmax_pred _ _ t0).
              by apply ARR in SCHED2.

      End Monotonicity.

      (* Next, we prove that the function is idempotent. *)
      Section Idempotence.

        (* The time after the last execution of job j is an idempotent function. *)
        Lemma last_execution_idempotent:
            time_after_last_execution j (time_after_last_execution j t)
            = time_after_last_execution j t.
          rename H_jobs_must_arrive_to_execute into ARR.
          intros t.
          rewrite {2 3}/time_after_last_execution.
          case EX: [ _,_].
            move: EX ⇒ /existsP [t0 SCHED].
            rewrite /time_after_last_execution.
            set ex := [ t0, _].
            have EX': ex.
              apply/existsP; rewrite addn1.
               (Ordinal (ltnSn _)).
                by apply bigmax_pred with (i0 := t0).
            rewrite EX'; f_equal.
            rewrite addn1; apply/eqP.
            set m := \max_(_ < t | _)_.
            have LT: m < m.+1 by done.
            rewrite eqn_leq; apply/andP; split.
              rewrite -ltnS; apply bigmax_ltn_ord with (i0 := Ordinal LT).
                by apply bigmax_pred with (i0 := t0).
              apply leq_trans with (n := Ordinal LT); first by done.
                by apply leq_bigmax_cond, bigmax_pred with (i0 := t0).
            apply negbT in EX; rewrite negb_exists in EX.
            move: EX ⇒ /forallP EX.
            rewrite /time_after_last_execution.
            set ex := [ _, _].
            suff EX': ex = false; first by rewrite EX'.
            apply negbTE; rewrite negb_exists; apply/forallP.
            intros x.
            apply/negP; intro SCHED.
            apply ARR in SCHED.
              by apply leq_ltn_trans with (p := job_arrival j) in SCHED;
                first by rewrite ltnn in SCHED.

      End Idempotence.

      (* Next, we show that time_after_last_execution is bounded by the identity function. *)
      Section BoundedByIdentity.

        (* Let t be any time no earlier than the arrival of j. *)
        Variable t: time.
        Hypothesis H_after_arrival: has_arrived job_arrival j t.

        (* Then, the time following the last execution of job j in the interval [0, t)
           occurs no later than time t. *)

        Lemma last_execution_bounded_by_identity:
          time_after_last_execution j t t.
          unfold time_after_last_execution.
          case EX: [ _, _]; last by done.
          move: EX ⇒ /existsP [t0 SCHED].
            by rewrite addn1; apply bigmax_ltn_ord with (i0 := t0).

      End BoundedByIdentity.

      (* In this section, we show that if the service received by a job
           remains the same, the time after last execution also doesn't change. *)

      Section SameLastExecution.

        (* Consider any time instants t and t'... *)
        Variable t t': time.

        (* which job j has received the same amount of service. *)
        Hypothesis H_same_service: service sched j t = service sched j t'.

        (* Then, we prove that the times after last execution relative to
             instants t and t' are exactly the same. *)

        Lemma same_service_implies_same_last_execution:
          time_after_last_execution j t = time_after_last_execution j t'.
          rename H_same_service into SERV.
          have IFF := same_service_implies_scheduled_at_earlier_times
                        sched j t t' SERV.
          rewrite /time_after_last_execution.
          rewrite IFF; case EX2: [ _, _]; [f_equal | by done].
          have EX1: [ x: 'I_t, job_scheduled_at j x] by rewrite IFF.
          clear IFF.
          move: t t' SERV EX1 EX2t1 t2; clear t t'.
          wlog: t1 t2 / t1 t2 ⇒ [EQ SERV EX1 EX2 | LE].
            by case/orP: (leq_total t1 t2); ins; [|symmetry]; apply EQ.

            set m1 := \max_(t < t1 | job_scheduled_at j t) t.
            set m2 := \max_(t < t2 | job_scheduled_at j t) t.
            moveSERV /existsP [t1' SCHED1'] /existsP [t2' SCHED2'].
            apply/eqP; rewrite eqn_leq; apply/andP; split.
              have WID := big_ord_widen_cond t2
                                             (fun xjob_scheduled_at j x) (fun xx).
                          rewrite /m1 /m2 {}WID //.
                          rewrite big_mkcond [\max_(t < t2 | _) _]big_mkcond.
                          apply leq_big_max; intros i _.
                          case AND: (_ && _); last by done.
                            by move: AND ⇒ /andP [SCHED _]; rewrite SCHED.
              destruct (leqP t2 m1) as [GEm1 | LTm1].
                apply leq_trans with (n := t2); last by done.
                  by apply ltnW, bigmax_ltn_ord with (i0 := t2').
              destruct (ltnP m2 t1) as [LTm2 | GEm2].
                apply leq_trans with (n := Ordinal LTm2); first by done.
                  by apply leq_bigmax_cond, bigmax_pred with (i0 := t2').
              have LTm2: m2 < t2 by apply bigmax_ltn_ord with (i0 := t2').
              have SCHEDm2: job_scheduled_at j m2 by apply bigmax_pred with (i0 := t2').
              exfalso; move: SERV ⇒ /eqP SERV.
              rewrite -[_ == _]negbK in SERV.
              move: SERV ⇒ /negP SERV; apply SERV; clear SERV.
              rewrite neq_ltn; apply/orP; left.
              rewrite /service /service_during.
              rewritebig_cat_nat with (n := m2) (p := t2);
                [simpl | by done | by apply ltnW].
              rewrite -addn1; apply leq_add; first by apply extend_sum.
              destruct t2; first by rewrite ltn0 in LTm1.
              rewrite big_nat_recl; last by done.
                by rewrite /service_at -/job_scheduled_at SCHEDm2.

      End SameLastExecution.

      (* In this section, we show that the service received by a job
         does not change since the last execution. *)

      Section SameService.

        (* We prove that, for any time t, the service received by job j
           before (time_after_last_execution j t) is the same as the service
           by j before time t. *)

        Lemma same_service_since_last_execution:
            service sched j (time_after_last_execution j t) = service sched j t.
          intros t; rewrite /time_after_last_execution.
          case EX: [ _, _].
            move: EX ⇒ /existsP [t0 SCHED0].
            set m := \max_(_ < _ | _) _; rewrite addn1.
            have LTt: m < t by apply: (bigmax_ltn_ord _ _ t0).
            rewrite leq_eqVlt in LTt.
            move: LTt ⇒ /orP [/eqP EQ | LTt]; first by rewrite EQ.
            rewrite {2}/service/service_during.
            rewritebig_cat_nat with (n := m.+1);
              [simpl | by done | by apply ltnW].
            rewrite [X in _ + X]big_nat_cond [X in _ + X]big1 ?addn0 //.
            movei /andP [/andP [GTi LTi] _].
            apply/eqP; rewrite eqb0; apply/negP; intro BUG.
            have LEi: (Ordinal LTi) m by apply leq_bigmax_cond.
              by apply (leq_ltn_trans LEi) in GTi; rewrite ltnn in GTi.
            apply negbT in EX; rewrite negb_exists in EX.
            move: EX ⇒ /forallP ALL.
            rewrite /service /service_during.
            rewrite (ignore_service_before_arrival job_arrival) // big_geq //.
            rewrite big_nat_cond big1 //; movei /andP [/= LTi _].
            by apply/eqP; rewrite eqb0; apply (ALL (Ordinal LTi)).

      End SameService.

      (* In this section, we show that for any smaller value of service, we can
         always find the last execution that corresponds to that service. *)

      Section ExistsIntermediateExecution.

        (* Assume that job j has completed by time t. *)
        Variable t: time.
        Hypothesis H_j_has_completed: completed_by job_cost sched j t.

        (* Then, for any value of service less than the cost of j, ...*)
        Variable s: time.
        Hypothesis H_less_than_cost: s < job_cost j.

        (* ...there exists a last execution where the service received
           by job j equals s. *)

        Lemma exists_last_execution_with_smaller_service:
            service sched j (time_after_last_execution j t0) = s.
          have SAME := same_service_since_last_execution.
          rename H_jobs_must_arrive_to_execute into ARR.
          move: H_j_has_completed ⇒ /eqP COMP.
          feed (exists_intermediate_point (service sched j));
            first by apply service_is_a_step_function.
          moveEX; feed (EX (job_arrival j) t).
            feed (cumulative_service_implies_scheduled sched j 0 t);
              first by apply leq_ltn_trans with (n := s);
              last by rewrite -/(service _ _ _) COMP.
            move ⇒ [t' [/= LTt SCHED]].
            apply leq_trans with (n := t'); last by apply ltnW.
              by apply ARR in SCHED.
          feed (EX s).
            apply/andP; split; last by rewrite COMP.
            rewrite /service /service_during.
            by rewrite (ignore_service_before_arrival job_arrival) // big_geq.
          move: EX ⇒ [x_mid [_ SERV]]; x_mid.
          by rewrite -SERV SAME.

      End ExistsIntermediateExecution.

      (* In this section we prove that before the last execution the job
         must have received strictly less service. *)

      Section LessServiceBeforeLastExecution.

        (* Let t be any time... *)
        Variable t: time.

        (* ...and consider any earlier time t0 no earlier than the arrival of job j... *)
        Variable t0: time.
        Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.

        (* ...and before the last execution of job j (with respect to time t). *)
        Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.

        (* Then, we can prove that the service received by j before time t0
           is strictly less than the service received by j before time t. *)

        Lemma less_service_before_start_of_suspension:
          service sched j t0 < service sched j t.
          rename H_no_earlier_than_arrival into ARR, H_before_last_execution into LT.
          set ex := time_after_last_execution in LT.
          set S := service sched.
          case EX:([ t0:'I_t, scheduled_at sched j t0]); last first.
            rewrite /ex /time_after_last_execution EX in LT.
            apply leq_trans with (p := t0) in LT; last by done.
            by rewrite ltnn in LT.
            rewrite /ex /time_after_last_execution EX in LT.
            set m := (X in _ < X + 1) in LT.
            apply leq_ltn_trans with (n := S j m);
              first by rewrite -/m addn1 ltnS in LT; apply extend_sum.
            move: EX ⇒ /existsP [t' SCHED'].
            have LTt: m < t by apply bigmax_ltn_ord with (i0 := t').
            rewrite /S /service /service_during.
            rewritebig_cat_nat with (p := t) (n := m); [simpl | by done | by apply ltnW].
            rewrite -addn1 leq_add2l; destruct t; first by done.
            rewrite big_nat_recl //.
            apply leq_trans with (n := scheduled_at sched j m); last by apply leq_addr.
            rewrite lt0n eqb0 negbK.
            by apply bigmax_pred with (i0 := t').

      End LessServiceBeforeLastExecution.

    End Lemmas.

  End TimeAfterLastExecution.

End LastExecution.