From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Import prosa.util.epsilon.
Require Import prosa.util.tactics.
Require Import prosa.model.task.concept.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** * Reduction of the search space for Abstract RTA *)
(** In this file, we prove that in order to calculate the worst-case response time 
    it is sufficient to consider only values of [A] that lie in the search space defined below. *)  

Section AbstractRTAReduction. 

  (** The response-time analysis we are presenting in this series of documents is based on searching 
     over all possible values of [A], the relative arrival time of the job respective to the beginning 
     of the busy interval. However, to obtain a practically useful response-time bound, we need to 
     constrain the search space of values of [A]. In this section, we define an approach to 
     reduce the search space. *)
  
  Context {Task : TaskType}.
  
  (** First, we provide a constructive notion of equivalent functions. *)
  Section EquivalentFunctions.
    
    (** Consider an arbitrary type [T]... *)
    Context {T : eqType}.

    (**  ...and two function from [nat] to [T]. *)
    Variables f1 f2 : nat -> T.

    (** Let [B] be an arbitrary constant. *) 
    Variable B : nat.
    
    (** Then we say that [f1] and [f2] are equivalent at values less than [B] iff
       for any natural number [x] less than [B] [f1 x] is equal to [f2 x].  *)
    Definition are_equivalent_at_values_less_than :=
      forall x, x < B -> f1 x = f2 x.

    (** And vice versa, we say that [f1] and [f2] are not equivalent at values 
       less than [B] iff there exists a natural number [x] less than [B] such
       that [f1 x] is not equal to [f2 x].  *)
    Definition are_not_equivalent_at_values_less_than :=
      exists x, x < B /\ f1 x <> f2 x.

  End EquivalentFunctions. 

  (** Let [tsk] be any task that is to be analyzed *)
  Variable tsk : Task.
  
  (** To ensure that the analysis procedure terminates, we assume an upper bound [B] on 
     the values of [A] that must be checked. The existence of [B] follows from the assumption 
     that the system is not overloaded (i.e., it has bounded utilization). *)
  Variable B : duration.

  (** Instead of searching for the maximum interference of each individual job, we 
     assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized 
     by the relative arrival time [A] of a potential job (see abstract_RTA.definitions.v file). *)
  Variable interference_bound_function : Task -> duration -> duration -> duration.

  (** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
     Note that [ε = 1] under discrete time. *)
  (** To ensure that the search converges more quickly, we only check values of [A] in the interval 
     <<[0, B)>> for which the interference bound function changes, i.e., every point [x] in which 
     [interference_bound_function (A - ε, x)] is not equal to [interference_bound_function (A, x)]. *)
  Definition is_in_search_space A :=
    A = 0 \/
    0 < A < B /\ are_not_equivalent_at_values_less_than
                  (interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
  
  (** In this section we prove that for every [A] there exists a smaller [A_sp] 
     in the search space such that [interference_bound_function(A_sp,x)] is 
     equal to [interference_bound_function(A, x)]. *)
  Section ExistenceOfRepresentative.

    (** Let [A] be any constant less than [B]. *) 
    Variable A : duration.
    Hypothesis H_A_less_than_B : A < B.
    
    (** We prove that there exists a constant [A_sp] such that:
       (a) [A_sp] is no greater than [A], (b) [interference_bound_function(A_sp, x)] is 
       equal to [interference_bound_function(A, x)] and (c) [A_sp] is in the search space.
       In other words, either [A] is already inside the search space, or we can go 
       to the "left" until we reach [A_sp], which will be inside the search space. *)
    Lemma representative_exists:
      exists A_sp, 
        A_sp <= A /\
        are_equivalent_at_values_less_than (interference_bound_function tsk A)
                                           (interference_bound_function tsk A_sp) B /\
        is_in_search_space A_sp.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
H_A_less_than_B: A < B
exists A_sp : nat,
  A_sp <= A /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk A)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
    Proof.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
H_A_less_than_B: A < B
exists A_sp : nat,
  A_sp <= A /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk A)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
      induction A as [|n].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
