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.

Module ScheduleConstruction.

  Import Job ArrivalSequence UniprocessorSchedule.

 (* In this section, we construct a schedule recursively by augmenting prefixes. *)
  Section ConstructionFromPrefixes.

    Context {Job: eqType}.

    (* Let arr_seq be any arrival sequence.*)
    Variable arr_seq: arrival_sequence Job.

    (* Assume we are given a function that takes an existing schedule prefix
       up to interval [0, t) and returns what should be scheduled at time t. *)

    Variable build_schedule:
      schedule Job time option Job.

    (* Then, starting from a base schedule, ... *)
    Variable base_sched: schedule Job.

    (* ...we can update individual times using the build_schedule function, ... *)
    Definition update_schedule (prev_sched: schedule Job)
                               (t_next: time) : schedule Job :=
      fun t
        if t == t_next then
          build_schedule prev_sched t
        else prev_sched t.

    (* ...which recursively generates schedule prefixes up to time t_max. *)
    Fixpoint schedule_prefix (t_max: time) : schedule Job :=
      if t_max is t_prev.+1 then
        update_schedule (schedule_prefix t_prev) t_prev.+1
        update_schedule base_sched 0.

    (* Based on the schedule prefixes, we construct a complete schedule. *)
    Definition build_schedule_from_prefixes := fun tschedule_prefix t t.

    (* In this section, we prove some lemmas about the construction. *)
    Section Lemmas.

      (* Let sched be the generated schedule. *)
      Let sched := build_schedule_from_prefixes.

      (* First, we show that the scheduler preserves its prefixes. *)
      Lemma prefix_construction_same_prefix:
         t t_max,
          t t_max
          schedule_prefix t_max t = sched t.

      Section ServiceDependent.

        (* If the generation function only depends on the service
         received by jobs during the schedule prefix, ...*)

        Hypothesis H_depends_only_on_service:
           sched1 sched2 t,
            ( j, service sched1 j t = service sched2 j t)
            build_schedule sched1 t = build_schedule sched2 t.

        (* ...then we can prove that the final schedule, at any time t,
         is exactly the result of the construction function. *)

        Lemma service_dependent_schedule_construction:
            sched t = build_schedule sched t.

      End ServiceDependent.

      Section PrefixDependent.

        (* If the generation function only depends on the schedule prefix, ... *)
        Hypothesis H_depends_only_on_prefix:
           (sched1 sched2: schedule Job) t,
            ( t0, t0 < t sched1 t0 = sched2 t0)
            build_schedule sched1 t = build_schedule sched2 t.

        (* ...then we can prove that the final schedule, at any time t,
         is exactly the result of the construction function. *)

        Lemma prefix_dependent_schedule_construction:
           t, sched t = build_schedule sched t.

      End PrefixDependent.

      Section ImmediateProperty.

        Variable P: option Job Prop.

        Hypothesis H_immediate_property:
           sched_prefix t, P (build_schedule sched_prefix t).

        Lemma immediate_property_of_schedule_construction:
           t, P (sched t).

      End ImmediateProperty.

    End Lemmas.

  End ConstructionFromPrefixes.

End ScheduleConstruction.