Require Import prosa.classic.util.all.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.

Section Defs.

(* Definition of a concrete task. *)
{
task_id: nat; (* for uniqueness *)
}.

(* To make it compatible with ssreflect, we define a decidable
equality for concrete tasks. *)

(* Next, we prove that task_eqdef is indeed an equality, ... *)
Proof.
unfold Equality.axiom; intros x y.
destruct (task_eqdef x y) eqn:EQ.
{
apply ReflectT.
unfold task_eqdef in ×.
move: EQ ⇒ /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PERIOD] /eqP DL] /eqP JITTER].
by destruct x, y; simpl in *; subst.
}
{
apply ReflectF.
unfold task_eqdef, not in *; intro BUG.
apply negbT in EQ; rewrite negb_and in EQ.
destruct x, y.
rewrite negb_and in EQ.
move: EQ ⇒ /orP [/orP [EQ | /eqP DL] | /eqP JITTER]; last by apply JITTER; inversion BUG.
rewrite negb_and in EQ.
move: EQ ⇒ /orP [EQ | /eqP DL]; last by apply DL; inversion BUG.
rewrite negb_and in EQ.
move: EQ ⇒ /orP [/eqP ID | /eqP PERIOD]; last by apply PERIOD; inversion BUG.
by apply ID; inversion BUG.
by apply DL; inversion BUG.
}
Qed.

(* ..., which allows instantiating the canonical structure. *)