H_A_less_than_B: 0 < B
exists A_sp : nat,
  A_sp <= 0 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk 0)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
H_A_less_than_B: 0 < B
exists A_sp : nat,
  A_sp <= 0 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk 0)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp exists 0; repeat split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
H_A_less_than_B: 0 < B
is_in_search_space 0
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
          by rewrite /is_in_search_space; left.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp have ALT:
          all (fun t => interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
          \/ has (fun t => interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B) apply/orP.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t) (iota 0 B)
|| has
     (fun t : duration =>
      interference_bound_function tsk n t
      != interference_bound_function tsk n.+1 t)
     (iota 0 B)
          rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
~~
(~~
 all
   (fun t : duration =>
    interference_bound_function tsk n t ==
    interference_bound_function tsk n.+1 t) (iota 0 B) &&
 ~~
 has
   (fun t : duration =>
    interference_bound_function tsk n t
    != interference_bound_function tsk n.+1 t)
   (iota 0 B))
          apply/negP; intros CONTR.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
CONTR: ~~
all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B) &&
~~
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
False
          move: CONTR => /andP [NALL /negP NHAS]; apply: NHAS.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
NALL: ~~
all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B)
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
            by rewrite -has_predC /predC in NALL.
        }
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: n < B ->
exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
        feed IHn; first by apply ltn_trans with n.+1.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
IHn: exists A_sp : nat,
  A_sp <= n /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp 
        move: IHn => [ASP [NEQ [EQ SP]]].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ALT: all
  (fun t : duration =>
   interference_bound_function tsk n t ==
   interference_bound_function tsk n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function tsk n t
   != interference_bound_function tsk n.+1 t)
  (iota 0 B)
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
        move: ALT => [/allP ALT| /hasP ALT].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp exists ASP; repeat split; try done.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
ASP <= n.+1
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
are_equivalent_at_values_less_than
  (interference_bound_function tsk n.+1)
  (interference_bound_function tsk ASP) B
          {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
ASP <= n.+1 by apply leq_trans with n. }
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
are_equivalent_at_values_less_than
  (interference_bound_function tsk n.+1)
  (interference_bound_function tsk ASP) B
          {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
are_equivalent_at_values_less_than
  (interference_bound_function tsk n.+1)
  (interference_bound_function tsk ASP) B intros x LT.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
x: nat
LT: x < B
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
            move: (ALT x) => T.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
x: nat
LT: x < B
T: x \in iota 0 B ->
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x feed T; first by rewrite mem_iota; apply/andP; split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
x: nat
LT: x < B
T: interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x 
            move: T => /eqP T.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall x : nat_eqType,
  interference_bound_function tsk n x ==
  interference_bound_function tsk n.+1 x}
x: nat
LT: x < B
T: interference_bound_function tsk n x =
interference_bound_function tsk n.+1 x
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
              by rewrite -T EQ.
          }
        }
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function tsk n.+1)
    (interference_bound_function tsk A_sp) B /\
  is_in_search_space A_sp exists n.+1; repeat split; try done.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
is_in_search_space n.+1
          rewrite /is_in_search_space; right.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
0 < n.+1 < B /\
are_not_equivalent_at_values_less_than
  (interference_bound_function tsk (n.+1 - ε))
  (interference_bound_function tsk n.+1) B
          split; first by  apply/andP; split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
ALT: exists2 x : nat_eqType,
  x \in iota 0 B &
  interference_bound_function tsk n x
  != interference_bound_function tsk n.+1 x
are_not_equivalent_at_values_less_than
  (interference_bound_function tsk (n.+1 - ε))
  (interference_bound_function tsk n.+1) B
          move: ALT => [y IN N].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
IN: y \in iota 0 B
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
are_not_equivalent_at_values_less_than
  (interference_bound_function tsk (n.+1 - ε))
  (interference_bound_function tsk n.+1) B
          exists y.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
IN: y \in iota 0 B
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
          move: IN; rewrite mem_iota add0n.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
0 <= y < B ->
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y move => /andP [_ LT].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT: y < B
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y 
          split; first by done.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT: y < B
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
          rewrite subn1 -pred_Sn.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
