Require Import prosa.util.epsilon.
Require Import prosa.util.tactics.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Require Import prosa.model.task.concept.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** * 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(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 : 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 (A - ε)) (interference_bound_function 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 A)
                                           (interference_bound_function A_sp) B /\
        is_in_search_space A_sp.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 A)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
    Proof.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 A)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
      induction A as [|n IHn].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 0)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function 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 n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 0)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp exists 0; repeat split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A: duration
H_A_less_than_B: 0 < B
is_in_search_space 0
          by rewrite /is_in_search_space; left.
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function 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 n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp have ALT:
          all (fun t => interference_bound_function n t == interference_bound_function n.+1 t) (iota 0 B)
          \/ has (fun t => interference_bound_function n t != interference_bound_function n.+1 t) (iota 0 B).
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t) (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t) (iota 0 B)
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t) (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t) (iota 0 B) apply/orP.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t) (iota 0 B)
|| has
     (fun t : duration =>
      interference_bound_function n t
      != interference_bound_function n.+1 t)
     (iota 0 B)
          rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
~~
(~~
 all
   (fun t : duration =>
    interference_bound_function n t ==
    interference_bound_function n.+1 t) (iota 0 B) &&
 ~~
 has
   (fun t : duration =>
    interference_bound_function n t
    != interference_bound_function n.+1 t) (iota 0 B))
          apply/negP; intros CONTR.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
CONTR: ~~
all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B) &&
~~
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t)
  (iota 0 B)
False
          move: CONTR => /andP [NALL /negP NHAS]; apply: NHAS.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
NALL: ~~
all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B)
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t) (iota 0 B)
            by rewrite -has_predC /predC in NALL.
        }
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function 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: 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 n)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
ALT: all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t)
  (iota 0 B)
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp 
        move: IHn => [ASP [NEQ [EQ SP]]].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A: duration
n: nat
H_A_less_than_B: n.+1 < B
ALT: all
  (fun t : duration =>
   interference_bound_function n t ==
   interference_bound_function n.+1 t)
  (iota 0 B) \/
has
  (fun t : duration =>
   interference_bound_function n t
   != interference_bound_function n.+1 t)
  (iota 0 B)
