diff --git a/RminStruct.v b/RminStruct.v
index 0507b95c563ace2a89f1deee9111e7e0832236f9..0605f61aa2959f32a27da68b9d73d0d86c2edc38 100644
--- a/RminStruct.v
+++ b/RminStruct.v
@@ -1,21 +1,5 @@
(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
-(******************************************************************************)
-(* Build dioid instances used in network calculus. *)
-(* *)
-(* F == set of functions nnR -> Rbar *)
-(* *)
-(* Fup == the dioid's set *)
-(* Fup_min x y == first dioid's operator <-> minimum between x y forall t *)
-(* Fup_min_conv == dioid's second operator <-> the min-plus convolution *)
-(* between x and y *)
-(* Fup_zero == dioid's zero element <-> the infinite function *)
-(* Fup_one == dioid's unit element <-> the function that is zero at zero *)
-(* and infinite otherwise *)
-(* Fup_leP == use this if you want to switch an inequality to dioid to F *)
-(* unfoldFup == use this lemma to switch between dioid and Fplus. *)
-(******************************************************************************)
-
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq bigop ssralg ssrnum rat.
@@ -24,6 +8,44 @@ From mathcomp.dioid Require Import HB_wrappers dioid.
From mathcomp.dioid Require Import complete_lattice complete_dioid.
Require Import nngenum.
+(******************************************************************************)
+(* Dioid instances used in network calculus. *)
+(* *)
+(* * number dioids *)
+(* R+ == {nonneg R} *)
+(* Q == rat *)
+(* Q+ == {nonneg Q} *)
+(* Q+* == {posnum Q} *)
+(* \bar R and {nonnege R} are equipped with a complete lattice canonical *)
+(* structure, first law is min, second law is addition, zero element is +oo *)
+(* and unit element is 0. *)
+(* *)
+(* * functions dioids *)
+(* F == functions R+ -> \bar R *)
+(* Fplus == functions f in F such that for all x, 0 <= f x *)
+(* Fup == functions f in Fplus that are non decreasing *)
+(* F0up == functions f in Fup such that f 0 = 0 *)
+(* The first three types are equipped with a complete dioid canonical *)
+(* structure, first law is pointwise minimum, second law is min-plus *)
+(* convolution, zero element is the constant function +oo and unit element is *)
+(* the function equal to +oo everywhere except in 0 where it is 0. *)
+(* The last type is *not* a dioid. *)
+(* *)
+(* * pointwise addition of functions *)
+(* Moreover, F is equipped with a pointwise addition F_plus with neutral *)
+(* element F_0, accessible with following notations in scope F_scope (%F): *)
+(* f + g == pointwise addition of functions f and g *)
+(* f / g == deconvolution in dioid F *)
+(* -f == pointwise opposite of f *)
+(* f - g == pointwise subtraction of f and g *)
+(* \sum == notation for sum with bigop *)
+(* *)
+(* * other operators *)
+(* Fup_shift_l f d == the function in Fup equal to (f : Fup) shifted by d *)
+(* (i.e., t |-> f (t + d)) *)
+(* pseudo_inv_inf_nnR f == y |-> inf{ x | y <= f x } *)
+(******************************************************************************)
+
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
diff --git a/arrival_curves.v b/arrival_curves.v
index 93a4f76465ecead1586d4dc669845e30e2b6239e..e6398610b1361d1126256ed603e36a0a778642bb 100644
--- a/arrival_curves.v
+++ b/arrival_curves.v
@@ -1,16 +1,5 @@
(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
-(******************************************************************************)
-(* Definiton and properties of arrival curves in Network Calculus *)
-(* *)
-(* is_maximal_arrival A alpha <-> alpha is an arrival curve *)
-(* for the data flow A *)
-(* *)
-(* maximal_arrival_deconv{1,2} state that A / A *)
-(* is the smallest arrival curve for A *)
-(* *)
-(******************************************************************************)
-
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat.
From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
@@ -20,6 +9,16 @@ Require Import nngenum RminStruct.
Require Import cumulative_curves.
Require Import NCCoq.usual_functions.
+(******************************************************************************)
+(* Arrival curves in Network Calculus *)
+(* *)
+(* is_maximal_arrival A alpha <-> alpha is an arrival curve *)
+(* for the data flow A *)
+(* *)
+(* maximal_arrival_deconv{1,2} state that A / A *)
+(* is the smallest arrival curve for A *)
+(******************************************************************************)
+
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
diff --git a/cumulative_curves.v b/cumulative_curves.v
index 4bd2544d5c038a5e0f7265608cfc1310c16526d3..e958b437e296b42b48c03f457bb9c7d552283b70 100644
--- a/cumulative_curves.v
+++ b/cumulative_curves.v
@@ -1,19 +1,4 @@
-(******************************************************************************)
-(* Data flows for network calculus. *)
-(* *)
-(* We define the main object studied by network calculus. *)
-(* A flow cumulative function is a function from R+ to R+, *)
-(* non-decreasing, null at 0 and left continuous.It represents the total *)
-(* amount of data of a flow at *)
-(* some observation point up to observation time.See [DNC18, ยง1.3] *)
-(* *)
-(* flow_cc == the type for data flows *)
-(** A flow cumulative curve is a function R+ -> R+ that
- - is non-decreasing;
- - takes value 0 in 0;
- - is left-continuous. *)
-(* *)
-(******************************************************************************)
+(* Copyright : Lucien Rakotomalala, Pierre Roux and Marc Boyer. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
From mathcomp Require Import choice seq bigop ssralg ssrnum rat.
@@ -22,6 +7,29 @@ From mathcomp.dioid Require Import HB_wrappers dioid.
From mathcomp.dioid Require Import complete_lattice complete_dioid.
Require Import nngenum RminStruct.
+(******************************************************************************)
+(* Data flows for network calculus. *)
+(* *)
+(* We define the main object studied by network calculus. *)
+(* A data flow cumulative function is a function from R+ to R+, *)
+(* non-decreasing, null at 0 and left continuous. It represents the total *)
+(* amount of data of a flow at some observation point up to observation time. *)
+(* *)
+(* flow_cc == the type for data flows, functions in Fup that: *)
+(* * are equal to 0 at 0; *)
+(* * are left-continuous; *)
+(* * only take finite values. *)
+(* flow_cc are equipped with a coercion to Fup *)
+(* f%:fcc == the function in R+ -> R+ equal to f : flow_cc *)
+(* left_cont_closure f == the left continuous closure of f, i.e. *)
+(* t |-> sup{ f u | u < t } *)
+(* *)
+(* flow_cc iq equipped with an addition flow_cc_plus with neutral element *)
+(* flow_cc_0 and following notations in scope flow_cc_scope (%C): *)
+(* f + g == pointwise addition of functions f and g *)
+(* \sum == notation for sum with bigop *)
+(******************************************************************************)
+
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.