N: interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT: y < B
interference_bound_function tsk n y <>
interference_bound_function tsk n.+1 y
          intros CONTR; move: N => /negP N; apply: N.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function tsk n)
  (interference_bound_function tsk ASP) B
SP: is_in_search_space ASP
y: nat_eqType
LT: y < B
CONTR: interference_bound_function tsk n y =
interference_bound_function tsk n.+1 y
interference_bound_function tsk n y ==
interference_bound_function tsk n.+1 y
            by rewrite CONTR.
        }
    Qed.

  End ExistenceOfRepresentative.

  (** In this section we prove that any solution of the response-time recurrence for
     a given point [A_sp] in the search space also gives a solution for any point 
     A that shares the same interference bound. *)
  Section FixpointSolutionForAnotherA.

    (** Suppose [A_sp + F_sp] is a "small" solution (i.e. less than [B]) of the response-time recurrence. *)
    Variables A_sp F_sp : duration.
    Hypothesis H_less_than : A_sp + F_sp < B.
    Hypothesis H_fixpoint : A_sp + F_sp >= interference_bound_function tsk A_sp (A_sp + F_sp).

    (** Next, let [A] be any point such that: (a) [A_sp <= A <= A_sp + F_sp] and 
       (b) [interference_bound_function(A, x)] is equal to 
       [interference_bound_function(A_sp, x)] for all [x] less than [B]. *)
    Variable A : duration.
    Hypothesis H_bounds_for_A : A_sp <= A <= A_sp + F_sp.
    Hypothesis H_equivalent :
      are_equivalent_at_values_less_than
        (interference_bound_function tsk A)
        (interference_bound_function tsk A_sp) B.

    (** We prove that there exists a constant [F] such that [A + F] is equal to [A_sp + F_sp]
       and [A + F] is a solution for the response-time recurrence for [A]. *)
    Lemma solution_for_A_exists:
      exists F,
        A_sp + F_sp = A + F /\
        F <= F_sp /\
        A + F >= interference_bound_function tsk A (A + F).
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function tsk A_sp
  (A_sp + F_sp) <= A_sp + F_sp
A: duration
H_bounds_for_A: A_sp <= A <= A_sp + F_sp
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
exists F : nat,
  A_sp + F_sp = A + F /\
  F <= F_sp /\
  interference_bound_function tsk A (A + F) <= A + F
    Proof.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function tsk A_sp
  (A_sp + F_sp) <= A_sp + F_sp
A: duration
H_bounds_for_A: A_sp <= A <= A_sp + F_sp
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
exists F : nat,
  A_sp + F_sp = A + F /\
  F <= F_sp /\
  interference_bound_function tsk A (A + F) <= A + F  
      move: H_bounds_for_A => /andP [NEQ1 NEQ2].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function tsk A_sp
  (A_sp + F_sp) <= A_sp + F_sp
A: duration
H_bounds_for_A: A_sp <= A <= A_sp + F_sp
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= A_sp + F_sp
exists F : nat,
  A_sp + F_sp = A + F /\
  F <= F_sp /\
  interference_bound_function tsk A (A + F) <= A + F
      set (X := A_sp + F_sp) in *.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
exists F : nat,
  X = A + F /\
  F <= F_sp /\
  interference_bound_function tsk A (A + F) <= A + F
      exists (X - A); split; last split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X = A + (X - A)
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A)
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X = A + (X - A)
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A) by rewrite subnKC.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A)
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A) by rewrite leq_subLR /X leq_add2r.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A)
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: Task ->
duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function tsk A_sp X <=
X
A: duration
H_bounds_for_A: A_sp <= A <= X
H_equivalent: are_equivalent_at_values_less_than
  (interference_bound_function tsk A)
  (interference_bound_function tsk A_sp)
  B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function tsk A (A + (X - A)) <=
A + (X - A) by rewrite subnKC // H_equivalent.
    Qed.

  End FixpointSolutionForAnotherA.
  
End AbstractRTAReduction.