Library prosa.analysis.facts.tdma
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.model.schedule.tdma.
Require Import prosa.util.all.
From mathcomp Require Import div.
In this section, we define the properties of TDMA and prove some basic lemmas.
Consider any task set ts...
... with a TDMA policy
Consider any task in ts
Assume task_time_slot is valid time slot
Obviously, the TDMA cycle is greater or equal than any task time slot which is
in TDMA cycle
Lemma TDMA_cycle_ge_each_time_slot:
TDMA_cycle ts ≥ task_time_slot task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 29)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <= TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /TDMA_cycle (big_rem task) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <=
addn_comoid (task_time_slot task)
(\big[addn_comoid/0]_(y <- rem (T:=Task) task ts) task_time_slot y)
----------------------------------------------------------------------------- *)
apply:leq_trans; last by exact: leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 93)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <= task_time_slot task
----------------------------------------------------------------------------- *)
by apply leqnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
TDMA_cycle ts ≥ task_time_slot task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 29)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <= TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /TDMA_cycle (big_rem task) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <=
addn_comoid (task_time_slot task)
(\big[addn_comoid/0]_(y <- rem (T:=Task) task ts) task_time_slot y)
----------------------------------------------------------------------------- *)
apply:leq_trans; last by exact: leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 93)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task <= task_time_slot task
----------------------------------------------------------------------------- *)
by apply leqnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Thus, a TDMA cycle is always positive
Lemma TDMA_cycle_positive:
TDMA_cycle ts > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 < TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
TDMA_cycle ts > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 < TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Slot offset is less then cycle
Lemma Offset_lt_cycle:
task_slot_offset ts task < TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_slot_offset ts task < TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_slot_offset /TDMA_cycle big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
- apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 64)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
forall i : Task,
true ->
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
intros× T.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 66)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
i : Task
T : true
============================
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (slot_order i task);auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
- rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts | i != task) task_time_slot i <
task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
rewrite -subn_gt0 -addnBA.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 143)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 <
task_time_slot task +
(\sum_(i <- ts | i != task) task_time_slot i -
\sum_(i <- ts | i != task) task_time_slot i)
subgoal 2 (ID 144) is:
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
rewrite subnn addn0 //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 154)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 < task_time_slot task
subgoal 2 (ID 144) is:
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
exact: time_slot_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
easy.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
task_slot_offset ts task < TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_slot_offset ts task < TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_slot_offset /TDMA_cycle big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
- apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 64)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
forall i : Task,
true ->
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
intros× T.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 66)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
i : Task
T : true
============================
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 63) is:
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (slot_order i task);auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts)
(if prev_task != task then task_time_slot prev_task else 0) <
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
- rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts | i != task) task_time_slot i <
task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
rewrite -subn_gt0 -addnBA.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 143)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 <
task_time_slot task +
(\sum_(i <- ts | i != task) task_time_slot i -
\sum_(i <- ts | i != task) task_time_slot i)
subgoal 2 (ID 144) is:
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
rewrite subnn addn0 //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 154)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
0 < task_time_slot task
subgoal 2 (ID 144) is:
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
exact: time_slot_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts | i != task) task_time_slot i <=
\sum_(i <- ts | i != task) task_time_slot i
----------------------------------------------------------------------------- *)
easy.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
For a task, the sum of its slot offset and its time slot is
less then or equal to cycle.
Lemma Offset_add_slot_leq_cycle:
task_slot_offset ts task + task_time_slot task ≤ TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_slot_offset /TDMA_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task + task_time_slot task <=
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
rewrite addnC (bigD1_seq task) //=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 74)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task +
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task <=
task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
rewrite leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 123)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task <= \sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 132)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
replace (\sum_(i <- ts | i != task) task_time_slot i)
with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 153)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(i <- ts) (if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 155)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
forall i : Task,
true ->
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
intros×T.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 157)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
i : Task
T : true
============================
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
case (slot_order i task);auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 150)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
by rewrite -big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
uniq ts
----------------------------------------------------------------------------- *)
apply (set_uniq ts).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TimeSlotFacts.
task_slot_offset ts task + task_time_slot task ≤ TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_slot_offset /TDMA_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task + task_time_slot task <=
\sum_(tsk <- ts) task_time_slot tsk
----------------------------------------------------------------------------- *)
rewrite addnC (bigD1_seq task) //=.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 74)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
task_time_slot task +
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task <=
task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
rewrite leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 123)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
task_time_slot prev_task <= \sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 132)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
replace (\sum_(i <- ts | i != task) task_time_slot i)
with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 153)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\big[addn_monoid/0]_(i <- ts)
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
\sum_(i <- ts) (if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 155)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
forall i : Task,
true ->
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
intros×T.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 157)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
i : Task
T : true
============================
(if slot_order i task && (i != task) then task_time_slot i else 0) <=
(if i != task then task_time_slot i else 0)
subgoal 2 (ID 150) is:
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
case (slot_order i task);auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 150)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
\sum_(i <- ts) (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
subgoal 2 (ID 97) is:
uniq ts
----------------------------------------------------------------------------- *)
by rewrite -big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
============================
uniq ts
----------------------------------------------------------------------------- *)
apply (set_uniq ts).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TimeSlotFacts.
Now we prove that no two tasks share the same time slot at any time.
Consider any task in ts
Assume task_time_slot is valid time slot
Assume that slot order is total...
Hypothesis slot_order_total:
total_slot_order ts.
(*..., antisymmetric... *)
Hypothesis slot_order_antisymmetric:
antisymmetric_slot_order ts.
(*... and transitive. *)
Hypothesis slot_order_transitive:
transitive_slot_order.
total_slot_order ts.
(*..., antisymmetric... *)
Hypothesis slot_order_antisymmetric:
antisymmetric_slot_order ts.
(*... and transitive. *)
Hypothesis slot_order_transitive:
transitive_slot_order.
Then, we can prove that the difference value between two offsets is
at least a slot
Lemma relation_offset:
∀ tsk1 tsk2, tsk1 \in ts →
tsk2 \in ts →
slot_order tsk1 tsk2 →
tsk1 != tsk2 →
task_slot_offset ts tsk2 ≥
task_slot_offset ts tsk1 + task_time_slot tsk1 .
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
============================
forall tsk1 tsk2 : Task,
tsk1 \in ts ->
tsk2 \in ts ->
slot_order tsk1 tsk2 ->
tsk1 != tsk2 ->
task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2
----------------------------------------------------------------------------- *)
Proof.
intros× IN1 IN2 ORDER NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2
----------------------------------------------------------------------------- *)
rewrite /task_slot_offset big_mkcond addnC/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
\sum_(prev_task <- ts | slot_order prev_task tsk2 && (prev_task != tsk2))
task_time_slot prev_task
----------------------------------------------------------------------------- *)
replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 105)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
rewrite leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 111)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
apply leq_sum_seq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 112)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
forall i : Task,
i \in ts ->
true ->
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
intros× IN T.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 115)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
============================
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (slot_order i tsk1)eqn:SI2;auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 129)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
============================
(if true && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (i==tsk1)eqn:IT2;auto;simpl.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 195)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
============================
task_time_slot i <=
(if slot_order i tsk2 && true && (i != tsk2) then task_time_slot i else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (i==tsk2)eqn:IT1;simpl;auto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 210)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
IT1 : (i == tsk2) = true
============================
task_time_slot i <=
(if slot_order i tsk2 && true && false then task_time_slot i else 0)
subgoal 2 (ID 211) is:
task_time_slot i <=
(if slot_order i tsk2 && true && true then task_time_slot i else 0)
subgoal 3 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 211)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
IT1 : (i == tsk2) = false
============================
task_time_slot i <=
(if slot_order i tsk2 && true && true then task_time_slot i else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- by rewrite (slot_order_transitive _ _ _ SI2 ORDER).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- symmetry.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite big_mkcond /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(i <- ts)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite→bigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 500)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
move/eqP /eqP in ORDER.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 622)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
NEQ : tsk1 != tsk2
ORDER : slot_order tsk1 tsk2 = true
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite ORDER //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 766)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
have TS2: (tsk1 != tsk2) = true .
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 769)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(tsk1 != tsk2) = true
subgoal 2 (ID 771) is:
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply /eqP;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 771)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite TS2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 811)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
task_time_slot tsk1 +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite eqn_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 816)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 825)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\big[addn_monoid/0]_(i <- ts)
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) ==
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 853)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\big[addn_monoid/0]_(i <- ts)
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply eq_bigr;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 854)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
forall i : Task,
true ->
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
----------------------------------------------------------------------------- *)
intros× T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 860)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
i : Task
T : true
============================
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
----------------------------------------------------------------------------- *)
case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ tsk1 tsk2, tsk1 \in ts →
tsk2 \in ts →
slot_order tsk1 tsk2 →
tsk1 != tsk2 →
task_slot_offset ts tsk2 ≥
task_slot_offset ts tsk1 + task_time_slot tsk1 .
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
============================
forall tsk1 tsk2 : Task,
tsk1 \in ts ->
tsk2 \in ts ->
slot_order tsk1 tsk2 ->
tsk1 != tsk2 ->
task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2
----------------------------------------------------------------------------- *)
Proof.
intros× IN1 IN2 ORDER NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2
----------------------------------------------------------------------------- *)
rewrite /task_slot_offset big_mkcond addnC/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
\sum_(prev_task <- ts | slot_order prev_task tsk2 && (prev_task != tsk2))
task_time_slot prev_task
----------------------------------------------------------------------------- *)
replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 105)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
rewrite leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 111)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(i <- ts)
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
apply leq_sum_seq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 112)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
forall i : Task,
i \in ts ->
true ->
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
intros× IN T.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 115)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
============================
(if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (slot_order i tsk1)eqn:SI2;auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 129)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
============================
(if true && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (i==tsk1)eqn:IT2;auto;simpl.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 195)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
============================
task_time_slot i <=
(if slot_order i tsk2 && true && (i != tsk2) then task_time_slot i else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
case (i==tsk2)eqn:IT1;simpl;auto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 210)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
IT1 : (i == tsk2) = true
============================
task_time_slot i <=
(if slot_order i tsk2 && true && false then task_time_slot i else 0)
subgoal 2 (ID 211) is:
task_time_slot i <=
(if slot_order i tsk2 && true && true then task_time_slot i else 0)
subgoal 3 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 211)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
i : Task
IN : i \in ts
T : true
SI2 : slot_order i tsk1 = true
IT2 : (i == tsk1) = false
IT1 : (i == tsk2) = false
============================
task_time_slot i <=
(if slot_order i tsk2 && true && true then task_time_slot i else 0)
subgoal 2 (ID 102) is:
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- by rewrite (slot_order_transitive _ _ _ SI2 ORDER).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk
----------------------------------------------------------------------------- *)
- symmetry.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite big_mkcond /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
\sum_(i <- ts)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite→bigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 500)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2
NEQ : tsk1 != tsk2
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
move/eqP /eqP in ORDER.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 622)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
NEQ : tsk1 != tsk2
ORDER : slot_order tsk1 tsk2 = true
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
addn_comoid
(if slot_order tsk1 tsk2 && (tsk1 != tsk2)
then task_time_slot tsk1
else 0)
(\big[addn_comoid/0]_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite ORDER //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 766)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
have TS2: (tsk1 != tsk2) = true .
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 769)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
============================
(tsk1 != tsk2) = true
subgoal 2 (ID 771) is:
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply /eqP;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 771)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite TS2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 811)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
task_time_slot tsk1 +
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite eqn_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 816)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\sum_(i <- ts | i != tsk1)
(if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 825)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\big[addn_monoid/0]_(i <- ts)
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) ==
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 853)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
\big[addn_monoid/0]_(i <- ts)
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
\sum_(tsk <- ts)
(if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
then task_time_slot tsk
else 0)
----------------------------------------------------------------------------- *)
apply eq_bigr;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 854)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
============================
forall i : Task,
true ->
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
----------------------------------------------------------------------------- *)
intros× T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 860)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
IN1 : tsk1 \in ts
IN2 : tsk2 \in ts
ORDER : slot_order tsk1 tsk2 = true
NEQ : tsk1 <> tsk2
TS2 : (tsk1 != tsk2) = true
i : Task
T : true
============================
(if i != tsk1
then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
else 0) =
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
then task_time_slot i
else 0)
----------------------------------------------------------------------------- *)
case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Then, we proved that no two tasks share the same time slot at any time.
Lemma task_in_time_slot_uniq:
∀ tsk1 tsk2 t, tsk1 \in ts → task_time_slot tsk1 > 0 →
tsk2 \in ts → task_time_slot tsk2 > 0 →
task_in_time_slot ts tsk1 t →
task_in_time_slot ts tsk2 t →
tsk1 = tsk2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
============================
forall (tsk1 tsk2 : Task) (t : instant),
tsk1 \in ts ->
0 < task_time_slot tsk1 ->
tsk2 \in ts ->
0 < task_time_slot tsk2 ->
task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
Proof.
intros× IN1 SLOT1 IN2 SLOT2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
============================
task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite /task_in_time_slot.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
============================
(t + TDMA_cycle ts - task_slot_offset ts tsk1 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk1 ->
(t + TDMA_cycle ts - task_slot_offset ts tsk2 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set cycle:=TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
============================
(t + cycle - task_slot_offset ts tsk1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set O1:= task_slot_offset ts tsk1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 93)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set O2:= task_slot_offset ts tsk2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have CO1: O1 < cycle by apply Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have CO2: O2 < cycle by apply Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have C: cycle > 0 by apply (TDMA_cycle_positive tsk1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 119)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite GO1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 128)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite GO2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 130)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have SO1:O1 + task_time_slot tsk1 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have SO2:O2 + task_time_slot tsk2 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
repeat rewrite mod_elim;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 158)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
============================
(if O1 <= t %% cycle then t %% cycle - O1 else t %% cycle + cycle - O1) <
task_time_slot tsk1 ->
(if O2 <= t %% cycle then t %% cycle - O2 else t %% cycle + cycle - O2) <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
case (O1 ≤ t%%cycle)eqn:O1T;case (O2 ≤ t %%cycle)eqn:O2T;intros G1 G2;try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 238)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle - O1 < task_time_slot tsk1
G2 : t %% cycle - O2 < task_time_slot tsk2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
apply ltn_subLR in G1;apply ltn_subLR in G2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2943)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3097)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
fold O1 O2 in order;try ssrlia;auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 3171)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
order : slot_order tsk1 tsk2
============================
tsk1 != tsk2
subgoal 2 (ID 3175) is:
tsk2 != tsk1
----------------------------------------------------------------------------- *)
by move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3175)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
order : slot_order tsk2 tsk1
============================
tsk2 != tsk1
----------------------------------------------------------------------------- *)
apply /eqP;auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TimeSlotOrderFacts.
End TDMAFacts.
∀ tsk1 tsk2 t, tsk1 \in ts → task_time_slot tsk1 > 0 →
tsk2 \in ts → task_time_slot tsk2 > 0 →
task_in_time_slot ts tsk1 t →
task_in_time_slot ts tsk2 t →
tsk1 = tsk2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
============================
forall (tsk1 tsk2 : Task) (t : instant),
tsk1 \in ts ->
0 < task_time_slot tsk1 ->
tsk2 \in ts ->
0 < task_time_slot tsk2 ->
task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
Proof.
intros× IN1 SLOT1 IN2 SLOT2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
============================
task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite /task_in_time_slot.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
============================
(t + TDMA_cycle ts - task_slot_offset ts tsk1 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk1 ->
(t + TDMA_cycle ts - task_slot_offset ts tsk2 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set cycle:=TDMA_cycle ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
============================
(t + cycle - task_slot_offset ts tsk1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set O1:= task_slot_offset ts tsk1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 93)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
set O2:= task_slot_offset ts tsk2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have CO1: O1 < cycle by apply Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have CO2: O2 < cycle by apply Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have C: cycle > 0 by apply (TDMA_cycle_positive tsk1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 119)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
============================
(t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite GO1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 128)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
rewrite GO2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 130)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have SO1:O1 + task_time_slot tsk1 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
have SO2:O2 + task_time_slot tsk2 ≤ cycle by apply (Offset_add_slot_leq_cycle tsk2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
============================
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
repeat rewrite mod_elim;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 158)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
============================
(if O1 <= t %% cycle then t %% cycle - O1 else t %% cycle + cycle - O1) <
task_time_slot tsk1 ->
(if O2 <= t %% cycle then t %% cycle - O2 else t %% cycle + cycle - O2) <
task_time_slot tsk2 -> tsk1 = tsk2
----------------------------------------------------------------------------- *)
case (O1 ≤ t%%cycle)eqn:O1T;case (O2 ≤ t %%cycle)eqn:O2T;intros G1 G2;try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 238)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle - O1 < task_time_slot tsk1
G2 : t %% cycle - O2 < task_time_slot tsk2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
apply ltn_subLR in G1;apply ltn_subLR in G2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2943)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3097)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
============================
tsk1 = tsk2
----------------------------------------------------------------------------- *)
destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
fold O1 O2 in order;try ssrlia;auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 3171)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
order : slot_order tsk1 tsk2
============================
tsk1 != tsk2
subgoal 2 (ID 3175) is:
tsk2 != tsk1
----------------------------------------------------------------------------- *)
by move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3175)
Task : eqType
ts : {setTask}
H : TDMAPolicy Task
task : Task
H_task_in_ts : task \in ts
time_slot_positive : valid_time_slot ts
slot_order_total : total_slot_order ts
slot_order_antisymmetric : antisymmetric_slot_order ts
slot_order_transitive : transitive_slot_order
tsk1, tsk2 : Task
t : instant
IN1 : tsk1 \in ts
SLOT1 : 0 < task_time_slot tsk1
IN2 : tsk2 \in ts
SLOT2 : 0 < task_time_slot tsk2
cycle := TDMA_cycle ts : nat
O1 := task_slot_offset ts tsk1 : nat
O2 := task_slot_offset ts tsk2 : nat
CO1 : O1 < cycle
CO2 : O2 < cycle
C : 0 < cycle
GO1 : O1 %% cycle = O1
GO2 : O2 %% cycle = O2
SO1 : O1 + task_time_slot tsk1 <= cycle
SO2 : O2 + task_time_slot tsk2 <= cycle
O1T : (O1 <= t %% cycle) = true
O2T : (O2 <= t %% cycle) = true
G1 : t %% cycle < task_time_slot tsk1 + O1
G2 : t %% cycle < task_time_slot tsk2 + O2
NEQ : tsk1 <> tsk2
order : slot_order tsk2 tsk1
============================
tsk2 != tsk1
----------------------------------------------------------------------------- *)
apply /eqP;auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TimeSlotOrderFacts.
End TDMAFacts.