# Library prosa.implementation.definitions.arrival_bound

From HB Require Import structures.

Require Export prosa.implementation.definitions.extrapolated_arrival_curve.

Require Export prosa.implementation.definitions.extrapolated_arrival_curve.

# Implementation of a Task's Arrival Bound

Inductive task_arrivals_bound :=

| Periodic : nat → task_arrivals_bound

| Sporadic : nat → task_arrivals_bound

| ArrivalPrefix : ArrivalCurvePrefix → task_arrivals_bound.

| Periodic : nat → task_arrivals_bound

| Sporadic : nat → task_arrivals_bound

| ArrivalPrefix : ArrivalCurvePrefix → task_arrivals_bound.

To make it compatible with ssreflect, we define a decidable
equality for arrival bounds.

Definition task_arrivals_bound_eqdef (tb1 tb2 : task_arrivals_bound) :=

match tb1, tb2 with

| Periodic p1, Periodic p2 ⇒ p1 == p2

| Sporadic s1, Sporadic s2 ⇒ s1 == s2

| ArrivalPrefix s1, ArrivalPrefix s2 ⇒ s1 == s2

| _, _ ⇒ false

end.

match tb1, tb2 with

| Periodic p1, Periodic p2 ⇒ p1 == p2

| Sporadic s1, Sporadic s2 ⇒ s1 == s2

| ArrivalPrefix s1, ArrivalPrefix s2 ⇒ s1 == s2

| _, _ ⇒ false

end.

Next, we prove that task_eqdef is indeed an equality, ...

Lemma eqn_task_arrivals_bound : Equality.axiom task_arrivals_bound_eqdef.

Proof.

intros x y.

destruct (task_arrivals_bound_eqdef x y) eqn:EQ.

{ apply ReflectT; destruct x, y.

all: try by move: EQ ⇒ /eqP EQ; subst.

}

{ apply ReflectF; destruct x, y.

all: try by move: EQ ⇒ /eqP EQ.

all: by move: EQ ⇒ /neqP; intros NEQ1 NEQ2; apply NEQ1; inversion NEQ2.

}

Qed.

Proof.

intros x y.

destruct (task_arrivals_bound_eqdef x y) eqn:EQ.

{ apply ReflectT; destruct x, y.

all: try by move: EQ ⇒ /eqP EQ; subst.

}

{ apply ReflectF; destruct x, y.

all: try by move: EQ ⇒ /eqP EQ.

all: by move: EQ ⇒ /neqP; intros NEQ1 NEQ2; apply NEQ1; inversion NEQ2.

}

Qed.