ASP: nat
NEQ: ASP <= n
EQ: are_equivalent_at_values_less_than
  (interference_bound_function n)
  (interference_bound_function 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 n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
        move: ALT => [/allP ALT| /hasP ALT].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp exists ASP; repeat split=> //.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
are_equivalent_at_values_less_than
  (interference_bound_function n.+1)
  (interference_bound_function ASP) B
          intros x LT.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
x: nat
LT: x < B
interference_bound_function n.+1 x =
interference_bound_function ASP x
          move: (ALT x) => T.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
x: nat
LT: x < B
T: x \in iota 0 B ->
interference_bound_function n x ==
interference_bound_function n.+1 x
interference_bound_function n.+1 x =
interference_bound_function ASP x
          feed T; first by rewrite mem_iota; apply/andP; split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: {in iota 0 B,
  forall
    x : Datatypes_nat__canonical__eqtype_Equality,
  interference_bound_function n x ==
  interference_bound_function n.+1 x}
x: nat
LT: x < B
T: interference_bound_function n x ==
interference_bound_function n.+1 x
interference_bound_function n.+1 x =
interference_bound_function ASP x
          by move: T => /eqP<-; rewrite EQ.
        }
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp
        {
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
exists A_sp : nat,
  A_sp <= n.+1 /\
  are_equivalent_at_values_less_than
    (interference_bound_function n.+1)
    (interference_bound_function A_sp) B /\
  is_in_search_space A_sp exists n.+1; repeat split=> //.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
is_in_search_space n.+1
          rewrite /is_in_search_space; right.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
0 < n.+1 < B /\
are_not_equivalent_at_values_less_than
  (interference_bound_function (n.+1 - 1))
  (interference_bound_function n.+1) B
          split; first by  apply/andP; split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
ALT: exists2
  x : Datatypes_nat__canonical__eqtype_Equality,
  x \in iota 0 B &
  interference_bound_function n x
  != interference_bound_function n.+1 x
are_not_equivalent_at_values_less_than
  (interference_bound_function (n.+1 - 1))
  (interference_bound_function n.+1) B
          move: ALT => [y IN N].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
IN: y \in iota 0 B
N: interference_bound_function n y
!= interference_bound_function n.+1 y
are_not_equivalent_at_values_less_than
  (interference_bound_function (n.+1 - 1))
  (interference_bound_function n.+1) B
          exists y.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
IN: y \in iota 0 B
N: interference_bound_function n y
!= interference_bound_function n.+1 y
y < B /\
interference_bound_function (n.+1 - 1) y <>
interference_bound_function n.+1 y
          move: IN; rewrite mem_iota add0n.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
N: interference_bound_function n y
!= interference_bound_function n.+1 y
0 <= y < B ->
y < B /\
interference_bound_function (n.+1 - 1) y <>
interference_bound_function n.+1 y move => /andP [_ LT].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
N: interference_bound_function n y
!= interference_bound_function n.+1 y
LT: y < B
y < B /\
interference_bound_function (n.+1 - 1) y <>
interference_bound_function n.+1 y 
          split=> [//|].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
N: interference_bound_function n y
!= interference_bound_function n.+1 y
LT: y < B
interference_bound_function (n.+1 - 1) y <>
interference_bound_function n.+1 y
          rewrite subn1 -pred_Sn.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
N: interference_bound_function n y
!= interference_bound_function n.+1 y
LT: y < B
interference_bound_function n y <>
interference_bound_function n.+1 y
          intros CONTR; move: N => /negP N; apply: N.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: 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 n)
  (interference_bound_function ASP) B
SP: is_in_search_space ASP
y: Datatypes_nat__canonical__eqtype_Equality
LT: y < B
CONTR: interference_bound_function n y =
interference_bound_function n.+1 y
interference_bound_function n y ==
interference_bound_function 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 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 A)
        (interference_bound_function 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 A (A + F).
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
exists F : nat,
  A_sp + F_sp = A + F /\
  F <= F_sp /\
  interference_bound_function A (A + F) <= A + F
    Proof.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
exists F : nat,
  A_sp + F_sp = A + F /\
  F <= F_sp /\
  interference_bound_function A (A + F) <= A + F  
      move: H_bounds_for_A => /andP [NEQ1 NEQ2].
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
H_less_than: A_sp + F_sp < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function 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 A (A + F) <= A + F
      set (X := A_sp + F_sp) in *.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
exists F : nat,
  X = A + F /\
  F <= F_sp /\
  interference_bound_function A (A + F) <= A + F
      exists (X - A); split; last split.
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
X = A + (X - A)
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function A (A + (X - A)) <=
A + (X - A)
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
X = A + (X - A) by rewrite subnKC.
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
X - A <= F_sp by rewrite leq_subLR /X leq_add2r.
      -
Task: TaskType
tsk: Task
B: duration
interference_bound_function: duration ->
duration -> duration
A_sp, F_sp: duration
X:= A_sp + F_sp: nat
H_less_than: X < B
H_fixpoint: interference_bound_function 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 A)
  (interference_bound_function A_sp) B
NEQ1: A_sp <= A
NEQ2: A <= X
interference_bound_function A (A + (X - A)) <=
A + (X - A) by rewrite subnKC // H_equivalent.
    Qed.

  End FixpointSolutionForAnotherA.

End AbstractRTAReduction.

(** In this section, we prove a simple lemma that allows one to switch
    IBFs inside of the [is_in_search_space] predicate. *)
