Commit dfb60a45 authored by jonathan julou's avatar jonathan julou

moved overused lemmas in a separated file and proved some equivalences

parent 34dc35ca
Pipeline #18944 failed with stages
in 1 minute and 20 seconds
......@@ -3,8 +3,9 @@ From rt.restructuring.model.arrival Require Export periodic_jitter.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import ssromega.
From rt.util Require Import jonathan.
From rt.restructuring.analysis Require Export verify_up_to_t.
From rt.restructuring.model.arrival Require Export periodic_jitter_up_to_t.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
Set Bullet Behavior "Strict Subproofs".
......@@ -99,185 +100,6 @@ Section Periojitt_same_law.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
(*========================================================================*)
(* --- IV --- BASIC LEMMAS (some might already exist) --- IV --- *)
(*========================================================================*)
Local Lemma leq_plusplus: forall a b:nat, a<=b -> a.+1 <= b.+1.
Proof.
intros a b P.
ssromega.
Qed.
Local Lemma leq_plusplus_equivalence: forall a b:nat, a<=b <-> a.+1 <= b.+1.
Proof.
intros a b.
split. intro P. ssromega.
intro P. ssromega.
Qed.
Local Lemma lt_inversion: forall a:nat, (0 < a) = false -> a = 0.
Proof.
intro a.
intro P.
ssromega.
Qed.
Local Lemma not_leq: forall b a:nat, ~(a<=b) -> a>=b.
Proof.
induction b as [|b IHb].
- intros a P. ssromega.
- intros a P.
destruct (0<a) eqn:E.
+ assert (R: ~a.-1 <= b).
{
unfold not. intro Q.
unfold not in P.
apply leq_plusplus in Q.
apply P.
ssromega.
}
apply IHb in R.
apply leq_plusplus in R. rewrite <- Lt.S_pred_pos in R. exact R.
ssromega.
+ apply lt_inversion in E. subst a. exfalso.
unfold not in P. pose Q := leq0n. apply P. apply Q.
Qed.
Local Lemma not_leq_lt: forall b a:nat, ~(a<=b) -> a>b.
Proof.
induction b as [|b IHb].
- intros a P. unfold not in P.
destruct a eqn:E .
exfalso. apply P. apply leq0n.
ssromega.
- intros a P.
destruct (0<a) eqn:E.
+ assert (R: ~a.-1 <= b).
{
unfold not. intro Q.
unfold not in P.
apply leq_plusplus in Q.
apply P.
ssromega.
}
apply IHb in R.
apply leq_plusplus in R. rewrite <- Lt.S_pred_pos in R. exact R.
ssromega.
+ apply lt_inversion in E. subst a. exfalso.
unfold not in P. pose Q := leq0n. apply P. apply Q.
Qed.
Local Lemma neg_leq: forall b a:nat, (a<=b) = false -> a>=b.
Proof.
intros b a.
intro hyp.
assert (U: ~(a<=b)).
{ unfold not. intro P. ssromega. }
apply not_leq. exact U.
Qed.
Local Lemma neg_leq_lt: forall b a:nat, (a<=b) = false -> a>b.
Proof.
intros b a.
intro hyp.
assert (U: ~(a<=b)).
{ unfold not. intro P. ssromega. }
apply not_leq_lt. exact U.
Qed.
Local Lemma a_lt_b_and_b_leq_a: forall a b:nat, a.+1-b=0 -> b-a=0 -> False.
Proof.
intros a b.
intros P Q.
ssromega.
Qed.
Local Lemma a_leq_b_and_b_leq_a: forall a b:nat, a-b=0 -> b-a=0 -> a=b.
Proof.
intros a b.
intros P Q.
ssromega.
Qed.
Local Lemma leq_sub_r: forall (a b c : nat), a <= b - c -> a <= b.
Proof.
intros. ssromega.
Qed.
Local Lemma eq_each_side: forall (a b c: nat), a + c = b + c -> a = b.
Proof.
intros. ssromega.
Qed.
(*========================================================================*)
(* --- V --- SUM LEMMAS --- V --- *)
(*========================================================================*)
(*move into util/sum.v ?*)
Local Lemma sum_to_args_leq: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a <= b.
Proof.
intros a b F.
apply contraTT.
intro P.
unfold negb in P.
destruct (a<=b) eqn:E.
- exfalso. discriminate.
- move/eqP in E.
assert (Q: ~(a<=b)).
{
unfold not.
intro Q.
ssromega.
}
apply not_leq in Q.
unfold negb.
destruct (\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t) eqn: OwO.
move/eqP in OwO.
apply sum.extend_sum with (t1:=0) (t1':=0) (F := F) in Q.
move/eqP in Q. 2:reflexivity.
exfalso.
apply a_lt_b_and_b_leq_a with (a:= (\sum_(0 <= t < a) F t)) (b:= \sum_(0 <= t < b) F t).
exact OwO. exact Q.
exact P.
Qed.
(*move into util/sum.v ?*)
Local Lemma sum_to_args_lt: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a < b.
Proof.
intros a b F P.
assert (a <= b).
{ apply sum_to_args_leq with (F := F). exact P. }
destruct (a == b) eqn:E.
- exfalso.
move/eqP in E.
rewrite E in P.
ssromega.
- ssromega.
Qed.
(*========================================================================*)
......@@ -296,7 +118,7 @@ Section Periojitt_same_law.
assert (K: service_during sched pred_j 0 (job_arrival j).-1 < service_during sched pred_j 0 t).
{ apply leq_trans with (n := job_cost pred_j). ssromega. ssromega. }
unfold service_during in K.
apply sum_to_args_lt in K. ssromega.
apply jonathan.sum_to_args_lt in K. ssromega.
Qed.
......@@ -326,7 +148,7 @@ Section Periojitt_same_law.
unfold job_response_time_lower_bound in in_arr_seq_pred_j.
unfold completed_by in in_arr_seq_pred_j.
apply not_leq_lt in in_arr_seq_pred_j.
apply jonathan.not_leq_lt in in_arr_seq_pred_j.
assert (P: service sched pred_j (job_arrival pred_j + BCRT) < service sched pred_j (job_arrival j)).
{
apply leq_trans with (job_cost pred_j). exact in_arr_seq_pred_j. exact UwU.
......@@ -337,7 +159,7 @@ Section Periojitt_same_law.
assert (Q: (job_arrival pred_j + BCRT) <= (job_arrival j)).
{
apply sum_to_args_leq with (F:= service_at sched pred_j).
apply jonathan.sum_to_args_leq with (F:= service_at sched pred_j).
exact P.
}
exact Q.
......@@ -398,7 +220,7 @@ Section Periojitt_same_law.
unfold service_during in P.
assert (Q: (job_arrival j).-1 < (job_arrival pred_j + WCRT)).
{
apply sum_to_args_lt with (F:= service_at sched pred_j).
apply jonathan.sum_to_args_lt with (F:= service_at sched pred_j).
exact P.
}
ssromega.
......@@ -559,7 +381,7 @@ Local Ltac init_pipeline_lemma offset:=
unfold job_response_time_lower_bound in in_arr_seq_1.
unfold completed_by in in_arr_seq_1.
apply not_leq_lt in in_arr_seq_1.
apply jonathan.not_leq_lt in in_arr_seq_1.
assert (P: service sched pred_j (job_arrival pred_j + BCRT) < service sched pred_j (job_arrival j)).
{
......@@ -572,7 +394,7 @@ Local Ltac init_pipeline_lemma offset:=
assert (Q: (job_arrival pred_j + BCRT) < (job_arrival j)).
{
apply sum_to_args_lt with (F:= service_at sched pred_j).
apply jonathan.sum_to_args_lt with (F:= service_at sched pred_j).
exact P.
}
ssromega.
......@@ -601,7 +423,7 @@ Local Ltac init_pipeline_lemma offset:=
by (apply (arrival_propagation j pred_j end_bound in_arr_seq_2 in_arr_seq_1
in_task_2 in_task_1 dependency)).
rewrite leq_plusplus_equivalence.
rewrite jonathan.leq_plusplus_equivalence.
ssromega.
Qed.
......@@ -805,7 +627,7 @@ Local Ltac init_pipeline_lemma offset:=
unfold theoretical_arrival in same_arrival.
rewrite <- jitter_expr_ja in same_arrival.
rewrite <- jitter_expr_jb in same_arrival.
apply eq_each_side in same_arrival.
apply jonathan.eq_each_side in same_arrival.
assert (predecedence: pred_ja = pred_jb) by
apply (injection pred_ja pred_jb arr_bound_ja arr_bound_jb in_arr_seq_pred_ja in_arr_seq_pred_jb
......@@ -1024,7 +846,7 @@ End Periojitt_same_law.
From rt.restructuring.analysis.frame_by_frame Require Export cpa_temporal_step.
From rt.restructuring.analysis.analysis_up_to_t Require Export cpa_temporal_step.
Section Propagatability.
Context {PState : Type}.
......
......@@ -4,6 +4,7 @@ From mathcomp Require Export bigop path.
From rt.util Require Export list.
From rt.util Require Import ssromega.
From rt.util Require Import bigcat.
From rt.util Require Import jonathan.
Set Bullet Behavior "Strict Subproofs".
......@@ -78,34 +79,60 @@ Section Proofs.
Lemma lower_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_lower_bound_until_t sched arr_seq t R tsk)
-> task_response_time_lower_bound arr_seq sched tsk R.
<-> task_response_time_lower_bound arr_seq sched tsk R.
Proof.
intros tsk BCRT P.
unfold task_response_time_lower_bound.
intros j in_arr_seq in_task.
unfold task_response_time_lower_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
intros tsk BCRT.
split.
- intro P. unfold task_response_time_lower_bound.
intros j in_arr_seq in_task.
unfold task_response_time_lower_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
- intro Q. unfold task_response_time_lower_bound_until_t.
intros t j in_arr_seq in_task CBS.
unfold task_response_time_lower_bound in Q.
apply Q. exact in_arr_seq. exact in_task.
Qed.
Lemma upper_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_upper_bound_until_t sched arr_seq t R tsk)
-> task_response_time_upper_bound arr_seq sched tsk R.
<-> task_response_time_upper_bound arr_seq sched tsk R.
Proof.
intros tsk WCRT P.
unfold task_response_time_upper_bound.
intros j in_arr_seq in_task.
unfold task_response_time_upper_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
intros tsk WCRT.
split.
- intro P. unfold task_response_time_upper_bound.
intros j in_arr_seq in_task.
unfold task_response_time_upper_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
- intro Q. unfold task_response_time_upper_bound_until_t.
intros t j in_arr_seq in_task. split.
+ intro CBS. unfold task_response_time_upper_bound in Q.
apply Q. exact in_arr_seq. exact in_task.
+ intro PS. unfold task_response_time_upper_bound in Q.
unfold job_response_time_bound in Q.
unfold pending in PS. apply tactics.vlib__andb_split in PS.
destruct PS as [arrjt cpltjt].
unfold has_arrived in arrjt. unfold completed_by in cpltjt.
unfold completed_by in Q.
assert (cpltjt_rewritten: job_cost j > service sched j t). ssromega.
assert (R: service sched j t < service sched j (job_arrival j + WCRT)).
{ apply leq_trans with (job_cost j). exact cpltjt_rewritten.
apply Q. exact in_arr_seq. exact in_task. }
unfold service in R. unfold service_during in R.
assert (W: t <= job_arrival j + WCRT).
apply jonathan.sum_to_args_leq with (F := service_at sched j).
exact R. ssromega.
Qed.
End Proofs.
\ No newline at end of file
......@@ -3,7 +3,7 @@ From rt.restructuring.model.arrival Require Export periodic_jitter.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import ssromega.
From rt.util Require Import jonathan.
Set Bullet Behavior "Strict Subproofs".
......@@ -82,182 +82,9 @@ Section Periojitt_same_law.
theoretical_arrival j = theoretical_arrival pred_j + BCRT.
(*========================================================================*)
(* --- IV --- BASIC LEMMAS (some might already exist) --- IV --- *)
(*========================================================================*)
Local Lemma leq_plusplus: forall a b:nat, a<=b -> a.+1 <= b.+1.
Proof.
intros a b P.
ssromega.
Qed.
Local Lemma lt_inversion: forall a:nat, (0 < a) = false -> a = 0.
Proof.
intro a.
intro P.
ssromega.
Qed.
Local Lemma not_leq: forall b a:nat, ~(a<=b) -> a>=b.
Proof.
induction b as [|b IHb].
- intros a P. ssromega.
- intros a P.
destruct (0<a) eqn:E.
+ assert (R: ~a.-1 <= b).
{
unfold not. intro Q.
unfold not in P.
apply leq_plusplus in Q.
apply P.
ssromega.
}
apply IHb in R.
apply leq_plusplus in R. rewrite <- Lt.S_pred_pos in R. exact R.
ssromega.
+ apply lt_inversion in E. subst a. exfalso.
unfold not in P. pose Q := leq0n. apply P. apply Q.
Qed.
Local Lemma not_leq_lt: forall b a:nat, ~(a<=b) -> a>b.
Proof.
induction b as [|b IHb].
- intros a P. unfold not in P.
destruct a eqn:E .
exfalso. apply P. apply leq0n.
ssromega.
- intros a P.
destruct (0<a) eqn:E.
+ assert (R: ~a.-1 <= b).
{
unfold not. intro Q.
unfold not in P.
apply leq_plusplus in Q.
apply P.
ssromega.
}
apply IHb in R.
apply leq_plusplus in R. rewrite <- Lt.S_pred_pos in R. exact R.
ssromega.
+ apply lt_inversion in E. subst a. exfalso.
unfold not in P. pose Q := leq0n. apply P. apply Q.
Qed.
Local Lemma neg_leq: forall b a:nat, (a<=b) = false -> a>=b.
Proof.
intros b a.
intro hyp.
assert (U: ~(a<=b)).
{ unfold not. intro P. ssromega. }
apply not_leq. exact U.
Qed.
Local Lemma neg_leq_lt: forall b a:nat, (a<=b) = false -> a>b.
Proof.
intros b a.
intro hyp.
assert (U: ~(a<=b)).
{ unfold not. intro P. ssromega. }
apply not_leq_lt. exact U.
Qed.
Local Lemma a_lt_b_and_b_leq_a: forall a b:nat, a.+1-b=0 -> b-a=0 -> False.
Proof.
intros a b.
intros P Q.
ssromega.
Qed.
Local Lemma a_leq_b_and_b_leq_a: forall a b:nat, a-b=0 -> b-a=0 -> a=b.
Proof.
intros a b.
intros P Q.
ssromega.
Qed.
Local Lemma leq_sub_r: forall (a b c : nat), a <= b - c -> a <= b.
Proof.
intros. ssromega.
Qed.
Local Lemma eq_each_side: forall (a b c: nat), a + c = b + c -> a = b.
Proof.
intros. ssromega.
Qed.
(*========================================================================*)
(* --- V --- SUM LEMMAS --- V --- *)
(*========================================================================*)
(*move into util/sum.v ?*)
Local Lemma sum_to_args_leq: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a <= b.
Proof.
intros a b F.
apply contraTT.
intro P.
unfold negb in P.
destruct (a<=b) eqn:E.
- exfalso. discriminate.
- move/eqP in E.
assert (Q: ~(a<=b)).
{
unfold not.
intro Q.
ssromega.
}
apply not_leq in Q.
unfold negb.
destruct (\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t) eqn: OwO.
move/eqP in OwO.
apply sum.extend_sum with (t1:=0) (t1':=0) (F := F) in Q.
move/eqP in Q. 2:reflexivity.
exfalso.
apply a_lt_b_and_b_leq_a with (a:= (\sum_(0 <= t < a) F t)) (b:= \sum_(0 <= t < b) F t).
exact OwO. exact Q.
exact P.
Qed.
(*move into util/sum.v ?*)
Local Lemma sum_to_args_lt: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a < b.
Proof.
intros a b F P.
assert (a <= b).
{ apply sum_to_args_leq with (F := F). exact P. }
destruct (a == b) eqn:E.
- exfalso.
move/eqP in E.
rewrite E in P.
ssromega.
- ssromega.
Qed.
(*========================================================================*)
(* --- VI --- BOUNDING LEMMAS --- VI --- *)
(* --- IV --- BOUNDING LEMMAS --- IV --- *)
(*========================================================================*)
Lemma dependency_arrival_bound_BCRT: forall (j pred_j : Job),
......@@ -283,7 +110,7 @@ Section Periojitt_same_law.
unfold job_response_time_lower_bound in in_arr_seq_pred_j.
unfold completed_by in in_arr_seq_pred_j.
apply not_leq_lt in in_arr_seq_pred_j.
apply jonathan.not_leq_lt in in_arr_seq_pred_j.
assert (P: service sched pred_j (job_arrival pred_j + BCRT) < service sched pred_j (job_arrival j)).
{
apply leq_trans with (job_cost pred_j). exact in_arr_seq_pred_j. exact UwU.
......@@ -294,7 +121,7 @@ Section Periojitt_same_law.
assert (Q: (job_arrival pred_j + BCRT) <= (job_arrival j)).
{
apply sum_to_args_leq with (F:= service_at sched pred_j).
apply jonathan.sum_to_args_leq with (F:= service_at sched pred_j).
exact P.
}
exact Q.
......@@ -332,7 +159,7 @@ Section Periojitt_same_law.
unfold service_during in P.
assert (Q: (job_arrival j).-1 < (job_arrival pred_j + WCRT)).
{
apply sum_to_args_lt with (F:= service_at sched pred_j).
apply jonathan.sum_to_args_lt with (F:= service_at sched pred_j).
exact P.
}
ssromega.
......@@ -341,7 +168,7 @@ Section Periojitt_same_law.
(*========================================================================*)
(* --- VII --- LAST LEMMAS --- VII --- *)
(* --- V --- LAST LEMMAS --- V --- *)
(*========================================================================*)
(* returns the job that comes before the one given as argument
......@@ -395,7 +222,7 @@ Section Periojitt_same_law.
(*========================================================================*)
(* --- VIII --- LTAC COMMANDS FOR READABILITY --- VIII --- *)
(* --- VI --- LTAC COMMANDS FOR READABILITY --- VI --- *)
(*========================================================================*)
Local Ltac previous_job_init j in_arr_seq_two in_task_two dependency:=
......@@ -469,7 +296,7 @@ Section Periojitt_same_law.
(*========================================================================*)
(* --- IX --- SOME LEMMAS TO SOOTHE THE PIPELINE --- IX --- *)
(* --- VII --- SOME LEMMAS TO SOOTHE THE PIPELINE --- VII --- *)
(*========================================================================*)
Local Lemma absurd_case: forall offset j pred_j,
......@@ -496,7 +323,7 @@ Section Periojitt_same_law.
bound_init pred_j j in_arr_seq_two in_arr_seq_one in_task_two in_task_one j_predj_dependency.
apply neg_leq_lt in E.
apply jonathan.neg_leq_lt in E.
assert (lt_split: job_arrival j <= job_jitter j /\ job_arrival j <> job_jitter j).
split. ssromega. ssromega. destruct lt_split as [jj_leq jj_neq].
move/eqP in jj_leq.
......@@ -612,7 +439,7 @@ Section Periojitt_same_law.
unfold theoretical_arrival in same_arrival.
rewrite <- jitter_expr_ja in same_arrival.
rewrite <- jitter_expr_jb in same_arrival.
apply eq_each_side in same_arrival.
apply jonathan.eq_each_side in same_arrival.
assert (predecedence: pred_ja = pred_jb) by
apply (injection pred_ja pred_jb in_arr_seq_pred_ja in_arr_seq_pred_jb
......@@ -687,7 +514,7 @@ Section Periojitt_same_law.
(*========================================================================*)
(* --- IX --- FINAL RESULT --- IX --- *)
(* --- VIII --- FINAL RESULT --- VIII --- *)
(*========================================================================*)
(*for all tasks tsk1, tsk2,
......