Library rt.restructuring.model.processor.multiprocessor

(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.10.1 (October 2019)

----------------------------------------------------------------------------- *)

From mathcomp Require Export fintype.
From rt.restructuring.behavior Require Export all.

Section Schedule.

  Variable Job: JobType.
  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.

  Global Program Instance multiproc_state : ProcessorState Job (identical_state) :=
    {
      scheduled_on j s (cpu : processor num_cpus) := scheduled_in j (s cpu);
      service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
    }.
  Next Obligation.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  H0 : ~~
       ~~
       FiniteQuant.quant0b (T:=ordinal_finType num_cpus)
         (fun c : 'I_num_cpus =>
          FiniteQuant.ex (T:=ordinal_finType num_cpus)
            (, scheduled_in j (s c)) c)
  ============================
  \sum_(cpu < num_cpus) service_in j (s cpu) = 0

----------------------------------------------------------------------------- *)

    move: j s H0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 83)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  ============================
  forall (j : Job) (s : identical_state),
  ~~
  ~~
  FiniteQuant.quant0b (T:=ordinal_finType num_cpus)
    (fun c : 'I_num_cpus =>
     FiniteQuant.ex (T:=ordinal_finType num_cpus) (, scheduled_in j (s c)) c) ->
  \sum_(cpu < num_cpus) service_in j (s cpu) = 0

----------------------------------------------------------------------------- *)

    move⇒ j s /existsP Hsched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  ============================
  \sum_(cpu < num_cpus) service_in j (s cpu) = 0

----------------------------------------------------------------------------- *)

    apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 178)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  ============================
  \sum_(cpu < num_cpus) service_in j (s cpu) == 0

----------------------------------------------------------------------------- *)

    rewrite sum_nat_eq0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 184)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  ============================
  [forall (i | true), service_in j (s i) == 0]

----------------------------------------------------------------------------- *)

    apply/forallP=>/= c.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 210)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  c : 'I_num_cpus
  ============================
  service_in j (s c) == 0

----------------------------------------------------------------------------- *)

    rewrite service_implies_scheduled//.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 222)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  c : 'I_num_cpus
  ============================
  ~~ scheduled_in j (s c)

----------------------------------------------------------------------------- *)

    case: (boolP (scheduled_in _ _))=>//= Habs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 321)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  Hsched : ~ (exists x : ordinal_finType num_cpus, scheduled_in j (s x))
  c : 'I_num_cpus
  Habs : scheduled_in j (s c)
  ============================
  false

----------------------------------------------------------------------------- *)

    exfalso; apply: Hsched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 328)
  
  Job : JobType
  processor_state : Type
  H : ProcessorState Job processor_state
  num_cpus : nat
  j : Job
  s : identical_state
  c : 'I_num_cpus
  Habs : scheduled_in j (s c)
  ============================
  exists x : ordinal_finType num_cpus, scheduled_in j (s x)

----------------------------------------------------------------------------- *)

      by ∃ c.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Defined.
End Schedule.