From prosa.analysis Require Export facts.model.service_of_jobs.
From prosa Require Export model.preemption.fully_preemptive.

From probsa.rt.model Require Export abort_readiness.
From probsa.rt.model Require Export carry_in.
From probsa.rt.model.assumptions
     Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.

Local Open Scope nat_scope.

Section CompletionTimeExists.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {FP : FP_policy Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Hypothesis H_transitive_priorities : transitive hep_task.

  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

  Variable sched : pr_schedule μ (ideal.processor_state Job).
  Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
  Hypothesis H_respects_policy_at_preemption_point :
    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
  Hypothesis H_pr_jobs_must_be_ready_to_execute :
    pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.

  Hypothesis H_pr_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
  Hypothesis H_pr_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute sched.
  Hypothesis H_pr_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.

  Variable tsk : Task.
  Let V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work].

  Section StepByStepProof.

    Variable ω : Ω.

    Variables (t : instant) (Δ : duration).
    Hypothesis H_non_empty : 0 < Δ.

    Hypothesis H_workload_is_consumed :
      V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω ≤ Δ.

    Let ARR1 := [eta pr_arrivals_between 0 t].
    Let ARR2 := [eta pr_arrivals_between t (t + Δ)].

    Let P1 (ω : Ω) (j : Job) := before_deadline j ω t && hep_task (job_task j) tsk.
    Let P2 (j : Job) := hep_task (job_task j) tsk.

    Variable j : Job.
    Hypothesis H_hep_tsk : hep_task (job_task j) tsk.
    Hypothesis H_arrival : job_arrival j ω = Some t.
    Hypothesis H_deadline_in_future : t + Δ ≤ odflt0 (job_deadline j) ω.
    Hypothesis H_not_completed : ~~ pr_completed_by sched j (t + Δ) ω.

    Section Step1.

      Remark scheduled_if_before_deadline :
        ∀ j ω t,
          scheduled_at (sched ω) j t →
          before_deadline j ω t.
      Proof.
        intros.
        apply H_pr_jobs_must_be_ready_to_execute in H.
        move: H ⇒ /andP [PENDT DEADT].
        unfold before_deadline.
        by apply DEADT.
      Qed.

      Local Lemma some_job_scheduled :
        ∀ to,
          t ≤ to < t + Δ →
          ∃ j, scheduled_at (sched ω) j to ∧ (P1 ω j ∧ j \in ARR1 ω ∨ P2 j ∧ j \in ARR2 ω).
      Proof.
        intros to LEQ.
        have [δtm EQ]: ∃ δtm, (to = t + δtm)%nat by (∃ (to - t)%nat; ssrlia).
        subst to.

        have [jhp [SCHEDhp HEP]] :
          ∃ jhp,
            scheduled_at (sched ω) jhp (t + δtm)%nat
            ∧ hep_task (job_task jhp) tsk.
        { destruct (sched ω (t + δtm)%nat) as [s| ] eqn:SCHED; last first.
          { move: (H_work_conserving ω j (t + δtm)%N) ⇒ WORK.
            feed_n 2%nat WORK.
            { by ∃ t; apply H_arrivals_consistent. }
            { apply/andP; split; first (apply/andP; split); first (apply/andP; split).
              { by rewrite /has_arrived /prosa.behavior.job.job_arrival /sample0_arrivals //= H_arrival //= leq_addr. }
              { by apply: incompletion_monotonic; last apply H_not_completed; ssrlia. }
              { move: H_deadline_in_future.
                rewrite /prosa.behavior.job.job_deadline /sample0_deadlines /job_deadline
                        /job_deadline_from_task_deadline //= H_arrival //=.
                by eapply leq_trans; ssrlia.
              }
              { by rewrite scheduled_at_def SCHED. }
            }
            exfalso; move: WORK ⇒ [c SCHEDc].
            by rewrite scheduled_at_def SCHED in SCHEDc.
          }
          { destruct (s == j) eqn:EQ.
            { by move: EQ ⇒ /eqP EQ; subst; ∃ j; split; rewrite ?scheduled_at_def ?SCHED. }
            { ∃ s; split.
              { by rewrite scheduled_at_def SCHED. }
              { move: (H_respects_policy_at_preemption_point ω j s (t + δtm)%N) ⇒ RESP.
                feed_n 4%nat RESP.
                { by ∃ t; apply H_arrivals_consistent. }
                { by rewrite /preemption_time SCHED. }
                { apply/andP; split; first (apply/andP; split); first (apply/andP; split).
                  { by rewrite /has_arrived /prosa.behavior.job.job_arrival /sample0_arrivals //= H_arrival //= leq_addr. }
                  { by apply: incompletion_monotonic; last apply H_not_completed; ssrlia. }
                  { move: H_deadline_in_future.
                    rewrite /prosa.behavior.job.job_deadline /sample0_deadlines /job_deadline
                            /job_deadline_from_task_deadline //= H_arrival //=.
                    by eapply leq_trans; ssrlia.
                  }
                  { rewrite scheduled_at_def SCHED.
                    apply/negP ⇒ /eqP EQS; inversion EQS; subst.
                    by rewrite eq_refl in EQ.
                  }
                }
                { by rewrite scheduled_at_def SCHED. }
                by eapply H_transitive_priorities; [apply RESP | apply H_hep_tsk].
              }
            }
          }
        }

        ∃ jhp; split ⇒ //.
        have [Ao ARRo] := scheduled_at_implies_exists_arrival_time
                            sched H_pr_jobs_come_from_arrival_sequence _ _ _ SCHEDhp.
        have [GE|LTAo] := leqP t Ao.
        { right; split ⇒ //; unfold P2, ARR2.
          apply: arrived_between_implies_in_arrivals ⇒ //.
          { by apply pr_consistent_arrival_times. }
          { by ∃ Ao; apply H_arrivals_consistent. }
          { by apply: scheduled_at_implies_arrived_between; (try exact SCHEDhp); (try exact ARRo). }
        }
        { left; split.
          { apply/andP; split ⇒ //.
            apply: before_deadline_monotone; move: LEQ ⇒ /andP [LEQ _]; first apply LEQ.
            by apply scheduled_if_before_deadline.
          }
          { apply: arrived_between_implies_in_arrivals.
            { by apply pr_consistent_arrival_times. }
            { by ∃ Ao; apply H_arrivals_consistent. }
            { by apply: scheduled_at_implies_arrived_between'; eauto 1. }
          }
        }
      Qed.

    End Step1.

    Section Step2.

      Remark pr_service_of_jobs_cat :
        ∀ (P : pred Job) (jobs : seq Job) (t1 t2 t : instant) (ω : Ω),
          t1 ≤ t ≤ t2 →
          service_of_jobs (sched ω) P jobs t1 t2
          = service_of_jobs (sched ω) P jobs t1 t
            + service_of_jobs (sched ω) P jobs t t2.
      Proof.
        intros; rewrite /service_of_jobs -big_split //=.
        apply eq_big ⇒ //.
        by intros s Ps; rewrite service_during_cat //.
      Qed.

      Local Lemma lower_bound_on_service_of_jobs :
        Δ ≤
          service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
          + service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
      Proof.
        have CONS: @consistent_arrival_times _ (fun j ⇒ odflt0 (job_arrival j) ω) (arr_seq ω)
          by apply pr_consistent_arrival_times.
        have F1 := some_job_scheduled.
        clear H_deadline_in_future H_hep_tsk H_arrival
              H_not_completed H_non_empty H_workload_is_consumed.

        intros; induction Δ as [ | δ IHδ]; first by done.
        rewrite -addn1 !addnA; apply: leq_trans.
        { erewrite leq_add2r; apply IHδ.
          { intros to LEQ; specialize (F1 to).
            feed F1.
            { move: LEQ ⇒ /andP [T1 T2]; apply/andP; split; first by done.
              by apply: leq_trans; [apply T2 | rewrite addnS]. }
            destruct F1 as [jo [H0 H1]].
            ∃ jo; split ⇒ //.
            { destruct H1; first by left.
              right; split; first by apply H.
              destruct H.
              apply: arrived_between_implies_in_arrivals.
              { by apply pr_consistent_arrival_times. }
              { by apply: H_pr_jobs_come_from_arrival_sequence; eauto 1. }
              { apply @in_arrivals_implies_arrived_between
                  with (H := fun j ⇒ odflt0 (job_arrival j) ω) in H1;
                  last by apply pr_consistent_arrival_times.
                move: H1 ⇒ /andP [H21 H22]; apply/andP; split ⇒ //.
                apply: leq_ltn_trans; last first.
                { by move: LEQ ⇒ /andP [_ LEQ]; apply LEQ. }
                { by apply: scheduled_at_implies_arrived_between''; eauto 1. }
              }
            }
          }
        }
        { rewrite (pr_service_of_jobs_cat _ _ _ (t + δ + 1) (t + δ));
            last by apply/andP; split; apply leq_addr.
          rewrite -!addnA leq_add2l !addnA [X in (_ ≤ X)]addnC /ARR2 //= -[δ.+1]addn1 addnA.
          unshelve erewrite (@service_of_jobs_cat_scheduling_interval
                               Job (fun j ⇒ odflt0 (job_arrival j) ω) _ (arr_seq ω) CONS
                               (sched ω) _ _ _ (t + δ + 1) (t + δ));
            first last; try by apply H_pr_jobs_must_arrive_to_execute.
          { by apply/andP; split; rewrite leq_addr // leq_addr. }
          rewrite -!addnA leq_add2l !addnA.
          specialize (F1 (t + δ)); feed F1; first by apply/andP; split; ssrlia.

          destruct F1 as [jo [SCHEDo [[HEPo ARRo] | [HEPo ARRo]]]].
          { rewrite -addn1 leq_add // addn1 addn1; apply/sum_seq_cond_gt0P.
            ∃ jo; split; first by apply ARRo.
            split; first by apply HEPo.
            apply/sum_seq_cond_gt0P; ∃ (t + δ); rewrite mem_index_iota; split.
            { by apply/andP; split ⇒ //. }
            { by split ⇒ //; apply ideal_proc_model_ensures_ideal_progress. }
          }
          { rewrite -addn1 addnC leq_add // -service_of_jobs_cat_arrival_interval; last first.
            { by apply/andP; split; rewrite leq_addr. }
            apply/sum_seq_cond_gt0P; ∃ jo; split.
            { rewrite /ARR2 -addn1 addnA in ARRo.
              by rewrite addnA addn0; apply ARRo.
            }
            { split; first by apply HEPo.
              apply/sum_seq_cond_gt0P; ∃ (t + δ); rewrite mem_index_iota; split.
              { by apply/andP; split ⇒ //; rewrite !addn0 addn1. }
              { by split ⇒ //; apply ideal_proc_model_ensures_ideal_progress. }
            }
          }
        }
      Qed.

    End Step2.

    Section Step3.

      Local Lemma workload_le_service :
        V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω
        ≤ service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
          + service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
      Proof.
        move_neq_up TEMP.
        move: (H_workload_is_consumed) ⇒ LEm2; move_neq_down LEm2.
        apply: leq_ltn_trans.
        apply: lower_bound_on_service_of_jobs; eauto 1.
        by move_neq_up LEm2; move_neq_down TEMP.
      Qed.

    End Step3.

    Section Step4.

      Remark summand_wise_bound_implies_eq :
        ∀ (a b c d : nat),
          a ≥ c →
          b ≥ d →
          a + b ≤ c + d →
          a = c ∧ b = d.
      Proof.
        clear; intros × LE1 LE2 LE3.
        interval_to_duration d b k.
        interval_to_duration c a l.
        rewrite [_ d _]addnC addnA leq_add2r in LE3.
        destruct l, k.
        { by rewrite !addn0. }
        { rewrite -addSnnS addn0 in LE3.
          apply leq_addk in LE3.
          by rewrite ltnn in LE3. }
        { rewrite -addSnnS addn0 in LE3.
          apply leq_addk in LE3.
          by rewrite ltnn in LE3.
        }
        { rewrite -addSnnS -addn1 in LE3.
          apply leq_addk, leq_addk in LE3.
          rewrite -addSnnS in LE3.
          apply leq_addk in LE3.
          by rewrite ltnn in LE3.
        }
      Qed.

      Lemma carry_in_workload_eq_service_of_jobs :
        V t ω = service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
        ∧ pr_workload_of_hep_tasks tsk t (t + Δ) ω = service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ).
      Proof.
        have NEQ :
          Δ ≤ service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
              + service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ)
          by apply: lower_bound_on_service_of_jobs; eauto 1.

        have NEQ2 :
          V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω
          ≤ service_of_jobs (sched ω) (P1 ω) (ARR1 ω) t (t + Δ)
            + service_of_jobs (sched ω) P2 (ARR2 ω) t (t + Δ)
          by apply: workload_le_service; eauto 1.

        apply summand_wise_bound_implies_eq in NEQ2; last first.
        { apply service_of_jobs_le_workload.
          { by apply ideal_proc_model_provides_unit_service. }
          { by apply H_pr_completed_jobs_dont_execute. }
        }
        { rewrite /service_of_jobs big_mkcond //= [X in (_ ≤ X)]big_mkcond //=.
          rewrite big_seq //= [X in (_ ≤ X)]big_seq //= -big_mkcondr -big_mkcondr //=.
          apply leq_sum ⇒ jo /andP [INo /andP [BDo HEPo]].
          apply leq_subRL_impl; rewrite addnC service_cat; last by rewrite leq_addr.
          apply pr_service_bounded_by_pr_job_cost; eauto 1.
          by apply: ideal_proc_model_provides_unit_service.
        }
        by done.
      Qed.

    End Step4.

    Section Step5.

      Local Lemma j_completed :
        pr_completed_by sched j (t + Δ) ω.
      Proof.
        have CONS: @consistent_arrival_times _ (fun j ⇒ odflt0 (job_arrival j) ω) (arr_seq ω)
          by apply pr_consistent_arrival_times.
        edestruct carry_in_workload_eq_service_of_jobs as [EQ1 EQ2]; eauto 1.
        eapply workload_eq_service_impl_all_jobs_have_completed with (j0 := j) in EQ2; eauto 1 ⇒ //.
        { by apply: ideal_proc_model_provides_unit_service. }
        { by apply H_pr_jobs_must_arrive_to_execute. }
        { apply: arrived_between_implies_in_arrivals.
          { by apply pr_consistent_arrival_times. }
          { by ∃ t; apply H_arrivals_consistent. }
          rewrite /arrived_between /prosa.behavior.job.job_arrival //= H_arrival //=.
          by apply/andP; split ⇒ //; rewrite -addn1 leq_add.
        }
      Qed.

    End Step5.

  End StepByStepProof.

  Variable ω : Ω.

  Variables (t : instant) (Δ : duration).
  Hypothesis H_non_empty : 0 < Δ.

  Hypothesis H_workload_is_consumed :
    V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω ≤ Δ.

  Lemma completion_time_exists :
    ∃ δ,
      0 < δ ≤ Δ
      ∧ ∀ j,
        hep_task (job_task j) tsk →
        job_arrival j ω = Some t →
        t + δ ≤ odflt0 (job_deadline j) ω →
        pr_completed_by sched j (t + δ) ω.
  Proof.
    have CONS: @consistent_arrival_times _ (fun j ⇒ odflt0 (job_arrival j) ω) (arr_seq ω)
      by apply pr_consistent_arrival_times.
    have EX : ∃ Δ, (Δ > 0) && (V t ω + pr_workload_of_hep_tasks tsk t (t + Δ) ω ≤ Δ).
    { by ∃ Δ; apply/andP; split. }
    move: (ex_minnP EX) ⇒ [δm /andP [POSm LEm] MINm].
    ∃ δm; split.
    { by apply/andP; split; [ | apply MINm; apply/andP; split] ⇒ //. }
    intros j PRIO ARR DEAD.
    apply/negPn/negP ⇒ NCOMP; move: (NCOMP) ⇒ /negP T; apply: T.
    by apply j_completed; eauto 2.
  Qed.

End CompletionTimeExists.