``` ```

# System.v: Formalisation of Kahn networks

``` Set Implicit Arguments. Require Export Cpo_streams_type. ```

## Definition of nodes

``` ```
Definition of a multiple node :
• index for inputs with associated types
• index for outputs with associated types
• continuous function on corresponding streams
``` Definition DS_fam (I:Type)(SI:I -> Type) (i:I) := DS (SI i). Definition DS_prod (I:Type)(SI:I -> Type) := Dprodi (DS_fam SI). ```
• A node is a continuous function from inpits to outputs
``` Definition node_fun (I O : Type) (SI : I -> Type) (SO : O -> Type) :cpo               := DS_prod SI -C-> DS_prod SO. ```
• node with a single output
``` Definition snode_fun (I : Type) (SI : I -> Type) (SO : Type) : cpo := DS_prod SI -C-> DS SO. ```

## Definition of a system

``` ```
• Each link is either an input link or is associated to the output of a simple node, each input of that node is associated to a link with the apropriate type
``` Definition inlSL (LI LO:Type) (SL:(LI+LO)->Type) (i:LI) := SL (inl LO i). Definition inrSL (LI LO:Type) (SL:(LI+LO)->Type) (o:LO) := SL (inr LI o). ```
A system associates a continuous functions to a set of typed output links
``` Definition system (LI LO:Type) (SL:LI+LO->Type)     := Dprodi (fun (o:LO) => DS_prod SL -C-> DS (inrSL SL o)). ```

## Semantics of a system

``` ```
Each system defines a new node with inputs for the inputs of the system
``` ```

### Definition of the equations

``` ```
Equations are a continuous functional on links
``` Definition eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),      system SL -> DS_prod (inlSL SL) -> DS_prod SL -m> DS_prod SL. intros LI LO SL s init. exists (fun X : DS_prod SL => fun l : LI+LO =>                        match l return (DS (SL l)) with                             inl i => init i                           | inr o => s o X                       end). red;intros X Y Hle; intro l. case l; auto. Defined. Lemma eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)                (init : DS_prod (inlSL SL)) (X:DS_prod SL),                eqn_of_system s init X =                  fun l : LI+LO =>                  match l return (DS (SL l)) with                      inl i => init i                    | inr o => s o X                 end. trivial. Save. Lemma eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)                (init : DS_prod (inlSL SL)), continuous (eqn_of_system s init). intros; apply Dprodi_continuous with (Di:= fun i => DS (SL i)); intro. red; intros. rewrite fmon_comp_simpl. rewrite (Proj_simpl (O:=DS_fam SL)). rewrite (eqn_of_system_simpl (SL:=SL)). case i; intros; auto. apply (le_lub (c:=DS (SL (inl LO l)))) with     (f:=(Proj (DS_fam SL) (inl LO l) @ eqn_of_system s init) @ h)     (n:=O). rewrite (fcont_continuous (s l)). apply lub_le_compat; intro n; simpl. apply DSle_refl. Save. Hint Resolve eqn_of_system_cont. Definition EQN_of_system : forall (LI LO:Type) (SL:LI+LO->Type),                system SL -> DS_prod (inlSL SL) -> DS_prod SL -c> DS_prod SL. intros LI LO SL s init; exists (eqn_of_system s init); auto. Defined. Lemma EQN_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)                (init : DS_prod (inlSL SL)) (X:DS_prod SL),                EQN_of_system s init X = eqn_of_system s init X. trivial. Save. ```

### Properties of the equations

