Library rt.restructuring.model.processor.spin
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
From rt.restructuring.behavior Require Export all.
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: JobType.
Inductive processor_state :=
Idle
| Spin (j : Job)
| Progress (j : Job).
Section Service.
Variable j : Job.
Definition scheduled_on (s : processor_state) (_ : unit) : 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.
Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
{
scheduled_on := scheduled_on;
service_in := service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
j : Job
s : processor_state
H : ~~ [exists c, scheduled_on j s c]
============================
service_in j s = 0
----------------------------------------------------------------------------- *)
move: H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Job : JobType
j : Job
s : processor_state
============================
~~ [exists c, scheduled_on j s c] -> service_in j s = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' /existsP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
j, j' : Job
============================
~ (exists _ : unit_finType, j' == j) -> (j' == j) = 0
----------------------------------------------------------------------------- *)
rewrite /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 377)
Job : JobType
j, j' : Job
============================
~ (exists _ : unit_finType, j' == j) -> (if j' == j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP=>//=_[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 458)
Job : JobType
j, j' : Job
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.
Variable Job: JobType.
Inductive processor_state :=
Idle
| Spin (j : Job)
| Progress (j : Job).
Section Service.
Variable j : Job.
Definition scheduled_on (s : processor_state) (_ : unit) : 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.
Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
{
scheduled_on := scheduled_on;
service_in := service_in
}.
Next Obligation.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
j : Job
s : processor_state
H : ~~ [exists c, scheduled_on j s c]
============================
service_in j s = 0
----------------------------------------------------------------------------- *)
move: H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Job : JobType
j : Job
s : processor_state
============================
~~ [exists c, scheduled_on j s c] -> service_in j s = 0
----------------------------------------------------------------------------- *)
case: s=>//= j' /existsP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
j, j' : Job
============================
~ (exists _ : unit_finType, j' == j) -> (j' == j) = 0
----------------------------------------------------------------------------- *)
rewrite /nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 377)
Job : JobType
j, j' : Job
============================
~ (exists _ : unit_finType, j' == j) -> (if j' == j then 1 else 0) = 0
----------------------------------------------------------------------------- *)
case: ifP=>//=_[].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 458)
Job : JobType
j, j' : Job
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Defined.
End State.