Section SearchSpaceSwitch.

  (** Consider any type of tasks. *)
  Context {Task : TaskType}.

  (** Let [tsk] be any task that is to be analyzed. *)
  Variable tsk : Task.

  (** Similarly to the previous section, to ensure that the analysis
      procedure terminates, we assume an upper bound [B] on the values
      of [A] that must be checked. *)
  Variable B : duration.

  (** Given two IBFs [IBF1] and [IBF2] such that they are equal for
      all inputs, if an offset [A] is in the search space of [IBF1],
      then [A] is in the search space of [IBF2]. *)
  Lemma search_space_switch_IBF :
    forall IBF1 IBF2,
      (forall A Δ, A < B -> IBF1 A Δ = IBF2 A Δ) ->
      forall A,
        is_in_search_space B IBF1 A ->
        is_in_search_space B IBF2 A.
Task: TaskType
tsk: Task
B: duration
forall IBF1 IBF2 : nat -> duration -> duration,
(forall (A : nat) (Δ : duration),
 A < B -> IBF1 A Δ = IBF2 A Δ) ->
forall A : nat,
is_in_search_space B IBF1 A ->
is_in_search_space B IBF2 A
  Proof.
Task: TaskType
tsk: Task
B: duration
forall IBF1 IBF2 : nat -> duration -> duration,
(forall (A : nat) (Δ : duration),
 A < B -> IBF1 A Δ = IBF2 A Δ) ->
forall A : nat,
is_in_search_space B IBF1 A ->
is_in_search_space B IBF2 A
    move=> IBF1 IBF2 EQU A [EQ|[NEQ NEQU]]; first by left; subst.
Task: TaskType
tsk: Task
B: duration
IBF1, IBF2: nat -> duration -> duration
EQU: forall (A : nat) (Δ : duration),
A < B -> IBF1 A Δ = IBF2 A Δ
A: nat
NEQ: 0 < A < B
NEQU: are_not_equivalent_at_values_less_than
  (IBF1 (A - 1)) (IBF1 A) B
is_in_search_space B IBF2 A
    right; split; first by done.
Task: TaskType
tsk: Task
B: duration
IBF1, IBF2: nat -> duration -> duration
EQU: forall (A : nat) (Δ : duration),
A < B -> IBF1 A Δ = IBF2 A Δ
A: nat
NEQ: 0 < A < B
NEQU: are_not_equivalent_at_values_less_than
  (IBF1 (A - 1)) (IBF1 A) B
are_not_equivalent_at_values_less_than (IBF2 (A - 1))
  (IBF2 A) B
    move: NEQU => [x [LT NEQf]].
Task: TaskType
tsk: Task
B: duration
IBF1, IBF2: nat -> duration -> duration
EQU: forall (A : nat) (Δ : duration),
A < B -> IBF1 A Δ = IBF2 A Δ
A: nat
NEQ: 0 < A < B
x: nat
LT: x < B
NEQf: IBF1 (A - 1) x <> IBF1 A x
are_not_equivalent_at_values_less_than (IBF2 (A - 1))
  (IBF2 A) B
    exists x; split; first by done.
Task: TaskType
tsk: Task
B: duration
IBF1, IBF2: nat -> duration -> duration
EQU: forall (A : nat) (Δ : duration),
A < B -> IBF1 A Δ = IBF2 A Δ
A: nat
NEQ: 0 < A < B
x: nat
LT: x < B
NEQf: IBF1 (A - 1) x <> IBF1 A x
IBF2 (A - 1) x <> IBF2 A x
    move: NEQf.
Task: TaskType
tsk: Task
B: duration
IBF1, IBF2: nat -> duration -> duration
EQU: forall (A : nat) (Δ : duration),
A < B -> IBF1 A Δ = IBF2 A Δ
A: nat
NEQ: 0 < A < B
x: nat
LT: x < B
IBF1 (A - 1) x <> IBF1 A x ->
IBF2 (A - 1) x <> IBF2 A x
    by rewrite !EQU //=; lia.
  Qed.

End SearchSpaceSwitch.