``` ```
The equations are monotonic with respect to the inputs and the system
``` Lemma EQN_of_system_mon : forall (LI LO:Type) (SL:LI+LO->Type)             (s1 s2 : system SL) (init1 init2 : DS_prod (inlSL SL)),             s1 <= s2 -> init1 <= init2 -> EQN_of_system s1 init1 <= EQN_of_system s2 init2. intros; apply fcont_le_intro; intro X. repeat (rewrite (EQN_of_system_simpl)); repeat (rewrite (eqn_of_system_simpl)). intro l; case l; auto. intros; apply (H l0 X). Save. Definition Eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),                (system SL) -m> DS_prod (inlSL SL) -M-> DS_prod SL -C-> DS_prod SL. intros; exact (le_compat2_mon (EQN_of_system_mon (SL:=SL))). Defined. Lemma Eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)                (init:DS_prod (inlSL SL)), Eqn_of_system SL s init = EQN_of_system s init. trivial. Save. ```
The equations are continuous with respect to the inputs
``` Lemma Eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type),             continuous2 (Eqn_of_system SL). red; intros. rewrite (Eqn_of_system_simpl (SL:=SL)). apply (fcont_le_intro (D1:=DS_prod SL) (D2:=DS_prod SL)); intro X. rewrite EQN_of_system_simpl; rewrite eqn_of_system_simpl; intro l. case_eq l; intros. rewrite fcont_lub_simpl. unfold DS_prod; repeat (rewrite Dprodi_lub_simpl). apply lub_le_compat; intro n; auto. unfold system; rewrite Dprodi_lub_simpl. repeat rewrite fcont_lub_simpl. unfold DS_prod; rewrite Dprodi_lub_simpl. apply lub_le_compat. intro n; simpl; auto. Save. Hint Resolve Eqn_of_system_cont. Lemma Eqn_of_system_cont2 : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL),             continuous (Eqn_of_system SL s). red; intros; apply continuous2_right; auto. Save. Lemma Eqn_of_system_cont1 : forall (LI LO:Type) (SL:LI+LO->Type),             continuous (Eqn_of_system SL). auto. Save. Definition EQN_of_SYSTEM (LI LO:Type) (SL:LI+LO->Type)        : system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL -C-> DS_prod SL        := continuous2_cont (Eqn_of_system_cont (SL:=SL)). ```

### Solution of the equations

``` ```
The solution is defined as the smallest fixpoint of the equations it is a monotonic function of the inputs
``` Definition sol_of_system (LI LO:Type) (SL:LI+LO->Type)     : system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL := FIXP (DS_prod SL) @@_ EQN_of_SYSTEM SL. Lemma sol_of_system_simpl :     forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),     sol_of_system SL s init = FIXP (DS_prod SL) (EQN_of_system s init). trivial. Save. Lemma sol_of_system_eq : forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),     sol_of_system SL s init == eqn_of_system s init (sol_of_system SL s init). intros; rewrite sol_of_system_simpl. apply (fixp_eq (D:=DS_prod SL) (f:=eqn_of_system s init)); auto. Save. ```

### New node from the system

``` ```
We can choose an arbitrary set of outputs
``` Definition node_of_system (O:Type)(LI LO:Type) (SL:LI+LO->Type)(indO : O -> LO) :           system SL -C-> node_fun (fun i : LI => SL (inl LO i)) (fun o : O => SL (inr LI (indO o))) := DLIFTi (DS_fam SL) (fun o => inr LI (indO o)) @@_ (sol_of_system SL). ```
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (24 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (10 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

# Global Index

## D

DS_fam [definition, in Systems]
DS_prod [definition, in Systems]

## E

EQN_of_SYSTEM [definition, in Systems]
eqn_of_system [definition, in Systems]
EQN_of_system [definition, in Systems]
Eqn_of_system [definition, in Systems]
eqn_of_system_cont [lemma, in Systems]
Eqn_of_system_cont [lemma, in Systems]
Eqn_of_system_cont1 [lemma, in Systems]
Eqn_of_system_cont2 [lemma, in Systems]
EQN_of_system_mon [lemma, in Systems]
EQN_of_system_simpl [lemma, in Systems]
Eqn_of_system_simpl [lemma, in Systems]
eqn_of_system_simpl [lemma, in Systems]

## I

inlSL [definition, in Systems]
inrSL [definition, in Systems]

## N

node_fun [definition, in Systems]
node_of_system [definition, in Systems]

## S

snode_fun [definition, in Systems]
sol_of_system [definition, in Systems]
sol_of_system_eq [lemma, in Systems]
sol_of_system_simpl [lemma, in Systems]
system [definition, in Systems]
Systems [library]

# Lemma Index

## E

eqn_of_system_cont [in Systems]
Eqn_of_system_cont [in Systems]
Eqn_of_system_cont1 [in Systems]
Eqn_of_system_cont2 [in Systems]
EQN_of_system_mon [in Systems]
EQN_of_system_simpl [in Systems]
Eqn_of_system_simpl [in Systems]
eqn_of_system_simpl [in Systems]

## S

sol_of_system_eq [in Systems]
sol_of_system_simpl [in Systems]

# Definition Index

## D

DS_fam [in Systems]
DS_prod [in Systems]

## E

EQN_of_SYSTEM [in Systems]
eqn_of_system [in Systems]
EQN_of_system [in Systems]
Eqn_of_system [in Systems]

## I

inlSL [in Systems]
inrSL [in Systems]

## N

node_fun [in Systems]
node_of_system [in Systems]

## S

snode_fun [in Systems]
sol_of_system [in Systems]
system [in Systems]

# Library Index

## S

Systems

 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (24 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (10 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)